5
$\begingroup$

I was learning about type systems from Benjamin C. Pierce's Types and Programming Languages and came across the Lambda cube in the chapter on Higher-Order Polymorphism. After reading up more about it on Wikipedia I learnt about its generalization, Pure type system where it is mentioned that

It is a major open problem in the field whether this is always the case, i.e. whether a (weakly) normalizing PTS always has the strong normalization property.This is known as the Barendregt–Geuvers–Klop conjecture.

However, I am unable to think of practical applications of a proof (or disproof) of the above conjecture (perhaps due to my limited knowledge of type theory).

Question: What are the practical applications of a proof (or disproof) of the Barendregt–Geuvers–Klop conjecture?

Update I found a paper that proves that Weak normalization implies strong normalization in a class of non-dependent pure type systems, however it says nothing about applications

$\endgroup$
7
$\begingroup$

I'm not (exactly) an expert, but my understanding is that there are very few practical applications of this conjecture, except possibly simplifying the decision procedure for type-checking in normalizing theories, by allowing one to choose any reduction strategy with confidence.

My feeling about this conjecture is that it is an important litmus test on our understanding of normalization proofs in general, which at the moment (though this is rapidly changing) are somewhat ad hoc.

In particular, weak normalization proofs seem remarkably simpler, possibly due to weakly normalizing terms having the structure of a Partial Combinatory Algebra, which is not the case for strongly normalizing terms, as explained at length in a '93 paper by Hyland and Ong. Even simpler are proofs of existence of normal forms, which are the result of applying the technique of Normalization by Evaluation, which, IMO, are the "conceptually correct" proofs.

Given the difference of these 3 notions (SN, WN, existence of normal forms), one might be surprised that we have no examples of "natural" type systems where they don't all coincide (though for the latter 2, one can simply reason about the combinatorics of reductions). In the limited case of PTSes, this is what the BGK conjecture asks.

A satisfying resolution to the question would explain why a proof of WN or NbE can be promoted to a proof of SN, possibly by building a notion of normalization model which coincides in the case of PTSes. This desire for understanding is the principal motivation for the conjecture.

| cite | improve this answer | |
$\endgroup$
  • 1
    $\begingroup$ In which sense is our understanding of normalisation proofs "rapidly changing"? I've stopped following this field for a while. $\endgroup$ – Martin Berger Jan 3 at 15:19
  • $\begingroup$ The two papers "Normalization by gluing for free $\lambda$-theories" (arxiv.org/pdf/1809.08646.pdf) and "Gluing for Type Theory" (drops.dagstuhl.de/opus/volltexte/2019/10532/pdf/…) are from 2018 and 2019, respecively, and give a nice synthetic overview of the NbE approach. $\endgroup$ – cody Jan 3 at 16:49
  • 4
    $\begingroup$ IMHO you should delete the "not an expert" qualification. $\endgroup$ – Andrej Bauer Jan 4 at 7:42
  • 2
    $\begingroup$ I'll delete it only when I understand why the Coquand-Herbelin technique doesn't generalize to dependent PTSes :) $\endgroup$ – cody Jan 5 at 16:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.