What is the diference between $\lambda x.1$ and $1$?

I know that I can $$(\lambda x.1) 0 \rhd_\beta 1$$. This is the constant 1, but can I contract it automatically? I mean, is $$1$$ the normal form of $$(\lambda x.1)$$?

It seems reasonable to do it but when goes to combinators this sense stops, I mean, if I can $$\lambda x.1 \rhd_\beta 1$$, then I would $$\lambda xy.y \rhd_\beta \lambda y.y$$ but $$(\lambda xy.y) a b \rhd_\beta b$$ and $$(\lambda x.1) a b \rhd_\beta 1 b$$ so that $$\lambda x.1 \not\equiv_\beta 1$$

What rules I'm missing on Lambda cauculus that forbids the contraction $$\lambda x.1 \rhd_\beta 1$$?

• $\lambda x.1$ is a function that gets $x$ as input and outputs $1$. In contrast, $1$ is just $1$. Nov 12 '20 at 10:29

$$\lambda$$-contraction is defined as $$(\lambda v.M)N \triangleright_\beta M[v/N]$$. A $$\lambda$$-term of the form $$(\lambda v.M)N$$ is called a redex (= reducible expression). In order to reduce a term, you need a redex -- that's just how $$\lambda$$-contraction is defined.
The reason that $$\lambda x.1$$ can not be any further reduced is that it does not contain any redex: It is not and does not contain any terms of the form $$(\lambda v.M)N$$, so $$\lambda$$-contraction is just not applicable anywhere. The term thus already is in normal form.
In contrast, $$(\lambda x.1)0$$ contains a redex, namely itself -- with $$v = x$$, $$M = 1$$ and $$N = 0$$ --, and $$\lambda$$-contraction yields the normal form $$1$$.
Obviously $$\lambda x.1$$ and $$1$$ are non-equivalent normal forms: One is a function that yields a number, the other one is a number.
$$(\lambda x.1)$$ is different from $$(\lambda x.1)0$$ in the same way in which, say, $$f: x \mapsto x^2$$ is different from $$f(2)\ (= 4)$$. A function is not the same as the value of the function at an argument, and a function can not be applied to yield a value without an argument present.

• Hmm redex was the missing bit. So only applications are redexes!? Nov 12 '20 at 12:34
• Yes, and only applications where the left part is an abstraction. E.g. $((\lambda x.x)(\lambda y.y))(1)$ would not be itself a redex, because the term on the left is an application, not an abstraction. (But though the term as a whole is not a redex, it contains the redex $((\lambda x.x)(\lambda y.y))$, which can be contracted to $\lambda y.y$, yielding a new redex $(\lambda y.y)1$, which reduces to $1$.) Nov 12 '20 at 12:52
• Thank you @lemontree, I will implement call by value semantics this will be very useful, if you got curious github.com/dhilst/funcyou/blob/master/lambdac.py it's a weekend project but it's being fun :) Thank you so much! Nov 13 '20 at 14:14
• With $\equiv_\alpha$ included in $\triangleright_\beta$, it's equialent, yes. It's just not part of the elementary contraction. Nov 15 '20 at 12:40
• For feedback on your code, I suggest you ask at codereview.stackexchange.com and state specifically which parts you are unsure about. Nov 29 '20 at 20:22