3
$\begingroup$

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

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

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

$\endgroup$
10
  • $\begingroup$ Hmm redex was the missing bit. So only applications are redexes!? $\endgroup$
    – geckos
    Nov 12 '20 at 12:34
  • 2
    $\begingroup$ 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$.) $\endgroup$
    – lemontree
    Nov 12 '20 at 12:52
  • $\begingroup$ 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! $\endgroup$
    – geckos
    Nov 13 '20 at 14:14
  • 1
    $\begingroup$ With $\equiv_\alpha$ included in $\triangleright_\beta$, it's equialent, yes. It's just not part of the elementary contraction. $\endgroup$
    – lemontree
    Nov 15 '20 at 12:40
  • 1
    $\begingroup$ For feedback on your code, I suggest you ask at codereview.stackexchange.com and state specifically which parts you are unsure about. $\endgroup$
    – lemontree
    Nov 29 '20 at 20:22

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.