X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_simply_typed_lambda.mdwn;h=14e21729d3c573984875fcdd4dca223008622f1a;hp=6c97df3ca82b684700e293e05abf0d6bc1a5d7f7;hb=c70ea8653fd391ba094c8a64419f3532af2076ce;hpb=6417e111947a187f839267b3e6ca8d4e81cfcf4f

diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 6c97df3c..14e21729 100644
--- a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ -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.
 
+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.