From b3692b97a5c63520b99305b318400f502bfd1b5a Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 13 Mar 2016 19:52:46 -0400
Subject: [PATCH] LambdaCalculus chapter: a nonterminating lambda term

---
 LambdaCalculusAndTypeSoundness.v | 15 +++++++++++++++
 frap_book.tex                    | 11 +++++++++++
 2 files changed, 26 insertions(+)

diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v
index 300ddba..ec9d464 100644
--- a/LambdaCalculusAndTypeSoundness.v
+++ b/LambdaCalculusAndTypeSoundness.v
@@ -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 *)
diff --git a/frap_book.tex b/frap_book.tex
index fa108e3..cc1b9c2 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -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}