SKI Combinatory Logic

This file defines the syntax and operational semantics (reduction rules) of combinatory logic, using the SKI basis.

Main definitions

• SKI: the type of expressions in the SKI calculus,
• Red: single-step reduction of SKI expressions,
• MRed: multi-step reduction of SKI expressions,
• CommonReduct: the relation between terms having a common reduct,

Notation

• ⬝ : application between SKI terms,
• ⇒ : single-step reduction,
• ⇒* : multi-step reduction,

References

The setup of SKI combinatory logic is standard, see for example:

• https://en.m.wikipedia.org/wiki/SKI_combinator_calculus
• https://en.m.wikipedia.org/wiki/Combinatory_logic

inductive SKI : Type

An SKI expression is built from the primitive combinators S, K and I, and application.

• S : SKI

  S-combinator, with semantics $λxyz.xz(yz)

• K : SKI

  K-combinator, with semantics $λxy.x$

• I : SKI

  I-combinator, with semantics $λx.x$

• app : SKI → SKI → SKI

  Application $x y ↦ xy$

instance instReprSKI : Repr SKI

Equations

• instReprSKI = { reprPrec := reprSKI✝ }

instance instDecidableEqSKI : DecidableEq SKI

Equations

• instDecidableEqSKI = decEqSKI✝

def SKI.«term_⬝_» : Lean.TrailingParserDescr

Application $x y ↦ xy$

Equations

• SKI.«term_⬝_» = Lean.ParserDescr.trailingNode `SKI.«term_⬝_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ ") (Lean.ParserDescr.cat `term 101))

def SKI.applyList (f : SKI) (xs : List SKI) : SKI

Apply a term to a list of terms

Equations

• f.applyList xs = List.foldl (fun (x1 x2 : SKI) => x1.app x2) f xs

theorem SKI.applyList_concat (f : SKI) (ys : List SKI) (z : SKI) : f.applyList (ys ++ [z]) = (f.applyList ys).app z

Reduction relations between SKI terms

inductive SKI.Red : SKI → SKI → Prop

Single-step reduction of SKI terms

• red_S (x y z : SKI) : (((S.app x).app y).app z).Red ((x.app z).app (y.app z))

  The operational semantics of the S,

• red_K (x y : SKI) : ((K.app x).app y).Red x

  K,

• red_I (x : SKI) : (I.app x).Red x

  and I combinators.

• red_head (x x' y : SKI) : x.Red x' → (x.app y).Red (x'.app y)

  Reduction on the head

• red_tail (x y y' : SKI) : y.Red y' → (x.app y).Red (x.app y')

  and tail of an SKI term.

def SKI.«term_⇒_» : Lean.TrailingParserDescr

Notation for single-step reduction

Equations

• SKI.«term_⇒_» = Lean.ParserDescr.trailingNode `SKI.«term_⇒_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇒ ") (Lean.ParserDescr.cat `term 91))

def SKI.MRed : SKI → SKI → Prop

Multi-step reduction of SKI terms

Equations

• SKI.MRed = Relation.ReflTransGen SKI.Red

def SKI.«term_⇒*_» : Lean.TrailingParserDescr

Notation for multi-step reduction (by analogy with the Kleene star)

Equations

• SKI.«term_⇒*_» = Lean.ParserDescr.trailingNode `SKI.«term_⇒*_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇒* ") (Lean.ParserDescr.cat `term 91))

theorem SKI.MRed.refl (a : SKI) : a.MRed a

theorem SKI.MRed.single {a b : SKI} (h : a.Red b) : a.MRed b

theorem SKI.MRed.S (x y z : SKI) : (((SKI.S.app x).app y).app z).MRed ((x.app z).app (y.app z))

theorem SKI.MRed.K (x y : SKI) : ((SKI.K.app x).app y).MRed x

theorem SKI.MRed.I (x : SKI) : (SKI.I.app x).MRed x

theorem SKI.MRed.head {a a' : SKI} (b : SKI) (h : a.MRed a') : (a.app b).MRed (a'.app b)

theorem SKI.MRed.tail (a : SKI) {b b' : SKI} (h : b.MRed b') : (a.app b).MRed (a.app b')

instance SKI.MRed.instTrans : IsTrans SKI MRed

theorem SKI.MRed.transitive : Transitive MRed

instance SKI.MRed.instIsRefl : IsRefl SKI MRed

theorem SKI.MRed.reflexive : Reflexive MRed

instance SKI.MRedTrans : Trans Red MRed MRed

Equations

• SKI.MRedTrans = { trans := @SKI.MRedTrans._proof_1 }

instance SKI.MRedRedTrans : Trans MRed Red MRed

Equations

• SKI.MRedRedTrans = { trans := @SKI.MRedRedTrans._proof_1 }

instance SKI.RedMRedTrans : Trans Red Red MRed

Equations

• SKI.RedMRedTrans = { trans := @SKI.RedMRedTrans._proof_1 }

theorem SKI.parallel_mRed {a a' b b' : SKI} (ha : a.MRed a') (hb : b.MRed b') : (a.app b).MRed (a'.app b')

theorem SKI.parallel_red {a a' b b' : SKI} (ha : a.Red a') (hb : b.Red b') : (a.app b).MRed (a'.app b')

def SKI.CommonReduct : SKI → SKI → Prop

Express that two terms have a reduce to a common term.

Equations

• SKI.CommonReduct = Relation.Join SKI.MRed

theorem SKI.commonReduct_of_single {a b : SKI} (h : a.MRed b) : a.CommonReduct b

theorem SKI.symmetric_commonReduct : Symmetric CommonReduct

theorem SKI.reflexive_commonReduct : Reflexive CommonReduct