Problem # 26
Submitted by Henk Barendregt
Statement. Assign (in an ‘easy’ way) ordinals to terms of the simply typed
lambda calculus such that reduction of the term yields a smaller ordinal.
Problem Origin. First posed by Kurt Gödel.
[PRINT this PROBLEM]
Construct an ‘easy’ assignment of (possibly trans-ﬁnite) ordinals to terms of
the simply typed lambda calculus, i.e. a map
By the fact that the ordinals are well-ordered, this immediately shows
that -reduction on simply typed lambda terms is strongly normalizing
- This item in the list of open problems is actually not a problem but a
(mathematical) ‘koan’. A problem, according to [Pólya, 2004], should
have the property that a candidate solution is clearly recognizable as
such in a well-deﬁned way. The proof of correctness of the candidate
solution still may be hard. A koan, according to Jan Willem Klop, is
a non-precise question for which the space of solutions is a priori not
But once a right solution is given, it should be recognizable as such. For
example, two centuries ago it was a mathematical koan what is the right
deﬁnition of the notion ‘continuous function’ on the real numbers. Or
one century ago, there was the koan ‘Why do some isomorphisms feel
to be more natural than other ones?’ The pondering over this question
by Eilenberg and MacLane led to the introduction of the notion of a
category. The present item is a koan, because the notion of ‘easy’ in its
formulation is not well-deﬁned.
- Once we know SN() on , we can deﬁne
This assignment satisﬁes (+) and even assigns ﬁnite ordinals to terms.
But the purpose of this ‘koan’ is to prove SN in an easy way and this
‘solution’ presupposes that SN holds.
- In [de Vrijer, 1987] the value of (ii) is deﬁned by an analysis of
. But the construction is not ‘easy’.
- Alan Turing has given a simple map (1) such that for all not in
normal form there exists a reduct such that . This
establishes weak normalization (WN), but not SN. In “Alan Turing:
His Work and Impact”, see [Barendregt and Manzonetto, 2013].
- W.A. Howard (see [Howard,
1970]), to whom (personal communication) Gödel had originally asked
the present koan for the system (also including numerals and the
recursor) and [Wilken and Weiermann, 2012], made signiﬁcant steps
(but not a ﬁnal one) towards solving this item. Howard’s construction
works only for combinatory terms. Wilken and Weiermann, extending
Howard’s work, assigns ordinals to terms and their previous reduction
past; this establishes SN, but doesn’t solve Gödel’s koan.
References for # 26
[Barendregt and Manzonetto, 2013] Barendregt, H. and Manzonetto, G.
(2013). Turing’s contributions to lambda calculus. In Cooper, S. B.
and van Leeuwen, J., editors, Alan Turing: His Work and Impact, pages
[de Vrijer, 1987] de Vrijer, R. (1987). Exactly estimating functionals
and strong normalization. Indagationes Mathematicae, 49:479–493.
[Howard, 1970] Howard, W. (1970). Assignment of ordinals to terms for
primitive recursive functionals of ﬁnite type. In A. Kino, J. M. and Vesley,
R., editors, Intuitionism and Proof Theory: Proceedings of the Summer
Conference at Buffalo N.Y. 1968, volume 60 of Studies in Logic and the
Foundations of Mathematics, pages 443 – 458. Elsevier.
[Pólya, 2004] Pólya, G. (2004). How to Solve It: A New Aspect of
Mathematical Method. Penguin mathematics. Princeton University Press.
Expanded version of the 1988 edition, with a new foreword by John H.
[Wilken and Weiermann, 2012] Wilken, G. and Weiermann, A. (2012).
Derivation lengths classiﬁcation of Gödel’s extending Howard’s
assignment. Logical Methods in Computer Science, 8(1):44.
Last modified: July 21, 2014