一种基于交互网络的纯函数式编程语言。
/* 皮亚诺算数：2*2 */
Zero >> Add(#x, @y) => #x -> @y
Zero >> Mul(#x, @y) => #x -> Erase, @y <- Zero
S(#x) >> Add(#y, @w) =>
#x -> Add(#y, @z),
@w <- S(#z)
S(#x) >> Mul(#y, @w) =>
#y -> Dup(@u, @v),
#x -> Mul(#u, @z),
#z -> Add(#v, @w)
S(#x) >> Dup(@u, @v) => #x -> Dup(@y, @z), @u <- S(#z), @v <- S(#y)
Zero >> Dup(@x, @y) => @x <- Zero, @y <- Zero
S(#x) >> Erase => #x -> Erase
Zero >> Erase => _
Main <| #result |>
@two <- S(S(Zero))
#two -> Dup(@x, @y)
#x -> Mul(#y, @result)
保存为 example.zz，然后运行：
$ zamuza run example.zz --timing
S(S(S(S(Zero))))
[Reductions: 62, CPU time: 0.000125, R/s: 496000.000000]运行：
zamuza run <FILE> [--stack-size X] [--trace] [--timing]
编译：
zamuza compile <FILE> -o <OUTPUT> [--stack-size X] [--trace] [--timing]
编译为C语言：
zamuza compile <FILE> -o <OUTPUT> -f c [--stack-size X] [--trace] [--timing]
在Zamuza中，语法单元分为三种类型：变量、规约函数和构造函数。
变量是以 # 或 @ 开头的标识符，例如 #x 和 @x。这些标识符的前缀用于在编译时区分变量的用途。在运行时，#x和@x被视为同一个变量。
构造函数是函数表达式，例如 S(#x)。可以将构造函数视为接收一系列表达式作为参数，并返回一个"封装"了这些参数的结构。举个例子，我们可以使用 Cons(#x, #xs) 来表示列表构造，例如 Cons(1, Cons(2, Nil)) 表示列表 [1, 2]。Nil 是一个特殊的构造函数，它没有参数，表示空列表。
规约函数是具有形式类似 Add(#y, @w) 的函数。与构造函数不同，规约函数的表达式中包含像 @w 这样的变量，这些变量表示“计算结果”。例如，语句#x -> Add(#y, @w)的含义是变量 w 的值是 x 和 y 的和。
对于初次接触规约函数的人来说，这个概念可能有些奇怪，因为它的表达方式与计算含义有所不同。在常见的编程语言中，我们通常使用 Add(2, 3) 来表示 2+3 的结果。但是在 Zamuza 中，规约函数 Add(#y, @w) 实际上表示一个尚未完成的计算过程，它等待一个缺失的参数。因此，语句 #x -> Add(#y, @w) 将外部的一个变量输入到这个计算过程中，完成计算。
为了更容易理解程序，Zamuza中使用 # 和 @ 来区分变量的使用方式。以 #x 表示的变量是“输入型”变量，用于向外部提供值；而以 @x 表示的变量是“输出型”变量，用于接收一个值。构造函数的参数全部是输入型变量 #x，而规约函数的参数至少包含一个输出型变量 @x。
变量和函数组合形成表达式。例如，S(#x) 是一个表达式，Add(#x, @y) 也是一个表达式。表达式可以嵌套，例如 Add(S(#x), @y)。
表达式嵌套时，构造函数 S(#...) 可以出现在一切输入型变量 #x 可以出现的位置，例如，对于规约函数 Add(#x, @y)，表达式 Add(S(#x), @y) 是合法的，而 Add(#x, S(@y)) 是不合法的。
规约函数 Add(..@..) 可以出现在一切输出型变量 @y 可以出现的位置，例如，对于规约函数 Mul(#x, @y)，表达式 Mul(#x, Add(#y, @z)) 是合法的，而 Mul(Add(#x, @y), @z) 是不合法的。
两个表达式通过 -> 或 <- 相连，形成语句。例如，#x -> Add(#y, @z) 和 @z <- S(#x) 都是语句。语句的含义是对称的。也就是说，#x -> Add(#y, @z) 和 Add(#y, @z) <- #x 是完全等价的。
只有输入型变量 #x 和最外层是构造函数的表达式 S(#...) 可以出现在 -> 的左侧，而只有输出型变量 @y 和最外层是规约函数的表达式 Add(..@..) 可以出现在 -> 的右侧。例如，#x -> Add(#y, @z) 和 Add(#x, @y) <- S(#z) 都是合法的，而 S(#y) <- #x 是不合法的。
在 Zamuza 中，规则可以理解为函数定义，它们描述了规约函数的计算过程。
例如，在皮亚诺算数中，我们可以使用下面的规则来定义加法：
Zero >> Add(#x, @y) => #x -> @y
S(#x) >> Add(#y, @w) => #x -> Add(#y, @z), S(#z) -> @w
我们可以这样解释这两条规则：
- 如果要计算
0 + x，那么结果y获得x的值。 - 如果要计算
x' + y，其中x'是x的后继S(x)，那么我们可以先计算x + y，把结果存入z中，然后将z的后继S(z)赋给w。
一条规则分为两部分，左部分是规约函数遇到的计算情景，右部分是规约函数的计算过程。为了在左右两部分加以区分，左部分使用 >> 与 << 号，右部分使用 -> 与 <- 号。
规则的左部分是 >> 或 << 连接的两个表达式。这一部分中，两个表达式必须是一个规约函数和一个构造函数，而且表达式不能存在嵌套。例如，#x >> Add(#y, @z) => ... 和 S(S(#x)) >> Add(#y, @z) => ... 都是不合法的。
规则的右部分是若干条语句，语句之间使用 , 分隔，表示规约函数的计算过程。如果规则的右部分不需要任何计算，那么使用下划线 _ 来指定一个空的语句列表。例如，Zero >> Erase => _ 就是一个不需要任何计算的规则。
在规则之外，Zamuza 程序可以包含若干条顶级语句。顶级语句不属于任何规则，在程序开始执行时就被执行。
顶级语句以 :: 后接一条语句的形式出现。例如，:: #x -> Add(#y, @z) 是一条顶级语句，它的含义是在程序开始执行时，将 #x 的值传递给 Add(#y, @z)。
顶级语句之外，还有一条特殊的语法，它的格式是 $ = ...，用于定义程序的输出。等号右侧的值可以是输入型变量 #x，或者构造函数表达式 S(#...)。例如，$ = #x 表示程序的输出是 #x 的值，而 $ = S(#x) 表示程序的输出是 #x 的后继 S(#x)。
在 Zamuza 中，变量的使用有严格的限制。
在一条规则以内，变量必须恰好出现两次，并且满足输入输出守恒。也就是说，变量的两次出现要么一次在左部分，一次在右部分，并且输入/输出型相同，要么两次都在右部分，并且一次是输入型，另一次是输出型。例如，下面这些规则是不合法的：
S(#x) >> R(#y, @z) => #x -> @z /* 变量 y 只在左边出现一次 */
S(#x) >> R(#y, @x) => #y -> E /* 变量 x 在左边出现两次 */
Z >> R(#x, @y) => S(#z) -> @y, #x -> E /* 变量 z 只在右边出现一次 */
Z >> R(#x, @y) => #x -> @z, #y -> @z /* 变量 y, z 输入输出不守恒 */
Z >> R(#x, @y) => S(#z) -> @y, #x -> R(#x, @z) /* 变量 x 一共出现三次 */
而在全部的顶级语句之内，变量需要满足类似于一条规则右部分的限制，即：变量恰好出现两次，并且一次是输入型，一次是输出型。例如，下面的顶级语句是不合法的：
:: #x -> Add(#y, @z)
:: #y -> Add(#y, @w)
:: #y -> @z
$ = #w
/*
* 变量 x 只出现一次
* 变量 y 出现了四次
* 变量 y, z 的输入输出不守恒
*/
Zamuza 为变量使用设置严格的限制，是为了简化计算模型。Zamuza 的函数对应交互网络中的一个节点，而变量对应交互网络中的一条边。在上述限制下，变量可以作为图中的有向边，连接两个节点。
实际编程中，有时会出现规则中的变量只在左侧出现一次，或者在右侧出现多次的情况。这时，一般可以引入 Erase 与 Dup(@u, @v) 两个规约函数，分别用于删除变量和复制变量。此时，还需要定义构造函数与 Erase 和 Dup 的交互规则，以保证程序的正确运行。
更多 Zamuza 的例子，可以参考 examples 目录下的程序。
计算模型是对计算机的运行方式和组织结构的抽象描述。它可以看作是一种计算机的“理论模型”，它不关心计算机的具体实现，而只关心计算机的运行方式。
常见的计算模型有图灵机、λ演算、元胞自动机、抽象重写系统等。图灵机是应用最广泛的计算模型，也是与真实计算机最接近的计算模型。λ演算是一种基于函数的计算模型，它是许多函数式编程语言的理论基础。这些计算模型都是图灵完备的，换言之，它们都有相同的计算能力。
Zamuza 语言的计算模型是一种称为 交互网络 的特殊计算模型，它的计算能力与图灵机等其他计算模型相同，但可以方便地实现惰性求值等特性。
交互网络是一种图形化的计算模型，它可以看作由若干个交互器（Agents）和交互器间相连的边组成的特殊的图。交互网络的计算过程是通过对图上的一些特殊结构反复进行局部重写来实现的。
Zamuza 语言实际上是对交互网络的一种文本编码。上面的例子中，形如 #x -> Mul(#y, @result) 的每一项都表示交互网络中的一个子图，而 S(#x) >> Erase => #x -> Erase 这样的语句则表示对交互网络中的一条重写规则。
关于交互网络的更多信息，可以参考这篇文章。
抽象重写系统是一种形式化的计算模型，它将计算过程看作是对抽象语句的重写，这一过程类似于模式匹配。例如下面的 Haskell 代码：
qsort [] = []
qsort (x:xs) =
qsort (filter (< x) xs) ++ [x] ++ qsort (filter (>= x) xs)可以看作：当遇到左侧的表达式模式时，将其重写为右侧的表达式。
抽象重写系统提供了对“函数定义”这一概念的另一种视角，在抽象重写系统中，参数模式是自然存在而无需特殊处理的。虽然 Zamuza 的计算模型基于交互网络，但它的语法和心智模型十分接近一个抽象重写系统。
- 简单类型检查（输入/输出类型）
- 将 Dup 和 Erase 实现为内置函数
- 改进错误提示
- 编译器调试信息
- Lafont Y. Interaction combinators[J]. Information and Computation, 1997, 137(1): 69-101.
- Hassan A, Mackie I, Sato S. An implementation model for interaction nets[J]. arXiv preprint arXiv:1505.07164, 2015.
- Inpla: Interaction nets as a programming language. (GitHub)
- HVM: A massively parallel, optimal functional runtime in Rust. (GitHub)
本项目根据GNU通用公共许可证v3.0许可 - 有关详细信息，请参见LICENSE文件。