Remove Aviary_html.
parent
24a48bfac2
commit
cd8fec9483
|
|
@ -13,8 +13,7 @@ use. Their inclusion here serves more as pseudo-documentation than anything.
|
||||||
university press, 2000.
|
university press, 2000.
|
||||||
-/
|
-/
|
||||||
|
|
||||||
/--
|
/-- #### Bald Eagle
|
||||||
#### Bald Eagle
|
|
||||||
|
|
||||||
`E'xy₁y₂y₃z₁z₂z₃ = x(y₁y₂y₃)(z₁z₂z₃)`
|
`E'xy₁y₂y₃z₁z₂z₃ = x(y₁y₂y₃)(z₁z₂z₃)`
|
||||||
-/
|
-/
|
||||||
|
|
@ -22,36 +21,31 @@ def E' (x : α → β → γ)
|
||||||
(y₁ : δ → ε → α) (y₂ : δ) (y₃ : ε)
|
(y₁ : δ → ε → α) (y₂ : δ) (y₃ : ε)
|
||||||
(z₁ : ζ → η → β) (z₂ : ζ) (z₃ : η) := x (y₁ y₂ y₃) (z₁ z₂ z₃)
|
(z₁ : ζ → η → β) (z₂ : ζ) (z₃ : η) := x (y₁ y₂ y₃) (z₁ z₂ z₃)
|
||||||
|
|
||||||
/--
|
/-- #### Becard
|
||||||
#### Becard
|
|
||||||
|
|
||||||
`B₃xyzw = x(y(zw))`
|
`B₃xyzw = x(y(zw))`
|
||||||
-/
|
-/
|
||||||
def B₃ (x : α → ε) (y : β → α) (z : γ → β) (w : γ) := x (y (z w))
|
def B₃ (x : α → ε) (y : β → α) (z : γ → β) (w : γ) := x (y (z w))
|
||||||
|
|
||||||
/--
|
/-- #### Blackbird
|
||||||
#### Blackbird
|
|
||||||
|
|
||||||
`B₁xyzw = x(yzw)`
|
`B₁xyzw = x(yzw)`
|
||||||
-/
|
-/
|
||||||
def B₁ (x : α → ε) (y : β → γ → α) (z : β) (w : γ) := x (y z w)
|
def B₁ (x : α → ε) (y : β → γ → α) (z : β) (w : γ) := x (y z w)
|
||||||
|
|
||||||
/--
|
/-- #### Bluebird
|
||||||
#### Bluebird
|
|
||||||
|
|
||||||
`Bxyz = x(yz)`
|
`Bxyz = x(yz)`
|
||||||
-/
|
-/
|
||||||
def B (x : α → γ) (y : β → α) (z : β) := x (y z)
|
def B (x : α → γ) (y : β → α) (z : β) := x (y z)
|
||||||
|
|
||||||
/--
|
/-- #### Bunting
|
||||||
#### Bunting
|
|
||||||
|
|
||||||
`B₂xyzwv = x(yzwv)`
|
`B₂xyzwv = x(yzwv)`
|
||||||
-/
|
-/
|
||||||
def B₂ (x : α → ζ) (y : β → γ → ε → α) (z : β) (w : γ) (v : ε) := x (y z w v)
|
def B₂ (x : α → ζ) (y : β → γ → ε → α) (z : β) (w : γ) (v : ε) := x (y z w v)
|
||||||
|
|
||||||
/--
|
/-- #### Cardinal Once Removed
|
||||||
#### Cardinal Once Removed
|
|
||||||
|
|
||||||
`C*xyzw = xywz`
|
`C*xyzw = xywz`
|
||||||
-/
|
-/
|
||||||
|
|
@ -59,50 +53,48 @@ def C_star (x : α → β → γ → δ) (y : α) (z : γ) (w : β) := x y w z
|
||||||
|
|
||||||
notation "C*" => C_star
|
notation "C*" => C_star
|
||||||
|
|
||||||
/--
|
/-- #### Cardinal
|
||||||
#### Cardinal
|
|
||||||
|
|
||||||
`Cxyz = xzy`
|
`Cxyz = xzy`
|
||||||
-/
|
-/
|
||||||
def C (x : α → β → δ) (y : β) (z : α) := x z y
|
def C (x : α → β → δ) (y : β) (z : α) := x z y
|
||||||
|
|
||||||
/--
|
/-- #### Converse Warbler
|
||||||
#### Converse Warbler
|
|
||||||
|
|
||||||
`W'xy = yxx`
|
`W'xy = yxx`
|
||||||
-/
|
-/
|
||||||
def W' (x : α) (y : α → α → β) := y x x
|
def W' (x : α) (y : α → α → β) := y x x
|
||||||
|
|
||||||
/--
|
/-- #### Dickcissel
|
||||||
#### Dickcissel
|
|
||||||
|
|
||||||
`D₁xyzwv = xyz(wv)`
|
`D₁xyzwv = xyz(wv)`
|
||||||
-/
|
-/
|
||||||
def D₁ (x : α → β → δ → ε) (y : α) (z : β) (w : γ → δ) (v : γ) := x y z (w v)
|
def D₁ (x : α → β → δ → ε) (y : α) (z : β) (w : γ → δ) (v : γ) := x y z (w v)
|
||||||
|
|
||||||
/--
|
/-! #### Double Mockingbird
|
||||||
#### Dove
|
|
||||||
|
`M₂xy = xy(xy)`
|
||||||
|
-/
|
||||||
|
|
||||||
|
/-- #### Dove
|
||||||
|
|
||||||
`Dxyzw = xy(zw)`
|
`Dxyzw = xy(zw)`
|
||||||
-/
|
-/
|
||||||
def D (x : α → γ → δ) (y : α) (z : β → γ) (w : β) := x y (z w)
|
def D (x : α → γ → δ) (y : α) (z : β → γ) (w : β) := x y (z w)
|
||||||
|
|
||||||
/--
|
/-- #### Dovekie
|
||||||
#### Dovekie
|
|
||||||
|
|
||||||
`D₂xyzwv = x(yz)(wv)`
|
`D₂xyzwv = x(yz)(wv)`
|
||||||
-/
|
-/
|
||||||
def D₂ (x : α → δ → ε) (y : β → α) (z : β) (w : γ → δ) (v : γ) := x (y z) (w v)
|
def D₂ (x : α → δ → ε) (y : β → α) (z : β) (w : γ → δ) (v : γ) := x (y z) (w v)
|
||||||
|
|
||||||
/--
|
/-- #### Eagle
|
||||||
#### Eagle
|
|
||||||
|
|
||||||
`Exyzwv = xy(zwv)`
|
`Exyzwv = xy(zwv)`
|
||||||
-/
|
-/
|
||||||
def E (x : α → δ → ε) (y : α) (z : β → γ → δ) (w : β) (v : γ) := x y (z w v)
|
def E (x : α → δ → ε) (y : α) (z : β → γ → δ) (w : β) (v : γ) := x y (z w v)
|
||||||
|
|
||||||
/--
|
/-- #### Finch Once Removed
|
||||||
#### Finch Once Removed
|
|
||||||
|
|
||||||
`F*xyzw = xwzy`
|
`F*xyzw = xwzy`
|
||||||
-/
|
-/
|
||||||
|
|
@ -110,99 +102,95 @@ def F_star (x : α → β → γ → δ) (y : γ) (z : β) (w : α) := x w z y
|
||||||
|
|
||||||
notation "F*" => F_star
|
notation "F*" => F_star
|
||||||
|
|
||||||
/--
|
/-- #### Finch
|
||||||
#### Finch
|
|
||||||
|
|
||||||
`Fxyz = zyx`
|
`Fxyz = zyx`
|
||||||
-/
|
-/
|
||||||
def F (x : α) (y : β) (z : β → α → γ) := z y x
|
def F (x : α) (y : β) (z : β → α → γ) := z y x
|
||||||
|
|
||||||
/--
|
/-- #### Goldfinch
|
||||||
#### Goldfinch
|
|
||||||
|
|
||||||
`Gxyzw = xw(yz)`
|
`Gxyzw = xw(yz)`
|
||||||
-/
|
-/
|
||||||
def G (x : α → γ → δ) (y : β → γ) (z : β) (w : α) := x w (y z)
|
def G (x : α → γ → δ) (y : β → γ) (z : β) (w : α) := x w (y z)
|
||||||
|
|
||||||
/--
|
/-- #### Hummingbird
|
||||||
#### Hummingbird
|
|
||||||
|
|
||||||
`Hxyz = xyzy`
|
`Hxyz = xyzy`
|
||||||
-/
|
-/
|
||||||
def H (x : α → β → α → γ) (y : α) (z : β) := x y z y
|
def H (x : α → β → α → γ) (y : α) (z : β) := x y z y
|
||||||
|
|
||||||
/--
|
/-- #### Identity Bird
|
||||||
#### Identity Bird
|
|
||||||
|
|
||||||
`Ix = x`
|
`Ix = x`
|
||||||
-/
|
-/
|
||||||
def I (x : α) : α := x
|
def I (x : α) : α := x
|
||||||
|
|
||||||
/--
|
/-- #### Kestrel
|
||||||
#### Kestrel
|
|
||||||
|
|
||||||
`Kxy = x`
|
`Kxy = x`
|
||||||
-/
|
-/
|
||||||
def K (x : α) (_ : β) := x
|
def K (x : α) (_ : β) := x
|
||||||
|
|
||||||
/--
|
/-! #### Lark
|
||||||
#### Owl
|
|
||||||
|
`Lxy = x(yy)`
|
||||||
|
-/
|
||||||
|
|
||||||
|
/-! #### Mockingbird
|
||||||
|
|
||||||
|
`Mx = xx`
|
||||||
|
-/
|
||||||
|
|
||||||
|
/-- #### Owl
|
||||||
|
|
||||||
`Oxy = y(xy)`
|
`Oxy = y(xy)`
|
||||||
-/
|
-/
|
||||||
def O (x : (α → β) → α) (y : α → β) := y (x y)
|
def O (x : (α → β) → α) (y : α → β) := y (x y)
|
||||||
|
|
||||||
/--
|
/-- #### Phoenix
|
||||||
#### Phoenix
|
|
||||||
|
|
||||||
`Φxyzw = x(yw)(zw)`
|
`Φxyzw = x(yw)(zw)`
|
||||||
-/
|
-/
|
||||||
def Φ (x : β → γ → δ) (y : α → β) (z : α → γ) (w : α) := x (y w) (z w)
|
def Φ (x : β → γ → δ) (y : α → β) (z : α → γ) (w : α) := x (y w) (z w)
|
||||||
|
|
||||||
/--
|
/-- #### Psi Bird
|
||||||
#### Psi Bird
|
|
||||||
|
|
||||||
`Ψxyzw = x(yz)(yw)`
|
`Ψxyzw = x(yz)(yw)`
|
||||||
-/
|
-/
|
||||||
def Ψ (x : α → α → γ) (y : β → α) (z : β) (w : β) := x (y z) (y w)
|
def Ψ (x : α → α → γ) (y : β → α) (z : β) (w : β) := x (y z) (y w)
|
||||||
|
|
||||||
/--
|
/-- #### Quacky Bird
|
||||||
#### Quacky Bird
|
|
||||||
|
|
||||||
`Q₄xyz = z(yx)`
|
`Q₄xyz = z(yx)`
|
||||||
-/
|
-/
|
||||||
def Q₄ (x : α) (y : α → β) (z : β → γ) := z (y x)
|
def Q₄ (x : α) (y : α → β) (z : β → γ) := z (y x)
|
||||||
|
|
||||||
/--
|
/-- #### Queer Bird
|
||||||
#### Queer Bird
|
|
||||||
|
|
||||||
`Qxyz = y(xz)`
|
`Qxyz = y(xz)`
|
||||||
-/
|
-/
|
||||||
def Q (x : α → β) (y : β → γ) (z : α) := y (x z)
|
def Q (x : α → β) (y : β → γ) (z : α) := y (x z)
|
||||||
|
|
||||||
/--
|
/-- #### Quirky Bird
|
||||||
#### Quirky Bird
|
|
||||||
|
|
||||||
`Q₃xyz = z(xy)`
|
`Q₃xyz = z(xy)`
|
||||||
-/
|
-/
|
||||||
def Q₃ (x : α → β) (y : α) (z : β → γ) := z (x y)
|
def Q₃ (x : α → β) (y : α) (z : β → γ) := z (x y)
|
||||||
|
|
||||||
/--
|
/-- #### Quixotic Bird
|
||||||
#### Quixotic Bird
|
|
||||||
|
|
||||||
`Q₁xyz = x(zy)`
|
`Q₁xyz = x(zy)`
|
||||||
-/
|
-/
|
||||||
def Q₁ (x : α → γ) (y : β) (z : β → α) := x (z y)
|
def Q₁ (x : α → γ) (y : β) (z : β → α) := x (z y)
|
||||||
|
|
||||||
/--
|
/-- #### Quizzical Bird
|
||||||
#### Quizzical Bird
|
|
||||||
|
|
||||||
`Q₂xyz = y(zx)`
|
`Q₂xyz = y(zx)`
|
||||||
-/
|
-/
|
||||||
def Q₂ (x : α) (y : β → γ) (z : α → β) := y (z x)
|
def Q₂ (x : α) (y : β → γ) (z : α → β) := y (z x)
|
||||||
|
|
||||||
/--
|
/-- #### Robin Once Removed
|
||||||
#### Robin Once Removed
|
|
||||||
|
|
||||||
`R*xyzw = xzwy`
|
`R*xyzw = xzwy`
|
||||||
-/
|
-/
|
||||||
|
|
@ -210,36 +198,36 @@ def R_star (x : α → β → γ → δ) (y : γ) (z : α) (w : β) := x z w y
|
||||||
|
|
||||||
notation "R*" => R_star
|
notation "R*" => R_star
|
||||||
|
|
||||||
/--
|
/-- #### Robin
|
||||||
#### Robin
|
|
||||||
|
|
||||||
`Rxyz = yzx`
|
`Rxyz = yzx`
|
||||||
-/
|
-/
|
||||||
def R (x : α) (y : β → α → γ) (z : β) := y z x
|
def R (x : α) (y : β → α → γ) (z : β) := y z x
|
||||||
|
|
||||||
/--
|
/-- #### Sage Bird
|
||||||
#### Sage Bird
|
|
||||||
|
|
||||||
`Θx = x(Θx)`
|
`Θx = x(Θx)`
|
||||||
-/
|
-/
|
||||||
partial def Θ [Inhabited α] (x : α → α) := x (Θ x)
|
partial def Θ [Inhabited α] (x : α → α) := x (Θ x)
|
||||||
|
|
||||||
/--
|
/-- #### Starling
|
||||||
#### Starling
|
|
||||||
|
|
||||||
`Sxyz = xz(yz)`
|
`Sxyz = xz(yz)`
|
||||||
-/
|
-/
|
||||||
def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
|
def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
|
||||||
|
|
||||||
/--
|
/-- #### Thrush
|
||||||
#### Thrush
|
|
||||||
|
|
||||||
`Txy = yx`
|
`Txy = yx`
|
||||||
-/
|
-/
|
||||||
def T (x : α) (y : α → β) := y x
|
def T (x : α) (y : α → β) := y x
|
||||||
|
|
||||||
/--
|
/-! #### Turing Bird
|
||||||
#### Vireo Once Removed
|
|
||||||
|
`Uxy = y(xxy)`
|
||||||
|
-/
|
||||||
|
|
||||||
|
/-- #### Vireo Once Removed
|
||||||
|
|
||||||
`V*xyzw = xwyz`
|
`V*xyzw = xwyz`
|
||||||
-/
|
-/
|
||||||
|
|
@ -247,15 +235,13 @@ def V_star (x : α → β → γ → δ) (y : β) (z : γ) (w : α) := x w y z
|
||||||
|
|
||||||
notation "V*" => V_star
|
notation "V*" => V_star
|
||||||
|
|
||||||
/--
|
/-- #### Vireo
|
||||||
#### Vireo
|
|
||||||
|
|
||||||
`Vxyz = zxy`
|
`Vxyz = zxy`
|
||||||
-/
|
-/
|
||||||
def V (x : α) (y : β) (z : α → β → γ) := z x y
|
def V (x : α) (y : β) (z : α → β → γ) := z x y
|
||||||
|
|
||||||
/--
|
/-- #### Warbler
|
||||||
#### Warbler
|
|
||||||
|
|
||||||
`Wxy = xyy`
|
`Wxy = xyy`
|
||||||
-/
|
-/
|
||||||
|
|
|
||||||
|
|
@ -1,58 +0,0 @@
|
||||||
<!DOCTYPE html>
|
|
||||||
<html>
|
|
||||||
<head>
|
|
||||||
<meta charset="utf-8">
|
|
||||||
<meta name="viewport" content="width=device-width">
|
|
||||||
<title>Bookshelf.Combinator.Aviary</title>
|
|
||||||
<script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
|
|
||||||
<script id="MathJax-script" async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
|
|
||||||
</head>
|
|
||||||
<body>
|
|
||||||
<h1>Bookshelf.Combinator.Aviary</h1>
|
|
||||||
<p>
|
|
||||||
A list of birds as defined in <i>To Mock a Mockingbird</i>.
|
|
||||||
Refer to <a href="./Aviary.html">Bookshelf/Combinator/Aviary</a>
|
|
||||||
for implementation examples.
|
|
||||||
</p>
|
|
||||||
<ul>
|
|
||||||
<li><b>Bald Eagle:</b> \(\hat{E}xy_1y_2y_3z_1z_2z_3 = x(y_1y_2y_3)(z_1z_2z_3)\)</li>
|
|
||||||
<li><b>Becard:</b> \(B_3xyzw = x(y(zw))\)</li>
|
|
||||||
<li><b>Blackbird:</b> \(B_1xyzw = x(yzw)\)</li>
|
|
||||||
<li><b>Bluebird:</b> \(Bxyz = x(yz)\)</li>
|
|
||||||
<li><b>Bunting:</b> \(B_2xyzwv = x(yzwv)\)</li>
|
|
||||||
<li><b>Cardinal Once Removed:</b> \(C^*xyzw = xywz\)</li>
|
|
||||||
<li><b>Cardinal:</b> \(Cxyz = xzy\)</li>
|
|
||||||
<li><b>Converse Warbler:</b> \(W'xy = yxx\)</li>
|
|
||||||
<li><b>Dickcissel:</b> \(D_1xyzwv = xyz(wv)\)</li>
|
|
||||||
<li><b>Double Mockingbird:</b> \(M_2xy = xy(xy)\)</li>
|
|
||||||
<li><b>Dove:</b> \(Dxyzw = xy(zw)\)</li>
|
|
||||||
<li><b>Dovekie:</b> \(D_2xyzwv = x(yz)(wv)\)</li>
|
|
||||||
<li><b>Eagle:</b> \(Exyzwv = xy(zwv)\)</li>
|
|
||||||
<li><b>Finch Once Removed:</b> \(F^*xyzw = xwzy\)</li>
|
|
||||||
<li><b>Finch:</b> \(Fxyz = zyx\)</li>
|
|
||||||
<li><b>Goldfinch:</b> \(Gxyzw = xw(yz)\)</li>
|
|
||||||
<li><b>Hummingbird:</b> \(Hxyz = xyzy\)</li>
|
|
||||||
<li><b>Identity Bird:</b> \(Ix = x\)</li>
|
|
||||||
<li><b>Kestrel:</b> \(Kxy = x\)</li>
|
|
||||||
<li><b>Lark:</b> \(Lxy = x(yy)\)</li>
|
|
||||||
<li><b>Mockingbird:</b> \(Mx = xx\)</li>
|
|
||||||
<li><b>Owl:</b> \(Oxy = y(xy)\)</li>
|
|
||||||
<li><b>Phoenix:</b> \(\Phi xyzw = x(yw)(zw)\)</li>
|
|
||||||
<li><b>Psi Bird:</b> \(\Psi xyzw = x(yz)(yw)\)</li>
|
|
||||||
<li><b>Quacky Bird:</b> \(Q_4xyz = z(yx)\)</li>
|
|
||||||
<li><b>Queer Bird:</b> \(Qxyz = y(xz)\)</li>
|
|
||||||
<li><b>Quirky Bird:</b> \(Q_3xyz = z(xy)\)</li>
|
|
||||||
<li><b>Quixotic Bird:</b> \(Q_1xyz = x(zy)\)</li>
|
|
||||||
<li><b>Quizzical Bird:</b> \(Q_2xyz = y(zx)\)</li>
|
|
||||||
<li><b>Robin Once Removed:</b> \(R^*xyzw = xzwy\)</li>
|
|
||||||
<li><b>Robin:</b> \(Rxyz = yzx\)</li>
|
|
||||||
<li><b>Sage Bird:</b> \(\Theta x = x(\Theta x)\)</li>
|
|
||||||
<li><b>Starling:</b> \(Sxyz = xz(yz)\)</li>
|
|
||||||
<li><b>Thrush:</b> \(Txy = yx\)</li>
|
|
||||||
<li><b>Turing Bird:</b> \(Uxy = y(xxy)\)</li>
|
|
||||||
<li><b>Vireo Once Removed:</b> \(V^*xyzw = xwyz\)</li>
|
|
||||||
<li><b>Vireo:</b> \(Vxyz = zxy\)</li>
|
|
||||||
<li><b>Warbler:</b> \(Wxy = xyy\)</li>
|
|
||||||
</ul>
|
|
||||||
</body>
|
|
||||||
</html>
|
|
||||||
Loading…
Reference in New Issue