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

    \[\begin{align*} \equiv_\beta &\,\, m\,\, j \end{align*}\]

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

    \[\begin{align*} \equiv_\beta &\,\, m\,\, j \end{align*}\]

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

    \[\begin{align*} \equiv_\beta &\,\, (\lambda y. (y\,\,(y\,\, j)))\,\, m \\ \equiv_\beta &\,\, m\,\,(m\,\, j) \end{align*}\]

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

    \[\begin{align*} \equiv_\beta &\,\, (\lambda x.(m\cnct{}x))\cnct{}j \\ \equiv_\beta &\,\, m\cnct{}j \end{align*}\]

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

    \[\begin{align*} \equiv_\beta &\,\, (\lambda y . y\,\, y) (\lambda x.x\,\, a) \\ \equiv_\beta &\,\, (\lambda x.x\,\, a) (\lambda x.x\,\, a) \\ \equiv_\beta &\,\, (\lambda x.x\,\, a) a \\ \equiv_\beta &\,\, a\,\, a \end{align*}\]

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

    \[\begin{align*} \equiv_\beta &\,\, (\lambda y.(\lambda a.a)\,\, y\,\, y) b \\ \equiv_\beta &\,\, (\lambda a.a)\,\, b\,\, b\\ \equiv_\beta &\,\, b\,\, b\\ \end{align*}\]

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

    \[\begin{align*} \equiv_\beta &\,\, (\lambda y.y\,\, x) (\lambda y.y\,\, x) z \\ \equiv_\beta &\,\, (\lambda y.y\,\, x) x z \\ \equiv_\beta &\,\, x\,\, x\,\, z \end{align*}\]

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

    \[\begin{align*} \equiv_\beta &\,\, (\lambda y.y) (\lambda y.y) (\lambda y.y)\\ \equiv_\beta &\,\, (\lambda y.y) (\lambda y.y)\\ \equiv_\beta &\,\, (\lambda y.y) \\ \end{align*}\]

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

    \(\equiv_\beta gx\)

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

    \(\equiv_\beta gxa\)

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

    \(\equiv_\beta gax\)

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

    \(\equiv_\beta ga\)

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

    \(\equiv_\beta \lambda y \lambda z.f(yz)\)

With logical forms:

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

    \(\equiv_\beta sleeps'john'\)

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

    \(\equiv_\beta \forall x. student'x \to sleeps'x\)

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

    \(\equiv_\beta think'(sleeps'john')\cnct{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)))\)

    \(\equiv_\beta \exists x. student'x\land think'(sleeps'john')x\)

From LC public exercises (by Anıl Öğdül):

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

    \(\equiv_\beta a'\)

    Since the variable \(x\) does not appear as a free variable in the body \(a'\), the argument \(b'\) has no slot to fill and is discarded during \(\beta\)-reduction.

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

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

    The existential quantifier \(\exists x\) creates a local scope that binds the second \(x\) (in \(r'b'x\)). Consequently, the \(x\) inside the quantifier cannot be substituted, and only the first \(x\) (in \(p' x\)) is replaced by \(a'\).

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

    \(\equiv_\beta p'b' \to q'b'c'\)

    Here, the inner \(\lambda x\) binds the occurences of \(x\)s in the body of the inner lambda \(p'x \rightarrow q'xc'\), if we put parantheses according to the right-hand rule \((\lambda x (\lambda x. p' x \rightarrow q' x c'))\). When the first argument \(a'\) is applied, it finds no free occurrences of \(x\) to bind to and is discarded. The second argument \(b'\) is then successfully applied to the inner \(\lambda x\), replacing the occurrences of \(x\).

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

    \(\equiv_\alpha(\x\E z.r'x\,z)y\)

    \(\equiv_\beta\E z.r'y\,z\)

    If the free argument \(y\) were substituted directly, it would accidentally fall under the scope of the existential quantifier \(\exists y\), resulting in \(\exists y.r'yy\). In order to keep the meaning intact, we rename the bound variable \(y\) to a fresh variable \(z\), applying \(\alpha\)-conversion before performing the \(\beta\)-reduction.