Exploring the Peano Axioms Through Algebraic Data Types

Re:Exploring the Peano Axioms Through Algebraic Data Types by quietbritishjim on Tuesday January 15, 2019 @11:05AM (#18912111)

Let'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)

[ Parent | on HN ]

Re:Exploring the Peano Axioms Through Algebraic Data Types by jjaredsimpson on Tuesday January 15, 2019 @07:26PM (#18917162)

You 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

[ Parent | on HN ]

Re:Exploring the Peano Axioms Through Algebraic Data Types by quietbritishjim on Thursday January 17, 2019 @11:47AM (#18932263)

Oops, 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)

[ Parent | on HN ]