Definition
Interaction Calculus
The Interaction Calculus is a minimal term rewriting system inspired by the Lambda Calculus (λC), but with some key differences that make it inherently more efficient, in a way that closely resembles Lamping’s optimal λ-calculus evaluator, and more expressive, in some ways. In particular:
- Vars are affine: they can only occur up to one time.
- Vars are global: they can occur anywhere in the program.
- It features first-class superpositions and duplications.
Global lambdas allow the IC to express concepts that aren’t possible on the traditional λC, including continuations, linear HOAS, and mutable references. Superpositions and duplications allow the IC to be optimally evaluated, making some computations exponentially faster. Finally, being fully affine makes its garbage collector very efficient, and greatly simplifies parallelism.
It has been established by Victor Taelin.