Skip to main content
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 ...
András Kovács's user avatar
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 ...
Jason Rute's user avatar
  • 9,195
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 ...
Matthew McQuaid's user avatar
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 ...
Mike Shulman's user avatar
  • 3,200
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 ...
Trebor's user avatar
  • 4,025
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 ...
András Kovács's user avatar
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 ...
gallais's user avatar
  • 1,266
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 ...
Andrej Bauer's user avatar
  • 9,802
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 ...
Pierre-Marie Pédrot's user avatar
5 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 ...
Rafaël Bocquet's user avatar
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}$ ...
Jason Rute's user avatar
  • 9,195
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: ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible