add Q comparing our exposition to The Little Schemer's
[lambda.git] / topics / _week5_simply_typed_lambda.mdwn
index 6c97df3..14e2172 100644 (file)
@@ -255,3 +255,12 @@ the predecessor function in the lambda calculus.  Could one of them
 possibly be simply-typeable?  It turns out that this can't be done.
 See the works cited by Oleg for details.
 
 possibly be simply-typeable?  It turns out that this can't be done.
 See the works cited by Oleg for details.
 
+Because lists are (in effect) a generalization of the Church numbers,
+computing the tail of a list is likewise beyond the reach of the
+simply-typed lambda calculus.
+
+This result is surprising.  It illustrates how recursion is built into
+the structure of the Church numbers (and lists).  Most importantly for
+the discussion of the simply-typed lambda calculus, it demonstrates
+that even fairly basic recursive computations are beyond the reach of
+a simply-typed system.