Menu
I am trying to make function for computing sum of list elements and length of list in lambda calculus.
Example of a list: a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n))sum a should return 6 and len a should return 3.
I wrote recursive versions:
len = λl.if (empty l) 0 (plus 1 (len (tail l)))
sum = λl.if (empty l) 0 (plus (head l) (sum (tail l)))
where if, empty, plus, tail are other lamda functions.
Then I did some trick with fixed-point combinator:
len = λl.if (empty l) 0 (plus 1 (len (tail l)))
len = λfl.if (empty l) 0 (plus 1 (f (tail l))) len
len = Y λfl.if (empty l) 0 (plus 1 (f (tail l)))
where Y = λf.(λx.f(x x))(λx.f(x x))
Just the same for sum. So now I have non-recursive versions. But I can't get beta normal form using beta reduction here.
I wonder if there is beta normal forms of these functions and how they look like.
363
In lambda calculus, lists are represented using pairs, with the first item of the pair representing the head of the list, and the second item representing the rest of the list. A special value, nil, at as the second item of the pair terminates the list.
Semantics of Lambda Expressions Evaluating a lambda expression is called reduction . The basic reduction rule involves substituting expressions for free variables in a manner similar to the way that the parameters in a function definition are passed as arguments in a function call.
Evaluation is done by repeatedly finding a reducible expression (called a redex) and reducing it by a function evaluation until there are no more redexes. Example 1: The lambda expression (λx. x)y in its entirety is a redex that reduces to y.
The λ-calculus was invented by Alonzo Church in the 1930s to study the interaction of functional abstraction and function application from an abstract, purely mathematical point of view.
These can be implemented much more easily given that a list is encoded by its own iterator:
a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n))
means that a list is a function of two arguments: one to use on cons nodes and one to use at the end on the nil constructor.
As a consequence you can implement length by saying:
cons node and return +1
nil with 0
which translates to:
length := λl. l (λ_. plus 1) 0
which would expand to (at each line the expression in bold is being either unfolded or reduced):
length a
(λl. l (λ_. plus 1) 0) a
(λl. l (λ_. plus 1) 0) (λcn.c 1 (c 2 (c 3 n)))
(λcn. c 1 (c 2 (c 3 n))) (λ_. plus 1) 0
(λn. (λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))) 0
(λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))
(plus 1) ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))
(plus 1) ((plus 1) ((λ_. plus 1) 3 0))
(plus 1) ((plus 1) ((plus 1) 0))
(plus 1) ((plus 1) 1)
(plus 1) 2
= 3Similarly, you can implement sum by saying:
+ to combine the value stored in a cons and the result of evaluating the tailnil by 0
which translates to:
sum := λl. l plus 0
which would expand to
sum a
(λl. l plus 0) a
(λl. l plus 0) (λcn.c 1 (c 2 (c 3 n)))
(λcn. c 1 (c 2 (c 3 n))) plus 0
(λn. plus 1 (plus 2 (plus 3 n))) 0
plus 1 (plus 2 (plus 3 0))
plus 1 (plus 2 3)
plus 1 5
= 6If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
