Binding Semantics

Abstract interface for H&K-style assignment-based binding semantics.

structure Interfaces.BindingSemantics.Position : Type

A position in a syntactic structure.

• index : Nat

  Linear index (word position)

instance Interfaces.BindingSemantics.instReprPosition : Repr Position

Equations

• Interfaces.BindingSemantics.instReprPosition = { reprPrec := Interfaces.BindingSemantics.instReprPosition.repr }

def Interfaces.BindingSemantics.instReprPosition.repr : Position → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Interfaces.BindingSemantics.instDecidableEqPosition.decEq (x✝ x✝¹ : Position) : Decidable (x✝ = x✝¹)

Equations

• Interfaces.BindingSemantics.instDecidableEqPosition.decEq { index := a } { index := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Interfaces.BindingSemantics.instDecidableEqPosition : DecidableEq Position

Equations

• Interfaces.BindingSemantics.instDecidableEqPosition = Interfaces.BindingSemantics.instDecidableEqPosition.decEq

def Interfaces.BindingSemantics.instBEqPosition.beq : Position → Position → Bool

Equations

• Interfaces.BindingSemantics.instBEqPosition.beq { index := a } { index := b } = (a == b)
• Interfaces.BindingSemantics.instBEqPosition.beq x✝¹ x✝ = false

instance Interfaces.BindingSemantics.instBEqPosition : BEq Position

Equations

• Interfaces.BindingSemantics.instBEqPosition = { beq := Interfaces.BindingSemantics.instBEqPosition.beq }

def Interfaces.BindingSemantics.instHashablePosition.hash : Position → UInt64

Equations

• Interfaces.BindingSemantics.instHashablePosition.hash { index := a } = mixHash 0 (hash a)

instance Interfaces.BindingSemantics.instHashablePosition : Hashable Position

Equations

• Interfaces.BindingSemantics.instHashablePosition = { hash := Interfaces.BindingSemantics.instHashablePosition.hash }

structure Interfaces.BindingSemantics.BindingRelation : Type

A binding relation: which binder binds which bindee.

• binder : Position

  Position of the binder (quantifier, λ-operator, etc.)

• bindee : Position

  Position of the bindee (pronoun, trace, etc.)

• varIndex : Nat

  The variable index used in the assignment function

instance Interfaces.BindingSemantics.instReprBindingRelation : Repr BindingRelation

Equations

• Interfaces.BindingSemantics.instReprBindingRelation = { reprPrec := Interfaces.BindingSemantics.instReprBindingRelation.repr }

def Interfaces.BindingSemantics.instReprBindingRelation.repr : BindingRelation → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Interfaces.BindingSemantics.instDecidableEqBindingRelation : DecidableEq BindingRelation

Equations

• Interfaces.BindingSemantics.instDecidableEqBindingRelation = Interfaces.BindingSemantics.instDecidableEqBindingRelation.decEq

def Interfaces.BindingSemantics.instDecidableEqBindingRelation.decEq (x✝ x✝¹ : BindingRelation) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

structure Interfaces.BindingSemantics.BindingConfig : Type

A complete binding configuration for a structure.

• bindings : List BindingRelation

  All binding relations in the structure

• freeVariables : List (Position × Nat)

  Positions that are free (unbound) variables

instance Interfaces.BindingSemantics.instReprBindingConfig : Repr BindingConfig

Equations

• Interfaces.BindingSemantics.instReprBindingConfig = { reprPrec := Interfaces.BindingSemantics.instReprBindingConfig.repr }

def Interfaces.BindingSemantics.instReprBindingConfig.repr : BindingConfig → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

class Interfaces.BindingSemantics.HasBindingConfig (T : Type) : Type 1

What a syntactic theory must provide for H&K binding semantics.

• Structure : Type

  The theory's syntactic structure type

• bindingConfig : Structure T → BindingConfig

  Extract binding configuration from a structure

def Interfaces.BindingSemantics.binders {T : Type} [HasBindingConfig T] (s : HasBindingConfig.Structure T) : List Position

Get all binders in a structure

Equations

• Interfaces.BindingSemantics.binders s = List.map (fun (x : Interfaces.BindingSemantics.BindingRelation) => x.binder) (Interfaces.BindingSemantics.HasBindingConfig.bindingConfig s).bindings

def Interfaces.BindingSemantics.bindees {T : Type} [HasBindingConfig T] (s : HasBindingConfig.Structure T) : List Position

Get all bindees in a structure

Equations

• Interfaces.BindingSemantics.bindees s = List.map (fun (x : Interfaces.BindingSemantics.BindingRelation) => x.bindee) (Interfaces.BindingSemantics.HasBindingConfig.bindingConfig s).bindings

def Interfaces.BindingSemantics.isBound {T : Type} [HasBindingConfig T] (s : HasBindingConfig.Structure T) (p : Position) : Bool

Is position p bound in structure s?

Equations

• Interfaces.BindingSemantics.isBound s p = (Interfaces.BindingSemantics.HasBindingConfig.bindingConfig s).bindings.any fun (x : Interfaces.BindingSemantics.BindingRelation) => x.bindee == p

def Interfaces.BindingSemantics.isBinder {T : Type} [HasBindingConfig T] (s : HasBindingConfig.Structure T) (p : Position) : Bool

Is position p a binder in structure s?

Equations

• Interfaces.BindingSemantics.isBinder s p = (Interfaces.BindingSemantics.HasBindingConfig.bindingConfig s).bindings.any fun (x : Interfaces.BindingSemantics.BindingRelation) => x.binder == p

def Interfaces.BindingSemantics.binderOf {T : Type} [HasBindingConfig T] (s : HasBindingConfig.Structure T) (p : Position) : Option Position

Get the binder for a bound position (if any)

Equations

• One or more equations did not get rendered due to their size.

def Interfaces.BindingSemantics.varIndexOf {T : Type} [HasBindingConfig T] (s : HasBindingConfig.Structure T) (p : Position) : Option Nat

Get the variable index for a bound position

Equations

• One or more equations did not get rendered due to their size.

def Interfaces.BindingSemantics.boundBy {T : Type} [HasBindingConfig T] (s : HasBindingConfig.Structure T) (binder : Position) : List Position

Get all positions bound by a given binder

Equations

• One or more equations did not get rendered due to their size.

def Interfaces.BindingSemantics.BindingConfig.wellFormed (bc : BindingConfig) : Bool

A binding configuration is well-formed.

Equations

• One or more equations did not get rendered due to their size.

def Interfaces.BindingSemantics.hasWellFormedBinding {T : Type} [HasBindingConfig T] (s : HasBindingConfig.Structure T) : Bool

A structure has well-formed binding

Equations

• Interfaces.BindingSemantics.hasWellFormedBinding s = (Interfaces.BindingSemantics.HasBindingConfig.bindingConfig s).wellFormed

def Interfaces.BindingSemantics.bindingEquivalent {T1 T2 : Type} [HasBindingConfig T1] [HasBindingConfig T2] (s1 : HasBindingConfig.Structure T1) (s2 : HasBindingConfig.Structure T2) : Bool

Two theories agree on binding if they produce equivalent configurations.

Equations

• One or more equations did not get rendered due to their size.