A programming language and model of computation that matches the optimal λ-calculus reduction algorithm perfectly.
A programming language and model of computation that matches the optimal λ-calculus reduction algorithm perfectly.
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:
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:
…
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:
…
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 (like λx.(x x)).
IC32 is implemented in portable C.
Each Term is represented as a 32-bit word, split into the following fields:
The tag field can be one of the following:
VAR: 0x00LAM: 0x01APP: 0x02ERA: 0x03NUM: 0x04SUC: 0x05SWI: 0x06TMP: 0x07SP0: 0x08SP1: 0x09SP2: 0x0ASP3: 0x0BSP4: 0x0CSP5: 0x0DSP6: 0x0ESP7: 0x0FCX0: 0x10CX1: 0x11CX2: 0x12CX3: 0x13CX4: 0x14CX5: 0x15CX6: 0x16CX7: 0x17CY0: 0x18CY1: 0x19CY2: 0x1ACY3: 0x1BCY4: 0x1CCY5: 0x1DCY6: 0x1ECY7: 0x1FThe val field depends on the variant:
VAR: points to a Lam node ({bod: Term}) or a substitution.LAM: points to a Lam node ({bod: Term}).APP: points to an App node ({fun: Term, arg: Term}).ERA: unused.NUM: stores an unsigned integer.SUC: points to a Suc node ({num: Term})SWI: points to a Swi node ({num: Term, ifZ: Term, ifS: Term})SP{L}: points to a Sup node ({lft: Term, rgt: Term}).CX{L}: points to a Dup node ({val: Term}) or a substitution.CY{L}: points to a Dup node ({val: Term}) or a substitution.A node is a consecutive block of its child terms. For example, the SUP term points to the memory location where its two child terms are stored.
Variable terms (VAR, CX{L}, and CY{L}) point to the location where the
substitution will be placed. As an optimization, that location is always the
location of the corresponding binder node (like a Lam or Dup). When the
interaction occurs, we replace the binder node by the substituted term, with the
'sub' bit set. Then, when we access it from a variable, we retrieve that term,
clearing the bit.
On SUPs and DUPs, the 'L' stands for the label of the corresponding node.
Note that there is no explicit DUP term. That's because Dup nodes are special:
they aren't part of the AST, and they don't store a body; they "float" on the
heap. In other words, λx. !&0{x0,x1}=x; &0{x0,x1} and !&0{x0,x1}=x; λx. &0{x0,x1} are both valid, and stored identically in memory. As such, the only
way to access a Dup node is via its bound variables, CX{L} and CY{L}.
Before the interaction, the Dup node stores just the duplicated value (no body).
After a collapse is triggered (when we access it via a CX{L} or CY{L}
variable), the first half of the duplicated term is returned, and the other half
is stored where the Dup node was, allowing the other variable to get it as a
substitution. For example, the DUP-SUP interaction could be implemented as:
…
The NUM, SUC and SWI terms extend the IC with unboxed unsigned integers.
On IC32, all bound variables have global range. For example, consider the term:
λt.((t x) λx.λy.y)
Here, the x variable appears before its binder, λx. Since runtime variables
must point to their bound λ's, linking them correctly requires caution. A way to
do it is to store two structures at parse-time:
Whenever we parse a name, we add the current location to the 'uses' array, and whenever we parse a binder (lams, lets, etc.), we add a variable term pointing to it to the 'vars' map. Then, once the parsing is done, we run iterate through the 'uses' array, and write, to each location, the corresponding term. Below are some example parsers using this strategy:
…
Converting IC32 terms to strings faces two challenges:
First, IC32 terms and nodes don't store variable names. As such, we must generate fresh, unique variable names during stringification, and maintain a mapping from each binder's memory location to its assigned name.
Second, on IC32, Dup nodes aren't part of the main program's AST. Instead, they "float" on the heap, and are only reachable via DP0 and DP1 variables. Because of that, by stringifying a term naively, Col nodes will be missing.
To solve these, we proceed as follows:
Before stringifying, we pass through the full term, and assign a id to each variable binder we find (on lam, let, dup, etc.)
We also register every Dup node we found, avoiding duplicates (remember the same dup node is pointed to by up to 2 variables, DP0 and DP1)
Then, to stringify the term, we first stringify each DUP node, and then we stringify the actual term. As such, the result will always be in the form:
! &{x0 x1} = t0
! &{x2 x3} = t1
! &{x4 x5} = t2
...
term
With no Dup nodes inside the ASTs of t0, t1, t2 ... and term.
No open issues yet, or sync has not completed.