Smullyan.Aviary

A collection of combinator birds representable in Lean. Certain duplicators, e.g. mockingbirds, are not directly expressible since they would require encoding a signature in which an argument has types α and α → α.

Duplicators that are included, e.g. the warbler, are not exactly correct considering they still have the same limitation described above during actual use. Their inclusion here serves more as pseudo-documentation than anything.

def E' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {ε : Sort u_5} {ζ : Sort u_6} {η : Sort u_7} (x : α → β → γ) (y₁ : δ → ε → α) (y₂ : δ) (y₃ : ε) (z₁ : ζ → η → β) (z₂ : ζ) (z₃ : η) : γ

Bald Eagle

E'xy₁y₂y₃z₁z₂z₃ = x(y₁y₂y₃)(z₁z₂z₃)

Equations

• E' x y₁ y₂ y₃ z₁ z₂ z₃ = x (y₁ y₂ y₃) (z₁ z₂ z₃)

def B₃ {α : Sort u_1} {ε : Sort u_2} {β : Sort u_3} {γ : Sort u_4} (x : α → ε) (y : β → α) (z : γ → β) (w : γ) : ε

Becard

B₃xyzw = x(y(zw))

Equations

• B₃ x y z w = x (y (z w))

def B₁ {α : Sort u_1} {ε : Sort u_2} {β : Sort u_3} {γ : Sort u_4} (x : α → ε) (y : β → γ → α) (z : β) (w : γ) : ε

Blackbird

B₁xyzw = x(yzw)

Equations

• B₁ x y z w = x (y z w)

def B {α : Sort u_1} {γ : Sort u_2} {β : Sort u_3} (x : α → γ) (y : β → α) (z : β) : γ

Bluebird

Bxyz = x(yz)

Equations

• B x y z = x (y z)

def B₂ {α : Sort u_1} {ζ : Sort u_2} {β : Sort u_3} {γ : Sort u_4} {ε : Sort u_5} (x : α → ζ) (y : β → γ → ε → α) (z : β) (w : γ) (v : ε) : ζ

Bunting

B₂xyzwv = x(yzwv)

Equations

• B₂ x y z w v = x (y z w v)

def C_star {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (x : α → β → γ → δ) (y : α) (z : γ) (w : β) : δ

Cardinal Once Removed

C*xyzw = xywz

Equations

• C* x y z w = x y w z

def «termC*» : Lean.ParserDescr

Equations

• «termC*» = Lean.ParserDescr.node `termC* 1024 (Lean.ParserDescr.symbol "C*")

def C {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (x : α → β → δ) (y : β) (z : α) : δ

Cardinal

Cxyz = xzy

Equations

• C x y z = x z y

def W' {α : Sort u_1} {β : Sort u_2} (x : α) (y : α → α → β) : β

Converse Warbler

W'xy = yxx

Equations

• W' x y = y x x

def D₁ {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} {ε : Sort u_4} {γ : Sort u_5} (x : α → β → δ → ε) (y : α) (z : β) (w : γ → δ) (v : γ) : ε

Dickcissel

D₁xyzwv = xyz(wv)

Equations

• D₁ x y z w v = x y z (w v)

Double Mockingbird

M₂xy = xy(xy)

def D {α : Sort u_1} {γ : Sort u_2} {δ : Sort u_3} {β : Sort u_4} (x : α → γ → δ) (y : α) (z : β → γ) (w : β) : δ

Dove

Dxyzw = xy(zw)

Equations

• D x y z w = x y (z w)

def D₂ {α : Sort u_1} {δ : Sort u_2} {ε : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (x : α → δ → ε) (y : β → α) (z : β) (w : γ → δ) (v : γ) : ε

Dovekie

D₂xyzwv = x(yz)(wv)

Equations

• D₂ x y z w v = x (y z) (w v)

def E {α : Sort u_1} {δ : Sort u_2} {ε : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (x : α → δ → ε) (y : α) (z : β → γ → δ) (w : β) (v : γ) : ε

Eagle

Exyzwv = xy(zwv)

Equations

• E x y z w v = x y (z w v)

def F_star {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (x : α → β → γ → δ) (y : γ) (z : β) (w : α) : δ

Finch Once Removed

F*xyzw = xwzy

Equations

• F* x y z w = x w z y

def «termF*» : Lean.ParserDescr

Equations

• «termF*» = Lean.ParserDescr.node `termF* 1024 (Lean.ParserDescr.symbol "F*")

def F {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α) (y : β) (z : β → α → γ) : γ

Finch

Fxyz = zyx

Equations

• F x y z = z y x

def G {α : Sort u_1} {γ : Sort u_2} {δ : Sort u_3} {β : Sort u_4} (x : α → γ → δ) (y : β → γ) (z : β) (w : α) : δ

Goldfinch

Gxyzw = xw(yz)

Equations

• G x y z w = x w (y z)

def H {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α → β → α → γ) (y : α) (z : β) : γ

Hummingbird

Hxyz = xyzy

Equations

• H x y z = x y z y

def I {α : Sort u_1} (x : α) : α

Identity Bird

Ix = x

Equations

• I x = x

def K {α : Sort u_1} {β : Sort u_2} (x : α) : β → α

Kestrel

Kxy = x

Equations

• K x✝ x = x✝

Lark

Lxy = x(yy)

Mockingbird

Mx = xx

def O {α : Sort u_1} {β : Sort u_2} (x : (α → β) → α) (y : α → β) : β

Owl

Oxy = y(xy)

Equations

• O x y = y (x y)

def Φ {β : Sort u_1} {γ : Sort u_2} {δ : Sort u_3} {α : Sort u_4} (x : β → γ → δ) (y : α → β) (z : α → γ) (w : α) : δ

Phoenix

Φxyzw = x(yw)(zw)

Equations

• Φ x y z w = x (y w) (z w)

def Ψ {α : Sort u_1} {γ : Sort u_2} {β : Sort u_3} (x : α → α → γ) (y : β → α) (z : β) (w : β) : γ

Psi Bird

Ψxyzw = x(yz)(yw)

Equations

• Ψ x y z w = x (y z) (y w)

def Q₄ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α) (y : α → β) (z : β → γ) : γ

Quacky Bird

Q₄xyz = z(yx)

Equations

• Q₄ x y z = z (y x)

def Q {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α → β) (y : β → γ) (z : α) : γ

Queer Bird

Qxyz = y(xz)

Equations

• Q x y z = y (x z)

def Q₃ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α → β) (y : α) (z : β → γ) : γ

Quirky Bird

Q₃xyz = z(xy)

Equations

• Q₃ x y z = z (x y)

def Q₁ {α : Sort u_1} {γ : Sort u_2} {β : Sort u_3} (x : α → γ) (y : β) (z : β → α) : γ

Quixotic Bird

Q₁xyz = x(zy)

Equations

• Q₁ x y z = x (z y)

def Q₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α) (y : β → γ) (z : α → β) : γ

Quizzical Bird

Q₂xyz = y(zx)

Equations

• Q₂ x y z = y (z x)

def R_star {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (x : α → β → γ → δ) (y : γ) (z : α) (w : β) : δ

Robin Once Removed

R*xyzw = xzwy

Equations

• R* x y z w = x z w y

def «termR*» : Lean.ParserDescr

Equations

• «termR*» = Lean.ParserDescr.node `termR* 1024 (Lean.ParserDescr.symbol "R*")

def R {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α) (y : β → α → γ) (z : β) : γ

Robin

Rxyz = yzx

Equations

• R x y z = y z x

partial def Θ {α : Sort u_1} [Inhabited α] (x : α → α) : α

Sage Bird

Θx = x(Θx)

def S {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α → β → γ) (y : α → β) (z : α) : γ

Starling

Sxyz = xz(yz)

Equations

• S x y z = x z (y z)

def T {α : Sort u_1} {β : Sort u_2} (x : α) (y : α → β) : β

Thrush

Txy = yx

Equations

• T x y = y x

Turing Bird

Uxy = y(xxy)

def V_star {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (x : α → β → γ → δ) (y : β) (z : γ) (w : α) : δ

Vireo Once Removed

V*xyzw = xwyz

Equations

• V* x y z w = x w y z

def «termV*» : Lean.ParserDescr

Equations

• «termV*» = Lean.ParserDescr.node `termV* 1024 (Lean.ParserDescr.symbol "V*")

def V {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (x : α) (y : β) (z : α → β → γ) : γ

Vireo

Vxyz = zxy

Equations

• V x y z = z x y

def W {α : Sort u_1} {β : Sort u_2} (x : α → α → β) (y : α) : β

Warbler

Wxy = xyy

Equations

• W x y = x y y