Extraordinary Ordinals(text.marvinborner.de) |
Extraordinary Ordinals(text.marvinborner.de) |
He illustrates some numerals in each system with a graphical notation that strongly reminds me of interaction nets [1], a computational model closely related to lambda calculus. The notation they use for lambda terms is rather non-standard. Compare
> In β-reduction, k[(x⇒b)←a]⊳k[b{a/x}]k[(x⇒b)←a]⊳k[b{a/x}]
with Wikipedia's [2]
> The β-reduction rule states that a β-redex, an application of the form (λx. t) s, reduces to the term t[x:=s].
The k[...] part means that β-reduction steps can happen in arbitrary contexts.
[0] https://www.researchgate.net/publication/323000057_Linear_Nu...
b{a/x}
means: expression b with variable x inside it replaced by expression a.
So their beta-reduction line just says that if k = ... (λx.b) a ...
it can be reduced to k = ... c ...
where c is the expression b, but with all occurrences of variable x replaced by expression a.I think Tk(x) denotes "the definition of variable k is expression x" and the square brackets are "k[x]" something like "in the context of definition k, value of expression x". So I suspect that
a=Tk(x)
a[y]
would be effectively (λk.y)x
But yes, not very clear on explaining the notation. Also seems to have some typos e.g. at the beginning have "x ∈ k, x, y" which looks to me should be "x ∋ k, x, y" (or of course "k, x, y ∈ x").