[Previous]  [Up]

#### Problem # 26

Submitted by Henk Barendregt
Date: 2014
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

such that
By the fact that the ordinals are well-ordered, this immediately shows that -reduction on simply typed lambda terms is strongly normalizing (SN).

1. 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 clear. 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.
2. 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.
3. In [de Vrijer, 1987] the value of (ii) is deﬁned by an analysis of . But the construction is not ‘easy’.
4. 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].
5. 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 139–143. Elsevier.

[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. Conway.

[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.

[Previous]  [Up]