# MaiaVictor/Symmetric-Interaction-Calculus

A programming language and model of computation that matches the optimal λ-calculus reduction algorithm perfectly.
Latest commit 1e74be3 Oct 23, 2018
Type Name Latest commit message Commit time
Failed to load latest commit information.
src
.gitignore Aug 30, 2018
Cargo.lock Oct 23, 2018
Cargo.toml Oct 23, 2018
drawing.jpeg Aug 30, 2018

# Symmetric Interaction Calculus

The Symmetric Interaction Calculus is a minimal programming language and model of computation obtained by slightly modifying the Lambda Calculus so that it matches perfectly the abstract part of Lamping's optimal reduction algorithm. Characteristics:

1. Like the Lambda Calculus, it can easily express algebraic datatypes and arbitrary recursive algorithms.

2. Like Turing Machines, it can be evaluated through simple, constant-time operations.

3. Unlike the Lambda Calculus (and like Rust), it does not require garbage-collection.

4. Unlike the Lambda Calculus, all intermediate steps of its optimal reduction correspond to terms.

5. Unlike the Lambda Calculus, terms can be reduced not only optimally, but efficiently (i.e., no oracles).

6. Unlike both, it is intrinsically parallel.

7. It is isomorphic to symmetric interaction combinators, a beautiful model of computation.

## Syntax

The syntax is obtained by simply extending the Lambda Calculus with `pairs` and `let`:

```term ::=
| λx. term                 -- abstraction
| (term term)              -- application
| (term,term)              -- pair
| let (p,q) = term in term -- definition
| x                        -- variable```

Except variables are restricted to occur only once and are freed to occur globally (why?).

## Reduction rules

There are 4 reduction rules. Two of them are usual: the application of a lambda, and the projection of a pair. The other two deal with the previously unspecified cases: "applying a pair" and "projecting a lambda". The first performs a parallel application, and the second performs an incremental duplication. All of them are constant-time operations.

```-- Rule 0: lambda-application

((λx.f) a)
----------
f [x / a]

-- Rule 1: pair-projection

let (p,q) = (u,v) in t
----------------------
t [p / u] [q / v]

-- Rule 2: pair-application

((u,v) a)
----------------
let (x0,x1) = a
in ((u x0),(v x1))

-- Rule 3: lambda-projection

let (p,q) = (λx.f) in t
-----------------------
let (p,q) = f in t
[p / λx0.p]
[q / λx1.q]
[x / (x0,x1)]```

Here, `[a / b]` stands for a global substitution of the occurrence of `a` by `b`, and `x0`, `x1` are fresh variables. I've used additional parenthesis around lambdas to make the reading clearer.

## Examples

### Example 0: lambda-application and pair-projection (nothing new).

```λu. λv. let (a,b) = (λx.x, λy.y) in (a u, b v)
----------------------------------------------  pair-projection
λu. λv. ((λx.x) u, (λy.y) v)
---------------------------- lambda-application
λu. λv. ((λx.x) u, v)
--------------------- lambda-application
λu. λv. (u, v)```

### Example 1: using lambda-projection to copy a function.

```let (a,b) = λx.λy.λz.y in (a,b)
------------------------------- lambda-projection
let (a,b) = λy.λz.y in (λx0.a, λx1.b)
--------------------------------------- lambda-projection
let (a,b) = λz. (y0,y1) in (λx0.λy0.a, λx1.λy1.b)
-------------------------------------------------- lambda-projection
let (a,b) = (y0,y1) in (λx0.λy0.λz0.a, λx1.λy1.λz1.b)
----------------------------------------------------- pair-projection
(λx0.λy0.λz0.y0, λx1.λy1.λz1.y1)```

### Example 2: demonstrating pair-application.

```((λx.x, λy.y) λt.t)
------------------- pair-application
let (a0,a1) = λt. t in ((λx.x) a0, (λy.y) a1)
--------------------------------------------- lambda-projection
let (a0,a1) = (t0,t1) in ((λx.x) λt0.a0, (λy.y) λt1.a1)
-------------------------------------------------------  pair-projection
((λx.x) λt0.t0, (λy.y) λt1.t1)
------------------------------- lambda-application
((λx.x) λt0.t0, λt1.t1)
----------------------- lambda-application
(λt0.t0, λt1.t1)```

### Example 3: 2 + 3.

This is equivalent to:

```data Nat = S Nat | Z

add : Nat -> Nat -> Nat

main : Nat
main = add (S (S (S Z))) (S (S Z))```

Full reduction.

### Example 4: applying not 8 times to True.

Full reduction.

Here is a handwritten reduction of 2^(2^2).

You can’t perform that action at this time.