What I have learnt:
- What is an interaction net, its deduction & interaction rules,
- How deduction rules can be changed into interaction rules -- you "link" the two sides of one deduction rule, "magically" turn their arrows up and rearrange the bubbles, and then split them according to the rearrangement, and
- You can use interaction rules to simply represent a interaction programming language's syntax.
What I am confused of:
Why interaction rules can be used as syntaxes: they haven't told me how to translate interaction rules back into deduction rules, they are only giving one direction of the translation.
Why interaction rules are chosen for syntaxes: since there've been already deduction rules for describing the net's behavior, why even use harder-to-read interaction rules to describe it? Otherwise you can just use deduction rules and translate it into interaction rules when using any interaction PLs. Is it easier to be applied in some technical details? How does interaction rules work on one sentence like
(Cons Nil Nil)?