[PL-sem-jr] Talk tomorrow, 11/30

[Jed Davis]

Here, incidentally, is a definition of Ackermann's function in Coq:

Fixpoint ack m := fix ackm n :=
  match (m, n) with
    | (O, n) => S n
    | (S m', O) => ack m' 1
    | (S m', S n') => ack m' (ackm n')
  end.

What we're doing here that can't be done in primitive recursive
arithmetic is, I think, the outer fixpoint, which constructs a function
in nat->nat (rather than just a first-order value) by structural
induction/recursion on m.

-- 
(let ((C call-with-current-continuation)) (apply (lambda (x y) (x y)) (map
((lambda (r) ((C C) (lambda (s) (r (lambda l (apply (s s) l))))))  (lambda
(f) (lambda (l) (if (null? l) C (lambda (k) (display (car l)) ((f (cdr l))
(C k)))))))    '((#\J #\d #\D #\v #\s) (#\e #\space #\a #\i #\newline)))))