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 引擎）
- 許可證：公有領域