λ-calculus. Part Two: Practice
The idea, a short plan and links to the main sources for this article were given to me by the habrauseur z6Dabrata , for which many thanks to him.
The first part gave us a theoretical idea of what is lambda calculus. In this article we will follow the informal practice-practice-practice command and see it in action.
As mentioned earlier, in pure typeless lambda calculus, everything is missing except functions. So even such basic things as numbers or boolean values need to be implemented by themselves. More precisely, it is necessary to create some active entities that will behave like the objects we need. And, of course, the coding process will consist in writing the corresponding functions.
')
We start with the simplest:
The
Here
Let's see how it will work:
Since the
The definition of the main Boolean operators is also not difficult. For example, a conjunction (logical “and”) would look like this:
We will only encode natural numbers, for which we recall Peano's axioms , which determine their set. The implementation will continue to be based on functions that behave in a given context like a unit, a pair, etc. Actually, this is one of the features of lambda calculus: entities written in its terms do not have self-sufficiency, since they embody the behavior of an object.
So, we need a function that takes two arguments: a fixed initial value and a function to determine the next element ( the following function ). The number will be encoded in the number of applications of the following function to the initial value:
It is easy to see that zero is encoded in the same way as the logical False. Nevertheless, one should not draw any far-reaching conclusions from this: this is just a coincidence.
The task of the following function is to add one to the given number. Those. as an argument, it will take the value that needs to be increased, and which is also a function of two arguments. Thus, the total function
Here
Suppose we need to get from the “one”
The function performing the addition of two Church numbers will take two terms:
As an example, add
The multiplication function can be determined through the addition function. In the end, multiplying
There is another way to define multiplication on Church numbers, without using
For example, multiply
The last unexamined operation is subtraction - not the most trivial thing on the Church numbers. Those interested can study it themselves, for example, according to Benjamin Pierce’s book, Types and Programming Languages .
Quotation to attract attention from the wiki summary on lambda calculus : “If you do not understand anything, do not be upset. Subtraction invented Cleene when they pulled out a wisdom tooth. And now the anesthesia is not the same. ”
As you can see, technically nothing complicated in lambda calculus is present: it all comes down to elementary substitutions and reductions. But such a small set of tools is enough to implement active entities, if desired, that behave like pairs, lists, recursive functions, etc. They will be quite cumbersome, but, as already mentioned, the λ-calculus is not intended for writing programs, but for studying and specifying programming languages and type systems. What, in fact, copes with.
The first part gave us a theoretical idea of what is lambda calculus. In this article we will follow the informal practice-practice-practice command and see it in action.
Church Boolean Constants
As mentioned earlier, in pure typeless lambda calculus, everything is missing except functions. So even such basic things as numbers or boolean values need to be implemented by themselves. More precisely, it is necessary to create some active entities that will behave like the objects we need. And, of course, the coding process will consist in writing the corresponding functions.
')
We start with the simplest:
True and False . Two terms embodying the behavior of these constants are as follows:tru = λt.λf.t | Two-argument function that always returns the first argument. |
fls = λt.λf.f | A two-argument function that always returns the second argument. |
The
if for such Boolean constants will be:if = λb. λx. λy.bxyHere
b is tru or fls , x is the then branch, y is the else branch.Let's see how it will work:
if fls teSince the
if condition if false ( fls ), an expression from the else branch ( e in our case) must be returned.(λb. λx. λy. bxy) fls te | by definition if |
(λx. λy. fls xy) te | reduction of the underlined expression from the previous line |
(λy. fls ty) e | reduction of the underlined expression from the previous line |
fls te | reduction of the underlined expression from the previous line |
(λt.λf. f) t e | by definition fls |
(λf. f) e | reduction of the underlined expression from the previous line |
e | reduction of the underlined expression from the previous line |
The definition of the main Boolean operators is also not difficult. For example, a conjunction (logical “and”) would look like this:
and = λx. λy. xy flsand gets two boolean values x and y . The first is substituted x (currying). If he is tru ( tru y fls after the reduction), then y will return, which then will also be “checked” for truth. Thus, we will get the final tru only in the case when both x and y “true”. In all other options, the answer is fls .Exercise
Define a logical "or" and "not."
Answer
or = λx.λy. x tru ynot = λx. x fls truChurch numbers
We will only encode natural numbers, for which we recall Peano's axioms , which determine their set. The implementation will continue to be based on functions that behave in a given context like a unit, a pair, etc. Actually, this is one of the features of lambda calculus: entities written in its terms do not have self-sufficiency, since they embody the behavior of an object.
So, we need a function that takes two arguments: a fixed initial value and a function to determine the next element ( the following function ). The number will be encoded in the number of applications of the following function to the initial value:
0 ≡ λs.λz. z | the function s is applied to the initial value z zero times |
1 ≡ λs.λz. sz | the function s is applied to the initial value z once |
2 ≡ λs.λz. s (sz) | the function s is applied to the initial value z two times |
| ... | and so on |
It is easy to see that zero is encoded in the same way as the logical False. Nevertheless, one should not draw any far-reaching conclusions from this: this is just a coincidence.
The task of the following function is to add one to the given number. Those. as an argument, it will take the value that needs to be increased, and which is also a function of two arguments. Thus, the total function
(+1) has three arguments: the preceding Church number n , the function to be applied n+1 times to the initial value, and the initial value itself. It looks like this:scc = λn. λs. λz. s (nsz)Here
nsz is the function s applied to z times. But we need to apply it n+1 times, whence the explicit s (nsz) is taken.Suppose we need to get from the “one”
one = λs.λz. sz one = λs.λz. sz "two" two = λs.λz. s (sz) two = λs.λz. s (sz) . It will happen like this:scc one s' z' | s' and z' - not to confuse the substituted values with the names of variables |
(λn. λs. λz. s (nsz)) one s' z' | by definition scc |
(λs. λz. s (one sz)) s' z' | reduction of the underlined expression from the previous line |
(λz. s' (one s' z)) z' | reduction of the underlined expression from the previous line |
s' (one s' z') | reduction of the underlined expression from the previous line |
s' ( (λs.λz. sz) s' z ') | by definition one |
s' ( (λz. s' z) z' ) | reduction of the underlined expression from the previous line |
s' (s' z') | reduction of the underlined expression from the previous line |
two s' z' | by definition two |
Arithmetic operations
Addition
The function performing the addition of two Church numbers will take two terms:
x and y , which in turn also have two arguments - s (the function of following) and z (the initial value). Addition will consist in first applying s to z x times, and then y again.plus = λx. λy. λs. λz. xs (ysz)As an example, add
one = λs.λz. sz one = λs.λz. sz and two = λs.λz. s (sz) two = λs.λz. s (sz) . The answer should look like this: three = λs.λz. s (s (sz)) three = λs.λz. s (s (sz)) .plus one two s' z' | s' and z' - not to confuse the substituted values with the names of variables |
(λx. λy. λs. λz. xs (ysz)) one two s' z' | by definition plus |
one s' (two s' z') | after reduction |
(λs.λz. sz) s' (two s' z') | by definition one |
s' (two s' z') | after reduction |
s' (( λs.λz. s (sz) s' z') | by definition two |
s' (s' (s' z')) | after reduction |
three s' z' | by definition three |
Multiplication
The multiplication function can be determined through the addition function. In the end, multiplying
x by y means adding x copies of y .times = λx. λy. x (plus y) zThere is another way to define multiplication on Church numbers, without using
plus . His idea is that to get the product x and y you need x times to take y times the function s applied to the initial value:times' = λx.λy.λs.λz. x (ys) zFor example, multiply
two = λs.λz. s (sz) two = λs.λz. s (sz) for three = λs.λz. s (s (sz)) three = λs.λz. s (s (sz)) . The result should be: six = λs.λz. s (s (s (s (s (sz))))) six = λs.λz. s (s (s (s (s (sz))))) .times' two three s' z' | s' and z' - not to confuse the substituted values with the names of variables |
(λx.λy.λs.λz. x (ys) z) two three s' z' | by definition times' |
two (three s') z' | after reduction |
(λs.λz. s (sz)) (three s') z' | by definition two |
three s' ((three s') z') | after reduction |
(λs.λz. s (s (sz))) s' ((three s') z') | by definition three |
s' (s' (s' ((three s') z'))) | after reduction |
s' (s' (s' (((λs.λz. s (s (sz))) s') z'))) | by definition three |
s' (s' (s' (( (λz. s' (s' (s' z))) z' ))) | after reduction |
s' (s' (s' (s' (s' (s' z'))))) | reduction of underlined expression |
six s' z' | by definition six |
Exercise
Determine the term for exponentiation
Answer
For
x to the power of y :power = λx.λy.λs.λz . yxszThe last unexamined operation is subtraction - not the most trivial thing on the Church numbers. Those interested can study it themselves, for example, according to Benjamin Pierce’s book, Types and Programming Languages .
Quotation to attract attention from the wiki summary on lambda calculus : “If you do not understand anything, do not be upset. Subtraction invented Cleene when they pulled out a wisdom tooth. And now the anesthesia is not the same. ”
Conclusion
As you can see, technically nothing complicated in lambda calculus is present: it all comes down to elementary substitutions and reductions. But such a small set of tools is enough to implement active entities, if desired, that behave like pairs, lists, recursive functions, etc. They will be quite cumbersome, but, as already mentioned, the λ-calculus is not intended for writing programs, but for studying and specifying programming languages and type systems. What, in fact, copes with.
List of sources
Source: https://habr.com/ru/post/215991/
All Articles