1
$\begingroup$

I'm just getting started with STLC (Simply Typed Lambda Calculus) and I'm trying to understand an evaluation rule I've been given in some lecture notes by my professor. What it says is the following:

(λx. x(λx. x)) (u r) evaluates to (u r) (λx. x)

I don't really get this at all. Can someone point out which step I'm misunderstanding in my evaluation;

(λx. x(λx. x)) (u r) // Start state, not evaluated

(λx. λz. z) (u r) // Replacing occurences of x in first lambda function with the
                  // second lambda function, and then renaming the input variable x
                  // in the second lambda function (this is allowed, right?)

r                 // x gets replaced by u (no occurences) and z gets replaced by r
                  // - resulting in the final result r.
Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ In your second line, an instance of $x$ went missing. It should be $(\lambda x.\, x(\lambda z.\, z)) \; (u\; r)$. $\endgroup$
    – Yuval Filmus
    Commented May 22, 2018 at 10:35
  • 1
    $\begingroup$ Actually, I think that you did not parse the term correctly. It should be read as $(\lambda x.(x\; (\lambda x.x)))\;(u\;r)$, not as $((\lambda x.x)\;(\lambda x.x))\;(u\;r)$. $\endgroup$
    – Rodolphe Lepigre
    Commented May 22, 2018 at 10:40
  • 1
    $\begingroup$ In the first one, $(\lambda x.(x\;(\lambda x.x)))$ corresponds to a function, taking as input a function (argument $x$), which is applied to the identity function $\lambda x.x$ (or ($\alpha$-)equivalently $\lambda y.y$). The second one has a very different nature because it denote the application of the identity function to the identity function, which reduces to the identity function. $\endgroup$
    – Rodolphe Lepigre
    Commented May 22, 2018 at 12:12
  • 1
    $\begingroup$ Yes, the term $u\;r$ should definitely reduce to a function, but it does not really matter for the first reduction steps that you want to take. Remember that you only want to evaluate your term to $(u\;r)\;(\lambda x.x)$, which corresponds to the application of $u$ to the argument $r$ and $\lambda x.x$ (which are given one after the other, and not the two at once). $\endgroup$
    – Rodolphe Lepigre
    Commented May 22, 2018 at 12:39
  • 1
    $\begingroup$ You are welcome, I added my comments as an answer. $\endgroup$
    – Rodolphe Lepigre
    Commented May 22, 2018 at 13:14

2 Answers 2

Reset to default
3
$\begingroup$

(Summary of my explanations in the comments under the questions)

I think that you did not parse the term correctly. It should be read as $(λx.(x\;(λx.x)))\;(u\;r)$, not as $((λx.x)\;(λx.x))\;(u\;r)$. In the former, $(λx.(x\;(λx.x)))$ corresponds to a function taking as input a function (argument $x$), which is applied to the identity function $λx.x$ (or $α$-equivalently $λy.y$). In the latter, the term $((λx.x)\;(λx.x))$ has a very different nature because it denote the application of the identity function to the identity function, which reduces to the identity function.

Improve this answer
$\endgroup$
4
$\begingroup$

The term

(λx. x(λx. x)) (u r)

parses as

(λx. M) N
where M=(x (λx. x)) and N=(u r)

so, we can perform a $\beta$ step and obtain

M{N/x}
= (x (λx. x)){(u r) / x}
= (x{(u r) / x}   (λx. x){(u r) / x})
= ((u r)   (λx. x){(u r) / x})
= ((u r)   (λx. x))

The last term is also usually written as (u r) (λx. x) or even u r (λx. x).

A tricky part of this step is the substitution (λx. x){(u r) / x} = (λx. x). This derives from the general rule stating that for any terms A,B:

(λx. A){B / x} = (λx. A)

Indeed, the intuition here is that a substitution {B / x} only substitutes the free occurrences of x, and there are no free occurrences of x in (λx. A). This is coherent with the fact that the bound variable x in (λx. A) could be $\alpha$-converted to any fresh variable name y, obtaining (λy. A{y / x}), where x is no longer present at all (free or bound).

By comparison, this step is wrong

(λx. x(λx. x)) (u r) --> (λx. λz. z) (u r)

First, when you apply a $\beta$ step, the $\lambda x$ disappears. So, we can not have both $\lambda x$ and $\lambda z$ in the residual term. If we change the term, modifying the parentheses, we get

((λx. x)(λx. x)) (u r) --> (λz. z) (u r)

but the starting term is completely different from the original one, where (λx. x(λx. x)) (u r) is read as ((λx. (x(λx. x))) (u r)) instead.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you! However, I really don't understand why λx. x(λx. x) is read as λx. (x(λx. x)) instead of (λx. x) (λx. x). I don't even know what the x before the second lambda means in the first example, it looks like a function application but x isn't a function. $\endgroup$
    – Nyfiken Gul
    Commented May 22, 2018 at 12:10
  • $\begingroup$ @NyfikenGul There is no deep reason: it's only a notational convention meant to reduce the number of parentheses one has to write. Usually, lambdas extend their scope to the right as possible. E.g. $\lambda x.ABCD$ means $(\lambda x.(((AB)C)D))$. This convention enables us to write things like $S=\lambda xyz.xz(yz)$ without additional parentheses. $\endgroup$
    – chi
    Commented May 22, 2018 at 13:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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