1. State the type of the whole expression; there are partial type decorations:

    \[\begin{gather*} \lambda x.\con{student}_{et}x\\ \lambda x.\con{read}_{e(et)}x\,\con{anna}_{e}\\ \lambda p\exists x. p_{et}\, x\\ \lambda y\lambda x.\con{admire}_{e(et)}y\, x\\ \lambda f\lambda g\lambda x.f_{e(tt)}\,x(gx) \end{gather*}\]
  2. Identify bound and free variables in:

    \[\begin{gather*} \lambda x.\con{student}x\\ \lambda x.\con{admire}y\cnct x\\ \lambda p\lambda x.p\cnct x\land \con{student}x q\cnct x\\ \end{gather*}\]
  3. Reduce each expression as far as possible.

    \[\begin{gather*} (\lambda x.\con{student}x)\con{anna}\\ (\lambda x\lambda y.\con{admire}x\,y)\con{ben}\\ (\lambda p.p\,\con{anna})(\lambda x.\con{linguist}x)\\ (\lambda q\exists x.q\,x)(\lambda y.\con{book}y)\\ (\lambda p\lambda q\forall x. p\,x \to q\,x)(\lambda x.\con{student}x)(\lambda x.\con{admire}x\con{anna})\\ (\lambda p.\lambda q.\exists x.p\,x\land q\,x)(\lambda x.\con{student}x\land \exists y. \con{book}y\land \con{read}y\,x) \end{gather*}\]

Updated: