<p>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.</p>

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

<p>In particular, weak normalization proofs seem remarkably simpler, possibly due to weakly normalizing terms having the structure of a <a href="https://ncatlab.org/nlab/show/partial+combinatory+algebra" rel="noreferrer">Partial Combinatory Algebra</a>, which is not the case for strongly normalizing terms, as explained at length in a '93 paper by <a href="https://www.dpmms.cam.ac.uk/~martin/Research/Pub91-00/ho93.pdf" rel="noreferrer">Hyland and Ong</a>. Even simpler are proofs of <strong>existence of normal forms</strong>, which are the result of applying the technique of <a href="http://www.cse.chalmers.se/~peterd/papers/NbeMLTTEqualityJudgements.pdf" rel="noreferrer">Normalization by Evaluation</a>, which, IMO, are the "conceptually correct" proofs.</p>

<p>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.</p>

<p>A satisfying resolution to the question would <em>explain</em> why a proof of WN or NbE can be <strong>promoted</strong> 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.</p>

CC BY-SA 4.0
2020-01-03T15:19:38.430Z
In which sense is our understanding of normalisation proofs "rapidly changing"? I've stopped following this field for a while.
Martin Berger
CC BY-SA 4.0
2020-01-03T16:49:07.107Z
The two papers "Normalization by gluing for free $\lambda$-theories" (https://arxiv.org/pdf/1809.08646.pdf) and "Gluing for Type Theory" (https://drops.dagstuhl.de/opus/volltexte/2019/10532/pdf/LIPIcs-FSCD-2019-25.pdf) are from 2018 and 2019, respecively, and give a nice synthetic overview of the NbE approach.
cody
CC BY-SA 4.0
2020-01-04T07:42:05.810Z
IMHO you should delete the "not an expert" qualification.
Andrej Bauer
CC BY-SA 4.0
2020-01-05T16:25:21.813Z
I'll delete it only when I understand why the Coquand-Herbelin technique doesn't generalize to dependent PTSes :)
cody
CC BY-SA 4.0
2020-01-03T15:10:08.120Z
2020-01-03T15:10:08.120Z
cody
<p>I was learning about type systems from Benjamin C. Pierce's <em>Types and Programming Languages</em> and came across the <a href="https://en.wikipedia.org/wiki/Lambda_cube" rel="noreferrer">Lambda cube</a> in the chapter on Higher-Order Polymorphism. After reading up more about it on Wikipedia I learnt about its generalization, <a href="https://en.wikipedia.org/wiki/Pure_type_system" rel="noreferrer">Pure type system</a> where it is mentioned that</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>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).</p>

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

<p><strong>Update</strong>
I found a paper that proves that <a href="https://core.ac.uk/download/pdf/82789255.pdf" rel="noreferrer">Weak normalization implies strong normalization in a class
of non-dependent pure type systems</a>, however it says nothing about applications</p>

<type-theory><lambda-calculus>
Applications of Barendregt–Geuvers–Klop conjecture
brj
# Applications of Barendregt–Geuvers–Klop conjecture

(Asked by: username_0 on 2020-01-02)

I was learning about type systems from Benjamin C. Pierce's *Types and Programming Languages* and came across the [Lambda cube](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/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](https://core.ac.uk/download/pdf/82789255.pdf), however it says nothing about applications

**Tags:** type-theory, lambda-calculus


---

## 1 answers

### Answer by username_1 on 2020-01-03. Score: 12

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](https://ncatlab.org/nlab/show/partial+combinatory+algebra), which is not the case for strongly normalizing terms, as explained at length in a '93 paper by [Hyland and Ong](https://www.dpmms.cam.ac.uk/~martin/Research/Pub91-00/ho93.pdf). Even simpler are proofs of **existence of normal forms**, which are the result of applying the technique of [Normalization by Evaluation](http://www.cse.chalmers.se/~peterd/papers/NbeMLTTEqualityJudgements.pdf), 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.

> **Comments:**
> **username_2**: In which sense is our understanding of normalisation proofs "rapidly changing"? I've stopped following this field for a while.  
> **username_1**: The two papers "Normalization by gluing for free $\lambda$-theories" (https://arxiv.org/pdf/1809.08646.pdf) and "Gluing for Type Theory" (https://drops.dagstuhl.de/opus/volltexte/2019/10532/pdf/LIPIcs-FSCD-2019-25.pdf) are from 2018 and 2019, respecively, and give a nice synthetic overview of the NbE approach.  
> **username_3**: IMHO you should delete the "not an expert" qualification.  
> **username_1**: I'll delete it only when I understand why the Coquand-Herbelin technique doesn't generalize to dependent PTSes :)  

---

