LambdaCalculus chapter: a nonterminating lambda term

This commit is contained in:
Adam Chlipala 2016-03-13 19:52:46 -04:00
parent 6367baba66
commit b3692b97a5
2 changed files with 26 additions and 0 deletions

View file

@ -81,6 +81,21 @@ Module Ulc.
Notation "\ x , e" := (Abs x e) (at level 50).
Infix "@" := App (at level 49, left associativity).
(* Believe it or not, this is a Turing-complete language! Here's an example
* nonterminating program. *)
Example omega := (\"x", "x" @ "x") @ (\"x", "x" @ "x").
Theorem omega_no_eval : forall v, eval omega v -> False.
Proof.
induct 1.
invert H.
invert H0.
simplify.
apply IHeval3.
trivial.
Qed.
(** * Church Numerals, everyone's favorite example of lambda terms in
* action *)

View file

@ -2095,6 +2095,17 @@ Substitute the argument value in the body of the abstraction, evaluate the resul
Note that we only ever need to evaluate \emph{closed} terms\index{closed terms}, meaning terms that are not open, so we obey the restriction on substitution sketched above.
It may be surprising that these two rules are enough to define the full semantics of a Turing-complete language!
Indeed, $\lambda$-calculus is Turing-complete, and we must be able to find nonterminating programs.
Here is one example.
\begin{eqnarray*}
\Omega &=& (\lambda x. \; x \; x) \; (\lambda x. \; x \; x) \\
\end{eqnarray*}
\begin{theorem}
$\Omega$ does not evaluate to anything. In other words, $\bigstep{\Omega}{v}$ implies a contradiction.
\end{theorem}
\begin{proof}
By induction on the derivation of $\bigstep{\Omega}{v}$.
\end{proof}
\section{A Quick Case Study in Program Verification: Church Numerals}