Questions tagged [normalization]
Use this tag for normalization: the process of reducing something (e.g. a formula) to a better form by a given criterion.
8
questions
2
votes
0
answers
48
views
Comparison of normal forms in Normalization by Evaluation
From what I understand of Normalization by Evaluation (NbE) as a technique to implement conversion, it 1) computes (some representation of) normal forms for each of the terms to compare, and 2) ...
- 2,812
2
votes
1
answer
116
views
Canonical forms of combinators
Binders are painful when dealing with metatheory. Combinators are one potential approach to avoid the pain of binders. But it'd be nice if I could normalize combinators to canonical forms. Is there ...
- 2,546
7
votes
1
answer
188
views
What is a neutral term?
A neutral/normal term in the lambda calculus is typically defined
data nf = Lam of nf | Neu of ne
data ne = Var of int | App of ne * nf
Now the question is what to ...
- 1,908
10
votes
1
answer
179
views
Normalization by evaluation for extensional type theories
Is there material on how to implement normalization for (any flavor of) ETT?
This describes techniques related to doing untyped normalization. But there are (operational and semantic) problems when ...
- 3,061
16
votes
1
answer
925
views
How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
This document showed that Lean's impredicative universe of strict propositions breaks normalization (of proofs) in a way that canonicity and logical consistency are unaffected, because the ...
- 4,992
10
votes
3
answers
846
views
Constructive proof of strong normalization for simply typed lambda calculus
I'm reading Girard's Proofs and Types, and in section 4.4 he writes:
Lemma: t is strongly normalisable iff there is a number ...
- 345
3
votes
1
answer
86
views
Is unguarded fixpoint reduction consistent?
In Coq, there are two restrictions on fixpoints to retain normalization:
Recursive calls can only be done on structurally smaller arguments, enforced by a guard condition during type checking; and
...
- 896
17
votes
1
answer
153
views
What are the advantages of normalization by evaluation over traditional reduction-based normalization?
I think in NBE, you get rid of certain substitutions, and it solves the problem of binding representation (so you don't have to use indices or capture-avoiding substitution or something). But I ...
- 4,992