6 releases
Uses old Rust 2015
0.1.5 | Sep 18, 2018 |
---|---|
0.1.4 | Sep 18, 2018 |
0.1.0 | Aug 30, 2018 |
#419 in Programming languages
28 downloads per month
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, 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.
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 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
add (S n) m = S (add n m)
add Z m = m
main : Nat
main = add (S (S (S Z))) (S (S Z))