GoKawiilExtraordinary Ordinals Marvin Borner Abstract draw some lambda encodings of numbers as graphs.
make them extraordinary. draw some lambda encodings of numbers as graphs.make them extraordinary.
Syntax.
E x p r e s s i o n s e , b , f , a ∷ = x V a r i a b l e ∣ x ⇒ b A b s t r a c t i o n ∣ f ← a A p p l i c a t i o n V a r i a b l e s x ∈ k , x , y , … N u m b e r s n ∈ 0 , 1 , 2 , … \small\begin{array}{lrcll} \mathrm{Expressions}\quad & e,b,f,a & {\Coloneqq} & x & \quad\mathrm{Variable} \\ & & {\mid} & x\Rightarrow b & \quad\mathrm{Abstraction} \\ & & {\mid} & f\leftarrow a & \quad\mathrm{Application} \\ \mathrm{Variables} & x & {\in} & \mathsf{k}, \mathsf{x}, \mathsf{y}, \dots \\ \mathrm{Numbers} & n & {\in} & 0, 1, 2, \dots \end{array} ExpressionsVariablesNumberse,b,f,axn::=∣∣∈∈xx⇒bf←ak,x,y,…0,1,2,…VariableAbstractionApplication
There are 3 categories—Linear, Affine, and Non-Linear—each having several encodings. Notably, every presented encoding can be used for arithmetic.
(all diagrams are drawn by hand in latex+tikz without ai; pow: source, draft notes)
Linear
Variables x x x are names for the edges connecting free vertices.
Application. T ( k [ f ← a ] ) \mathcal{T}(k[f\leftarrow a]) T(k[f←a]):
Abstraction. T ( k [ x ⇒ b ] ) \mathcal{T}(k[x\Rightarrow b]) T(k[x⇒b]):
... continue reading