Basic results for the SKI calculus

Main definition

• Polynomial: the type of SKI terms with fixed number of "holes" (read: free variables).

Notation

• ⬝' : application between polynomials,
• &i : the ith free variable of a polynomial.

Main results

• Bracket abstraction: an algorithm Polynomial.toSKI to convert a polynomial $Γ(x_0, ..., x_{n-1})$ into a term such that (Polynomial.toSKI_correct) Γ.toSKI ⬝ t₁ ⬝ ... ⬝ tₙ reduces to Γ(t₁, ..., tₙ).

References

For a presentation of the bracket abstraction algorithm see: https://web.archive.org/web/19970727171324/http://www.cs.oberlin.edu/classes/cs280/labs/lab4/lab43.html#@l13

Polynomials and the bracket astraction algorithm

inductive Cslib.SKI.Polynomial (n : ℕ) : Type

A polynomial is an SKI terms with free variables.

• term {n : ℕ} : SKI → SKI.Polynomial n
• var {n : ℕ} : Fin n → SKI.Polynomial n
• app {n : ℕ} : SKI.Polynomial n → SKI.Polynomial n → SKI.Polynomial n

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

Application between polynomials

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.«term&_» : Lean.ParserDescr

Notation by analogy with pointers in C

Equations

• Cslib.SKI.«term&_» = Lean.ParserDescr.node `Cslib.SKI.«term&_» 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&") (Lean.ParserDescr.cat `term 101))

instance Cslib.SKI.CoeTermPolynomial (n : ℕ) : Coe SKI (SKI.Polynomial n)

Equations

• Cslib.SKI.CoeTermPolynomial n = { coe := Cslib.SKI.Polynomial.term }

def Cslib.SKI.Polynomial.eval {n : ℕ} (Γ : SKI.Polynomial n) (l : List SKI) (hl : l.length = n) : SKI

Substitute terms for the free variables of a polynomial

Equations

• (Cslib.SKI.Polynomial.term x).eval l hl = x
• (Cslib.SKI.Polynomial.var i).eval l hl = l[i]
• (Γ_2.app Δ).eval l hl = (Γ_2.eval l hl).app (Δ.eval l hl)

def Cslib.SKI.Polynomial.varFreeToSKI (Γ : SKI.Polynomial 0) : SKI

A polynomial with no free variables is a term

Equations

• Γ.varFreeToSKI = Γ.eval [] Cslib.SKI.Polynomial.varFreeToSKI._proof_1

def Cslib.SKI.Polynomial.elimVar {n : ℕ} : SKI.Polynomial (n + 1) → SKI.Polynomial n

Inductively define a polynomial Γ' so that (up to the fact that we haven't defined reduction on polynomials) Γ' ⬝ t ↠ Γ[xₙ ← t].

Equations

• (Cslib.SKI.Polynomial.term x_1).elimVar = (Cslib.SKI.Polynomial.term Cslib.SKI.K).app (Cslib.SKI.Polynomial.term x_1)
• (Cslib.SKI.Polynomial.var i).elimVar = if h : ↑i < n then (Cslib.SKI.Polynomial.term Cslib.SKI.K).app (Cslib.SKI.Polynomial.var (Fin.ofNat n ↑i)) else Cslib.SKI.Polynomial.term Cslib.SKI.I
• (Γ.app Δ).elimVar = ((Cslib.SKI.Polynomial.term Cslib.SKI.S).app Γ.elimVar).app Δ.elimVar

@[irreducible]

theorem Cslib.SKI.Polynomial.elimVar_correct {n : ℕ} (Γ : SKI.Polynomial (n + 1)) {ys : List SKI} (hys : ys.length = n) (z : SKI) : RedSKI.MRed ((Γ.elimVar.eval ys hys).app z) (Γ.eval (ys ++ [z]) ⋯)

Correctness for the elimVar algorithm, which provides the inductive step of the bracket abstraction algorithm. We induct backwards on the list, corresponding to applying the transformation from the inside out. Since we haven't defined reduction for polynomials, we substitute arbitrary terms for the inner variables.

def Cslib.SKI.Polynomial.toSKI {n : ℕ} (Γ : SKI.Polynomial n) : SKI

Bracket abstraction, by induction using SKI.Polynomial.elimVar

Equations

• Γ_2.toSKI = Γ_2.varFreeToSKI
• Γ_2.toSKI = Γ_2.elimVar.toSKI

theorem Cslib.SKI.Polynomial.toSKI_correct {n : ℕ} (Γ : SKI.Polynomial n) (xs : List SKI) (hxs : xs.length = n) : RedSKI.MRed (Γ.toSKI.applyList xs) (Γ.eval xs hxs)

Correctness for the toSKI (bracket abstraction) algorithm.

Basic auxiliary combinators.

Each combinator is defined by a polynomial, which is then proved to have the reduction property we want. Before each definition we provide its lambda calculus equivalent. If there is accepted notation for a given combinator, we use that (given everywhere a capital letter), otherwise we choose a descriptive name.

def Cslib.SKI.RPoly : SKI.Polynomial 2

Reversal: R := λ x y. y x

Equations

• Cslib.SKI.RPoly = (Cslib.SKI.Polynomial.var 1).app (Cslib.SKI.Polynomial.var 0)

def Cslib.SKI.R : SKI

A SKI term representing R

Equations

• Cslib.SKI.R = Cslib.SKI.RPoly.toSKI

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

def Cslib.SKI.BPoly : SKI.Polynomial 3

Composition: B := λ f g x. f (g x)

Equations

• Cslib.SKI.BPoly = (Cslib.SKI.Polynomial.var 0).app ((Cslib.SKI.Polynomial.var 1).app (Cslib.SKI.Polynomial.var 2))

def Cslib.SKI.B : SKI

A SKI term representing B

Equations

• Cslib.SKI.B = Cslib.SKI.BPoly.toSKI

theorem Cslib.SKI.B_def (f g x : SKI) : RedSKI.MRed (((B.app f).app g).app x) (f.app (g.app x))

def Cslib.SKI.CPoly : SKI.Polynomial 3

C := λ f x y. f y x

Equations

• Cslib.SKI.CPoly = ((Cslib.SKI.Polynomial.var 0).app (Cslib.SKI.Polynomial.var 2)).app (Cslib.SKI.Polynomial.var 1)

def Cslib.SKI.C : SKI

A SKI term representing C

Equations

• Cslib.SKI.C = Cslib.SKI.CPoly.toSKI

theorem Cslib.SKI.C_def (f x y : SKI) : RedSKI.MRed (((C.app f).app x).app y) ((f.app y).app x)

def Cslib.SKI.RotRPoly : SKI.Polynomial 3

Rotate right: RotR := λ x y z. z x y

Equations

• Cslib.SKI.RotRPoly = ((Cslib.SKI.Polynomial.var 2).app (Cslib.SKI.Polynomial.var 0)).app (Cslib.SKI.Polynomial.var 1)

def Cslib.SKI.RotR : SKI

A SKI term representing RotR

Equations

• Cslib.SKI.RotR = Cslib.SKI.RotRPoly.toSKI

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

def Cslib.SKI.RotLPoly : SKI.Polynomial 3

Rotate left: RotR := λ x y z. y z x

Equations

• Cslib.SKI.RotLPoly = ((Cslib.SKI.Polynomial.var 1).app (Cslib.SKI.Polynomial.var 2)).app (Cslib.SKI.Polynomial.var 0)

def Cslib.SKI.RotL : SKI

A SKI term representing RotL

Equations

• Cslib.SKI.RotL = Cslib.SKI.RotLPoly.toSKI

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

def Cslib.SKI.DelPoly : SKI.Polynomial 1

Self application: δ := λ x. x x

Equations

• Cslib.SKI.DelPoly = (Cslib.SKI.Polynomial.var 0).app (Cslib.SKI.Polynomial.var 0)

def Cslib.SKI.Del : SKI

A SKI term representing δ

Equations

• Cslib.SKI.Del = Cslib.SKI.DelPoly.toSKI

theorem Cslib.SKI.del_def (x : SKI) : RedSKI.MRed (Del.app x) (x.app x)

def Cslib.SKI.HPoly : SKI.Polynomial 2

H := λ f x. f (x x)

Equations

• Cslib.SKI.HPoly = (Cslib.SKI.Polynomial.var 0).app ((Cslib.SKI.Polynomial.var 1).app (Cslib.SKI.Polynomial.var 1))

def Cslib.SKI.H : SKI

A SKI term representing H

Equations

• Cslib.SKI.H = Cslib.SKI.HPoly.toSKI

theorem Cslib.SKI.H_def (f x : SKI) : RedSKI.MRed ((H.app f).app x) (f.app (x.app x))

def Cslib.SKI.YPoly : SKI.Polynomial 1

Curry's fixed-point combinator: Y := λ f. H f (H f)

Equations

• Cslib.SKI.YPoly = ((Cslib.SKI.Polynomial.term Cslib.SKI.H).app (Cslib.SKI.Polynomial.var 0)).app ((Cslib.SKI.Polynomial.term Cslib.SKI.H).app (Cslib.SKI.Polynomial.var 0))

def Cslib.SKI.Y : SKI

A SKI term representing Y

Equations

• Cslib.SKI.Y = Cslib.SKI.YPoly.toSKI

theorem Cslib.SKI.Y_def (f : SKI) : RedSKI.MRed (Y.app f) ((H.app f).app (H.app f))

theorem Cslib.SKI.Y_correct (f : SKI) : (Y.app f).CommonReduct (f.app (Y.app f))

The fixed-point property of the Y-combinator

def Cslib.SKI.fixedPoint (f : SKI) : SKI

It is useful to be able to produce a term such that the fixed point property holds on-the-nose, rather than up to a common reduct. An alternative is to use Turing's fixed-point combinator (defined below).

Equations

• f.fixedPoint = (Cslib.SKI.H.app f).app (Cslib.SKI.H.app f)

theorem Cslib.SKI.fixedPoint_correct (f : SKI) : RedSKI.MRed f.fixedPoint (f.app f.fixedPoint)

def Cslib.SKI.ThAuxPoly : SKI.Polynomial 2

Auxiliary definition for Turing's fixed-point combinator: ΘAux := λ x y. y (x x y)

Equations

• Cslib.SKI.ThAuxPoly = (Cslib.SKI.Polynomial.var 1).app (((Cslib.SKI.Polynomial.var 0).app (Cslib.SKI.Polynomial.var 0)).app (Cslib.SKI.Polynomial.var 1))

def Cslib.SKI.ThAux : SKI

A term representing ΘAux

Equations

• Cslib.SKI.ThAux = Cslib.SKI.ThAuxPoly.toSKI

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

def Cslib.SKI.Th : SKI

Turing's fixed-point combinator: Θ := (λ x y. y (x x y)) (λ x y. y (x x y))

Equations

• Cslib.SKI.Th = Cslib.SKI.ThAux.app Cslib.SKI.ThAux

theorem Cslib.SKI.Th_correct (f : SKI) : RedSKI.MRed (Th.app f) (f.app (Th.app f))

A SKI term representing Θ

Church Booleans

def Cslib.SKI.IsBool (u : Bool) (a : SKI) : Prop

A term a represents the boolean value u if it is βη-equivalent to a standard Church boolean.

Equations

• Cslib.SKI.IsBool u a = ∀ (x y : Cslib.SKI), Cslib.SKI.RedSKI.MRed ((a.app x).app y) (if u = true then x else y)

theorem Cslib.SKI.isBool_trans (u : Bool) (a a' : SKI) (h : RedSKI.MRed a a') (ha' : IsBool u a') : IsBool u a

def Cslib.SKI.TT : SKI

Standard true: TT := λ x y. x

Equations

• Cslib.SKI.TT = Cslib.SKI.K

theorem Cslib.SKI.TT_correct : IsBool true TT

def Cslib.SKI.FF : SKI

Standard false: FF := λ x y. y

Equations

• Cslib.SKI.FF = Cslib.SKI.K.app Cslib.SKI.I

theorem Cslib.SKI.FF_correct : IsBool false FF

def Cslib.SKI.Cond : SKI

Conditional: Cond x y b := if b then x else y

Equations

• Cslib.SKI.Cond = Cslib.SKI.RotR

theorem Cslib.SKI.cond_correct (a x y : SKI) (u : Bool) (h : IsBool u a) : RedSKI.MRed (((SKI.Cond.app x).app y).app a) (if u = true then x else y)

def Cslib.SKI.Neg : SKI

Neg := λ a. Cond FF TT a

Equations

• Cslib.SKI.Neg = (Cslib.SKI.Cond.app Cslib.SKI.FF).app Cslib.SKI.TT

theorem Cslib.SKI.neg_correct (a : SKI) (ua : Bool) (h : IsBool ua a) : IsBool (decide ¬ua = true) (SKI.Neg.app a)

def Cslib.SKI.AndPoly : SKI.Polynomial 2

And := λ a b. Cond (Cond TT FF b) FF a

Equations

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

def Cslib.SKI.And : SKI

A SKI term representing And

Equations

• Cslib.SKI.And = Cslib.SKI.AndPoly.toSKI

theorem Cslib.SKI.and_def (a b : SKI) : RedSKI.MRed ((SKI.And.app a).app b) (((SKI.Cond.app (((SKI.Cond.app TT).app FF).app b)).app FF).app a)

theorem Cslib.SKI.and_correct (a b : SKI) (ua ub : Bool) (ha : IsBool ua a) (hb : IsBool ub b) : IsBool (ua && ub) ((SKI.And.app a).app b)

def Cslib.SKI.OrPoly : SKI.Polynomial 2

Or := λ a b. Cond TT (Cond TT FF b) b

Equations

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

def Cslib.SKI.Or : SKI

A SKI term representing Or

Equations

• Cslib.SKI.Or = Cslib.SKI.OrPoly.toSKI

theorem Cslib.SKI.or_def (a b : SKI) : RedSKI.MRed ((SKI.Or.app a).app b) (((SKI.Cond.app TT).app (((SKI.Cond.app TT).app FF).app b)).app a)

theorem Cslib.SKI.or_correct (a b : SKI) (ua ub : Bool) (ha : IsBool ua a) (hb : IsBool ub b) : IsBool (ua || ub) ((SKI.Or.app a).app b)

Pairs

def Cslib.SKI.MkPair : SKI

MkPair := λ a b. ⟨a,b⟩

Equations

• Cslib.SKI.MkPair = Cslib.SKI.Cond

def Cslib.SKI.Fst : SKI

First projection

Equations

• Cslib.SKI.Fst = Cslib.SKI.R.app Cslib.SKI.TT

def Cslib.SKI.Snd : SKI

Second projection

Equations

• Cslib.SKI.Snd = Cslib.SKI.R.app Cslib.SKI.FF

theorem Cslib.SKI.fst_correct (a b : SKI) : RedSKI.MRed (Fst.app ((MkPair.app a).app b)) a

theorem Cslib.SKI.snd_correct (a b : SKI) : RedSKI.MRed (Snd.app ((MkPair.app a).app b)) b

def Cslib.SKI.UnpairedPoly : SKI.Polynomial 2

Unpaired f ⟨x, y⟩ := f x y, cf Nat.unparied.

Equations

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

def Cslib.SKI.Unpaired : SKI

A term representing Unpaired

Equations

• Cslib.SKI.Unpaired = Cslib.SKI.UnpairedPoly.toSKI

theorem Cslib.SKI.unpaired_def (f p : SKI) : RedSKI.MRed ((SKI.Unpaired.app f).app p) ((f.app (Fst.app p)).app (Snd.app p))

theorem Cslib.SKI.unpaired_correct (f x y : SKI) : RedSKI.MRed ((SKI.Unpaired.app f).app ((MkPair.app x).app y)) ((f.app x).app y)

def Cslib.SKI.PairPoly : SKI.Polynomial 3

Pair f g x := ⟨f x, g x⟩, cf Primrec.Pair.

Equations

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

def Cslib.SKI.Pair : SKI

A SKI term representing Pair

Equations

• Cslib.SKI.Pair = Cslib.SKI.PairPoly.toSKI

theorem Cslib.SKI.pair_def (f g x : SKI) : RedSKI.MRed (((SKI.Pair.app f).app g).app x) ((MkPair.app (f.app x)).app (g.app x))