Search code, repositories, users, issues, pull requests...

The Interaction Calculus (IC) is a minimal programming language and model of computation obtained by "completing" the affine Lambda Calculus in a way that matches perfectly Lamping's optimal reduction algorithm. It can also be seen as a textual syntax for Symetric Interaction Combinators: both views are equivalent. As a model of computation, the IC has compeling characteristics:

Where, a <- b stands for a global, linear substitution of a by b. It can be performed in O(1) by a simple array write, which, in turn, makes all rewrite rules above O(1) too.

But annihilations only happen when identical nodes interact. On interaction nets, it is possible for different nodes to interact, which triggers another rule, the commutation. That rule could be seen as handling the following expressions:

But how could we "project" a lambda or "apply" a pair? On the Lambda Calculus, these cases are undefined and stuck, and should be type errors. Yet, by interpreting the effects of the commutation rule on the interaction combinator point of view, we can propose a reasonable reduction for these lambda expressions:

Leave a Comment