The λ-calculus

List the free variables of the term $\lambda x.\, x\, y\, (\lambda y.\, y\, z)$. Enter each variable name once.

What does $(\lambda x.\, \lambda y.\, x)\, y$ reduce to in one β-step (with $y$ free)?

With Church numerals $\bar n = \lambda f\, x.\, f^n\, x$, the term $\bar 3\, \bar 2$ (the numeral $3$ applied to the numeral $2$) β-reduces to a Church numeral $\bar k$. What is $k$?

Which of these terms have no normal form? Here $\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x)$, $K = \lambda x\, y.\, x$, $I = \lambda x.\, x$. Choose all that apply.

Why does the proof of the Church–Rosser theorem go through parallel reduction $\Rightarrow$ instead of showing directly that one-step reduction $\to$ has the diamond property?

In Turing's proof of weak normalisation we contract a redex $R = (\lambda x{:}A.\, P)\, Q$ of maximal degree $d$ chosen so that $Q$ contains no redex of degree $d$. Which part of the argument needs this choice?

Which of these terms has a type in the simply typed λ-calculus (for suitable types on the bound variables)?

In the lesson's Lean file, Step t u is one β-step and ReflTransGen Step t u is $t \twoheadrightarrow u$. Which statement is the Church–Rosser theorem, as proved there?

Python's lambda can run Church numerals directly. With church(n) and to_int below, define times(m, n) and exp(m, n) returning the Church numerals for $m \cdot n$ and $m^n$, using only application and lambda (no conversion to int inside them).