Church-Encoded Lists in SKI Combinatory Logic

Church-encoded lists for proving SKI ≃ TM equivalence. A list is encoded as λ c n. c a₀ (c a₁ (... (c aₖ n)...)) where each aᵢ is a Church numeral.

Church List Representation

def Cslib.SKI.IsChurchList : List ℕ → SKI → Prop

A term correctly Church-encodes a list of natural numbers.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.SKI.IsChurchList [] x✝ = ∀ (c n : Cslib.SKI), Relation.ReflTransGen Cslib.SKI.Red ((x✝.app c).app n) n

theorem Cslib.SKI.isChurchList_trans {ns : List ℕ} {cns cns' : SKI} (h : Relation.ReflTransGen Red cns cns') (hcns' : IsChurchList ns cns') : IsChurchList ns cns

IsChurchList is preserved under multi-step reduction of the term.

structure Cslib.SKI.IsChurchListPair (prev curr : List ℕ) (p : SKI) : Prop

Both components of a pair are Church lists.

• fst : IsChurchList prev (Fst.app p)
• snd : IsChurchList curr (Snd.app p)

theorem Cslib.SKI.isChurchListPair_trans {prev curr : List ℕ} {p p' : SKI} (hp : Relation.ReflTransGen Red p p') (hp' : IsChurchListPair prev curr p') : IsChurchListPair prev curr p

IsChurchListPair is preserved under reduction.

Nil: The empty list

def Cslib.SKI.List.NilPoly : SKI.Polynomial 2

nil = λ c n. n

Equations

• Cslib.SKI.List.NilPoly = Cslib.SKI.Polynomial.var 1

def Cslib.SKI.List.Nil : SKI

The SKI term for the empty list.

Equations

• Cslib.SKI.List.Nil = Cslib.SKI.List.NilPoly.toSKI

theorem Cslib.SKI.List.nil_def (c n : SKI) : Relation.ReflTransGen Red ((Nil.app c).app n) n

Reduction: Nil ⬝ c ⬝ n ↠ n.

theorem Cslib.SKI.List.nil_correct : IsChurchList [] Nil

The empty list term correctly represents [].

Cons: Consing an element onto a list

def Cslib.SKI.List.ConsPoly : SKI.Polynomial 4

cons = λ x xs c n. c x (xs c n)

Equations

• Cslib.SKI.List.ConsPoly = ((Cslib.SKI.Polynomial.var 2).app (Cslib.SKI.Polynomial.var 0)).app (((Cslib.SKI.Polynomial.var 1).app (Cslib.SKI.Polynomial.var 2)).app (Cslib.SKI.Polynomial.var 3))

def Cslib.SKI.List.Cons : SKI

The SKI term for list cons.

Equations

• Cslib.SKI.List.Cons = Cslib.SKI.List.ConsPoly.toSKI

theorem Cslib.SKI.List.cons_def (x xs c n : SKI) : Relation.ReflTransGen Red ((((Cons.app x).app xs).app c).app n) ((c.app x).app ((xs.app c).app n))

Reduction: Cons ⬝ x ⬝ xs ⬝ c ⬝ n ↠ c ⬝ x ⬝ (xs ⬝ c ⬝ n).

theorem Cslib.SKI.List.cons_correct {x : ℕ} {xs : List ℕ} {cx cxs : SKI} (hcx : IsChurch x cx) (hcxs : IsChurchList xs cxs) : IsChurchList (x :: xs) ((Cons.app cx).app cxs)

Cons preserves Church list representation.

theorem Cslib.SKI.List.singleton_correct {x : ℕ} {cx : SKI} (hcx : IsChurch x cx) : IsChurchList [x] ((Cons.app cx).app Nil)

Singleton list correctness.

def Cslib.SKI.List.toChurch : List ℕ → SKI

The canonical SKI term for a Church-encoded list.

Equations

• Cslib.SKI.List.toChurch [] = Cslib.SKI.List.Nil
• Cslib.SKI.List.toChurch (x_1 :: xs) = (Cslib.SKI.List.Cons.app (Cslib.SKI.toChurch x_1)).app (Cslib.SKI.List.toChurch xs)

@[simp]

theorem Cslib.SKI.List.toChurch_nil : toChurch [] = Nil

toChurch [] = Nil.

@[simp]

theorem Cslib.SKI.List.toChurch_cons (x : ℕ) (xs : List ℕ) : toChurch (x :: xs) = (Cons.app (SKI.toChurch x)).app (toChurch xs)

toChurch (x :: xs) = Cons ⬝ SKI.toChurch x ⬝ toChurch xs.

theorem Cslib.SKI.List.toChurch_correct (ns : List ℕ) : IsChurchList ns (toChurch ns)

toChurch ns correctly represents ns.

Head: Extract the head of a list

def Cslib.SKI.List.HeadDPoly : SKI.Polynomial 2

headD d xs = xs K d (returns d for empty list)

Equations

• Cslib.SKI.List.HeadDPoly = ((Cslib.SKI.Polynomial.var 1).app (Cslib.SKI.Polynomial.term Cslib.SKI.K)).app (Cslib.SKI.Polynomial.var 0)

def Cslib.SKI.List.HeadD : SKI

The SKI term for list head with default.

Equations

• Cslib.SKI.List.HeadD = Cslib.SKI.List.HeadDPoly.toSKI

theorem Cslib.SKI.List.headD_def (d xs : SKI) : Relation.ReflTransGen Red ((HeadD.app d).app xs) ((xs.app K).app d)

Reduction: HeadD ⬝ d ⬝ xs ↠ xs ⬝ K ⬝ d.

theorem Cslib.SKI.List.headD_correct {d : ℕ} {cd : SKI} (hcd : IsChurch d cd) {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns cns) : IsChurch (ns.headD d) ((HeadD.app cd).app cns)

General head-with-default correctness.

def Cslib.SKI.List.Head : SKI

The SKI term for list head (default 0).

Equations

• Cslib.SKI.List.Head = Cslib.SKI.List.HeadD.app Cslib.SKI.Zero

theorem Cslib.SKI.List.head_def (xs : SKI) : Relation.ReflTransGen Red (Head.app xs) ((xs.app K).app SKI.Zero)

Reduction: Head ⬝ xs ↠ xs ⬝ K ⬝ Zero.

theorem Cslib.SKI.List.head_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) : IsChurch (ns.headD 0) (Head.app cns)

Head correctness (default 0).

Tail: Extract the tail of a list

def Cslib.SKI.List.TailStepPoly : SKI.Polynomial 2

Step function for tail: (prev, curr) → (curr, cons h curr)

Equations

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

def Cslib.SKI.List.TailStep : SKI

The step function for computing list tail.

Equations

• Cslib.SKI.List.TailStep = Cslib.SKI.List.TailStepPoly.toSKI

theorem Cslib.SKI.List.tailStep_def (h p : SKI) : Relation.ReflTransGen Red ((TailStep.app h).app p) ((MkPair.app (Snd.app p)).app ((Cons.app h).app (Snd.app p)))

Reduction of the tail step function.

def Cslib.SKI.List.TailPoly : SKI.Polynomial 1

tail xs = Fst (xs TailStep (MkPair Nil Nil))

Equations

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

def Cslib.SKI.List.Tail : SKI

The tail of a Church-encoded list.

Equations

• Cslib.SKI.List.Tail = Cslib.SKI.List.TailPoly.toSKI

theorem Cslib.SKI.List.tail_def (xs : SKI) : Relation.ReflTransGen Red (Tail.app xs) (Fst.app ((xs.app TailStep).app ((MkPair.app Nil).app Nil)))

Reduction: Tail ⬝ xs ↠ Fst ⬝ (xs ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil)).

@[simp]

theorem Cslib.SKI.List.tail_init : IsChurchListPair [] [] ((MkPair.app Nil).app Nil)

The initial pair (nil, nil) satisfies the invariant.

theorem Cslib.SKI.List.tailStep_correct {x : ℕ} {xs : List ℕ} {cx p : SKI} (hcx : IsChurch x cx) (hp : IsChurchListPair xs.tail xs p) : IsChurchListPair xs (x :: xs) ((TailStep.app cx).app p)

The step function preserves the tail-computing invariant.

theorem Cslib.SKI.List.tailFold_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) : ∃ (p : SKI), Relation.ReflTransGen Red ((cns.app TailStep).app ((MkPair.app Nil).app Nil)) p ∧ IsChurchListPair ns.tail ns p

theorem Cslib.SKI.List.tail_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) : IsChurchList ns.tail (Tail.app cns)

Tail correctness.

Prepending zero to a list (for Code.zero')

def Cslib.SKI.List.PrependZeroPoly : SKI.Polynomial 1

PrependZero xs = cons 0 xs = Cons ⬝ Zero ⬝ xs

Equations

• Cslib.SKI.List.PrependZeroPoly = ((Cslib.SKI.Polynomial.term Cslib.SKI.List.Cons).app (Cslib.SKI.Polynomial.term Cslib.SKI.Zero)).app (Cslib.SKI.Polynomial.var 0)

def Cslib.SKI.List.PrependZero : SKI

Prepend zero to a Church-encoded list.

Equations

• Cslib.SKI.List.PrependZero = Cslib.SKI.List.PrependZeroPoly.toSKI

theorem Cslib.SKI.List.prependZero_def (xs : SKI) : Relation.ReflTransGen Red (PrependZero.app xs) ((Cons.app SKI.Zero).app xs)

Reduction: PrependZero ⬝ xs ↠ Cons ⬝ Zero ⬝ xs.

theorem Cslib.SKI.List.prependZero_correct {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns cns) : IsChurchList (0 :: ns) (PrependZero.app cns)

Prepending zero preserves Church list representation.

Successor on list head (for Code.succ)

def Cslib.SKI.List.SuccHead : SKI

SuccHead xs = cons (succ (head xs)) nil

Equations

• Cslib.SKI.List.SuccHead = (Cslib.SKI.B.app ((Cslib.SKI.C.app Cslib.SKI.List.Cons).app Cslib.SKI.List.Nil)).app ((Cslib.SKI.B.app Cslib.SKI.Succ).app Cslib.SKI.List.Head)

theorem Cslib.SKI.List.succHead_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) : IsChurchList [ns.headD 0 + 1] (SuccHead.app cns)

SuccHead correctly computes a singleton containing succ(head ns).