Which definition to use in the $\lambda$-calculus problem

Question

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.

Answer 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.