[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-finite) ordinals to terms of the simply typed lambda calculus, i.e. a map

# : Λ → → {α ∣ α is an ordinal}, (1)
such that
∀M, N ∈ Λ →[M → β N ⇒ #M > #N ]. (2)
By the fact that the ordinals are well-ordered, this immediately shows that β -reduction on simply typed lambda terms is strongly normalizing (SN).

Comments.

  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-defined 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 clear1 . 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 definition 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-defined.
  2. Once we know SN(→ β ) on Λ→ , we can define
    #M = the length of the longest path from M to normal form.
    This assignment satisfies (+) and even assigns finite 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 #M of (ii) is defined by an analysis of M . But the construction is not ‘easy’.
  4. Alan Turing has given a simple map (1) such that for all M not in β normal form there exists a reduct N such that #M > #N . 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 T (also including numerals and the recursor) and [Wilken and Weiermann, 2012], made significant steps (but not a final 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 finite 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 classification of Gödel’s T extending Howard’s assignment. Logical Methods in Computer Science, 8(1):44.

[Previous]  [Up]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014