SASyLF - 言語ゲーム

SASyLF というのは証明の手伝いをしてくれるツールです。Coq より簡単だそうです。

実行方法と学び方

ホームページ http://www.cs.cmu.edu/~aldrich/SASyLF/
SASyLF-Emacs-Mode http://github.com/hesam/SASyLF-Emacs-Mode/tree/master

SASyLF を実行するには java が必要です。Coq と違ってファイルに証明を書いて、それが間違っていたら教えてくれます。正しければシンプルに No errors found. と表示されます。

java -jar SASyLF.jar ファイル名.slf

SASyLF の練習をするには exercises にあるファイルを読むとよいと思います。exercises/exercise1.slf の解答編は examples/sum.slf にあります。exercise1.slf では、自然数の加算の定理を証明しています。ここでは、この exercise1.slf を見て行きます。

一番単純な SASyLF ファイル

エラーの出ない最低限のファイルを紹介します。最低 syntax 定義が必要なようです。terminal(終端記号)というのは証明に使うデータの事を言います。関数言語的に言うと、終端記号が値で非終端記号が型です。この場合 Haskell 風に言うと data N = Z | S N です。コメントは java と同じです。

// 終端記号の定義
terminals z s

// 文法定義。非終端記号 n は z または s n
syntax
n ::= z
  | s n

例えばこれを nat.slf として保存して実行した結果はこんな感じです。

$ java -jar SASyLF.jar nat.slf 
nat.slf: No errors found.

公理

次に jugment(公理) の定義です。judgment の書き方は

judgment 公理名 : 結果の型

前提文
--- 規則名
結果文

これで、もしも前提が世界に存在していたら結果も存在するという意味になります。前提が無い時は、規則がいつでも成り立ちます。規則の結果は結果の型とマッチしていないといけません。自然数の例を挙げます。

judgment sum: n + n = n

--------- sum-z
z + n = n

n1 + n2 = n3
-------------------- sum-s
(s n1) + n2 = (s n3)

間違えやすいのは、z + n = n は「z + n の結果が n だ」という意味ではなく、「z + n = n という関係がこの世界に存在する」という意味で、= の記号に特別なニュアンスはありません。これを add z n n のように prolog っぽく書いても一緒です。SASyLF での証明とは、与えられた syntax と jugment を使ってあるパターンを導く経路を書く事です。

あと z + n = n の記法自体も気持ち悪いです。気持ちは分かるけど 0 + Int = Int と書いているような物で、型と値がごちゃ混ぜで、非終端記号を変数名として使っています。sum-s のようにそれぞれの変数を区別する必要がある場合は数字やプライムを使って n1, n2, n1', n1'', ... のように書けます。この場合、n1 や n2 は自動的に n にマッチする値という事になります。

証明

ではいよいよ証明してみましょう。最初の証明は (0 + 1) + n = n + 1 です。定理の書き方はこんな感じです。

theorem 定理名 : forall 前提 exists 結果文
  規則名 : 文 by 理由 ...
  規則名 : 結果文
end theorem

前提には、syntax (ある何かが存在する時)か jugment (ある規則が成り立つ時)をゼロ個以上指定出来ます。この場合「どんな自然数 n でも (0 + 1) + n = n + 1 が存在する」と言いたいので前提は文になります。最後に exists に書いた結果文とマッチする文が書けたら成功です。試しにやってみます。

theorem n_plus_1_equals_s_n : forall n exists (s z) + n = (s n).
  d1: (s z) + n = (s n) by unproved
end theorem

おや、何か変ですね。理由の所に unproved と書いてインチキをしてしまいました。このように、とりあえず分からない所を unproved と書いて誤摩化す事が出来るのが SASyLF の最大の素晴らしい点だと思います。とりあえず問題だけ書いて、後でじっくり考える事が出来るのです。学校の先生が作っただけの事はあります。

では順にやってみます。(s z) + n = (s n) に似た奴を分かっている規則から探せば良いです。sum-s の結果である (s n1) + n2 = (s n3) がしっくり来るようなので、もう一度 sum-s を見てみましょう。

n1 + n2 = n3
-------------------- sum-s
(s n1) + n2 = (s n3)

sum-s の n1, n2, n3 にそれぞれ z, n, n を代入すると、z + n = n　ならば (s z) + n = (s n) と変形できます。とりあえずここまで使って、分からない部分は unproved として残し、SASyLF を実行して合ってるかどうか確認します。

theorem n_plus_1_equals_s_n : forall n exists (s z) + n = (s n).
  d1: z + n = n             by unproved
  d2: (s z) + n = (s n)     by rule sum-s on d1 // sum-s に d1 を代入
end theorem

次に unproved にしてある z + n = n に似ている奴を規則の結果から探します。すると sum-z がそのまんまです。しかも、sum-z の前提は空なので無条件に成り立ちます。という事でこれで証明完了です。

Induction を使った証明

今度は induction を使って n + 0 = n を証明します。induction は数学的帰納法に使います。この場合、n がゼロの時とその他の場合に分けて証明すれば、全ての場合で証明出来た事になります。証明の内容は省略して場合分けの形だけ書いてみます。n がゼロの時は z + z = z、(s n1) の時は (s n1) + z = (s n1) をそれぞれ証明すれば完成です。

theorem sum-z-rh: forall n exists n + z = n.
  d1: n + z = n by induction on n: // n で case に分ける
    case z is // n == z の場合
      d2: z + z = z by unproved
    end case
    case s n1 is // n == (s n1) の場合
      d4: (s n1) + z = (s n1) by unproved
    end case
  end induction
end theorem

次に証明の内容を埋めます。n がゼロの場合はそのまま sum-z の結果とマッチするので簡単です。

n が (s n1) の場合、とりあえず、n1 を仮定に代入して n1 + z = n1 を得ます。その仮定から sum-s によって (s n1) + z = (s n1) を導く事が出来るので、全体として証明出来た事になります。

theorem sum-z-rh: forall n exists n + z = n.
  d1: n + z = n by induction on n: // n で case に分ける
    case z is // n == z の場合
      d2: z + z = z           by rule sum-z // sum-z の下とマッチ
    end case
    case s n1 is // n == (s n1) の場合
      d3: n1 + z = n1         by induction hypothesis on n1 // d1 の n に n1 を代入
      d4: (s n1) + z = (s n1) by rule sum-s on d3 // sum-s に d3 を代入
    end case
  end induction
end theorem

前提が規則である場合の証明

次に、n1 + n2 = n3 なら n1 + (n2 + 1) = (n3 + 1) という事を証明してみます。SASyLF の書き方で言うと forall d1: n1 + n2 = n3 exists n1 + (s n2) = (s n3) になります。

今度は条件が jugment なので、場合分けがちょっとややこしいです。この場合、sum-z と sum-s の二通りの規則から条件である n1 + n2 = n3 が導かれます。例によって unproved で書いてみます。

theorem sum-s-rh: forall d1: n1 + n2 = n3 exists n1 + (s n2) = (s n3).
  // d1 (jugment sum) にある rule で場合分けする。
  d2: n1 + (s n2) = s n3 by induction on d1:
    case rule // sum-z の場合
      
      ----------------- sum-z
      dzc: z + n = n // この結論を n1 + (s n2) = (s n3) の形に変形出来たら OK
    is
      dz1: z + (s n) = (s n) by unproved
    end case
    case rule // sum-s の場合
      dsp: n1' + n2' = n3'
      -------------------- sum-s
      dsc: (s n1') + n2' = (s n3') // この結論を n1 + (s n2) = (s n3) の形に変形出来たら OK
    is
      ds2: (s n1') + (s n2') = (s (s n3')) by unproved
    end case
  end induction
end theorem

実際の証明は次の通りです。証明の進め方は大体 sum-z-rh と同じなので省略します。

theorem sum-s-rh: forall d1: n1 + n2 = n3 exists n1 + (s n2) = (s n3).
  // d1 (jugment sum) にある rule で場合分けする。
  d2: n1 + (s n2) = s n3 by induction on d1:
    case rule // sum-z の場合
      
      ----------------- sum-z
      dzc: z + n = n // この結論を n1 + (s n2) = (s n3) の形に変形出来たら OK
    is
      dz1: z + (s n) = (s n) by rule sum-z
    end case
    case rule // sum-s の場合
      dsp: n1' + n2' = n3'
      -------------------- sum-s
      dsc: (s n1') + n2' = (s n3') // この結論を n1 + (s n2) = (s n3) の形に変形出来たら OK
    is
      // n1' + n2' = n3' より
      ds1: n1' + (s n2') = (s n3') by induction hypothesis on dsp
      // forall n1' + n2' = n3' exists (s n1') + n2' = (s n3') に n1' + (s n2') = (s n3') を代入
      ds2: (s n1') + (s n2') = (s (s n3')) by rule sum-s on ds1
    end case
  end induction
end theorem

ファイル全体を http://gist.github.com/153807 に貼っておきます。