5 ms·
Exploring the Peano Axioms Through Algebraic Data Types
- jeremysalwen 8y agoWould have been cool to show it in Coq as well, to make the connection to formal mathematics more clear!
- jjaredsimpson 8y agoI don't understand how .add as defined could terminate. Base case is 0 add y = 0 Recursion is Sx add y = Sy add x Which is of course _swap_ Shouldn't it be = S (x add y)
- caf 8y agoThe recursion is S(x) add y => x add S(y), which recurses until the x becomes O() so it hits the base case.
- quietbritishjim 8y agoLet's try it with x = 2, y = 5: S(2) add 5 (i.e. 3 + 5) => 2 add S(5) (i.e. 2 + 6) => S(1) add 6 (i.e. 2 + 6) => 1 add S(6) (i.e. 1 + 7) => S(0) add 7 (i.e. 1 + 7) => 0 add S(7) (i.e. 0 + 8) => 0 add 8 => 8 (base case) I agree that your rule would work too though: S(2) add 5 => S(1 add 5) => S(S(0 add 5)) Seems more sensible to me, and by adding the same rule to the right hand side we end up only needing a single base case (that 0+0=0) => S(S(S(0 add 4))) ... => S(S(S(S(S(S(S(S(0 add 0)))))))) => S(S(S(S(S(S(S(S(0)))))))) = 8 (that is the definition of 8)
- jjaredsimpson 8y agoYou swapped the order of method arguments though you are doing x add Sy which isn't the same as Sy add x Number.prototype.add = function (y) { var x = Number(this) return x===0 ? y : (y+1).add(x-1) } console.log(Number(3).add(2)) // infinite
- quietbritishjim 8y agoOops, sorry, I see what you mean now. You're right, it looks like this is a mistake: S: innerX => S(y).add(innerX) It should be S: innerX => S(innerX).add(y)
- intuitionist 8y agoStrictly speaking, aren’t these the axioms of Robinson arithmetic (a much weaker system)? For Peano arithmetic you need the axiom schema of induction as well.
- choeger 8y agoI think structural induction over S will do just fine.
- traderjane 8y agoI thought that the recursively enumerable structure was given by the Axiom of Induction.