typo in 2nd diagram (of commutation law)
tribbloid opened this issue · 1 comments
tribbloid commented
original:
Lambda Application Pair Application
let {a b} = (λx body) in cont ({fst snd} arg)
------------------------------ ---------------
a <- (λx0 b0) let {x0 x1} = arg in
b <- (λx1 b1) {(fst x0) (snd x1)}
x <- {x0 x1}
let {b0 b1} = body in
cont
ret arg ret arg ret arg ret arg
| | | | | | | |
|___| | | |___| | |
let \#/ /_\ /_\ app \ / /#\ /#\
| ==> | \/ | | ==> | \/ |
| |_ /\ _| | |_ /\ _|
lam /_\ \#/ \#/ pair /#\ \ / \ /
| | | | | | | |
| | | | | | | |
x body x body var body var body
"The projection of a lambda "The application of a pair is a pair
substitutes the projected vars of the first element and the second
by a copies of the lambda that element applied to projections of the
return its projected body, with application argument."
the bound variable substituted
by the new lambda vars paired."
should be:
Lambda Duplication Pair Application
let {a b} = (λx body) in cont ({fst snd} arg)
------------------------------ ---------------
a <- (λx0 b0) let {x0 x1} = arg in
b <- (λx1 b1) {(fst x0) (snd x1)}
x <- {x0 x1}
let {b0 b1} = body in
cont
a b a b ret arg ret arg
| | | | | | | |
|___| | | |___| | |
let \#/ /_\ /_\ app \ / /#\ /#\
| ==> | \/ | | ==> | \/ |
| |_ /\ _| | |_ /\ _|
lam /_\ \#/ \#/ pair /#\ \ / \ /
| | | | | | | |
| | | | | | | |
x body x body fst snd fst snd
"The projection of a lambda "The application of a pair is a pair
substitutes the projected vars of the first element and the second
by a copies of the lambda that element applied to projections of the
return its projected body, with application argument."
the bound variable substituted
by the new lambda vars paired."
tribbloid commented
I also realised that any reference to "superposition" or "node labelling/coloring" has been removed in HVM2, should this doc be considered obsolete?