言語ゲーム

とあるエンジニアが嘘ばかり書く日記

Twitter: @propella

線形論理とコンピュータ革命

週末は Linear Logic and Permutation Stack -- The Forth Shall Be First http://home.pipeline.com/~hbaker1/ForthStack.html 読んでいた。思ったのは、線形論理が私の人生の疑問の半分くらいを解決するだろうという事。そしてアランさんの言うコンピュータ革命とはこういう事なのかも知れないという事。

身分不相応にも未来を予測してみる。近い将来、小学校で習う算数は線形論理に基づいた物になる。未来の子供達は、カッコや優先順位や変数に悩まされる私達の数学を見て、何て野蛮で非能率なのだと言うだろう。まるで我々が漢数字やローマ数字の数学を、きわめて技巧的で非論理的だと思うように。

線形論理に基づくプログラミングとは、変数の使用を一度しか認めないプログラミングの事を言う。一度しか認めなくてプログラムなんか書けるのか?!単純な例を示す。

// 普通の言語
function double (x) {
  return x + x;
}

// 線形論理
function double (x) {
  x1, x2 = dup(x);
  return x1 + x2;
}

線形論理では変数の使用を一度しか認めないので、x + x が出来ない。だから x を二回使いたい場合は dup() を使って二つに分ける必要がある。わざわざ dup() が必要になってくるなんて面倒だけど、よく考えると今まで何故同じ変数を何回も使えたのか、そちらの方が不気味に思えてくる。自然界の物は勝手に二つに分かれたりしない。 変数を二回使って良いなんてのは、2月が28日しか無いのと同じような勝手な約束事でしかない。勝手な約束事を削る事で、新しい単純な世界が見えてくる。

上では普通の言語にあわせた記法で書いたので利点がイマイチ分からないが、線形論理をより自然に表記出来る Joy で書いてみる。Joy では上の関数はこう書く。

DEFINE double == dup +.

関数 double は数字を見つけるとそれを dup (複製)し + (足し算)する。システムはプログラム中で double という単語が現れると何時でも dup + と交換出来る。明示的に値の複製を dup で指定しないといけない一方で、変数の書き換えが要らない。つまり、プログラム中で

print double(3);

なんて文があった場合に、わざわざ x に 3 を入れて。。。とやら無くても、直接

3 double put.
    ↓
3 dup + put.

という書き換えが出来る。変数 x って中学で習うのかな?自分が中学生の時、変数の複雑な対応付けが出来なくて非常に困った。そして今でも出来ない。x が無かったらどれほど幸せか!

ただ、残念ながら変数が沢山ある場合を Joy 記法で書くと逆に複雑になる。従って記法に関しては改良の余地が山ほどある。大切なのは、線形論理という物がより過去のしがらみから開放された基本的な論理であって、基本的だという事は応用の余地が広いという事だ。線形論理を使う事によって、異なる数学のモデルに共通する基礎が、小学生にもおのずと見えてくるような記法を構成出来ると信じている。

上記の論文が書かれたのが 1993 年なのに、いまだに線形論理がブームになっていないという事はもしかして滅茶苦茶外した事を書いているのかも知れないが、一応メモとして残しておく。