I am trying to understand Church's Numerals for 4:

$$4 = \lambda f.\, \lambda x.\, f f f f x\,.$$

This will be evaluated in the following order:

$$\lambda f.\, \lambda x.\, (f (f (f (f x) ) ) )\,.$$

My question is why the function body will not evaluate left outer most, like

$$( ( ( ( (f f) f) f) f) x)\,?$$


Function application is not associative. It may seem at first that this is valid because function composition is associative, but according to Wikipedia,

Bracketing may be used and may be needed to disambiguate terms. For example, ${\lambda x.((\lambda x.x)x)}$ and ${(\lambda x.(\lambda x.x))x}$ denote different terms (although they coincidentally reduce to the same value). Here the first example defines a function that defines a function and returns the result of applying $x$ to the child-function (apply function then return), while the second example defines a function that returns a function for any input and then returns it on application of $x$ (return function then apply).

$\lambda f.\lambda x.((ff)f)x$ is a distinct lambda term from $\lambda f.\lambda x.(f(ff))x$.

  • $\begingroup$ I see the confusion here. What is called associativity can actually mean two different things, one is at the syntax level, another is whether two different associativity leads to the same result. $\endgroup$
    – 盛安安
    Feb 2 '17 at 15:22
  • $\begingroup$ @盛安安 Precisely. The Wikipedia page clearly states that two lambda terms are considered distinct, even if they reduce to the same value. The thing to remember is that function composition is associative, but not function application. $\endgroup$
    – Riley
    Feb 2 '17 at 15:30

The thing is, the church numeral for number 4 is $λf.λx.f(f(f(f(x))))$ [ Wiki ].

It can not be evaluated either way, because we have function application, not composition. Also, it is left associative, not right, that's why we need the paretheses.

  • $\begingroup$ Is this term λf.λx.f(f(f(f(x)))) a function composition, also right associative right? $\endgroup$ Feb 2 '17 at 15:04
  • 1
    $\begingroup$ In lambda calculus, we always have left associative application (The answer in the comments is wrong). That's why we need to add parenthesis, so the term becomes what we want. If we were to write f f x, this would be the same as (f f) x, as you said in your question, and that is not what we want. $\endgroup$
    – Euge
    Feb 2 '17 at 17:06
  • $\begingroup$ Regarding composition, you have to define it separately, like this: comp = λf.λg.λx. f(g(x)). So when we have a term like f f x, we must apply f to f and x $\endgroup$
    – Euge
    Feb 2 '17 at 17:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.