内容
レイフィケーション
2006年の正月に、「ゲーデルの不完全性定理」に関する記事を何本か続けて書きました。
- 最初の記事： プログラマのための「ゲーデルの不完全性定理」(1)
3本目の記事である「プログラマのための「ゲーデルの不完全性定理」(3)：自己適用からゲーデル化へ」の「メタレベルも取り込むこと：レイフィケーション」という節に次のような絵を入れています。
この絵は、「記述される対象物」と「その対象物に関する記述」の構造が何段階かのメタ階層を作っている状況において、符号化により「対象と記述」が領域の内部へと埋め込まれる様子です。
この記事で既にレイフィケーションという言葉を使っています。
それから2年後、2008年の正月には、「いまさらながらだけど、オブジェクトとクラスの関係を究めてみようよ」という記事を書きました。このとき使った絵は次です。
対象となるデータがいる場所と、メタレベルの概念がいる場所を、1階と2階のフロアとして描いています*1。実は、イギリスのように、1階→地階＝0階、2階→1階 と呼んだほうが都合がいいのですが、ここでは日本の習慣に従います。
2つのフロアを横から見て簡略化して描くと：
手書きの字が読みにくいですが、1階にいるデータ（オブジェクト）は S1, S2, P。2階にいるクラスは左から Class, Object, String, Person です。上向きの矢印が is-instance-of の関係。2階から1階に落ちていく下向きの点線矢印がレイフィケーションです。
3階まで描くと次のようです。
3階にメタクラスCLASSがいて、そのレイフィケーションの結果が2階のClassクラス、さらにレイフィケーションして1階（データ）まで落としたのが Class.class というデータです。
形式化された証明と算術プログラミング
2007年夏に書いた「圏論的指数の周辺：ラムダ計算、デカルト閉圏、ノイマン型コンピュータ」の「ノイマン／ゲーデルの箱庭風景」の節から引用します。
[ノイマンとゲーデルに]共通する手法は、理念的な世界の存在（ただし、計算可能関数のようなたちの良い存在）を、具象的なデータのなかにエンコードしてしまうことです。具象的なデータは、目の前にあり手で触れるモノです。よって、理念的な外部世界を、目の前にある具象的対象物に投影して閉じ込めることができます。世界全体がスノーグローブ（和風の表現なら、箱庭の小世界）と同型になるわけです。
ここで使っている言葉「スノーグローブ」は僕のお気に入りで、このブログには何度も出てきます。今年（2012年）の記事でも「スノーグローブ」概念を振り返ったりしてます。
現代のコンピュータの原理は、自分自身をも含む外部の世界を操作可能なデータに符号化してしまうことです。符号化された世界がスノーグローブです。符号化＝レイフィケーションですから、レイフィケーションされたイメージをスノーグローブと呼んでいることになります。
言葉の選び方は、まーなんでもいいのですが、「メタレベルの存在物→データ」というマップがコンピューティングにおいて本質的な役割を担っていることには注意してください。
実際のコンピュータが登場する以前に、「メタレベルの存在物→データ」の方法を駆使したのがゲーデルです。Aが何かの命題だとして、それが形式的な論理式として表現されているとしましょう。推論や証明という行為も形式化された論理システムSで表現されているとします。
S |- A という記法は、命題（論理式）Aが論理システムSで証明可能だということです。ゲーデル符号化とは、論理式という人工言語を自然数にコンパイルする方法です。Code(A) がコンパイル結果である自然数だとして、自然数上の関数*2 provable:NaturalNumber→Boolean があって、次が成立するとウレシイわけです。
- 「S |- A」 ⇔ 「provabl(Code(A)) = true」
ゲーデルによる結果は、「必ず S |- A か S |- ¬A が成立する」に対しては否定的だと言えますが、しかし、Code(A) や provable(n)（nは自然数）を組み立てることを実際に遂行しています。もう少し詳しいことは、前述の「プログラマのための「ゲーデルの不完全性定理」(1) 」や次の記事にあります。
メタプログラミングと妖精さん達
レイフィケーション、つまり「メタレベルの存在物→データ」というマップですが、これは知的好奇心や衒学趣味を満たす意味しか持たないのでしょうか。実務や現場とは無関係なのでしょうか？
僕は、レイフィケーションは極めて実用性が高いソフトウェア的手法だと思っています。そもそも現代のコンピュータの原理である、というのも肯定する理由のひとつですが、一般のソフトウェアシステムにおいても、レイフィケーションができればメタプログラミングができます。メタプログラミングとは、メタレベルにいる概念的な存在物をプログラムから参照したり操作したりすることです。そのメタプログラミングは実用性が高い、と信じているのです（もちろん、信じる根拠がさらに必要ですが）。
メタプログラミングを実行するためには、本来ならメタレベルにいる存在物をプログラムから参照可能／操作可能なレベルに落とさなくてはなりません。そうです、レイフィケーションですね。精密なレイフィケーションができれば、それだけパワフルなメタプログラミング能力を獲得できます。
メタプログラミングによって出来ることの喩え話に、僕はしばしば「小人さん」とか「妖精さん」という言葉を使います（例えば「スノーグローブのなかの小人さん達」）。妖精さんは、「少し知的なんだけど、やっぱり退屈なこと」「機械的にはできないけど、人間にとっては辛い作業」を人間に代わって片付けてくれるのです。メタプログラミングにより、親切で勤勉な妖精さんを創りだすことができます。
レイフィケーションとメタプログラミング、それにより創り出された妖精さん達は、ゲーデルの発想からの派生物のなかでもとても実利的なものだと思います。
