Solution: Notational conventions

  1. Restoration:

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

      \[\equiv (\lambda f.(\lambda g.(\lambda h.(\lambda x.(f(g(h x)))))))\]

    2. \(xxxx\)

      \[\equiv (((xx)x)x)\]

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

      \[\equiv (\lambda x.(x(\lambda y.y)))\]

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

      \[\equiv (\lambda x.(x(\lambda y.((yx)x)))x)\]
  2. Elimination:

    1. \((xy)\)

      \(\equiv xy\)

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

      \(\equiv x(yz)\)

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

      \(\equiv xyz\)

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

      \(\equiv \lambda x.x\)

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

      \(\equiv \lambda y\lambda x.x\)

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

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

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

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

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

      \(\equiv x\lambda x.x\)

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

      \(\equiv (\lambda y\lambda x.x)\lambda x.x\)

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

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

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

      \(\equiv x(yz)(xyz)\)

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

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

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

      \(\equiv ab(cd)(ef(gh))\)

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

      \(\equiv (\lambda x.(\lambda y.yx)(\lambda v.v)zu)(\lambda w.w)\)