4 ms·
What about big T, square/angle brackets, and braces?
by lefra 5mo ago
What 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").