月刊やさしいTaPL：「項の名無し表現」の気持ちをPythonと無限のポエムで理解する（型システム入門６章）

# 概要

TaPLと略されるTypes and Programming Languagesという本があります。
この本の６章が少し難しいという話があったので読んでみたところ、確かにある程度数学に慣れていないと難しそうな記述があったので、その気持を簡単に理解することに努めます。
手を動かさないと理解が進まないだろうと思ったので、実際に計算もします。

# 名無し表現のモチベーションと、この章の目的

５章以前で、（型無しの）ラムダ計算を導入しているのですが、ラムダ計算を用いて実際に新しい式を作ろうとすると、変数名の衝突が問題になる場合があります。たとえば、
$\sf{\lambda x. \lambda x. x}$
こんな書き方をしてしまうと、右端の$\sf x$をどう扱うべきかという問題が生じます。これは最後の束縛が有効というような定義の仕方をすれば一意に解釈ができますが、しかし人間にとって易しくありません。
これを避けるための書き換えのルールなどはいくつかありますが、そのうちの「名無し表現」によって項を表現することで変数束縛を明快な形に書き換える、という方法があります。
端的に言うと、"最初の束縛変数"はすべて0として、その次の束縛変数はすべて1、その次の束縛変数はすべて2、...という定め方をすることで、束縛変数の名前の明示をしないようにする、ということになります。
先の例であれば、
$\sf{\lambda . \lambda . 0}$と書くと"内側"=右側の$\lambda$に対応する変数を返すような関数に意味的に対応していて、
$\sf{\lambda . \lambda . 1}$と書くと"外側"=左側の$\lambda$に対応する変数を返すような関数に意味的に対応している、
ということになります。（この関数は、2変数関数のカリー化と思えば、$\sf (y,x)$を引数として受けて$\sf x$を返したり$\sf y$を返したりする関数と思うことができます。）

このような記法を導入した場合に、**【（ラムダ）抽象に対して（関数）適用を行う形の式の書き換えをする】という最も基本的な規則であるβ簡約がどのように表されるのか**、という事を説明します。
ただし、β簡約をいきなり定義する前に、項の定義、シフトの定義、代入の定義を経て、それからβ簡約の定義を行う構成になっています。

この章においては、良くも悪くもこの本の特徴である**微妙に厳密ではないが、しかし工学的な本としては十分厳密**というものが非常に色濃く出ていると思いました。そのあたり、随所で解説をしながら読み進めます。

# 6.1.2. 定義（項）

$n$を$0$以上の整数として、以下の条件を満たす最小の集合族$\mathcal{T}=\lbrace \mathcal{T_0, T_1, T_2, \cdots} \rbrace $を項と呼ぶ。

1. $0\leq \sf{k} < n$のとき、$\sf{k} \in \mathcal{T_n}$.
2. $\sf{t_1} \in \mathcal{T_n}$かつ$n>0$のとき、$\lambda.\sf{t_1} \in \mathcal{T_{n-1}}$.
3. $\sf{t_1,t_2} \in \mathcal{T_n}$のとき、$(\sf{t_1,t_2}) \in \mathcal{T_n}$.

## 定義の解説

以下、この3行を少し丁寧に解説します。ただし、最小性の説明は数学的に詳しく気になる人だけでよいと思います。本質的なのは、この定義によって帰納的にどのような集合（族）が定まるのか？ということです。

### 集合族とは

原文では、

> Note that this is a standard inductive definition, except that what we are defining is a family of sets indexed by numbers, rather than a single set.

と書いてありますが、これがある意味で曲者で、まず集合族とは何か？という話になります。
集合族とは、**この場面においては**早い話が単純に集合の集合であって、集合たちを添え字付けたものになります。今回の定義においては、$\mathcal{T_0,T_1,T_2,\cdots}$というのはそれぞれ集合だということですね。

### 最小性（１）：一般には複数存在し得ること

この$\mathcal{T_0,T_1,T_2,\cdots}$たちが満たす関係式というのが1,2,3になっていて、かつ、**これらを満たす最小の集合である**ということを要請しています。
というのも、例えば…いま最小のものたちを$\mathcal{T} = \mathcal{T_0,T_1,T_2,\cdots}$とするとき、適当な自然数$m$を取ってきて、以下のようにして新しい集合族$\mathcal{S}$を構成します。

- $n\leq m$ではすべて$\mathcal{S_n} = \mathcal{T_m}$
- $n > m$ではすべて$\mathcal{S_n} = \mathcal{T_n}$

そうすると、実はこの$\mathcal{S}$も最小性以外の$\mathcal{T}$の条件を満たすことが（適当な計算によって）わかります。従って、最小性以外の条件だけでは、そのような集合族は複数存在し得るのですね。

### 最小性（２）：そもそも最小の集合族の存在が自明でないこと

ここで、一層難しいことを言うと、そもそも"最小"という条件を満たすものが一意に定まるか否かは、実は自明なことではありません。というのも、一般に集合$A$と集合$B$には$A \subset B$でも$B \subset A$でも（$A = B$でも）ない場合があって、そのような場合には比較ができず、この２つの集合の間に"最小"という概念を定めることは通常はできないからです。
従って、"最小の集合族"という言い回しも、実は全く自明ではなくて、そもそもそのようなものが存在するのか？というところから考える必要があります。もちろん実際には存在するのですが、それを示すには、上記の最小性以外の条件を満たす"集合"$\lbrace \mathcal{U} \\ | \\ 各条件を満たす \rbrace$を考えたときに、$\cap \mathcal{U}=\lbrace \mathcal{\cap U_0, \cap U_1, \cap U_2, \cdots} \rbrace$が同じ条件を満たすことを言えばよいです。ここで、$\mathcal{\cap U_n}$というのは、取り得る$\mathcal{U_n}$たちすべてについての共通部分を意味します。（通常は、これは添字集合$I$を用いて各$\mathcal{U_n}$を$\mathcal{U_{n,i}}$などと表しておいて、$\cap_{i \in I} \mathcal{U_{n,i}}$などと書きます。）

というのも、今回の場合は1.の条件により条件を満たす集合が空でないことが保証されているため、最小性以外のすべての条件を満たす集合についての共通部分をとれば、**そのすべての集合についての共通部分が条件を満たすならば**自然にそれが（空でない）最小の集合となるからです。

さて、1の条件については自明ですが、2については
$\sf{t_1} \in \cap \mathcal{U_n}$かつ$n>0$のとき、$\lambda.\sf{t_1} \in \mathcal{U}$が任意の$\mathcal{U}$について言えるので
$\sf{t_1} \in \cap \mathcal{U_{n-1}}$
といえます。
3についても2と同様なので、従って$\cap \mathcal{U}$も同様の条件を満たすことがわかったので、最小性以外の条件を満たすものたちについての共通部分を取ると、ある空でない最小の集合（族）が定まることがわかりました。

※**注意：**もともとは2つの要素の共通部分で書いていたのですが、一般の命題については$\mathcal{U_{n,i}\cap U_{n,j}}$が条件を満たすからといって$\cap \mathcal{U_n}$が条件を満たすと言うことはできないので、結局、無限を用いた記法に改めました。一般論については、例えば閉集合$[0,1]=\lbrace x \\ | \\ 0 \leq x \leq 1 \rbrace $を含む**開集合（開区間：境界が等号ではなく不等号になっているやつ）**の族などをとると、個々の開集合の共通部分は開集合になりますが、その開集合族の共通部分は[0,1]で閉です。

### 実際の項の形

さて、上記の項の定義は「含まれない項」についての定義は特にないため、3つの条件が矛盾するようなことはなく、従って定義によって空でない集合族が定まることはわかりました。
一方で、具体的な形は何も分かっていません。
この定義は帰納的な定義となっているので、具体的に書き下すことにしましょう。
ただ、その前に、$\mathcal{T_0}$は無限集合である（要素が無限に存在する集合である）ということに注意をしておきます。実際、3の条件によって、1つでも要素が存在すれば$\sf{(t_1(t_1(t_1 \cdots t_1 )))}$という形の要素をいくらでも作れるので、要素は無限に存在します。

### よくない書き下し例

```python3:bad_example.py
from itertools import product

terms = []
n = 0
while n <= 4:
    # rule 1
    current = [str(j) for j in range(n)]
    # rule 2
    if n > 0:
        child = ['λ.' + c for c in current]
        terms[n - 1] += child
    # rule 3
    current += ['(' + a + ' ' + b + ')' for a, b in product(current, current)]
    terms.append(current)
    n += 1

print('\n'.join([', '.join(t) for t in terms]))
```

```
λ.0
0, (0 0), λ.0, λ.1
0, 1, (0 0), (0 1), (1 0), (1 1), λ.0, λ.1, λ.2
0, 1, 2, (0 0), (0 1), (0 2), (1 0), (1 1), (1 2), (2 0), (2 1), (2 2), λ.0, λ.1, λ.2, λ.3
0, 1, 2, 3, (0 0), (0 1), (0 2), (0 3), (1 0), (1 1), (1 2), (1 3), (2 0), (2 1), (2 2), (2 3), (3 0), (3 1), (3 2), (3 3), λ.0, λ.1, λ.2, λ.3, λ.4
```

これは、**とてもよくない例**です。
$\mathcal{T_n}$たちは無限に存在するので、途中までの書き下し例としてはこれで良いようにも見えますが、例えば$\lambda.\lambda.0$というようなものは出てきません。このやり方で出てくるのは、$\lambda$がたかだか一つの項だけです。
このような書き出し方を例えていうと、分数を列挙するときに、$1/2,1/3,1/4,1/5,\cdots $と列挙しているようなものですね。たしかに分数を列挙してはいますが、いつまでたっても$2/3$などは出てこないでしょうし、仮分数のように1より大きな分数の存在を知ることもできません。つまり、書いて属性を理解しようとしたつもりなのに、何も理解できない酷い例ですね。
では、どのように改善すればよいのでしょうか。

### ましな書き下し例

さきほどの分数についての~~ポエム~~たとえに少しヒントがあります。（正の）分数の場合、以下のようにすると、すべての分数がどこかには出てくるような書き下し方になります：
$1/1,1/2,2/1,1/3,2/2,3/1,1/4,2/3,3/2,4/1,\cdots$
これは一つの方向に対して伸ばしてしまわずに、分子分母の合計が2になる、3になる、4になる、…という条件で書いているのですね。
これと同じようなことを考えてみると…、例えば、文字数によって区切るという方法があります。
2のルールも、3のルールも、必ず項を構成する文字数は増加するので、文字数が一定以下の項はある程度制限ができるはずです。ただ、1のルールによって、任意の$n>0$に対して$\sf{1}\in \mathcal{T_n}$なので、単純な文字数だけではなく、$n$の深さも考慮するようにしてみます。
そうすると、少しマシな書き下し方ができます。

```python3:example.py
from itertools import product


class CostBaseTerm():
    index = 0
    cost = 0
    literal = ''
    
    def __init__(self, index, cost, literal):
        self.index = index
        self.cost = cost
        self.literal = literal


def first_rule(index, num):
    return CostBaseTerm(index, index, str(num))


def second_rule(term):
    return CostBaseTerm(term.index - 1, term.cost + 1, 'λ.' + term.literal)


def third_rule(term_a, term_b):
    return CostBaseTerm(
        term_a.index, term_a.cost + term_b.cost,
        '(' + term_a.literal + ' ' + term_b.literal + ')')


terms = []
cost = 0
while cost <= 6:
    terms.append([first_rule(cost, i) for i in range(cost)])
    for i in range(cost):
        if i > 0:
            for term in terms[i]:
                if term.cost == cost - 1:
                    terms[i - 1].append(second_rule(term))
        for term_a, term_b in product(terms[i], terms[i]):
            if term_a.cost + term_b.cost == cost:
                terms[i].append(third_rule(term_a, term_b))
    cost += 1

print('\n'.join([', '.join([t.literal for t in part_term]) for part_term in terms[:1]]))
```

printのところで、$\mathcal{T_0}$に限定しています。出力結果に適当に改行を入れると以下のようになります。

```
λ.0, λ.(0 0), (λ.0 λ.0), λ.(0 (0 0)), λ.((0 0) 0), λ.λ.0, λ.λ.1,
(λ.0 λ.(0 0)), (λ.(0 0) λ.0), λ.(0 (0 (0 0))), λ.(0 ((0 0) 0)),
λ.(0 λ.0), λ.(0 λ.1), λ.((0 0) (0 0)), λ.((0 (0 0)) 0), λ.(((0 0) 0) 0),
λ.(λ.0 0), λ.(λ.1 0), (λ.0 (λ.0 λ.0)), (λ.0 λ.(0 (0 0))), (λ.0 λ.((0 0) 0)),
(λ.0 λ.λ.0), (λ.0 λ.λ.1), (λ.(0 0) λ.(0 0)), ((λ.0 λ.0) λ.0), (λ.(0 (0 0)) λ.0), (λ.((0 0) 0) λ.0), (λ.λ.0 λ.0), (λ.λ.1 λ.0), λ.(0 (0 (0 (0 0)))),
λ.(0 (0 ((0 0) 0))), λ.(0 (0 λ.0)), λ.(0 (0 λ.1)), λ.(0 ((0 0) (0 0))),
λ.(0 ((0 (0 0)) 0)), λ.(0 (((0 0) 0) 0)), λ.(0 (λ.0 0)), λ.(0 (λ.1 0)),
λ.((0 0) (0 (0 0))), λ.((0 0) ((0 0) 0)), λ.((0 0) λ.0), λ.((0 0) λ.1),
λ.((0 (0 0)) (0 0)), λ.(((0 0) 0) (0 0)), λ.(λ.0 (0 0)), λ.(λ.1 (0 0)),
λ.((0 (0 (0 0))) 0), λ.((0 ((0 0) 0)) 0), λ.((0 λ.0) 0), λ.((0 λ.1) 0),
λ.(((0 0) (0 0)) 0), λ.(((0 (0 0)) 0) 0), λ.((((0 0) 0) 0) 0), λ.((λ.0 0) 0),
λ.((λ.1 0) 0),
λ.λ.(0 0), λ.λ.(0 1), λ.λ.(1 0), λ.λ.(1 1), λ.λ.λ.0, λ.λ.λ.1, λ.λ.λ.2
```

$\mathcal{T_0}$の中にも2が出てきます。これは、$\mathcal{T_3}$に含まれる2に対して2つ目のルールを3回適用した結果の項です。
帰納的な定義だけだとなかなか把握することが難しい場合もありますが、このように書き下してみると、実は$\mathcal{T_0}$の中には自由変数が居ないということがわかります。
同じ深さで$\mathcal{T_1}$を見てみると、

```
..., λ.λ.2, ..., (0 λ.λ.2), ..., (λ.λ.2 0)
```

となっていて、実はそれ以外の変数はすべて束縛されています。
実は、TaPLの本文には

> The elements of Tn are terms with *at most* n free variables, numbered between 0 and n − 1: a given element of Tn need not have free variables with all these numbers, or indeed any free variables at all.

と書いてあるのですが、確かにそうなっていそうですね。
というのは、実際、2の条件（操作）では自由変数が一つ減り、3の条件（操作）では自由変数の数は変わらないので、1で定まる自由変数が各$\mathcal{T_n}$の自由変数の上限を定めているのでした。
このようなことは、ある程度数学に慣れていれば自然に発想されると思いますが、実際には手を動かさないとわかりにくいと思います。ただ、手を動かすといっても、この帰納的な定義はそもそも無限集合を扱っているので、下手な触り方をすると間違った方向に理解が進んでしまいます。
そこで、今回は分数を列挙する時のうまいやり方との対比を用いて、重み付けをすることによって少しマシな列挙方法を用いて、実際の項に触れるという事をしました。

そもそも6章を読むには、以下の知識が前提だったので、この記事単独でもある程度読めるように内容を示しておきます。

# 5.3.1 定義（（名前付きの・名無しでない）項）

可算集合$\mathcal{V}$が与えられたとき、**$\mathcal{V}$を変数集合とする名前付きの項$\mathcal{T'}$**とは、以下で（帰納的に）定まる最小の集合とする。

1. 任意の$\sf{x \in \mathcal{V}}$に対して$\sf{x \in \mathcal{T'}}$：この形の項を変数と呼ぶ。
2. 任意の$\sf{x \in \mathcal{V}}, \sf{t} \in \mathcal{T'}$に対して$\sf{\lambda x.t} \in \mathcal{T'}$：この形の項を（ラムダ）抽象と呼ぶ。
3. 任意の$\sf{t_1, t_2} \in \mathcal{T'}$に対して$\sf{(t_1 t_2) \in \mathcal{T'}}$：この形の項を（関数）適用と呼ぶ。

※注：本書では単に$\mathcal{T}$となっていましたが、いまは名無し表現の定義との混同を避けるためにあえて$\mathcal{T'}$としています。

例によって最小性の確認などが必要ですが、名無しの項の場合と同様に考えれば自明なので省略します。
この、変数集合を用いて定まる項と、名無しの項の間の対応ルールの考え方として、コンテキストと呼ばれるものがあります。

# 6.1.3 定義（命名コンテキスト）

$\mathcal{V}$を変数集合とする。$\sf{x_0, \cdots, x_n \in \mathcal{V}}$に対して、**命名コンテキスト**$\Gamma = \sf{x_n, \cdots, x_0}$が与えられたときは、各Brujin添字$i$に対して$\sf{x_i}$を割り当てる。ラムダ抽象の結合が右側から行われることと合わせて、右側の変数から順に$0,1,2,\cdots$と割り当てることに注意しよう。$\Gamma$に登場する変数の集合を$\mathrm{dom}\Gamma$で表す。

要するに0から順番に適当な変数を割り当てるという、かなり普通のことを言っています。

# 6.2.1 定義（シフト）

$c,d$を$0$を含む自然数とする。項$\sf{t}$の**$c$を切片とする$d-$シフト**とは、以下のように定まる項のことで、これを$\uparrow^d_c$と書く。

$$\uparrow^d_c({\sf k}) = \begin{cases} {\sf k} && \mathrm{if} \\ {\sf k} < c \\\ {\sf k} + d && \mathrm{if} \\ {\sf k} \geq c \end{cases} $$

$$\uparrow^d_c(\lambda .{\sf t_1}) = \lambda .\uparrow^d_{c+1}({\sf t_1}) $$

$$\uparrow^d_c({\sf t_1 \\ t_2}) = (\uparrow^d_{c}({\sf t_1}) \\ \uparrow^d_{c}({\sf t_2})) $$

特に$\uparrow^d_0({\sf k})=\uparrow^d({\sf k})$と書くことがある。

これは定義の通りですが、帰納的な定義のそれぞれに対しての定義が与えられている、ということに注意することぐらいでしょうか。こちらの操作の場合は、書き下しとは違って、具体的な項が与えられた時の計算について順序などを深く考えずに簡単に行うことができます。
そのような点においては、帰納的な定義というのは非常に扱いやすい性質もあるものなんですね。

```python3:shift.py
def shift(d, c, t):
    if t[0] == 'λ':
        return 'λ.' + shift(d, c+1, t[2:])
    if t[0] == '(':
        pos = nest = 1
        while nest > 0:
            ch = t[pos]
            if ch == '(':
                nest += 1
            elif ch == ')':
                nest -= 1
            elif ch == ' ' and nest == 1:
                nest = 0
            pos += 1
        return '(' + shift(d, c, t[1:pos - 1]) + ' ' + shift(d, c, t[pos:-1]) + ')'
    n = int(t)
    return str(n) if n < c else str(n + d)

print(shift(2, 0, '(λ.0 (λ.0 λ.0))'))
print(shift(3, 0, '(0 (0 λ.1))'))
```

```
(λ.0 (λ.0 λ.0))
(3 (3 λ.4))
```

**注意：**$d$は負の整数であっても"形式的には"定まる場合がある。特に、対象となる項が自由変数として$-d$より小さい変数を含まない場合には、$d$が負の整数の場合にもうまく定まる。

本書では、$d$の範囲を明示せずに直感的になんとなく定義をしていますが、β簡約を明示する際に$d=-1$としています。これも、任意の項に対して正しく動くものではないのですが、しかしこの記法でも"その場合に限れば"問題ありません。（ということを示す練習問題が付いています。）

# 6.2.4 定義（代入）

${\sf t}$における変数${\sf j}$への${\sf s}$の**代入**${\sf \[ j \mapsto s \]}$を次で定める。

$${\sf \[ j \mapsto s \] \\ k} = \begin{cases} {\sf s} \\ \mathrm{if} \\ {\sf k = j} \\\ {\sf k} \\ \mathrm{otherwise} \end{cases}$$

$${\sf \[ j \mapsto s \] \\ \lambda .t_1} = {\sf \lambda . \[ j+1 \mapsto \uparrow ^1 s \] \\ t_1 }$$

$${\sf \[ j \mapsto s \] \\ ( t_1 \\ t_2 ) } = {\sf (\[ j \mapsto s \] \\ t_1 \\ \[ j \mapsto s \] \\ t_2)  } $$

この定義は、先ほどと同じパターンではあるものの、「代入」という言葉を使っているという点において、少し特殊です。
というのも、代入という言葉を目にすると、多くの人は既に代入というものをなんとなく知っているはずなので、それからの類推や対比で理解をしようとするのが自然です。
つまり、これは定義ではあるものの、一方で**それを代入と呼ぶという主張でもある**のですね。数学的な意味では差は無いですが、人間が読んで理解をする上では、じつは主張になっている定義が存在するということは重要なポイントと思います。
説明が長くなりましたが、では、確かにそれが代入と呼び表せるような内容なのかを確認してみましょう。
1つ目、3つ目はさもありなんという定義かと思います。2つ目は、${\sf s}$の自由変数の添字を1つずつシフトして${\sf j+1}$への代入という事になっています。
注意点としては、この操作では${\sf t_1}$の自由変数はシフトしないので、代入対象の変数が0であっても、元の式の0以外の自由変数が変化する場合があります(というかλが存在する場合で実際に置換が発生する場合は確実にそう)。代入対象の変数は、あくまでも**何番目の自由変数に代入するか**という事を意味していて、単純な置き換えではないことに注意しておきます。

こちらも例によって簡単に計算をすることができます。

```python3:substitution.py
def substitution(j, s, t):
    if t[0] == 'λ':
        return 'λ.' + substitution(j+1, shift(1,0,s), t[2:])
    if t[0] == '(':
        pos = nest = 1
        while nest > 0:
            ch = t[pos]
            if ch == '(':
                nest += 1
            elif ch == ')':
                nest -= 1
            elif ch == ' ' and nest == 1:
                nest = 0
            pos += 1
        return '(' + substitution(j, s, t[1:pos - 1]) + ' ' + substitution(j, s, t[pos:-1]) + ')'
    return s if int(t) == j else t

print(substitution(1, 'λ.1', '(λ.0 (λ.0 λ.0))'))
print(substitution(0, 'λ.0', '(0 (0 λ.1))'))
print(substitution(0, 'λ.3', 'λ.1'))
print(substitution(0, 'λ.3', 'λ.λ.1'))
print(substitution(1, 'λ.3', 'λ.λ.1'))
```

```
(λ.0 (λ.0 λ.0))
(λ.0 (λ.0 λ.λ.0))
λ.λ.4
λ.λ.1
λ.λ.1
```

ここまで書いてから、Recommended ★★★となっているExcerciseに以下のような記述があることに気づきました：

> The definition of substitution on nameless terms should agree with our informal definition of substitution on ordinary terms. (1) What theorem needs to be proved to justify this correspondence rigorously? (2) Prove it.

まさに、上で述べた通り、この定義の主張としての性質を踏まえた上で、自然な定義であるという事を確認するような練習問題になっているのでした。

# β簡約のポイント

β簡約は、抽象＋適用の形を、代入した形に置き換える操作のことを指すのでした。
つまり、（必ずしも名無しでない項に対して）

$$\sf (\lambda x.t \\ v) \to [x \mapsto v]t$$

という置き換えでした。
この置き換えにおいて、名無し表現の場合には、"変数番号のずれ"が問題となります。
例えば、$((\lambda .(1 \\ 0)) \\ \lambda .0)$というものがあったとして、これに簡約を適用するとき、次の２つのうちのいずれかが得られそうに思えます。

$$(1 \\ \lambda.0)$$

$$(0 \\ \lambda.0)$$

というのは、本当に素朴に代入をするだけとすると、$\lambda .(1 \\ 0)$という関数の引数0に対して$\lambda.0$を代入するので$1 \\ \lambda.0$になりそうですが、そうすると、この外にさらに$\lambda.$が付いている場合の挙動が理想的なものにならなくなってしまいます。
実際、例えばこれが$\lambda.((\lambda .(1 \\ 0)) \\ \lambda .0)$であったとすると、ここでいう1というのは外側の$\lambda$に対応していますが、もし内側の$\lambda$がβ簡約によってなくなってしまった場合には、束縛対象が0になるので、添字にずれが発生してしまうわけです。
そこで、$\lambda$を減らすような場合には、添字をきちんと戻す必要がある、ということになります。これを考慮して、以下のようなβ簡約の定義を得ることができます。

# 定義（β簡約）

$\sf t, v$を項とするとき、$(\sf \lambda .t \\ v)$に対する**β簡約**を次で定める。

$$\sf (\lambda .t \\ v) \to \uparrow^{-1}([0 \mapsto \uparrow^1 v]t)$$

これは、$\sf t$に出てくる変数0に対して、$\sf v$を代入してからシフトを1つ戻す（-1シフトする）ということなのですが、このとき$\sf v$に自由変数が含まれている場合には、その自由変数は1つ正方向にシフトしておいてから、後で-1して帳尻を合わせるということになります。
これを定義どおりにそのままpythonで書き写せば、β簡約が完成します。
なんと、実質一行ですね。

```python3:beta_reduction.py
def beta_reduction(t, v):
    return shift(-1, 0, substitution(0, shift(1, 0, v), t[2:]))

print(beta_reduction('λ.(1 0)', 'λ.0'))
print(beta_reduction('λ.(1 (0 2))', 'λ.0'))
```

```
(0 λ.0)
(0 (λ.0 1))
```

2つ目の例は、本書に書いてある(λ.1 0 2) (λ.0) → 0 (λ.0) 1に対応しているのでした。

# 余談

この本はこうした難しさがあるので、訳本の監訳者いわく、

> サポートサイトができたらジュンク堂トークのPDFも載ると思いますが、これだけは先に：型システム入門(TAPL)はとりあえず1,3,8,5,9,11章（＆2章の必要な部分）と、あとは好きな章を読めば「読んだ」ことにしても良いと思います！（60%本気）

ということだったので、そのような読み方もあるのかもしれません。

https://twitter.com/esumii/status/315135694462939137

ただ、型システムに関して言えば、基本的には本書は入門という位置づけのようです。
（訳書のタイトルは「型システム入門」）

> 内容はまさに「型システム」の「入門」なので非常に誠実だと思います

https://twitter.com/esumii/status/587897598683455491