SIC

lambda

VictorTaelin/Symmetric-Interaction-Calculus: A programming language and model of computation that matches the optimal λ-calculus reduction algorithm perfectly.

最適なλ-calculusの削減アルゴリズムに完全に一致するプログラミング言語と計算モデル。

Reduction rules

$[a/b]$ はglobal substitution

• 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)]

Example: 2 + 3

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))

Full Reduction

Example: 2^(2^2)

Lambda Diagrams と言われるらしい.