theory Exercise02 imports Main begin section {* $\lambda$-calculus *} subsection {* Church Numerals *} text {* \label{subsection:church-numerals} Recall the encoding of natural numbers as $\lambda$-terms via \emph{Church numerals}: $$n \equiv \lambda f \, x. \, f^n x$$ $\rhd$ Define a function $\mathrm{mult} \equiv \lambda m \, n. \, \ldots$ as a $\lambda$-term such that $\mathrm{mult} \, m \, n$ encodes $m \cdot n$, i.e.\ multiplication of Church numerals. *} subsection {* $\alpha \beta \eta$-Equivalence in Isabelle *} text {* Equality in Isabelle is (usually) modulo $\alpha \beta \eta$-equivalence. Therefore the theorem \texttt{refl}: \\ @{thm refl [no_vars]} is sufficient to prove the following lemmas: *} lemma alpha: "(\x. x) = (\y. y)" by (rule refl) lemma beta: "(\f. f x) f = f x" by (rule refl) lemma eta: "(\x. f x) = f" by (rule refl) text {* $\rhd$ Prove these lemmas in Isabelle. What happens wrt.\ $\alpha \beta \eta$-equivalence? *} subsection {* Church Numerals in Isabelle *} text {* In this exercise we will use Isabelle to perform computations with Church numerals. Isabelle's \emph{simplifier}, which is invoked on a proof state by @{text "simp"}, performs term rewriting. @{text "unfold"} can be used to unfold definitions. $\rhd$ Make yourself familiar with the @{text "definition"} command (Section~4.1.1 of the Isabelle/Isar Reference manual). Use it to define two functions @{term "add"} and @{term "mult"} (cf.\ Exercise~\ref{subsection:church-numerals}) which perform addition and multiplication, respectively, of Church numerals in Isabelle. In order to do so, replace the dummy definitions below. *} definition add :: 'dummy where "add = arbitrary" definition mult :: 'dummy where "mult = arbitrary" text {* $\rhd$ Prove the following lemmas. Which values are computed for @{text "?x"}? *} lemma "add (\f x. f (f x)) (\f x. f (f (f x))) = ?x" unfolding add_def -- {* we can unfold the definition first \dots *} apply simp done lemma "mult (\f x. f (f x)) (\f x. f (f (f x))) = ?x" by (simp add: mult_def) -- {* \dots\ or give it to the simplifier directly *} text {* $\rhd$ Compute $2 + 2 \cdot (3 + 1)$ in a similar fashion. *} section {* Simply-Typed Lambda Calculus *} subsection {* Type Inference *} text {* $\rhd$ Infer most general types for the following $\lambda$-terms. Give the full typing derivations. \begin{itemize} \item[(a)] $\lambda x \, y \, z. \, x \, z \, (y \, z)$ \item[(b)] $\lambda x \, y. \, x$ \item[(c)] $(\lambda x. \, x) \, (\lambda x. \, x)$ \end{itemize} *} text {* $\rhd$ Is the term $\, \lambda x. \, x \, x \,$ type correct? Justify your answer. *} end