# Tag Info

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
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 ...
• 9,195
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 ...
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,200
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,025
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

### 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,266
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 ...
• 9,802
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,335
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 ...

### 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}$ ...
• 9,195
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: ...