6 releases
Uses old Rust 2015
0.1.5  Sep 18, 2018 

0.1.4  Sep 18, 2018 
0.1.0  Aug 30, 2018 
#842 in Development tools
140KB
634 lines
Abstract Calculus
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, constanttime operations.

Unlike the Lambda Calculus (and like Rust), it does not require garbagecollection.

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.
Syntax
The syntax is obtained by simply extending the Lambda Calculus with pairs
and let
:
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?).
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 constanttime operations.
 Rule 0: lambdaapplication
((λx.f) a)

f [x / a]
 Rule 1: pairprojection
let (p,q) = (u,v) in t

t [p / u] [q / v]
 Rule 2: pairapplication
((u,v) a)

let (x0,x1) = a
in ((u x0),(v x1))
 Rule 3: lambdaprojection
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: lambdaapplication and pairprojection (nothing new).
λu. λv. let (a,b) = (λx.x, λy.y) in (a u, b v)
 pairprojection
λu. λv. ((λx.x) u, (λy.y) v)
 lambdaapplication
λu. λv. ((λx.x) u, v)
 lambdaapplication
λu. λv. (u, v)
Example 1: using lambdaprojection to copy a function.
let (a,b) = λx.λy.λz.y in (a,b)
 lambdaprojection
let (a,b) = λy.λz.y in (λx0.a, λx1.b)
 lambdaprojection
let (a,b) = λz. (y0,y1) in (λx0.λy0.a, λx1.λy1.b)
 lambdaprojection
let (a,b) = (y0,y1) in (λx0.λy0.λz0.a, λx1.λy1.λz1.b)
 pairprojection
(λx0.λy0.λz0.y0, λx1.λy1.λz1.y1)
Example 2: demonstrating pairapplication.
((λx.x, λy.y) λt.t)
 pairapplication
let (a0,a1) = λt. t in ((λx.x) a0, (λy.y) a1)
 lambdaprojection
let (a0,a1) = (t0,t1) in ((λx.x) λt0.a0, (λy.y) λt1.a1)
 pairprojection
((λx.x) λt0.t0, (λy.y) λt1.t1)
 lambdaapplication
((λx.x) λt0.t0, λt1.t1)
 lambdaapplication
(λt0.t0, λt1.t1)
Example 3: 2 + 3.
This is equivalent to:
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))