17
votes
Accepted
Constructive proof of strong normalization for simply typed lambda calculus
As Dan Doel says in the comments, the reason Kőnig's lemma is used is that Girard's definition of strong normalization is constructively too weak. It's defined as the non-existence of infinite ...
- 2,077
17
votes
Accepted
How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
To address a most important point, as suggested by Andrej Bauer, Lean's intended model is one where types are sets. Mario Carneiro showed in his master's thesis that Lean has such a set-theoretic ...
- 10.3k
10
votes
Accepted
What is a neutral term?
A neutral term is a variable, or an eliminator stuck on a neutral term. Basically a stack of eliminators applied to a variable.
These terms are called neutral, and distinguished from other normal ...
- 376
10
votes
Accepted
What are the advantages of normalization by evaluation over traditional reduction-based normalization?
When I asked this question of some people with experience implementing proof assistants, their answer was "eta-laws".
If you test equality using only some kind of reduction algorithm, then ...
- 3,270
7
votes
Accepted
Canonical forms of combinators
Combinators all have a predefined arity, and normal forms consist of underapplied combinators, whose arguments are normal forms. This is different from lambda calculi, where you also need neutral ...
- 4,344
7
votes
Accepted
Normalization by evaluation for extensional type theories
For many partial languages, although conversion is undecidable, we can decide conversion up to non-termination. For example, in pure LC, conversion is decidable for the
$\beta$-normalizing terms.
In ...
- 2,077
7
votes
Constructive proof of strong normalization for simply typed lambda calculus
For a modern take on the proof, you can have a look at POPLmark Reloaded.
The paper's appendix explains in great details what the (sometimes technical) proofs are. The paper comes with various ...
- 1,264
6
votes
Accepted
Comparison of normal forms in Normalization by Evaluation
I will present the conversion procedure that is used in András Kovács' Elaboration zoo and its extension to the η-rule for the unit type. It is based on Coquand's type-checking algorithm.
In ...
6
votes
Accepted
Conflicting terminology for completeness/soundness of normalization algorithm
Both answers are correct.
Soundness in general means “nothing bad happens”. In the context of equational theories, the following would be sound phenomena:
A theory is sound (with respect to a given ...
- 11k
5
votes
Accepted
Is unguarded fixpoint reduction consistent?
This is consistent.
First, this equality holds propositionally by eta-expansion of the constructor. Thus, if your type theory had equality reflection, it would also hold definitionally. Since ...
- 2,393
3
votes
Implementability of proof assistants for Infinitary logics with finite many terms
I don't think this question is well formed for the following reasons. As stated in the answer to a similar math stack exchange question, there are uncountable many $\mathcal{L}_{\omega_1, \omega}$ ...
- 10.3k
2
votes
Accepted
Higher Observational Type Theory: variables becoming free in reduction rules
I would guess the issue comes from the $\Delta$ you assumed was missing. As far as I can tell, when living over a general telescope, already
$$
Id_{Δ.(Π (x : A) B)}^δ(f, g)
≡ \Pi (u, v : A). \Pi(p: ...
- 6,008
Only top scored, non community-wiki answers of a minimum length are eligible