『プログラミング言語の基礎概念』第一章の復習と、自分が躓いたところをメモする

近況

神様あなたは

何でも知っていて

心悪しき人を打ち負かすんだろう

でも真夏の太陽は

罪を溶かして

見えないが確かに

背中にそれを焼き付ける

―― eastern youth『夏の日の午後』

要旨

今月の最後に『プログラミング言語の基礎概念』第二章の読書会があるので、それに向けて復習をする。意味論を記述するために、最少の推論規則から判断を導くための、導出システムを考える。これらには、ペアノ自然数を利用したりしている。

はじめに

こないだ、『プログラミング言語の基礎概念』の第一章の読書会に潜り込んできて、そういえば今月の最後にも第二章の奴が始まるので、せっかく惰性で参加するのだし、惰性で読書メモをとっておくのも、あとで勉強する人にとっては有益なのではないかと思ったので、メモしておく。

本文

最初のひっかかりポイント: n plus Z is nはどうやって導くの?

何らかの判断を形式化するということは、具体的には「1たす1は2である」といった自然数の加算(あるいは乗算)を形式化することである。基本的には、本書に書いてある形式化をそのまま当てはめれば良い。導出システムは、その規則に応じて、名前が付けられている。これらは便宜上のもの(つまり、規則の範囲を述べるもの)であるから、然程気にしなくてもよい(というのも、これらは拡張されるものである)と自分は理解している。

さて、ここで「1たす1は2である」を形式化する際に、前提となるのは「ペアノ自然数」であり、このブログでも過去に取り上げた。具体的には2 = S(S(Z))といったように、ゼロと、その次の数を、後続者関数(successor function)で書き記す事が出来る。さて、このように自然数を形式化すると、導出システムの規則も自然なものとなる。本書では、まず最初にn1 plus n2 is n3という形式を与え、それに対して次の規則を与えている。

• P-Zero -> Z plus n is nという判断を導いて良い
• P-Succ -> n1 plus n2 is n3ならば、S(n1) plus n2 is S(n3)を導いてもよい

ポイントは、基本的にこれらが置き換えによって成立しているということである。そして、P-Zeroのnは任意の自然数からスタートしてもよい。例えば、便宜的にZ plus S(S(S(Z))) is S(S(S(Z)))(このとき、S(S(S(Z)))は3を示しているとも考えられるが、考えられるという示唆のみにしておく)というのを考えた場合、

• P-Succ -> Z plus S(S(S(Z))) is S(S(S(Z)))

として、判断が導かれる。

さて、ここで気がつくことがひとつある。本書でも演習になっている部分であり、自分もちょっとだけ躓いたところであるのだが、この逆パターン、つまりS(S(S(Z))) plus Z is S(S(S(Z)))は、P-Zeroという形式から直接判断することは出来ない。ここで、一瞬戸惑うところでもあるのだが、次のように考えればいいことに気がついた。

つまり、

• Z plus n is nは、直接P-Zeroから導出できる
• n plus Z is nは、Z plus Z is Zを経路して、n回のP-Succが必要となる

と言える。これ自体は、練習問題1.3と関係するところではある。

二番目のひっかりポイント: S(Z) + S(Z) + S(Z) evalto S(S(S(Z)))を導出するの?

さて、ここでBNFと抽象構文木があるのだが、今回の読書メモでは飛ばす。ただ導出システムを解く上でポイントになるのは、私達が1 + 1 + 1 = 3として計算しているものは、下のように書き直すことが出来るということだ。

• 1 + 1 + 1 = (1 + 1) + 1 = 2 + 1 = 3

このような書き換え自体は無意味なものだけれど、しかし導出システムを導く上においては重要なものになる。実際、本書p.16では、「常識的な省略」として、次のように考えられると考えている:

• (S(Z) + S(Z)) + S(Z) = S(Z) + S(Z) + S(Z)

この何気ない省略だが、これが導出システムにおいて、非常に重要な問題になる。新しい規則として、次の二つを考える。

• E-Const -> n evalto n
• E-Plus -> e1 evalto n1かつe2 evalto n2かつn1 plus n2 is nならばe1 + e2 evalto nが導き出せる

いきなり、S(Z) + S(Z) + S(Z)としても、どこから手を付けていいのかわからなかったので、簡単な式から考えてみた。それはZ + Z + S(Z) evalto S(Z)という式である。この式だと、基本的にP-Zeroで導出が終了するので便利である:

ちなみに、オンライン導出システムでは、下のように書ける:

Z + Z + S(Z) evalto S(Z) by E-Plus {
  Z + Z evalto Z by E-Plus {
    Z evalto Z by E-Const {};
    Z evalto Z by E-Const {};
    Z plus Z is Z by P-Zero {};
  };
  S(Z) evalto S(Z) by E-Const {};
  Z plus S(Z) is S(Z) by P-Zero {};
};

さて、ここで見られるように、基本的には、まず最初の省略されたカッコの中から導出し、そのあとに残りの三番目を導出すればいい、ということがわかる。つまり:

これをオンライン導出システムで書くとこうなる。

S(Z) + S(Z) + S(Z) evalto S(S(S(Z))) by E-Plus {
  S(Z) + S(Z) evalto S(S(Z)) by E-Plus {
    S(Z) evalto S(Z) by E-Const {};
    S(Z) evalto S(Z) by E-Const {};
    S(Z) plus S(Z) is S(S(Z)) by P-Succ {
      Z plus S(Z) is S(Z) by P-Zero {};
    };
  };
  S(Z) evalto S(Z) by E-Const {};
  S(S(Z)) plus S(Z) is S(S(S(Z))) by P-Succ {
    S(Z) plus S(Z) is S(S(Z)) by P-Succ {
      Z plus S(Z) is S(Z) by P-Zero {};
    };
  }
};

この辺りについては、過去のエントリで『アンダースタンディング・コンピュテーション』を読みながら手で抽象構文木を作ったことが、理解に効いている可能性がありそうだ。

まとめ

この辺りの要領さえわかれば、第一章は突破できる気がした。この知見を元に、『プログラミング言語の基礎概念』第二章の読書会に挑みたい。

あと、紙に書いているときに、ちゃんと問題が解けたときは、下のようなコメントを書くと、かわいくて「やったー!!」感が出ることにも気がついたので、今後はガンガン利用していきたい。

プログラミング言語の基礎概念 (ライブラリ情報学コア・テキスト)

参考文献

論理学をつくる

この辺りの導出システムの判断自体については、先に上の本を読んでいたので直感的に掴めたけれども、この本自体は読まなくても、『プログラミング言語の基礎概念』自体は読めるけれども、判断はどうすればいいのかということ自体は掴めるので良い。

コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-

この辺りの判断システムがどのように関係していくのか、について、この本とは別の角度からアプローチしたい場合は、上の本が読み物として面白かった。この本では、S(S(Z))みたいなペアノ自然数をSS(Z)という、さらに括弧を略した方法を使っており、自分も紙でまず導出を書き下す場合には、こちらのSS(Z)的な記法を使っている。