0

From what I understand, a normal form is a $\lambda$-term with one of the following properties:

  1. $\lambda x.M$ with $M$ in normal form
  2. $xM_1...M_n$ with $n \geq 0$ and $M_1,...,M_n$ in normal form

Now say I have the term $\lambda x.y$, which according to the definition given, is in normal form. Would I be correct in saying that this can't be reduced to $y$?

Joël Abrahams
  • 103

1 Answers1

0

A bit late, but yes, you're right. With a term like $λx.y$, you cannot reduce it further without using it in an application.

If, for example, you had $(λx.y)(a)$, then you could reduce it to $y$, as $a$ would be erased. But you can't do anything without applying it to $a$.

Think of it as a function, with reduction being synonymous with evaluation of the function. If you have a function that takes an argument, you can't evaluate it (return a result) without supplying it an argument. However, as soon as you give it an argument, you can return a result.

In this case, the result is always $y$, but you still need an argument to be able to return a result.

Alex
  • 36