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.
The HVM is a fast, fully featured implementation of this calculus.
This repo now includes a reference implementation in C, which is also quite fast!
Now it also includes a single-file implementation in Haskell, great for learning!
This repository includes a reference implementation of the Interaction Calculus in plain C, with some additional features, like native numbers. To install it:
make clean
make
Then, run one of the examples:
./bin/ic run examples/test_0.ic
For learning, edit the Haskell file: it is simpler, and has a step debugger.
An IC term is defined by the following grammar:
Term ::=
| VAR: Name
| ERA: "*"
| LAM: "λ" Name "." Term
| APP: "(" Term " " Term ")"
| SUP: "&" Label "{" Term "," Term "}"
| DUP: "!" "&" Label "{" Name "," Name "}" "=" Term ";" Term
Where: - VAR represents a variable. - ERA represents an erasure. - LAM represents a lambda. - APP represents a application. - SUP represents a superposition. - DUP represents a duplication.
Lambdas are curried, and work like their λC counterpart, except with a relaxed scope, and with affine usage. Applications eliminate lambdas, like in λC, through the beta-reduce (APP-LAM) interaction.
Superpositions work like pairs. Duplications eliminate superpositions through the DUP-SUP interaction, which works exactly like a pair projection.
What makes SUPs and DUPs unique is how they interact with LAMs and APPs. When a SUP is applied to an argument, it reduces through the APP-SUP interaction, and when a LAM is projected, it reduces through the DUP-LAM interaction. This gives a computational behavior for every possible interaction: there are no runtime errors on the Interaction Calculus.
The 'Label' is just a numeric value. It affects the DUP-SUP interaction.
The core interaction rules are listed below:
(* a)
----- APP-ERA
*
(λx.f a)
-------- APP-LAM
x <- a
f
(&L{a,b} c)
----------------- APP-SUP
! &L{c0,c1} = c;
&L{(a c0),(b c1)}
! &L{r,s} = *;
K
-------------- DUP-ERA
r <- *
s <- *
K
! &L{r,s} = λx.f;
K
----------------- DUP-LAM
r <- λx0.f0
s <- λx1.f1
x <- &L{x0,x1}
! &L{f0,f1} = f;
K
! &L{x,y} = &L{a,b};
K
-------------------- DUP-SUP (if equal labels)
x <- a
y <- b
K
! &L{x,y} = &R{a,b};
K
-------------------- DUP-SUP (if different labels)
x <- &R{a0,b0}
y <- &R{a1,b1}
! &L{a0,a1} = a;
! &L{b0,b1} = b;
K
Where x <- t stands for a global substitution of x by t.
Since variables are affine, substitutions can be implemented efficiently by just
inserting an entry in a global substitution map (sub[var] = value). There is
no need to traverse the target term, or to handle name capture, as long as fresh
variable names are globally unique. It can also be implemented in a concurrent
setup with a single atomic-swap.
Below is a pseudocode implementation of these interaction rules:
def app_lam(app, lam):
sub[lam.nam] = app.arg
return lam.bod
def app_sup(app, sup):
x0 = fresh()
x1 = fresh()
a0 = App(sup.lft, Var(x0))
a1 = App(sup.rgt, Var(x1))
return Dup(sup.lab, x0, x1, app.arg, Sup(a0, a1))
def dup_lam(dup, lam):
x0 = fresh()
x1 = fresh()
f0 = fresh()
f1 = fresh()
sub[dup.lft] = Lam(x0, Var(f0))
sub[dup.rgt] = Lam(x1, Var(f1))
sub[lam.nam] = Sup(dup.lab, Var(x0), Var(x1))
return Dup(dup.lab, f0, f1, lam.bod, dup.bod)
def dup_sup(dup, sup):
if dup.lab == sup.lab:
sub[dup.lft] = sup.lft
sub[dup.rgt] = sup.rgt
return dup.bod
else:
a0 = fresh()
a1 = fresh()
b0 = fresh()
b1 = fresh()
sub[dup.lft] = Sup(sup.lab, Var(a0), Var(b0))
sub[dup.rgt] = Sup(sup.lab, Var(a1), Var(b1))
return Dup(dup.lab, a0, a1, sup.lft, Dup(dup.lab, b0, b1, sup.rgt, dup.bod))
Terms can be reduced to weak head normal form, which means reducing until the outermost constructor is a value (LAM, SUP, etc.), or until no more reductions are possible. Example:
def whnf(term):
while True:
match term:
case Var(nam):
if nam in sub:
term = sub[nam]
else:
return term
case App(fun, arg):
fun = whnf(fun)
match fun.tag:
case Lam: term = app_lam(term, fun)
case Sup: term = app_sup(term, fun)
case _ : return App(fun, arg)
case Dup(lft, rgt, val, bod):
val = whnf(val)
match val.tag:
case Lam: term = dup_lam(term, val)
case Sup: term = dup_sup(term, val)
case _ : return Dup(lft, rgt, val, bod)
case _:
return term
Terms can be reduced to full normal form by recursively taking the whnf:
def normal(term):
term = whnf(term)
match term:
case Lam(nam, bod):
bod_nf = normal(bod)
return Lam(nam, bod_nf)
case App(fun, arg):
fun_nf = normal(fun)
arg_nf = normal(arg)
return App(fun_nf, arg_nf)
...
case _:
return term
Below are some normalization examples.
Example 0: (simple λ-term)
(λx.λt.(t x) λy.y)
------------------ APP-LAM
λt.(t λy.y)
Example 1: (larger λ-term)
(λb.λt.λf.((b f) t) λT.λF.T)
---------------------------- APP-LAM
λt.λf.((λT.λF.T f) t)
----------------------- APP-LAM
λt.λf.(λF.t f)
-------------- APP-LAM
λt.λf.t
Example 2: (global scopes)
{x,(λx.λy.y λk.k)}
------------------ APP-LAM
{λk.k,λy.y}
Example 3: (superposition)
!{a,b} = {λx.x,λy.y}; (a b)
--------------------------- DUP-SUP
(λx.x λy.y)
----------- APP-LAM
λy.y
Example 4: (overlap)
({λx.x,λy.y} λz.z)
------------------ APP-SUP
! {x0,x1} = λz.z; {(λx.x x0),(λy.y x1)}
--------------------------------------- DUP-LAM
! {f0,f1} = {r,s}; {(λx.x λr.f0),(λy.y λs.f1)}
---------------------------------------------- DUP-SUP
{(λx.x λr.r),(λy.y λs.s)}
------------------------- APP-LAM
{λr.r,(λy.y λs.s)}
------------------ APP-LAM
{λr.r,λs.s}
Example 5: (default test term)
The following term can be used to test all interactions:
((λf.λx.!{f0,f1}=f;(f0 (f1 x)) λB.λT.λF.((B F) T)) λa.λb.a)
----------------------------------------------------------- 16 interactions
λa.λb.a
An Interaction Calculus term can be collapsed to a superposed tree of pure Lambda Calculus terms without SUPs and DUPs, by extending the evaluator with the following collapse interactions:
λx.*
------ ERA-LAM
x <- *
*
(f *)
----- ERA-APP
*
λx.&L{f0,f1}
----------------- SUP-LAM
x <- &L{x0,x1}
&L{λx0.f0,λx1.f1}
(f &L{x0,x1})
------------------- SUP-APP
!&L{f0,f1} = f;
&L{(f0 x0),(f1 x1)}
!&L{x0,x1} = x; K
----------------- DUP-VAR
x0 <- x
x1 <- x
K
!&L{a0,a1} = (f x); K
--------------------- DUP-APP
a0 <- (f0 x0)
a1 <- (f1 x1)
!&L{f0,f1} = f;
!&L{x0,x1} = x;
K
These interactions move a nested DUP out of a redex position.
(!&L{k0,k1}=k;f x)
------------------ APP-DUP
!&L{k0,k1}=k;(f x)
! &L{x0,x1} = (!$R{y0,y1}=Y;X); T
------------------------------------- DUP-DUP
! &L{x0,x1} = X; ! &L{y0,y1} = Y; T
They're only needed in implementations that store a DUP's body.
Another possible extension of IC is to include labels on lams/apps:
| LAM: "&" Label "λ" Name "." Term
| APP: "&" Label "(" Term " " Term ")"
The APP-LAM rule must, then, be extended with:
&L(&Rλx.bod arg)
----------------------- APP-LAM (if different labels)
x <- &Lλy.z
&Rλz.&L(body &R(arg y))
Consider the conventional Lambda Calculus, with pairs. It has two computational rules:
Lambda Application : (λx.body arg)
Pair Projection : let {a,b} = {fst,snd} in cont
When compiling the Lambda Calculus to Interaction Combinators:
lams and apps can be represented as constructor nodes (γ)
pars and lets can be represented as duplicator nodes (δ)
As such, lambda applications and pair projections are just annihilations:
Lambda Application Pair Projection
(λx.body arg) let {a,b} = {fst,snd} in cont
---------------- -----------------------------
x <- arg a <- fst
body b <- snd
cont
ret arg ret arg b a b a
| | | | | | | |
|___| | | |___| | |
app \ / \ / let \#/ \ /
| ==> \/ | ==> \/
| /\ | /\
lam /_\ / \ pair /#\ / \
| | | | | | | |
| | | | | | | |
x body x body fst snd fst snd
"The application of a lambda "The projection of a pair just
substitutes the lambda's var substitutes the projected vars
by the application's arg, and by each element of the pair, and
returns the lambda body." returns the continuation."
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:
Lambda Projection : let {a b} = (λx body) in cont
Pair Application : ({fst snd} arg)
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:
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."
This, in a way, completes the lambda calculus; i.e., previously "stuck" expressions now have a meaningful computation. That system, as written, is Turing complete, yet, it is very limited, since it isn't capable of cloning pairs, or cloning cloned lambdas. There is a simple way to greatly increase its expressivity, though: by decorating lets with labels, and upgrading the pair projection rule to:
let &i{a,b} = &j{fst,snd} in cont
---------------------------------
if i == j:
a <- fst
b <- snd
cont
else:
a <- &j{a0,a1}
b <- &j{b0,b1}
let &i{a0,a1} = fst in
let &i{b0,b1} = snd in
cont
That is, it may correspond to either an Interaction Combinator annihilation or
commutation, depending on the value of the labels &i and &j. This makes IC
capable of cloning pairs, cloning cloned lambdas, computing nested loops,
performing Church-encoded arithmetic up to exponentiation, expressing arbitrary
recursive functions such as the Y-combinators and so on. In other words, with
this simple extension, IC becomes extraordinarily powerful and expressive,
giving us a new foundation for symbolic computing, that is, in many ways, very
similar to the λ-Calculus, yet, with key differences that make it more
efficient in some senses, and capable of expressing new things (like call/cc,
O(1) queues, linear HOAS), but unable to express others (
$ claude mcp add Interaction-Calculus \
-- python -m otcore.mcp_server <graph>