λ-calculus

The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.

References

• A. Chargueraud, The Locally Nameless Representation
• See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which this is adapted

inductive Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty (Var : Type u_2) : Type u_2

Types of the polymorphic lambda calculus.

• top {Var : Type u_2} : Ty Var

  The type ⊤, with a single inhabitant.

• bvar {Var : Type u_2} : ℕ → Ty Var

  Bound variables that appear in a type, using a de-Bruijn index.

• fvar {Var : Type u_2} : Var → Ty Var

  Free type variables.

• arrow {Var : Type u_2} : Ty Var → Ty Var → Ty Var

  A function type.

• all {Var : Type u_2} : Ty Var → Ty Var → Ty Var

  A universal quantification.

• sum {Var : Type u_2} : Ty Var → Ty Var → Ty Var

  A sum type.

@[implicit_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedTy {a✝ : Type u_2} : Inhabited (Ty a✝)

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedTy = { default := Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedTy.default }

inductive Cslib.LambdaCalculus.LocallyNameless.Fsub.Term (Var : Type u_2) : Type u_2

Syntax of locally nameless lambda terms, with free variables over Var.

• bvar {Var : Type u_2} : ℕ → Term Var

  Bound term variables that appear under a lambda abstraction, using a de-Bruijn index.

• fvar {Var : Type u_2} : Var → Term Var

  Free term variables.

• abs {Var : Type u_2} : Ty Var → Term Var → Term Var

  Lambda abstraction, introducing a new bound term variable.

• app {Var : Type u_2} : Term Var → Term Var → Term Var

  Function application.

• tabs {Var : Type u_2} : Ty Var → Term Var → Term Var

  Type abstraction, introducing a new bound type variable.

• tapp {Var : Type u_2} : Term Var → Ty Var → Term Var

  Type application.

• let' {Var : Type u_2} : Term Var → Term Var → Term Var

  Binding of a term.

• inl {Var : Type u_2} : Term Var → Term Var

  Left constructor of a sum.

• inr {Var : Type u_2} : Term Var → Term Var

  Right constructor of a sum.

• case {Var : Type u_2} : Term Var → Term Var → Term Var → Term Var

  Case matching on a sum.

inductive Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding (Var : Type u_2) : Type u_2

A context binding.

• sub {Var : Type u_2} : Ty Var → Binding Var

  Subtype binding.

• ty {Var : Type u_2} : Ty Var → Binding Var

  Type binding.

@[implicit_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedBinding {a✝ : Type u_2} : Inhabited (Binding a✝)

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedBinding = { default := Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedBinding.default }

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fv {Var : Type u_1} [DecidableEq Var] : Ty Var → Finset Var

Free variables of a type.

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.top.fv = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.bvar a).fv = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar X).fv = {X}
• (σ.arrow τ).fv = σ.fv ∪ τ.fv
• (σ.all τ).fv = σ.fv ∪ τ.fv
• (σ.sum τ).fv = σ.fv ∪ τ.fv

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.fv {Var : Type u_1} [DecidableEq Var] : Binding Var → Finset Var

Free variables of a binding.

Equations

• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub σ).fv = σ.fv
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty σ).fv = σ.fv

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvTy {Var : Type u_1} [DecidableEq Var] : Term Var → Finset Var

Free type variables of a term.

Equations

• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar a).fvTy = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar a).fvTy = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.abs σ t₁).fvTy = σ.fv ∪ t₁.fvTy
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.tabs σ t₁).fvTy = σ.fv ∪ t₁.fvTy
• (t₁.tapp σ).fvTy = σ.fv ∪ t₁.fvTy
• t₁.inl.fvTy = t₁.fvTy
• t₁.inr.fvTy = t₁.fvTy
• (t₁.app t₂).fvTy = t₁.fvTy ∪ t₂.fvTy
• (t₁.let' t₂).fvTy = t₁.fvTy ∪ t₂.fvTy
• (t₁.case t₂ t₃).fvTy = t₁.fvTy ∪ t₂.fvTy ∪ t₃.fvTy

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvTm {Var : Type u_1} [DecidableEq Var] : Term Var → Finset Var

Free term variables of a term.

Equations

• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar a).fvTm = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar a).fvTm = {a}
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.abs σ t₁).fvTm = t₁.fvTm
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.tabs σ t₁).fvTm = t₁.fvTm
• (t₁.tapp σ).fvTm = t₁.fvTm
• t₁.inl.fvTm = t₁.fvTm
• t₁.inr.fvTm = t₁.fvTm
• (t₁.app t₂).fvTm = t₁.fvTm ∪ t₂.fvTm
• (t₁.let' t₂).fvTm = t₁.fvTm ∪ t₂.fvTm
• (t₁.case t₂ t₃).fvTm = t₁.fvTm ∪ t₂.fvTm ∪ t₃.fvTm

@[reducible, inline]

abbrev Cslib.LambdaCalculus.LocallyNameless.Fsub.Env (Var : Type u_2) : Type u_2

A context of bindings.

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.Env Var = Cslib.LambdaCalculus.LocallyNameless.Context Var (Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding Var)