Comment by marvinborner
1 day ago
The annihilating interaction between abstraction and application nodes is well-known in the area of interaction net research to ~correspond to β-reduction, as is also explained in the associated research paper [1].
α-conversion is not required in interaction nets. η-reduction is an additional rule not typically discussed, but see for example [2].
[1] https://arxiv.org/pdf/2505.20314
[2] https://www.sciencedirect.com/science/article/pii/S030439750...
> α-conversion is not required in interaction nets. η-reduction is an additional rule not typically discussed, but see for example [2].
Which makes the sloppy use of "λ-Reduction" in place of "β-reduction"--the only form of reduction or conversion applied here--even less defensible. Maybe them being non-native English speakers is partly to blame?