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
6 votes
1 answer
150 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 ...
user avatar
  • 1,662
9 votes
1 answer
141 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 ...
user avatar
  • 2,246
16 votes
1 answer
794 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 ...
user avatar
  • 4,136
9 votes
3 answers
766 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 ...
user avatar
3 votes
1 answer
78 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 ...
user avatar
  • 856
17 votes
1 answer
127 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 ...
user avatar
  • 4,136