The author presents most known numeral systems (ways of representing natural numbers) in lambda calculus, classified by whether the term use their bound variables exactly one time (linear), at most one time (affine), or multiple times (non-linear).
Mackie's paper [0] (one of the references) provides a good introduction to these. (although he strangely gets the definition of Church numerals wrong with "Church numerals encode numbers with repeated application: λx f. f^n x." in which he reversed the order of arguments f and x).
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.
The author unfortunately only describes about half of the syntax they use, or rather, they describe the syntax of the language but assume the reader is familiar with the (rather obscure even in a PLT context) metalanguage.
The author presents most known numeral systems (ways of representing natural numbers) in lambda calculus, classified by whether the term use their bound variables exactly one time (linear), at most one time (affine), or multiple times (non-linear). Mackie's paper [0] (one of the references) provides a good introduction to these. (although he strangely gets the definition of Church numerals wrong with "Church numerals encode numbers with repeated application: λx f. f^n x." in which he reversed the order of arguments f and x).
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...
[1] https://en.wikipedia.org/wiki/Interaction_nets
[2] https://en.wikipedia.org/wiki/Lambda_calculus
I think I lack context to see what this is about. The line graphs are pretty though, and I'd like to understand more.
The author unfortunately only describes about half of the syntax they use, or rather, they describe the syntax of the language but assume the reader is familiar with the (rather obscure even in a PLT context) metalanguage.
I didn’t understand that notation. Can someone please explain?
I think:
is: and is just application. I.e.What about big T, square/angle brackets, and braces?
yeah no idea
const f = (x) => x + 1;
Hmm nice I guess, but I expected it was going to be about transfinite ordinals. I wonder if it can be extended to them.
This should be "numerals"
This is beautiful art