Core Concepts

Relevant source files

• README.md
• haskell/main.hs
• haskell/main_debug.hs
• src/ic.h

This page explains the fundamental concepts of the Interaction Calculus (IC) and the theoretical underpinnings of the system implemented in this repository. It covers the core term representation, interaction rules, and evaluation strategies that form the basis of IC. For details about the implementation architecture, see Implementation Architecture.

What is Interaction Calculus?

The Interaction Calculus is a minimal term rewriting system inspired by Lambda Calculus, but with key differences that make it more efficient and expressive in certain ways:

1. Variables are affine: they can occur at most once in a term
2. Variables have global scope: they can be bound anywhere in the program
3. It features first-class superpositions and duplications

These properties allow IC to express concepts like continuations, linear HOAS, and mutable references, while also enabling optimal evaluation that can make some computations exponentially faster than in traditional Lambda Calculus.

Sources: README.md1-21

Term Structure

An IC term is defined by the following grammar:

Term ::=
  | VAR: Name                              // Variable
  | ERA: "*"                               // Erasure 
  | LAM: "λ" Name "." Term                 // Lambda
  | APP: "(" Term " " Term ")"             // Application
  | SUP: "&" Label "{" Term "," Term "}"   // Superposition
  | DUP: "!" "&" Label "{" Name "," Name "}" "=" Term ";" Term  // Duplication

Additionally, the C implementation extends this with numeric terms:

• NUM: Number
• SUC: Successor
• SWI: Switch (conditional)

Sources: README.md47-66 src/ic.h34-46 src/ic.h87-119

Term Representation Diagram

Sources: src/ic.h34-85 src/ic.h86-158

Core Interactions

The heart of Interaction Calculus lies in its interaction rules, which define how terms reduce when they meet. These rules govern the computational behavior of the system.

Application Interactions

Sources: README.md84-97 src/ic.h252-254

Duplication Interactions

Sources: README.md98-129 src/ic.h255-257

Numeric Interactions

The implementation extends IC with numeric operations:

Sources: src/ic.h260-266

Memory Management

The Interaction Calculus implementation uses a simple memory model consisting of a heap and a stack:

The heap stores terms, while the stack is used during evaluation. Memory allocation is handled through the ic_alloc function, which reserves space in the heap for terms.

Sources: src/ic.h165-180 src/ic.h196-210

Term Construction and Interaction

Terms are created and manipulated through a set of functions:

Function	Purpose	File Reference
ic_make_term	Create a term with given tag, label, value	src/ic.h217
ic_make_sup	Create a superposition	src/ic.h230
ic_make_co0/co1	Create duplication vars	src/ic.h231-232
ic_lam	Allocate a lambda node in heap	src/ic.h244
ic_app	Allocate an application node	src/ic.h245
ic_sup	Allocate a superposition node	src/ic.h246
ic_dup	Allocate a duplication node	src/ic.h247

These functions, combined with the interaction rules, form the foundation of computation in IC.

Sources: src/ic.h229-257

Evaluation Strategies

The system supports two main evaluation strategies:

1. Weak Head Normal Form (WHNF) - Reduces a term to its outermost constructor (similar to lazy evaluation)
2. Full Normal Form - Recursively normalizes all subterms (similar to eager evaluation)

The evaluation process applies the interaction rules recursively until no more reductions are possible or until the term is in the desired form.

Sources: README.md183-224 src/ic.h272-278

Substitution Mechanism

In IC, variable substitution is simpler than in traditional Lambda Calculus due to the affine nature of variables:

Since variables can only be used once, substitution can be implemented efficiently using a global substitution map or by setting a substitution bit in the term.

Sources: README.md134-138 src/ic.h221-227 src/ic.h63 src/ic.h136

Collapsing Optimization

The Interaction Calculus implementation includes optimization strategies, particularly "collapsing" to reduce the number of redexes in a term:

These rules allow for more efficient evaluation by eliminating superpositions and duplications before normalization.

Sources: README.md292-330

Uniqueness of Interaction Calculus

The Interaction Calculus is unique in its handling of previously "stuck" expressions in Lambda Calculus:

This "completion" of Lambda Calculus provides new computational capabilities while maintaining similar semantics.

Sources: README.md367-483

Implementation Details

The IC implementation in this repository is provided in multiple forms:

1. A C implementation with 32-bit and 64-bit variants
2. A Haskell reference implementation for learning purposes

The bit layout of terms differs between the 32-bit and 64-bit implementations:

Component	32-bit Layout	64-bit Layout
SUB bit	Bit 31	Bit 63
TAG	Bits 30-26 (5 bits)	Bits 62-56 (7 bits)
LAB	Part of TAG	Bits 55-40 (16 bits)
VAL	Bits 25-0 (26 bits)	Bits 39-0 (40 bits)

Sources: src/ic.h53-85 src/ic.h121-158

Summary

The Interaction Calculus provides a powerful computational model that combines the familiarity of Lambda Calculus with novel features like affine variables, global scope, and first-class superpositions and duplications. Its implementation in this repository showcases both theoretical elegance and practical efficiency.