Total combinatory algebras

A total combinatory structure on a type A, and the fact that any total combinatory algebra induces a partial combinatory algebra on the same type.

class LeanPool.PartialCombinatoryAlgebras.CA (A : Type u_1) extends LeanPool.PartialCombinatoryAlgebras.HasDot A : Type u_1

A (total) combinatory structure on a set A.

• dot : A → A → A
• K : A

  The K combinator.

• S : A

  The S combinator.

• eq_K {a b : A} : K ⬝ a ⬝ b = a

  The defining equation of K.

• eq_S {a b c : A} : S ⬝ a ⬝ b ⬝ c = a ⬝ c ⬝ (b ⬝ c)

  The defining equation of S.

def LeanPool.PartialCombinatoryAlgebras.Part.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (u : Part α) (v : Part β) : Part γ

Missing from Part.

Equations

• LeanPool.PartialCombinatoryAlgebras.Part.map₂ f u v = { Dom := u ⇓ ∧ v ⇓, get := fun (p : u ⇓ ∧ v ⇓) => f (u.get ⋯) (v.get ⋯) }

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.Part.map₂_Dom {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (u : Part α) (v : Part β) : ((map₂ f u v) ⇓) = (u ⇓ ∧ v ⇓)

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.Part.map₂_get {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (u : Part α) (v : Part β) (p : u ⇓ ∧ v ⇓) : (map₂ f u v).get p = f (u.get ⋯) (v.get ⋯)

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.Part.eq_map₂_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β) : map₂ f (Part.some a) (Part.some b) = Part.some (f a b)

@[reducible]

instance LeanPool.PartialCombinatoryAlgebras.CA.partialApp {A : Type} [d : HasDot A] : PartialApplication A

A total application induces a partial application

Equations

• LeanPool.PartialCombinatoryAlgebras.CA.partialApp = { app := LeanPool.PartialCombinatoryAlgebras.Part.map₂ LeanPool.PartialCombinatoryAlgebras.HasDot.dot }

theorem LeanPool.PartialCombinatoryAlgebras.CA.eq_app {A : Type} [HasDot A] {u v : Part A} (hu : u ⇓) (hv : v ⇓) : u ⬝ v = Part.some (u.get hu ⬝ v.get hv)

@[instance_reducible]

instance LeanPool.PartialCombinatoryAlgebras.CA.isPCA {A : Type} [CA A] : PCA A

A combinatory algebra is a PCA.

Equations

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