カリー／ハワード／ジラール対応とスパイダーエンジン

カリー／ハワード対応は、「論理⇔プログラム」の対応。典型例は、「連言と含意のNK」と「型付きタプル付きラムダ計算」の対応。型の計算（型推論）がNKの証明に対応している。

ジラールとその周辺による対応はもうちょっと範囲が広いし、少し観点が違うように思うので、カリー／ハワード／ジラール対応と呼ぼう。本編 http://d.hatena.ne.jp/m-hiyama/20090406/1238979506 でちょっと触れたことがある。

以下に出てくる証明は、人間の証明行為ではなくて、対象化されたデータとしての証明だから証明図ということにする。カリー／ハワード／ジラール対応では、証明図＝プログラム（証明図⇔プログラムという対応だが、イコールで書く）で、カット消去のような証明図の正規化がプログラムの実行＝式の評価に対応する。そして、正規化された証明図をジラールはdatumと呼ぶ。

すると、計算行為は、与えられた証明図を正規化することで、証明図の変形操作になる。「証明をすること」とはちょっと違う。計算行為の実行エンジンがコンピュータとかマシンなのだが、ここではエンジンと呼ぶ。

僕の感覚では、2つの世界が対応するというより、重なって同じものにみえる。つまりは文字通りに「証明図＝プログラム」。こうなると、「証明図を正規化するエンジン＝プログラムを実行するエンジン」となる。証明図もプログラムも絵図としてはスパイダーグラフで表現できる。つまり、「証明図を正規化するエンジン＝プログラムを実行するエンジン＝スパイダーグラフを正規化するエンジン」となる。

というわけで、証明図＝プログラム＝スパイダーグラフを評価or実行するエンジンをスパイダーエンジンと呼ぶ。スパイダーエンジンは概念的なマシンなので、VMと呼ぶのは語弊がある。Logical Machine = LM だろうか？ LM仕様をVM仕様に落としてソフトウェアで実装できる。

ソフトウェアで実装したスパイダーエンジンがCatyのエンジンとなる。ただし、いわゆるランタイムとは限らない。ジラールの言う計算（computation）は、どちらかというとコンパイルなので、スパイダーエンジン＝コンパイラに近い。もっとも、コンパイラとインタプリタ（ランタイム）の区別はどうでもよくて、境界線を自由に設定できるような定式化にしておかないとマズイだろうが。