Compute the result by using $\lambda$-calculus: $$+ (+ 2\,4) 1.$$ My question is: should I use definition of outer $+$ and then by $\beta$-reduction proceed until I am left with no $\beta$-redex any more. Then, again, use definition of next term that is first on left and proceed in that way, until I am left with only numbers and the $follower$-function and then use $applicative$-order $\beta$-reduction (on inner most $follower$-function). Or, hence I want $applicative$-order $\beta$-reduction, I should immediately proceed with innermost definition substitutions? Any help is appreciated. If it was unclear, I will write precicely what I mean on the example.
Asked
Active
Viewed 31 times
0
-
Are you conscious that you should find 7 ? – Jean Marie Nov 13 '17 at 21:38
-
Yes, I am. But, as a teaching fellow at our University said, "we are not allowed to use one reduction order, and then, at some point, another. We have to stick to one from the beginning to the end of calculation". So, what I ask is, whether or not the same applies for the definitions, i.e. can I do definitions of arithmetic operators and numbers in normal order, and then reductions in applicative order? – Nemanja Beric Nov 14 '17 at 05:38
1 Answers
1
Typically, for theoretical work at least, definitions are treated as meta-level notions. Presumably $+$ is defined as some lambda term, e.g. $\lambda m.\lambda n.\lambda z.m(n z)$, i.e. Church numerals. In this case, a term like $+(+2\ 4)1$ means $(\lambda m.\lambda n.\lambda z.m(n z))((\lambda m.\lambda n.\lambda z.m(n z))2\ 4)1$. (Presumably in this context, $1$, $2$, and $4$ would also be defined terms.) From there you can use applicative-order evaluation or normal-order evaluation or whatever evaluation order you like.
More "applied" lambda calculi may treat $+$ like a primitive constant and have special rules, usually called $\delta$-reductions, to deal with them. For example, you'd have a $\delta$-reduction that states $(+\ 2\ 4) \leadsto_\delta 6$. In this case, your notion of evaluation order could treat $\beta$-reductions and $\delta$-reductions differently, but typically they won't.
Finally, some lambda calculi do have some internal notion of "definition" and corresponding reduction rules for that. For example, Coq's $\zeta$-reductions. This is unusual though for theoretical work.
As an aside, it's ambiguous in your comment, but just to be clear, the restriction from your teaching fellow to "stick to one [reduction order]" is artificial. There is no requirement from the lambda calculus itself that you do this, though most implementations of the lambda calculus will consistently use applicative-order evaluation or normal-order evaluation. Or to put it another way, whatever approach you use is just another evaluation strategy. You could, for example, specify an evaluation strategy that randomly picks a redex and reduces it. That's a completely valid evaluation strategy.
Derek Elkins left SE
- 24,967