Documentation

Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName

Call-by-Name Evaluation #

source
inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.CBN {Var : Type u} :
Term Var → Term Var → Prop

A single step of Call-by-Name evaluation.

  • base {Var : Type u} {M N : Term Var} : M.Beta N → M.CBN N

    Top-level β-reduction.

  • app {Var : Type u} {Z M N : Term Var} : Z.LC → M.CBN N → (M.app Z).CBN (N.app Z)

    Evaluates the leftmost term.

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.CBN.lc_l {Var : Type u} {M N : Term Var} (step : M.CBN N) :
        M.LC

        The left side of a Call-by-Name step is locally closed.

        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.CBN.step_to_redex {Var : Type u} {M N : Term Var} (step : M.CBN N) :
        Relation.ReflTransGen FullBeta M N

        A single Call-by-Name step is a full β-reduction.

        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.CBN.to_redex {Var : Type u} {M N : Term Var} (step : Relation.ReflTransGen CBN M N) :
        Relation.ReflTransGen FullBeta M N

        Call-by-Name reduction is contained in full β-reduction.

        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.CBN.steps_app_l_cong {Var : Type u} {M M' N : Term Var} (step : Relation.ReflTransGen CBN M M') (lc_N : N.LC) :
        Relation.ReflTransGen CBN (M.app N) (M'.app N)

        Left congruence rule for application in Call-by-Name reduction.

        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.CBN.lc_r {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] (step : M.CBN N) :
        N.LC

        The right side of a Call-by-Name step is locally closed.

        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.CBN.steps_lc_r {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] (lc_M : M.LC) (step : Relation.ReflTransGen CBN M N) :
        N.LC

        The right side of a Call-by-Name reduction is locally closed.

        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.CBN.step_subst {Var : Type u} {M M' N : Term Var} [HasFresh Var] [DecidableEq Var] (x : Var) (h : M.CBN M') (lc_N : N.LC) :
        M[x := N].CBN M'[x := N]

        Substitution preserves a single Call-by-Name step.

        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.CBN.steps_subst {Var : Type u} {M M' N : Term Var} [HasFresh Var] [DecidableEq Var] (x : Var) (step : Relation.ReflTransGen CBN M M') (lc_N : N.LC) :
        Relation.ReflTransGen CBN M[x := N] M'[x := N]

        Substitution preserves Call-by-Name reduction.