| Submitted by Morten Heine Sørensen Date: 1993 Statement. Is every weakly normalizing PTS also strongly normalizing? Problem Origin. The problem was posed by Henk Barendregt, Herman Geuvers (2007) | |||||||||||||||
Abstract | |||||||||||||||
| The conjecture that the above statement can be answered in the positive is known as the Barendregt-Geuvers-Klop conjecture. It was presented to the originator by Henk Barendregt some time in 1994. Is is stated as (part of) Conjecture 8.1.2 in [Geuvers, 1993]. A partial solution, confirming that the conjecture is true for a certain class of nondependent systems, appeared in [Sørensen, 1997, Barthe et al., 2001]. It is natural to wonder how the result can be extended to larger classes of pure type systems. An obvious line of attack is to study translations that eliminate dependency, and to establish preservation of the necessary normalization properties (see Definition 6.5.23 in [Geuvers, 1993] for a translation eliminating dependency in the cube). Another idea, which will probably only lead to marginal improvements, is to replace the CPS-translation of [Sørensen, 1997, Barthe et al., 2001] by a simpler thunkification translation or another translation with similar properties (see [Gørtz et al., 2003]). A related conjecture is the so-called K-conjecture [Barthe, 1995], which is shown to follow from the Barendregt-Geuvers-Klop conjecture within the class of functional pure type systems [Barthe, 1998]. See also [Ketema et al., 2005]. | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||