4 ms·
Extraordinary Ordinals
- p1esk 5mo agoI didn’t understand that notation. Can someone please explain?
- ngruhn 5mo agoI think: x => a is: λx. a and f <- a is just application. I.e. f a
- lefra 5mo agoWhat about big T, square/angle brackets, and braces?
- ngruhn 5mo agoyeah no idea
- deleted 5mo ago[deleted]
- jz391 5mo agoBraces are substitution, so 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").
- jdw64 5mo agoconst f = (x) => x + 1;
- bananaflag 5mo agoThis should be "numerals"
- lefra 5mo agoI think I lack context to see what this is about. The line graphs are pretty though, and I'd like to understand more.
- dnnddidiej 5mo agoThis is beautiful art
- tromp 5mo agoThe 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_Numeral_Systems https://www.researchgate.net/publication/323000057_Linear_Nu... [1] https://en.wikipedia.org/wiki/Interaction_nets https://en.wikipedia.org/wiki/Interaction_nets [2] https://en.wikipedia.org/wiki/Lambda_calculus https://en.wikipedia.org/wiki/Lambda_calculus
- throwaway81523 5mo agoHmm nice I guess, but I expected it was going to be about transfinite ordinals. I wonder if it can be extended to them.
- Sharlin 5mo agoThe 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.
- 0rbiter 5mo agoInteresting. I wonder what the `s` functions in Scott & Church are.
- marvinborner 5mo agoThey are not functions, but variables. Maybe this helps, as they basically are "selectors": https://text.marvinborner.de/2024-11-18-00.html#tagged-unions https://text.marvinborner.de/2024-11-18-00.html#tagged-union...
- tug2024 5mo ago[dead]