この記事は定理証明アドベントカレンダー2013のたぶん7日目の記事です

誰でも定理証明器を作れるようになろうという趣旨です。ここではCoqのパクリみたいなサブセットを48時間で作ります。

タイトルの元ネタは http://en.wikibooks.org/wiki/Write_Yourself_a_Scheme_in_48_Hours です。というわけで、使う言語はHaskellですが、他の言語でも特に問題ないと思います。

定理証明器の部品は以下のものが必要です。

• 記述言語
• カーネル
• 証明支援言語
• その他

記述言語はCoqではGallinaといわれてる部分です。立派なプログラミング言語をひとつ設計しないといけません。このプログラミング言語によって、定理のステートメントを記述したり、証明を記述したり、関数を書いたり、データ構造を定義したりします。

カーネルは記述言語のインタープリタになります。プログラムを実行したり、型検査をしたりします。定理証明器のカーネルには、de Bruijnの基準という満たすべき条件があります。すなわち、カーネルはできるだけ小さく書いて、人間が簡単に読むことができるようにしましょう。そして、システムの健全性に関わる部分はこのカーネルの中に収めましょうということです。なので、なるべく手抜きして小さく書いてしまいましょう。

証明支援言語はCoqではLtacといわれている部分です。「intro」とか「apply」とかいったコマンド言語です。定理証明器を作ってみると、これらのコマンドが裏で何をやってるのか理解できるようになります。

その他の部分は今回はなるべく実装しません。主に型推論がここに入ります。他には入出力の管理とか面倒くさい部分です。

記述言語を設計する

定理証明器で使われるプログラム言語は依存型いう型システムを使ったらラムダ計算になります。言語自体はSchemeみたいなものなので、分からない人はSchemeを作るほうを読めばいいでしょう。言語を作るにはまず項がなんであるかを定めなければなりません。Schemeの場合は

data LispVal = Atom String
              | List [LispVal]
              | DottedList [LispVal] LispVal
              | Number Integer
              | String String
              | Bool Bool

なにやら、プログラム言語の項というよりはデータ構造を定めているように見えますね。これがなんとLisp系の言語の特徴で、プログラムとデータを同じ言語で書くのでした。データの部分を消して、純粋に計算の部分を取り出してくるとラムダ計算の項の定義になります

data Term = Var String      -- 変数 x
            | App Term Term    -- 関数適用 (f x)
            | Lam String Term  -- ラムダ式 (fun x -> f)

しかし、これだけでは定理証明器には使いにくいです。型システムを導入しましょう。依存型ではプログラムと型を同じ言語で書くので、ここに型に対応する項を追加してやればよいのです。Schemeと似てますね。今必要そうな型は関数の型だけのようなので、それを追加します。そして、ラムダ式で変数を束縛するときには毎回その型を書くことにしましょう。すなわち引数の型は必ず書かないといけません。

data Term = Var String
            | App Term Term
            | Lam String Type Term  -- ラムダ式 (fun x : T -> f)
            | Prod String Type Term  -- 関数の型 (forall x : T -> S)
            | Univ Int  -- 型の型

type Type = Term

さらに、型の型を足しておきました。なぜかというと、今追加した関数の型に対応する型がなかったからです。という風に進めていくと、今度は型の型の型が必要なので、それも下に追加しないといけないのではないかと感じられるかもしれませんが、型の型Univは整数をひとつ持つようにしたので、Univ 0の型はUniv 1とし、Univ 1の型はUniv 2という風に続ければ無限に定義を追加する必要はなくなります。他にも追加したい型が色々ありますが、それは後回しにしましょう。

項の一致

依存型の言語を実装するときは項を比較して等しいかどうかを確かめないといけないことがあります。例えば、関数 f の引数の型が T で、渡そうとしている値の型が S だった場合に、T と S は一致しないといけません。このとき、2つ注意する点があります。まず、T の中で束縛されている変数と、S の中で束縛されてる変数は名前が違うかもしれません。これは他の言語でもよくある問題です。例えば Haskell の場合は、a -> a と b -> b は同じ型ですが、使っている名前が違います。もう1つの注意点は計算をしてみないと等しいかどうか分からない場合があるということです。T という型と (fun x : U -> x) T という型は等しくならないと困ります。この場合は、(fun x : U -> x) T という関数適用の計算を1ステップ進めて、計算結果が T になるので等しいことが分かります。しかし、よく見ると、引数の型は U と書いてあるので、計算する前に T の型が U であることを確認しないといけません。すると、また内側で項の一致を確認しないといけないわけです。まとめると

• 束縛した変数の名前を変えても項の一致は変化しない
• 項の一致を確かめるためには計算を進める必要がある
• 項の計算を進めるためには型検査をする必要がある
• 型検査をするためには項の一致を確かめる必要がある

最初の問題を解決するために、de Bruijn インデックスという手法を使います。後ろの2つの問題は次回に回します。

de Bruijn インデックス

束縛された名前は自由につけかえてもよいという規則は項を比較する場合に不便なので、de Bruijnインデックスという手法を使います。これは単に名前の代わりに番号で変数を参照しようというだけのことです。変数を参照するときには、その束縛とどれだけ距離が離れてるかの数値を使います。直前で束縛された変数を使うにはインデックス0を使います(1にする流儀もあるので注意)、そのひとつ手前の変数を使うにはインデックス1を使います。こうすると、例えば、名前を使ったラムダ式

λ f. λ x. λ y. f y x

は

λ. λ. λ. 2 0 1

のように書けます。項の定義を対応するものに直しておきましょう

data Term = Var Int
            | App Term Term
            | Lam Term Term  -- ラムダ式 (fun 0 : T -> f)
            | Prod Term Term  -- 関数の型 (forall 0 : T -> S)
            | Univ Int  -- 型の型

この方法では、ラムダ式の引数は必ずインデックス0になるので、対応する値を持つ必要はなくなります。インデックスが上に突き抜けた場合はどう解釈すればいいのでしょうか？例えば、

λ. 2 0 1

は、2と1に対応する束縛が見つかりません。しかし、これは壊れた項ではありません。なぜなら、前の例で書いた

λ. λ. λ. 2 0 1

はこの項を部分項として含んでいます。このように、インデックスがはみ出ている項を開いた項と呼びます。インデックスが収まっている項は閉じた項です。

開いた項ははみ出したインデックスを外側で束縛してあげなければいけません。型がついている計算の場合は束縛するときに変数の型も必要です。はみ出したインデックスと型など他の情報の間の対応を文脈と呼びます。開いた項を考えるときは常に何かの文脈と対になっていると考えたほうが分かりやすいです。ここでは項と文脈の対を表を使って書くことにします。

型については、次回に回すのでここではS、T、Uという型があるとしましょう。この項は「2 0 1」という部分項を持っているので、対応する文脈を書いておきましょう

この表の変化を見れば、インデックスのはみ出した部分が文脈に入っているのがよく理解できると思います。これはCoqの証明画面を意識して書いています。

  A : Type
  a : A
  b : A
  c : A
  H : a = b
  H0 : b = c
  ============================
   a = c

Coq内部ではここに現れる変数はインデックスで管理されています。よって、同様の表を書くとこうなります。

分かりやすいように元の名前を括弧にいれて書いておきます。型は項なので、他の変数を参照していますが、参照は自分より上のインデックスにしかできません。しかも、そこから数えなおさないといけないのが難しいところです。ここをちゃんと身に付けておかないと定理証明器の実装は大変になります。

実はインデックスを1から始める流儀だと以下のようにもっと読みやすくなります。

よくみると、最後の行のインデックスが-1なので、1から始めると便利なんですね。ただし、普通の配列アクセスの流儀を使いたいときは0から始めたほうが余計な引き算がいらなくなります。この記事では0から始めることにします。

シフト

さて、元のとおりに0から始めるインデックスに戻り、文脈と項を操作する方法を考えます。

この文脈を操作して、インデックス3とインデックス2の間にスキマを4つ作りましょう。このときに、変数の参照を壊さないようにします。結果は次のようになります。

項の変化だけを見てみましょう。最初「4=2」だった項は「8=2」になりました。スキマを4つ作ったので、4を足しますが、インデックス3とインデックス2の間に作ったので、3以上だったところは4を足して、2以下だったところはそのまま変わらないことが分かります。この項の操作は特定の文脈に依存せずに同じやり方でできることが分かります。なので、項の操作として独立させて、シフト操作と呼びます。この操作の引数はスキマを開けるインデックスの番号nとスキマの数dになります。これにより、インデックスnとインデックスn-1の間にスキマdを作ったときの項の変化が計算できます。

termShift :: Int -> Int -> Term -> Term
termShift n d (Var i) | i >= n = Var (i + d)
                      | otherwise = Var i

操作したい項の中に変数束縛がある場合が問題です。例えば、項がラムダ式(fun 0 : T -> R)の場合はどうなるかを考えてみましょう。まず、対応する文脈をΓ、Δとします。すなわち、以下の表でΓとΔは複数の行の集まりを示しているとしましょう。そして、ΓとΔの間にスキマdを作りたいとします。（表のコラムを横につなぐ方法がわからなかったので、Γ Γ と書いていますが、横に繋がってる表が書きたかったのです）

これに、スキマdを作った結果は

このような項になるはずです。

次に部分項の文脈を求めます。前の章で部分項の文脈の計算を行ったことを思い出しましょう。

この表をよく見ると、部分項に対して必要な操作は、ちょうど今実装しようとしているシフトと同じものであることが分かります。ただし、RからR'を計算する場合は引数nがn+1に変わります。これを実装すると

termShift n d (Lam t r) =
  Lam (termShift n d t) (termShift (n + 1) d r)

課題: 他の場合を補完して、シフト操作を実装してみましょう。

簡約

次に計算を進めることにしましょう。計算をする際は文脈に変数の値を持たせることにします。宣言されているだけの変数は値を持たないので、2種類の束縛があることが分かります。文脈の型はLocalという名前にします。

data Binding = Decl Type
             | Def  Type Term

type Local = [Binding]

表を書くときにも値をもたせることにしましょう。

| インデックス | 値と型 |
|------:|:---:|:---:|
| 2 | : T |
| 1 | : S |
| 0 | := 0 : U |
| === | === |
| 項 | 2 0 1 |

Coqでも、let を使うと同様になります。

Coq < Goal forall A, forall a b : A, let c := b in a = b -> a = c.
1 subgoal
  
  ============================
   forall (A : Type) (a b : A), let c := b in a = b -> a = c

Unnamed_thm < intros.
1 subgoal
  
  A : Type
  a : A
  b : A
  c := b : A
  H : a = b
  ============================
   a = c

これを表で書くと、

となります。

ここで、計算を1ステップ進めてみましょう。値が定義されている変数はその値で置き換えることができます。項 3 = 1 (a = c) のインデックス1は値が0 (b) と定義されているので、計算の結果の項は 3 = 2 (a = b) となることが分かります。すなわち、次の表のような結果になります。

インデックス1の値はインデックス0なので素直に置き換えると 3 = 0 (a = H) になってしまいます。よってここでも何か変換を行わなければなりません。インデックス1の定義はそれより上の文脈を参照しているので、この項0は上の文脈とは異なる文脈を持っています。表にすると

となります。文脈が異なる項どうしを混ぜ合わせようとするときは、最初に文脈をそろえる必要があります。この場合はインデックス0の下にスキマを2つ作れば、文脈がそろいます。前の章で定義したシフト操作を使えば(n=0, d=2)、

このようになり、文脈がそろいます。ここで、シフトのパラメータはnは必ず0になり、dは置き換えようとしたインデックス+1になることが分かります。これを実装すると

reduceFull :: Local -> Term -> Term
reduceFull e (Var i) =
  case e!!i of
    Decl ty -> Var i
    Def ty t -> reduceFull e $ termShift 0 (i + 1) t

となります。変数が宣言されていた場合は計算が進まないので、そのまま元の項を返します。定義されていた場合は適切にシフトを行い、さらに計算を進めます。

次にβ簡約を考えましょう。関数適用 f a において、f がラムダ式だった場合はβ簡約ができます。表で書くと次のようになります。項 (fun 0 : T => R) a を文脈 Γ で計算している場合は

を変換して、

にすればいいことが分かります。まず、部分項に進んで、

と

という表ができます。ここで、上の表で、インデックス0の値をaにして計算を進めるとよいことがわかります。文脈はそろっているので直接

となります。これを再帰的に計算することで、結果の表

を得ることができます。しかし、これは欲しかったR'と文脈が異なっています。R'の文脈はΓだけだったのに対して、得られたR''では余計な行がひとつ付いています。再帰的に計算を呼び出した結果、R''の中ではインデックス0は参照されていないはずなので、安全にこの行を削除できるはずです。これもシフト操作により行うことができます。シフトにパラメーター(n=0, d=-1 ！)を渡すと1行削除されます。ただし、この操作は項の中で消えるインデックスを参照していない場合に限られます。そうでない場合は項が破壊されます。負のインデックスを持つ変数が現れるので、このバグはすぐに見つけることができます。実装すると

reduceFull e (App f a) =
  let a' = reduceFull e a in
  case reduceFull e f of
    Lam t body -> termShift 0 (-1) $ reduceFull (Def t a' : e) body
    f' -> App f' a'

この実装の場合は、reduceFullがとことん簡約してくれるので問題ありませんが、将来部分的な簡約を実装したくなったときはインデックス0への参照が残らないように気をつけてください。分かりやすい方法としては、インデックス0のところに全部代入する別の関数substを書くのがよいでしょう。ただし、もっと細かな評価戦略を使いたいときには subst は大雑把すぎて使いにくいです。 今回は簡単のために省略します。

残りの場合は計算を進めることはできないので、再帰呼び出しをして部分項を計算しましょう。束縛をまたぐ場合は文脈に宣言を追加します。

reduceFull e (Lam t r) =
  let t' = reduceFull e t in
  Lam t' (reduceFull (Decl t' : e) body)

課題: 残りの場合を実装して完成させましょう

比較

計算ができるようになったので、2つの項が一致するかどうかを確かめることができるようになります。まず、項の文脈はそろっている必要があります。よって、比較関数は文脈を1つと2つの項を受け取ることになります。

termEq :: Local -> Term -> Term -> Bool
termEq e t1 t2 =
  reduceFull e t1 == reduceFull e t2

de Bruijnインデックスを利用したことにより、名前の付け方を気にすることなく == で比較することができます。さらに、先に計算を完全に終わらせておくことで、上に書いた項の比較が完成します。

ここで注意があります。計算しようとしている項は型検査を通っていないといけません。型が正しくついていない項を計算すると無限ループになり結果が返ってこなくなる場合があります。しかし、型検査はまだ実装していませんし、型検査を行うには項の一致が分からないといけません。この循環論法は次回にやります。

次に重要なことは、完全に計算しなくても一致するかどうかは判定できることです。これは計算をweak head normal formまでしか進めないという風に実装しますが、ここではこの最適化は行わないことにします。しかし、ここを賢く実装することが高速な定理証明器を作るキモになります。

次回予告: 型検査をやります