Iota和Jot

在形式语言理论和计算机科学中，Iota（ι，发音如希腊字母 iota）和Jot（י，发音如希伯来字母 yodh）是两种极简的形式系统与编程语言。

这两个名称分别取自希腊语字母Ι（iota）和希伯来语字母Yodh（י/yodh）——分别是各自字母表中最小、最简单的字母，这一命名恰如其分地体现了这些语言的极简主义设计哲学。

它们的设计目标是比λ演算以及SKI组合子演算等更为人熟知的图灵完备系统更加简洁、更加基础。

因此，它们也被归类为图灵焦油坑（Turing tarpit）——即那些“在设计上尽可能小却仍然保持图灵完备性”的深奥的编程语言。

这两个系统仅使用两个基本符号，涉及两种基本操作。均由语言学教授克里斯·巴克于 2001 年设计创造。

Zot（2002 年）则是 Iota 的后继语言，通过引入延续传递风格（英文：Continuation-Passing Style, CPS）扩展了对输入/输出的支持能力。

## 历史与设计动机

克里斯·巴克设计这些语言的初衷是探索组合子逻辑中最简可能的完备基础。在组合子逻辑中，SKI组合子演算已经证明了仅需 S、K 和 I 三个组合子即可表达所有λ表达式。

巴克进一步追问：是否存在比 S 和 K 更加基础、更加简洁的表达方式？

这一追问引导他创造了 Iota——一种仅用单一基本组合子（通用 iota 组合子，标记为 ι）就能推导出 S、K、I 三个基本组合子的形式系统。

Jot 则在此基础上进一步简化表达方式，将程序表示为二进制串（即 0 和 1 的任意序列），从而为算法信息论中的哥德尔编号提供了一种自然的编码方案。

## 理论基础

### SKI 组合子演算的完备性

在组合子逻辑中，SKI组合子演算是一个经典的结果：任何 λ演算表达式都可以转化为仅使用以下三个组合子的形式：

- $$S = \lambda x.\lambda y.\lambda z. (x z) (y z)$$
- $$K = \lambda x.\lambda y. x$$
- $$I = \lambda x. x$$

这意味着 S、K、I 构成了一个完备集——它们足以表达所有可计算的函数。

### 通用 Iota 组合子

巴克的创新在于证明了仅需一个基本组合子即可推导出 S、K、I。他将这个通用组合子记为 ι（iota），其定义为：

$$\iota := \lambda f.((f\;S)\;K)$$

展开 λ 表达式，这一定义等价于：

$$\iota = \lambda f.\big(\big(f\;\lambda a.\lambda b.\lambda c.\big((a\;c)(b\;c)\big)\big)\;\lambda d.\lambda e.d\big)$$

#### 从 ι 推导 SKI

基于上述定义，可以推导出标准的 SKI 组合子：

$$\begin{aligned} I &= (\iota\;\iota) \\ K &= \big(\iota\;(\iota\;(\iota\;\iota))\big) \\ S &= \big(\iota\;(\iota\;(\iota\;(\iota\;\iota)))\big) \end{aligned}$$

这表明 ι 本身就是一个完备集——仅凭这一个组合子就能表达所有可计算函数。

## Iota 语言

Iota 是一种 LL(1) 形式语言，其语法使用前缀表示法来描述由通用 iota 组合子（ι）作为叶节点构成的二叉树，其中函数应用操作使用符号“0”表示。

### 语法定义

使用巴科斯范式（BNF）描述的 Iota 语法如下：

```abnf
iota = "1" / "0" iota iota
```

其中：

- "1" 表示基础组合子 ι
- "0" 表示函数应用

### 示例

二进制串｜解析为 SKI 表达式｜说明

1｜ι｜基础组合子

01｜(ι ι)｜ι 应用自身

((ι ι) (ι ι))｜两个 (ι ι) 的应用

(ι (ι (ι ι)))｜推导出 K 组合子的结构

((ι ι) (ι (ι (ι ι))))｜推导出 S 组合子的结构

### 程序终止性

值得注意的是，巴克证明了所有长度小于 27 个符号的 Iota 程序必定终止。这一性质使得 Iota 在研究停机问题和算法信息论时具有特殊的理论价值。

## Jot 语言

与 Iota 不同，Jot 采用一种更加极端的极简主义设计：它将程序直接定义为所有由 0 和 1 组成的正则语言。

### 语法定义

```abnf
jot = "" / jot "0" / jot "1"
; 即：空字符串，或任意 Jot 串后接 0 或 1
```

这意味着 Jot 程序可以是任意长度的二进制串，从空字符串（ε）到任意长度。

### 语义定义

Jot 的语义通过将二进制串转换为 SKI 表达式来赋予：

二进制串 w｜转换规则｜结果

ε（空串）｜I

w0｜$(([w]S)K)$｜将 w 应用于 S 和 K

w1｜$(S(K[w]))$｜将 S 应用到 K 和 w

其中 $[w]$ 表示字符串 w 的递归转换结果。

### 复合转换的示例

为了理解 Jot 的转换如何工作，以下推导空串后接五个 0 的转换过程：

$$\begin{aligned} [\varepsilon\;00000] &= (((((I\;S)K)S)K)S)K) \\ &= ([0000]\;((SK)K)) \\ &= ([000]\;((((SK)K)S)K)) \\ &= ([00]\;((((((SK)K)S)K)S)K)) \\ &= ([0]\;(((((((SK)K)S)K)S)K)S)K)) \\ &= (((((((SK)K)S)K)S)K)S)K) \end{aligned}$$

通过进一步展开，可以证明这最终等价于 $K$ 组合子。类似地，对空串后接六个 $1$ 后接三个 $0$ 的转换将产生 $S$ 组合子。

### 作为哥德尔编号

Jot 的设计使得任意 SKI 项都可以唯一的转换为一个二进制串，反之亦然。这使得 Jot 自然地成为算法的一种哥德尔编号系统——每个程序都有一个唯一的数字编码。

此外，Jot 揭示了 Iota 与更广泛二进制表示之间的深层联系：当 $[w] = \iota$ 时，$[w0] = (\iota[w])$。

## Zot 语言

Zot 是 Iota 系列的第三位成员，引入输入/输出机制。不同于前两者，Zot 采用延续传递风格来描述计算过程中的控制流。

### 语法定义

```abnf
zot = pot / ""
pot = iot / pot iot
iot = "0" / "1"
```

### 语义定义

在 Zot 中，每个基本符号产生一个延续：

符号｜产生的延续

1｜$\lambda c.\;L.\;L(\lambda l.\;R.\;R(\lambda r.\;c(lr)))$

0｜$\lambda c.\;c\;\iota$

计算从输入开始，通过一系列延续传递，最终产生输出。

### Positive Zot

Positive Zot 是 Zot 的一个变体，仅使用符号 1，通过不同的延续组合来表达计算。这一限制使得它成为研究组合子逻辑中"正交性"概念的工具。

## 与其他系统的比较

语言/系统｜符号数量｜基本操作｜表达能力

λ演算｜无限（变量）+ 3｜α转换、β约化、η转换｜图灵完备

SKI组合子演算｜3（S、K、I）｜应用｜图灵完备

Iota｜2（0、1）｜ι、函数应用｜图灵完备

Jot｜2（0、1）｜正则连接｜图灵完备

Unlambda｜2（S、K）｜函数应用｜图灵完备

Iota 和 Jot 的独特之处在于它们仅需两个符号即可达到图灵完备性，这在极简主义语言设计中是极为罕见的成就。

## 应用与影响

### 蔡廷常数研究

Iota 和 Jot 的极简特性使其成为研究蔡廷常数（Chaitin's constant）的理想工具。迈克尔·斯特伊（Michael Stay）在 2005 年的论文中证明了这些极简系统与算法信息论之间的深层联系。

### 深奥编程语言社区

作为图灵焦油坑的典型代表，Iota 和 Jot 在深奥的编程语言（Esoteric programming language，简称 esolang）社区中占有特殊地位。

它们证明了即使在极度受限的语法下，仍可实现完整的计算能力。

### 教育价值

这些语言被用于教授组合子逻辑和形式语义学的基本概念，因为它们的简洁性使得学生可以直观地理解从单个组合子构建完整计算系统的过程。

## 示例程序

### Iota 中的死循环

以下是一个永不终止的 Iota 程序：

```text
0101010101010101010101010101...（无限）
```

这是 (S(S(S...))) 形式的无限递归。

### Jot 中的无限循环

在 Jot 中，以下结构产生无限循环：

```text
1111111111111111...（无限个 1）
```

## 外部链接

- 克里斯·巴克主页（纽约大学）：https://web.archive.org/web/20181024173237/http://www.nyu.edu/projects/barker/Iota/
- Esolang Wiki 上的 Iota 词条
- Esolang Wiki 上的 Jot 词条
- Esolang Wiki 上的 Zot 词条
- Fundamenta Informaticae 上的相关论文：Very Simple Chaitin Machines for Concrete AIT（arXiv:cs/0508056）

## 延伸阅读

- Barendregt, H.P. (1984). The Lambda Calculus: Its Syntax and Semantics. North-Holland. ISBN 978-1848900660
- Hindley, J.R.; Seldin, J.P. (2008). Lambda-Calculus and Combinators: An Introduction. Cambridge University Press. ISBN 978-0521898850
- Chaitin, Gregory (1975). "A Theory of Program Size Formally Identical to Information Theory". Journal of the ACM, 22: 329–340.

## 基本资料

- 日语原文：Iota、Jot 与 Zot
- 编程范型：形式语言理论 · 图灵焦油坑 · 深奥的编程语言
- 语言家族：组合子逻辑
- 设计者：克里斯·巴克 (语言学家)
- 开发者：克里斯·巴克
- 发行日期：2001年
- yes：2001
- yes：2001年
- 类型系统：无类型
- 软件实现：Scheme 解释器、JavaScript
- dialects：Iota、Jot、Zot、Positive Zot
- 平台：跨平台（Scheme 解释器 / JavaScript 引擎）
- 许可证：公有领域