BETA

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

投稿日:2019-03-17
最終更新:2019-03-21
※この記事は外部サイト(https://qiita.com/sasanquaneuf/items/5b0bc...)からのクロス投稿です

※この記事はQiitaにもあるので、TeXの表記が化けている場合はQiitaの記事の方を確認ください:
https://qiita.com/sasanquaneuf/items/5b0bc0d771669c30934d

概要

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

名無し表現のモチベーション

5章以前で、(型無しの)ラムダ計算を導入しているのですが、ラムダ計算を用いて実際に新しい式を作ろうとすると、変数名の衝突が問題になる場合があります。たとえば、
$\sf{\lambda x. \lambda x. x}$
こんな書き方をしてしまうと、右端の$\sf x$をどう扱うべきかという問題が生じます。これは最後の束縛が有効というような定義の仕方をすれば一意に解釈ができますが、しかし人間にとって易しくありません。
これを避けるための書き換えのルールなどはいくつかありますが、そのうちの「名無し表現」によって項を表現することで変数束縛を明快な形に書き換える、という方法があります。

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}$というのはそれぞれ集合だということですね。

最小性(1):一般には複数存在し得ること

この$\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}$の条件を満たすことが(適当な計算によって)わかります。従って、最小性以外の条件だけでは、そのような集合族は複数存在し得るのですね。

最小性(2):そもそも最小の集合族の存在が自明でないこと

ここで、一層難しいことを言うと、そもそも"最小"という条件を満たすものが一意に定まるか否かは、実は自明なことではありません。というのも、一般に集合$A$と集合$B$には$A \subset B$でも$B \subset A$でも($A = B$でも)ない場合があって、そのような場合には比較ができず、この2つの集合の間に"最小"という概念を定めることは通常はできないからです。
従って、"最小の集合族"という言い回しも、実は全く自明ではなくて、そもそもそのようなものが存在するのか?というところから考える必要があります。もちろん実際には存在するのですが、それを示すには、上記の最小性以外の条件を満たす"集合"$\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 )))}$という形の要素をいくらでも作れるので、要素は無限に存在します。

よくない書き下し例

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$の深さも考慮するようにしてみます。
そうすると、少しマシな書き下し方ができます。

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})$と書くことがある。

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

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

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以外の自由変数が変化する場合があります(というかλが存在する場合で実際に置換が発生する場合は確実にそう)。代入対象の変数は、あくまでも何番目の自由変数に代入するかという事を意味していて、単純な置き換えではないことに注意しておきます。

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

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.

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

定義(β簡約)

この章は、β簡約まで述べるとおしまいですね。これは後ほど。

余談

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

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

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

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

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

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

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

技術ブログをはじめよう Qrunch(クランチ)は、プログラマの技術アプトプットに特化したブログサービスです
駆け出しエンジニアからエキスパートまで全ての方々のアウトプットを歓迎しております!
or 外部アカウントで 登録 / ログイン する
クランチについてもっと詳しく

この記事が掲載されているブログ

だべだべ - @sasanquaneufの技術ブログ

よく一緒に読まれる記事

0件のコメント

ブログ開設 or ログイン してコメントを送ってみよう
目次をみる
技術ブログをはじめよう Qrunch(クランチ)は、プログラマの技術アプトプットに特化したブログサービスです
or 外部アカウントではじめる
10秒で技術ブログが作れます!