Beta abbreviation in lambda calculus: is the score score important?
Given the following lambda expression where it \
resembles lambda
:
(\kf.f(\c.co)km)(\x.dox)(\le.le)
Is it wrong to convert (\c.co)k
to ko
? I did it and apparently it was wrong. The correct way would be to evaluate the external function first, that is, (\f.f(\c.co)(\x.dox)m)(\le.le)
it would be a desirable solution.
This is true because I cannot find any rule that could indicate what is in our lectures? If so, why can't I evaluate the internal functions first? I did it this way and my decision was correct nonetheless.
Sincerely.
source to share
I asked my TA, he said the app is left associative, which means
(\kf.f(\c.co)km)(\x.dox)(\le.le)
equivalent to
( [\kf.( [ f(\c.co) ]k )m ][\x.dox] )[ \le.le ]
This explains why k
it cannot be applied to (\c.co)
.: /
The parentheses / brackets are used for readability only.
Sincerely.
source to share
Thus, beta reduction in the (untyped) lambda calculus is what we call the merge rewrite rule. This means that if you can rewrite A
in B
with beta reduction, and also rewrite A
in C
with beta reduction, you can find several D
to B
rewrite D
and C
rewrite to D
- it will be, in fact, some common descendant. The theorem that shows this for the lambda calculus is usually calledThe Church-Rosser theorem . The general property is sometimes referred to as the diamond property, since the diagram resembles a diamond (the two paths fork, but end up connecting again). This also means that the end result of the "trailing" lambda expression will be the same regardless of how you decide to apply beta reduction.
However, not all lambda terms have the same end result. This means that untyped calculus is not what we call normalization. There are many lambda terms that will continually expand upon beta rebuild (never reaching irreducible or normal form). In these situations, it is useful to use some kind of system for ordering your rewrites, as this ensures that the evaluation of programs is performed in the same way for two identical programs.
Of course, you need to make sure that you follow the lambda binding rules, so you are not trying to apply terms to the wrong lambda variables.
source to share
This is obviously the way to go after the question has been satisfactorily answered. However, I had to struggle a bit with the "order of evaluation" in lambda calculus, and this more complicated answer mostly applies to offspring in case anyone has the same doubts. @ Danyel's answer was a lot of help and I will build on this.
As the OP states correctly, there is no explicit rule about the order of evaluation. However, the rule that applications are left-associative leads to the rule that an external application must be evaluated before internal applications.
In the expression
-
(\kf.f(\c.co)km)(\x.dox)(\le.le)
:
Let's make some simplifications (using the first principles that each term e
is either a variable x
, or an abstraction \x.y
, or an application e1e2
):
-
\c.co = e1
, -
\x.dox = e2
, -
\le.le = e3
...
This causes the original expression to be converted to:
-
(\kf.f(e1)km)(e2)(e3)
...
Consider the leftmost term in the above expression:
-
(\kf.(f(e1)km)) = e4
and take a close look at the body of the abstraction: - (fe1)km
, or(f(\c.co))km
Beta-redex (reducible expression) is a form expression (\x.e1)e2
. The above expression doesn't look like that and is not a beta redex (since based on the information available, f is not an abstraction). That is why it can not be reduced and why it was wrong to apply \c.co
to k
.
So, it e4
does not decrease and remains as it is, this leads to:
-
((e4)(e2))(e3)
...
((e4)(e2))
is the first beta redex, and indeed e2
replaces k
as indicated.
One more dot ((e4)(e2))
does not apply primarily to (e3)
for the same reason: it ( ((e4)(e2))e3
) is not a beta redex, it looks like this: ((\ Kf.body) e2) e3. The inner expression (\ kf.body) e2) is the first valid beta redex that can be reduced. Doing so results in the provided answer.
source to share