Combinatory logic primitives

The basis combinators B, T, S, I, K, C of combinatory logic, with the standard identities relating them (I = S K K, B = S (K _) _, T = C I).

These are the substrate of variable-free / combinatory semantics: CCG's combinatory rules correspond to them (forward composition to B, type-raising to T, the substitution rule to S; [Ste00a]), and continuation/applicative composition and Jacobson-style binding use the same algebra. They live here in Semantics/Composition/ alongside the other composition primitives rather than inside the CCG files.

Main definitions

• Combinator.B, Combinator.T, Combinator.S, Combinator.I, Combinator.K, Combinator.C

Main statements

• Combinator.B_comp — B is function composition
• Combinator.I_eq_SKK, Combinator.B_eq_S_K, Combinator.T_eq_CI — the basis identities of combinatory logic

References

• [CF58]
• [Smu85]

def Combinator.B {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α → β) : α → γ

B (composition): B f g x = f (g x).

Equations

• Combinator.B f g x = f (g x)

def Combinator.T {α : Type u_1} {β : Type u_2} (x : α) : (α → β) → β

T (type-raising): T x f = f x.

Equations

• Combinator.T x f = f x

def Combinator.S {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (g : α → β) : α → γ

S (substitution): S f g x = f x (g x).

Equations

• Combinator.S f g x = f x (g x)

def Combinator.I {α : Type u_1} : α → α

I (identity): I x = x.

Equations

• Combinator.I x = x

def Combinator.K {α : Type u_1} {β : Type u_2} (x : α) : β → α

K (constant): K x y = x.

Equations

• Combinator.K x x✝ = x

def Combinator.C {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (x : β) (y : α) : γ

C (commutation): C f x y = f y x.

Equations

• Combinator.C f x y = f y x

@[simp]

theorem Combinator.B_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α → β) (x : α) : B f g x = f (g x)

@[simp]

theorem Combinator.T_apply {α : Type u_1} {β : Type u_2} (x : α) (f : α → β) : T x f = f x

@[simp]

theorem Combinator.S_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (g : α → β) (x : α) : S f g x = f x (g x)

@[simp]

theorem Combinator.I_apply {α : Type u_1} (x : α) : I x = x

@[simp]

theorem Combinator.K_apply {α : Type u_1} {β : Type u_2} (x : α) (y : β) : K x y = x

@[simp]

theorem Combinator.C_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (x : β) (y : α) : C f x y = f y x

theorem Combinator.B_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α → β) : B f g = f ∘ g

B is function composition.

theorem Combinator.I_eq_SKK {α : Type u_1} : I = S K K

I = S K K: identity is derivable from S and K.

theorem Combinator.B_eq_S_K {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α → β) : B f g = S (K f) g

B = S (K _) _: composition is derivable from S and K.

theorem Combinator.T_eq_CI {α : Type u_1} {β : Type u_2} (x : α) : T x = C I x

T = C I: type-raising is C applied to the identity.

theorem Combinator.C_eq_B_T {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (x : β) (y : α) : C f x y = B (T x) f y

C f x y = B (T x) f y: C is derivable from B and T.