3 ms·
I didn’t understand that notation. Can someone please explain?
by p1esk 5mo ago
I 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;