Remember that application associates to left, \(a\, b\, c\) means \(((a b) c)\); and stacked lambdas associate to right, \((\lambda x\lambda y. x\,y\,y)\) means \((\lambda x.(\lambda y. x\,y\,y))\).

  1. Restore the parentheses and dots in the following:

    1. \(\lambda f \lambda g \lambda h \lambda x.(f(g(h x)))\)

    2. \(xxxx\)

    3. \(\lambda x.x\lambda y.y\)

    4. \(\lambda x.(x\lambda y.yxx)x\)

  2. Simplify the parentheses and dots in the following:

    1. \((xy)\)

    2. \((x(yz))\)

    3. \(((xy)z)\)

    4. \((\lambda x.x)\)

    5. \((\lambda y.(\lambda x.x))\)

    6. \((\lambda z.(x(\lambda y.(yz))))\)

    7. \((x(\lambda z.(\lambda y.(yz))))\)

    8. \((x(\lambda x.x))\)

    9. \(((\lambda y.(\lambda x.x))(\lambda x.x))\)

    10. \((((\lambda y.(\lambda x.x))(\lambda x.x))(xy))\)

    11. \(((x(yz))((xy)z))\)

    12. \((\lambda x.(\lambda y.(\lambda z.((xz)(yz)))))\)

    13. \((((ab)(cd))((ef)(gh)))\)

    14. \((\lambda x.((\lambda y.(yx))(\lambda v.v)z)u)(\lambda w.w)\)

🗝️

Reduce each expression as far as possible.

  1. \((\lambda x. (m\,\, x))\,\,j\)

  2. \((\lambda y. (y\,\, j))\,\,m\)

  3. \(((\lambda x.(\lambda y. (y\,\,(y\,\, x))))\,\, j)\,\,m\)

  4. \((\lambda y.(y\cnct{}j))(\lambda x.(m\cnct{}x))\)

  5. \((\lambda z.z) (\lambda y . y\,\, y) (\lambda x.x\,\, a)\)

  6. \((\lambda x\lambda y.x\,\, y\,\, y) (\lambda a.a) b\)

  7. \((\lambda x.x\,\, x) (\lambda y.y\,\, x) z\)

  8. \(((\lambda x.x\,\, x) (\lambda y.y)) (\lambda y.y)\)

  9. \((\lambda f.fx)g\)

  10. \((\lambda f.fx)ga\)

  11. \((\lambda f.fx)(ga)\)

  12. \((\lambda f\lambda x.fx)g a\)

  13. \((\lambda x\lambda y \lambda z.x(yz))f\)

Now some examples with logical forms:

  1. \((\lambda p.p\cnct{}john')(\lambda x.sleeps'x)\)

  2. \((\lambda p\lambda q.\forall x. p'x \to q'x)(\lambda x. student'x)(\lambda x. sleeps'x)\)

  3. \((\lambda p\lambda x.think'p\cnct{x})((\lambda p.p\cnct{}john')(\lambda x.sleeps'x))alice'\)

  4. \((\lambda p\lambda q.\exists x. p\cnct{x}\land q\cnct{x})(\lambda x. student' x)((\lambda p\lambda x.think'p\cnct{x})((\lambda p.p\cnct{}john')(\lambda x.sleeps'x)))\)

These are from LC public exercises

  1. \((\x.a') b'\)

  2. \((\x.p'x \to \E x.r'b'\, x) a'\)

  3. \((\x\x.p'x \to q'x\,c') a'\, b'\)

  4. \((\x\E y.r'x\,y)y\)

🗝️

Give the lambda term that needs to replace \(\alpha\) so that the reduction results as given.

  1. \(\alpha \cnct a \cnct b = b \cnct a\)

  2. \(\alpha \cnct a \cnct b \cnct c = a \cnct c \cnct b\)

  3. \(\alpha \cnct a \cnct b \cnct c = a \cnct (c \cnct b)\)

  4. \(\alpha \cnct a \cnct b = \lambda x.a \cnct x \cnct (b \cnct x)\)

  5. \(\alpha \cnct (\lambda x.a \cnct x)c = ac\)

  6. \(\alpha \cnct (\lambda x.a \cnct x)c = \lambda y.a(yc)\)

  7. \(\alpha \cnct (\lambda x.sleeps'x) = sleeps'john'\)

  8. \(\alpha \cnct sleeps' = sleeps'john'\)

  9. \(\alpha (\lambda x. walks'x) john' \equiv_{\beta} slow'(walks'john')\)

  10. \(\alpha (\lambda x. walks'x) john' \equiv_{\beta} slow'walks'john'\)

  11. \(\alpha\cnct{mary'}john'(\lambda x.walks'x) \equiv_{\beta} walks'john' \land walks'mary'\)

  12. \(\alpha(\lambda x. talks'x)(\lambda x.smiles'x)john'\equiv_{\beta} smiles'john' \land talks'john'\)

🗝️