The Abstract 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:
Like the Lambda Calculus, it can easily express algebraic datatypes and arbitrary recursive algorithms.
Like Turing Machines, it can be evaluated through simple, constant-time operations.
Unlike the Lambda Calculus (and like Rust), it does not require garbage-collection.
Unlike the Lambda Calculus, all intermediate steps of its optimal reduction correspond to terms.
Unlike the Lambda Calculus, terms can be reduced not only optimally, but efficiently (i.e., no oracles).
Unlike both, it is intrinsically parallel.
It is isomorphic to interaction combinators, a beautiful model of computation.
The syntax is obtained by simply extending the Lambda Calculus with pairs and let:
haskell
term ::=
| λx. term -- abstraction (affine function)
| (term term) -- application
| (term,term) -- superposition (pair)
| let (p,q) = term in term -- definition (let)
| x -- variable
Except variables are restricted to occur only once and are freed to occur globally (why?).
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.
```haskell -- Rule 0: lambda-application
f [x / a]
-- Rule 1: pair-projection
t [p / u] [q / v]
-- Rule 2: pair-application
let (x0,x1) = a in ((u x0),(v x1))
-- Rule 3: lambda-projection
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.
haskell
λ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)
haskell
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)
haskell
((λ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)
This is equivalent to:
```haskell data Nat = S Nat | Z
add : Nat -> Nat -> Nat add (S n) m = S (add n m) add Z m = m
main : Nat main = add (S (S (S Z))) (S (S Z)) ```