Standard Reduction and the Standardization Theorem #
References #
- [B. Calisto, Formalization in Coq of the Standardization Theorem for λ-calculus][Calisto2022]
- [M. Copes, A machine-checked proof of the Standardization Theorem in λ-calculus][Copes2018]
Main definitions #
A standard β-reduction sequence contracts redexes at non-decreasing positions. The index
n is the last position contracted.
- refl
{Var : Type u}
{n : ℕ}
{M : Term Var}
: StandardSeq n M M
The empty sequence.
- tail
{Var : Type u}
{n : ℕ}
{M P : Term Var}
{m : ℕ}
{N : Term Var}
: StandardSeq n M P → BetaAt m P N → n ≤ m → StandardSeq m M N
Append a β-step whose position is no earlier than the previous one.
Instances For
The Standard reduction relation.
- fvar
{Var : Type u}
(x : Var)
: (Term.fvar x).Standard (Term.fvar x)
Free variables standardly reduce to themselves.
- app
{Var : Type u}
{L L' M M' : Term Var}
: L.Standard L' → M.Standard M' → (L.app M).Standard (L'.app M')
Congruence rule for application.
- abs
{Var : Type u}
{m m' : Term Var}
(xs : Finset Var)
: (∀ x ∉ xs, (m.open' (Term.fvar x)).Standard (m'.open' (Term.fvar x))) → m.abs.Standard m'.abs
Congruence rule for lambda terms.
- rdx
{Var : Type u}
{m n m' p : Term Var}
: m.LC → n.LC → Relation.ReflTransGen CBN m m'.abs → (m'.open' n).Standard p → (m.app n).Standard p
Standard reduction of a head redex.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Basic properties #
A Call-by-Name reduction followed by a standard reduction is a standard reduction.
Call-by-Name reduction is contained in standard reduction.
Standard sequences #
Standard sequences preserve being an abstraction.
A standard sequence preceded by a step at position 0 remains standard.
A standard sequence stays standard when preceded by a Call-by-Name reduction.
Right congruence for standard sequences when the operator is an abstraction.
Right congruence for standard sequences when the operator is a non-abstraction.
Right application congruence for standard sequences.
The final position of a nonempty standard sequence is at most its target's redex count.
Reducing the operator of an application yields a standard sequence, with the final position bounded.
A nonempty operator reduction lifts to the application, bounded by the operator's redex count.
Append an operand step to a standard sequence of applications.
Compose an application sequence with a standard reduction of its operand.
If operator and operand each reduce by a standard sequence, so does the application.
Standardization #
Standard reduction is preserved by substitution.
A single full β-step is a standard reduction.
Standard reduction is contained in full β-reduction.
If a standard reduction reaches an abstraction, then its leading Call-by-Name reduction reaches an abstraction that standardly reduces to the same target.
A standard reduction followed by a full β-step is a standard reduction.
A standard reduction followed by a full β-reduction is a standard reduction.
Standard reduction is transitive.
Equations
Equations
Equations
The standardization theorem: every full β-reduction is a standard reduction.
Standard reduction coincides with full β-reduction on locally closed terms.
Equivalence with standard sequences #
Standard sequences preserve local closure.
Closing a variable and abstracting preserves a standard sequence.
Abstraction congruence for standard sequences.
A standard sequence is a full β-reduction.
A standard reduction gives a standard β-reduction sequence.
A standard β-reduction sequence gives a standard reduction.
Standard reduction coincides with the existence of a standard β-reduction sequence.