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 Cslib.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$

def Cslib.instReprSKI.repr : SKI → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cslib.instReprSKI.repr Cslib.SKI.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cslib.SKI.S")).group prec✝
• Cslib.instReprSKI.repr Cslib.SKI.K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cslib.SKI.K")).group prec✝
• Cslib.instReprSKI.repr Cslib.SKI.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cslib.SKI.I")).group prec✝

instance Cslib.instReprSKI : Repr SKI

Equations

• Cslib.instReprSKI = { reprPrec := Cslib.instReprSKI.repr }

def Cslib.instDecidableEqSKI.decEq (x✝ x✝¹ : SKI) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.S Cslib.SKI.S = isTrue ⋯
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.S Cslib.SKI.K = isFalse Cslib.instDecidableEqSKI.decEq._proof_1
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.S Cslib.SKI.I = isFalse Cslib.instDecidableEqSKI.decEq._proof_2
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.S (a.app a_1) = isFalse ⋯
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.K Cslib.SKI.S = isFalse Cslib.instDecidableEqSKI.decEq._proof_4
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.K Cslib.SKI.K = isTrue ⋯
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.K Cslib.SKI.I = isFalse Cslib.instDecidableEqSKI.decEq._proof_5
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.K (a.app a_1) = isFalse ⋯
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.I Cslib.SKI.S = isFalse Cslib.instDecidableEqSKI.decEq._proof_7
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.I Cslib.SKI.K = isFalse Cslib.instDecidableEqSKI.decEq._proof_8
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.I Cslib.SKI.I = isTrue ⋯
• Cslib.instDecidableEqSKI.decEq Cslib.SKI.I (a.app a_1) = isFalse ⋯
• Cslib.instDecidableEqSKI.decEq (a.app a_1) Cslib.SKI.S = isFalse ⋯
• Cslib.instDecidableEqSKI.decEq (a.app a_1) Cslib.SKI.K = isFalse ⋯
• Cslib.instDecidableEqSKI.decEq (a.app a_1) Cslib.SKI.I = isFalse ⋯

instance Cslib.instDecidableEqSKI : DecidableEq SKI

Equations

• Cslib.instDecidableEqSKI = Cslib.instDecidableEqSKI.decEq

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

Application $x y ↦ xy$

Equations

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

def Cslib.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 : Cslib.SKI) => x1.app x2) f xs

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

def Cslib.SKI.size : SKI → ℕ

The size of an SKI term is its number of combinators.

Equations

• Cslib.SKI.S.size = 1
• Cslib.SKI.K.size = 1
• Cslib.SKI.I.size = 1
• (a.app a_1).size = a.size + a_1.size

Reduction relations between SKI terms

inductive Cslib.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 Cslib.SKI.«term_⭢_» : Lean.TrailingParserDescr

Equations

• Cslib.SKI.«term_⭢_» = Lean.ParserDescr.trailingNode `Cslib.SKI.«term_⭢_» 1022 39 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⭢ ") (Lean.ParserDescr.cat `term 39))

def Cslib.SKI.«term_↠_» : Lean.TrailingParserDescr

Equations

• Cslib.SKI.«term_↠_» = Lean.ParserDescr.trailingNode `Cslib.SKI.«term_↠_» 1022 39 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↠ ") (Lean.ParserDescr.cat `term 39))

theorem Cslib.SKI.Red.ne {x y : SKI} : RedSKI.Red x y → x ≠ y

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

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

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

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

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

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

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

def Cslib.SKI.CommonReduct : SKI → SKI → Prop

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

Equations

• Cslib.SKI.CommonReduct = Relation.Join Cslib.SKI.RedSKI.MRed

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

theorem Cslib.SKI.symmetric_commonReduct : Symmetric CommonReduct

theorem Cslib.SKI.reflexive_commonReduct : Reflexive CommonReduct

theorem Cslib.SKI.commonReduct_head {x x' : SKI} (y : SKI) : x.CommonReduct x' → (x.app y).CommonReduct (x'.app y)

theorem Cslib.SKI.commonReduct_tail (x : SKI) {y y' : SKI} : y.CommonReduct y' → (x.app y).CommonReduct (x.app y')