Skip to main content

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.

Filter by
Sorted by
Tagged with
4 votes
0 answers
76 views

What are "empty compositions", and why are they bad?

Empty hcomps and empty systems are often mentioned in the context of cubical type theory, in particular related to the efficiency of evaluation, for example here and here. What exactly are they, and ...
Trebor's user avatar
  • 3,967
2 votes
1 answer
196 views

Conflicting terminology for completeness/soundness of normalization algorithm

While reading some articles about formalization of various normalization algorithms, I found that these two papers use the term completeness/soundness in opposite way. Hereditary Substitutions for ...
damhiya's user avatar
  • 123
-1 votes
1 answer
103 views

Implementability of proof assistants for Infinitary logics with finite many terms

Infinitary logic is a natural consequence of extending the length of proofs of first-order logic to a infinite ordinal level. By definition, since proof lengths are infinitely long, one should not ...
Ember Edison's user avatar
2 votes
1 answer
193 views

Higher Observational Type Theory: variables becoming free in reduction rules

This question is based on the talks given by Mike Shulman on higher observational type theory (part 1, part 2, part 3). In trying to understand the reduction rules of the calculus, I tried to work ...
idka's user avatar
  • 73
4 votes
1 answer
225 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) ...
Meven Lennon-Bertrand's user avatar
2 votes
2 answers
187 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 ...
Ms. Molly Stewart-Gallus's user avatar
7 votes
1 answer
319 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 ...
Couchy's user avatar
  • 2,231
11 votes
1 answer
277 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 ...
Trebor's user avatar
  • 3,967
18 votes
1 answer
1k 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 ...
ice1000's user avatar
  • 6,186
10 votes
2 answers
1k 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 ...
Itai Zukerman's user avatar
3 votes
1 answer
96 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 ...
ionchy's user avatar
  • 1,026
18 votes
1 answer
265 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 ...
ice1000's user avatar
  • 6,186