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

StackExchange Computer Science Q#132183, answer score: 6