Redex Positions

This module defines β-reduction at a given redex position and proves its basic properties.

Reference

• M. Copes, A machine-checked proof of the Standardization Theorem in λ-calculus

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.countRedexes {Var : Type u} : Term Var → ℕ

The number of β-redexes occurring in a term.

Equations

• (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.fvar a).countRedexes = 0
• (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.bvar a).countRedexes = 0
• m.abs.countRedexes = m.countRedexes
• (m.abs.app n).countRedexes = m.countRedexes + n.countRedexes + 1
• (m.app n).countRedexes = m.countRedexes + n.countRedexes

inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt {Var : Type u} : ℕ → Term Var → Term Var → Prop

BetaAt i M N reduces the redex at position i of M to obtain N; positions are counted from left to right.

• outer {Var : Type u} {M N : Term Var} : M.abs.LC → N.LC → BetaAt 0 (M.abs.app N) (M.open' N)

  The outermost redex sits at position 0.

• appL {Var : Type u} {i : ℕ} {M M' N : Term Var} : BetaAt i M M' → BetaAt (i + if M.IsAbs then 1 else 0) (M.app N) (M'.app N)

  Reducing the operator advances the position by one when the operator is an abstraction.

• appR {Var : Type u} {i : ℕ} {M M' N : Term Var} : BetaAt i M M' → BetaAt (i + N.countRedexes + if N.IsAbs then 1 else 0) (N.app M) (N.app M')

  Reducing the operand adds the operator's redex count, plus one when it is an abstraction.

• abs {Var : Type u} {i : ℕ} {M M' : Term Var} (xs : Finset Var) : (∀ x ∉ xs, BetaAt i (M.open' (fvar x)) (M'.open' (fvar x))) → BetaAt i M.abs M'.abs

  Reducing under a binder keeps the position.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.appNoAbsL {Var : Type u} {M M' N : Term Var} {i : ℕ} (h : BetaAt i M M') (hna : ¬M.IsAbs) : BetaAt i (M.app N) (M'.app N)

Reducing a non-abstraction operator keeps the position.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.appAbsL {Var : Type u} {M M' N : Term Var} {i : ℕ} (h : BetaAt i M M') (ha : M.IsAbs) : BetaAt (i + 1) (M.app N) (M'.app N)

Reducing an abstraction operator advances the position by one.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.appNoAbsR {Var : Type u} {M M' N : Term Var} {i : ℕ} (h : BetaAt i M M') (hna : ¬N.IsAbs) : BetaAt (i + N.countRedexes) (N.app M) (N.app M')

Reducing the operand adds the redex count of a non-abstraction operator.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.appAbsR {Var : Type u} {M M' N : Term Var} {i : ℕ} (h : BetaAt i M M') (ha : N.IsAbs) : BetaAt (i + N.countRedexes + 1) (N.app M) (N.app M')

Reducing the operand adds the redex count of an abstraction operator, plus one.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.countRedexes_openRec_fvar {Var : Type u} (M : Term Var) (k : ℕ) (x : Var) : (openRec k (fvar x) M).countRedexes = M.countRedexes

Opening with a free variable preserves the number of redexes.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.countRedexes_open_fvar {Var : Type u} (M : Term Var) (x : Var) : (M.open' (fvar x)).countRedexes = M.countRedexes

Opening the outermost binder with a free variable preserves the number of redexes.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.countRedexes_app_le {Var : Type u} (M N : Term Var) : M.countRedexes + N.countRedexes ≤ (M.app N).countRedexes

An application has at least as many redexes as its operator and operand combined.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.countRedexes_app_abs {Var : Type u} {M : Term Var} (ha : M.IsAbs) (N : Term Var) : (M.app N).countRedexes = M.countRedexes + N.countRedexes + 1

An application with an abstraction operator has one more redex than its parts.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.isAbs_r {Var : Type u} {M N : Term Var} {i : ℕ} (h : BetaAt i M N) (ha : M.IsAbs) : N.IsAbs

Contracting a redex of an abstraction yields an abstraction.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.cbn_not_isAbs {Var : Type u} {M N : Term Var} (h : M.CBN N) : ¬M.IsAbs

The source of a Call-by-Name step is never an abstraction.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.of_cbn_step {Var : Type u} {M N : Term Var} (h : M.CBN N) : BetaAt 0 M N

A single Call-by-Name step contracts the redex at position 0.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.countRedexes_subst_fvar {Var : Type u} [DecidableEq Var] (M : Term Var) (x y : Var) : M[x := fvar y].countRedexes = M.countRedexes

Renaming a free variable preserves the number of redexes.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.isAbs_subst_fvar {Var : Type u} {M : Term Var} [DecidableEq Var] {x y : Var} : M[x := fvar y].IsAbs ↔ M.IsAbs

Renaming a free variable preserves being an abstraction.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.to_step {Var : Type u} {M N : Term Var} {i : ℕ} [DecidableEq Var] (h : BetaAt i M N) (lc : M.LC) : M.FullBeta N

A BetaAt step is a full β-step.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.le_countRedexes {Var : Type u} {M N : Term Var} {i : ℕ} [HasFresh Var] (h : BetaAt i M N) : i ≤ N.countRedexes

The position of a contracted redex is at most the redex count of the result.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.rename {Var : Type u} {M M' : Term Var} {i : ℕ} [HasFresh Var] [DecidableEq Var] (h : BetaAt i M M') (x y : Var) : BetaAt i M[x := fvar y] M'[x := fvar y]

Renaming a free variable preserves the position of the contracted redex.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.lc_r {Var : Type u} {M M' : Term Var} {i : ℕ} [HasFresh Var] [DecidableEq Var] (h : BetaAt i M M') (lc : M.LC) : M'.LC

Contracting a redex preserves local closure.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.abs_close {Var : Type u} {M M' : Term Var} {i : ℕ} [HasFresh Var] [DecidableEq Var] {x : Var} (h : BetaAt i M M') (lc : M.LC) : BetaAt i (closeRec 0 x M).abs (closeRec 0 x M').abs

Closing a variable and abstracting preserves the position of the contracted redex.