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 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 SKI.«term_⬝'_» : Lean.TrailingParserDescr

Application between polynomials

Equations

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

def SKI.«term&_» : Lean.ParserDescr

Notation by analogy with pointers in C

Equations

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

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

Equations

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

def 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

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

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

A polynomial with no free variables is a term

Equations

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

def 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

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

@[irreducible]

theorem SKI.Polynomial.elimVar_correct {n : ℕ} (Γ : SKI.Polynomial (n + 1)) {ys : List SKI} (hys : ys.length = n) (z : SKI) : ((Γ.elimVar.eval ys hys).app z).MRed (Γ.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 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 SKI.Polynomial.toSKI_correct {n : ℕ} (Γ : SKI.Polynomial n) (xs : List SKI) (hxs : xs.length = n) : (Γ.toSKI.applyList xs).MRed (Γ.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 SKI.RPoly : SKI.Polynomial 2

Reversal: R := λ x y. y x

Equations

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

def SKI.R : SKI

A SKI term representing R

Equations

• SKI.R = SKI.RPoly.toSKI

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

def SKI.BPoly : SKI.Polynomial 3

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

Equations

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

def SKI.B : SKI

A SKI term representing B

Equations

• SKI.B = SKI.BPoly.toSKI

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

def SKI.CPoly : SKI.Polynomial 3

C := λ f x y. f y x

Equations

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

def SKI.C : SKI

A SKI term representing C

Equations

• SKI.C = SKI.CPoly.toSKI

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

def SKI.RotRPoly : SKI.Polynomial 3

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

Equations

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

def SKI.RotR : SKI

A SKI term representing RotR

Equations

• SKI.RotR = SKI.RotRPoly.toSKI

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

def SKI.RotLPoly : SKI.Polynomial 3

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

Equations

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

def SKI.RotL : SKI

A SKI term representing RotL

Equations

• SKI.RotL = SKI.RotLPoly.toSKI

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

def SKI.δPoly : SKI.Polynomial 1

Self application: δ := λ x. x x

Equations

• SKI.δPoly = (SKI.Polynomial.var 0).app (SKI.Polynomial.var 0)

def SKI.δ : SKI

A SKI term representing δ

Equations

• SKI.δ = SKI.δPoly.toSKI

theorem SKI.δ_def (x : SKI) : (δ.app x).MRed (x.app x)

def SKI.HPoly : SKI.Polynomial 2

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

Equations

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

def SKI.H : SKI

A SKI term representing H

Equations

• SKI.H = SKI.HPoly.toSKI

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

def SKI.YPoly : SKI.Polynomial 1

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

Equations

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

def SKI.Y : SKI

A SKI term representing Y

Equations

• SKI.Y = SKI.YPoly.toSKI

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

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

The fixed-point property of the Y-combinator

def 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 = (SKI.H.app f).app (SKI.H.app f)

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

def SKI.ΘAuxPoly : SKI.Polynomial 2

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

Equations

• SKI.ΘAuxPoly = (SKI.Polynomial.var 1).app (((SKI.Polynomial.var 0).app (SKI.Polynomial.var 0)).app (SKI.Polynomial.var 1))

def SKI.ΘAux : SKI

A term representing ΘAux

Equations

• SKI.ΘAux = SKI.ΘAuxPoly.toSKI

theorem SKI.ΘAux_def (x y : SKI) : ((ΘAux.app x).app y).MRed (y.app ((x.app x).app y))

def SKI.Θ : SKI

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

Equations

• SKI.Θ = SKI.ΘAux.app SKI.ΘAux

theorem SKI.Θ_correct (f : SKI) : (Θ.app f).MRed (f.app (Θ.app f))

A SKI term representing Θ

Church Booleans

def 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

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

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

def SKI.TT : SKI

Standard true: TT := λ x y. x

Equations

• SKI.TT = SKI.K

theorem SKI.TT_correct : IsBool true TT

def SKI.FF : SKI

Standard false: FF := λ x y. y

Equations

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

theorem SKI.FF_correct : IsBool false FF

def SKI.Cond : SKI

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

Equations

• SKI.Cond = SKI.RotR

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

def SKI.Neg : SKI

Neg := λ a. Cond FF TT a

Equations

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

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

def 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 SKI.And : SKI

A SKI term representing And

Equations

• SKI.And = SKI.AndPoly.toSKI

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

theorem 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 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 SKI.Or : SKI

A SKI term representing Or

Equations

• SKI.Or = SKI.OrPoly.toSKI

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

theorem 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 SKI.MkPair : SKI

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

Equations

• SKI.MkPair = SKI.Cond

def SKI.Fst : SKI

First projection

Equations

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

def SKI.Snd : SKI

Second projection

Equations

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

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

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

def SKI.UnpairedPoly : SKI.Polynomial 2

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

Equations

• SKI.UnpairedPoly = ((SKI.Polynomial.var 0).app ((SKI.Polynomial.term SKI.Fst).app (SKI.Polynomial.var 1))).app ((SKI.Polynomial.term SKI.Snd).app (SKI.Polynomial.var 1))

def SKI.Unpaired : SKI

A term representing Unpaired

Equations

• SKI.Unpaired = SKI.UnpairedPoly.toSKI

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

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

def SKI.PairPoly : SKI.Polynomial 3

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

Equations

• SKI.PairPoly = ((SKI.Polynomial.term SKI.MkPair).app ((SKI.Polynomial.var 0).app (SKI.Polynomial.var 2))).app ((SKI.Polynomial.var 1).app (SKI.Polynomial.var 2))

def SKI.Pair : SKI

A SKI term representing Pair

Equations

• SKI.Pair = SKI.PairPoly.toSKI

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