Documentation

Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LeftmostReduction

The Leftmost Reduction Theorem #

Reference #

source
def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaNormal {Var : Type u} (m : Term Var) :
Prop

A term is in normal form when it contains no β-redexes.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost {Var : Type u} :
    Term Var → Term Var → Prop

    Leftmost reduction: a β-reduction contracting the redex at position 0.

    Equations
    Instances For
      source
      def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_⭢ℓ_» :
      Lean.TrailingParserDescr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_↠ℓ_» :
        Lean.TrailingParserDescr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaNormal.app_inv {Var : Type u} {L M : Term Var} (h : (L.app M).BetaNormal) :
          ¬L.IsAbs ∧ L.BetaNormal ∧ M.BetaNormal

          In a normal-form application, both sides are normal and the operator is not an abstraction.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaNormal.abs_open {Var : Type u} {M : Term Var} {x : Var} (h : M.abs.BetaNormal) :
          (M.open' (fvar x)).BetaNormal

          The body of a normal-form abstraction opens to a normal form.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.steps_isAbs_r {Var : Type u} {M N : Term Var} (h : Relation.ReflTransGen Leftmost M N) (ha : M.IsAbs) :
          N.IsAbs

          Leftmost reduction preserves being an abstraction.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.steps_app_l_cong {Var : Type u} {L L' M : Term Var} (h : Relation.ReflTransGen Leftmost L L') (hna : ¬L'.IsAbs) :
          Relation.ReflTransGen Leftmost (L.app M) (L'.app M)

          Left congruence for leftmost reduction, provided the target is not an abstraction.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.BetaAt.app_r_cong {Var : Type u} {L M M' : Term Var} {i : ℕ} (h : BetaAt i M M') (hL : L.BetaNormal) (hna : ¬L.IsAbs) :
          BetaAt i (L.app M) (L.app M')

          Reducing the operand across a non-abstraction normal form keeps the position.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.steps_app_r_cong {Var : Type u} {L M M' : Term Var} (h : Relation.ReflTransGen Leftmost M M') (hL : L.BetaNormal) (hna : ¬L.IsAbs) :
          Relation.ReflTransGen Leftmost (L.app M) (L.app M')

          Right congruence for leftmost reduction, provided the operator is a non-abstraction normal form.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.steps_app_cong {Var : Type u} {L L' M M' : Term Var} (hL : Relation.ReflTransGen Leftmost L L') (hM : Relation.ReflTransGen Leftmost M M') (hnf : L'.BetaNormal) (hna : ¬L'.IsAbs) :
          Relation.ReflTransGen Leftmost (L.app M) (L'.app M')

          Congruence for leftmost reduction on applications whose reduced operator is a non-abstraction normal form.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.of_cbn {Var : Type u} {M N : Term Var} (h : Relation.ReflTransGen CBN M N) :
          Relation.ReflTransGen Leftmost M N

          Call-by-Name reduction is contained in leftmost reduction.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.steps_lc_r {Var : Type u} {M M' : Term Var} [DecidableEq Var] [HasFresh Var] (h : Relation.ReflTransGen Leftmost M M') (lc : M.LC) :
          M'.LC

          Leftmost reduction preserves local closure.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.steps_abs_close {Var : Type u} {M M' : Term Var} [DecidableEq Var] [HasFresh Var] {x : Var} (h : Relation.ReflTransGen Leftmost M M') (lc : M.LC) :
          Relation.ReflTransGen Leftmost (closeRec 0 x M).abs (closeRec 0 x M').abs

          Leftmost reduction is preserved by closing a variable and abstracting.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.steps_abs_cong {Var : Type u} {M M' : Term Var} [DecidableEq Var] [HasFresh Var] (xs : Finset Var) (cofin : ∀ x ∉ xs, Relation.ReflTransGen Leftmost (M.open' (fvar x)) (M'.open' (fvar x))) (lc : M.abs.LC) :
          Relation.ReflTransGen Leftmost M.abs M'.abs

          Cofinite congruence rule for leftmost reduction under an abstraction.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.of_standard {Var : Type u} {M N : Term Var} [DecidableEq Var] [HasFresh Var] (h : M.Standard N) (hn : N.BetaNormal) :
          Relation.ReflTransGen Leftmost M N

          A standard reduction to a normal form is a leftmost reduction.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Leftmost.normalization {Var : Type u} {M N : Term Var} [DecidableEq Var] [HasFresh Var] (lc : M.LC) (h : Relation.ReflTransGen FullBeta M N) (hn : N.BetaNormal) :
          Relation.ReflTransGen Leftmost M N

          The leftmost reduction theorem: if a term β-reduces to a normal form, then leftmost reduction reaches it.