Japanese version
An important part of Peano's axiom is the successor function. Do you remember it? The successor function is a fucntion to make a successor number of the input number. We described a machine called ``SUCC1'' as an implementation of the successor function.
When we define numbers as the answer of what is the numbers, we could define numbers by enumerating all numbers. But, mathematicians are lazy, or must be lazy, and it is quite difficult to enumerate all the numbers which is infinite. Mathematicians' answer is that: 1. create the first number, 2. create a function which generates the next number. Then each mathematician applies them to generate an arbitrary number. They do not use concrete examples 1,2,3, ..., but, they abstract the property of numbers and use the property to define the numbers. Do you also remember the story of abstraction?
A generator of ``successor number'' is a function, thetefore it is a λ. If we have the first number and this λ, we can generate all the numbers. The vending machine gensym3141 can provide a vending machine (vending machine No.6931471805) , which input is a vending machine and the output is a successor vending machine. The vending machine No.1 is ``herring vending machine.'' The vending machine No.2 is ``sandwich vending machine.'' The vending machine No.3 is ``herring sandwich vending machine.'' If vending machine No.6931471805 gets vending machine No.1, the output is vending machine No.2. As the same way, if it gets vending machine No.2, the output is vending machine No.3. Then what is the output of vending machine No.6931471805, of course it is vending machine No.6931471806. This is just one of a vending machine, however, an intelligent life form usually feel something special on such machine. Therefore there is a name, SUCC. The λ of this SUCC is:
SUCC := λn f x. f (n f x)
If you read the Wikipedia's lambda calculus page, you might try to apply this to numbers. If you can easily get the next number, you do not need to read this article anymore. I could not do that and I spent for a week to figure it out. I am writing this article, because I lost this point. This article could be just a supplement of Wikipedia's lambda calculus page. I hope you can find something interesting when you want to apply the SUCC function.
An important part of Peano's axiom is the successor function. Do you remember it? The successor function is a fucntion to make a successor number of the input number. We described a machine called ``SUCC1'' as an implementation of the successor function.
When we define numbers as the answer of what is the numbers, we could define numbers by enumerating all numbers. But, mathematicians are lazy, or must be lazy, and it is quite difficult to enumerate all the numbers which is infinite. Mathematicians' answer is that: 1. create the first number, 2. create a function which generates the next number. Then each mathematician applies them to generate an arbitrary number. They do not use concrete examples 1,2,3, ..., but, they abstract the property of numbers and use the property to define the numbers. Do you also remember the story of abstraction?
A generator of ``successor number'' is a function, thetefore it is a λ. If we have the first number and this λ, we can generate all the numbers. The vending machine gensym3141 can provide a vending machine (vending machine No.6931471805) , which input is a vending machine and the output is a successor vending machine. The vending machine No.1 is ``herring vending machine.'' The vending machine No.2 is ``sandwich vending machine.'' The vending machine No.3 is ``herring sandwich vending machine.'' If vending machine No.6931471805 gets vending machine No.1, the output is vending machine No.2. As the same way, if it gets vending machine No.2, the output is vending machine No.3. Then what is the output of vending machine No.6931471805, of course it is vending machine No.6931471806. This is just one of a vending machine, however, an intelligent life form usually feel something special on such machine. Therefore there is a name, SUCC. The λ of this SUCC is:
SUCC := λn f x. f (n f x)
If you read the Wikipedia's lambda calculus page, you might try to apply this to numbers. If you can easily get the next number, you do not need to read this article anymore. I could not do that and I spent for a week to figure it out. I am writing this article, because I lost this point. This article could be just a supplement of Wikipedia's lambda calculus page. I hope you can find something interesting when you want to apply the SUCC function.
Comments