ATSプログラミング入門:
PrevChapter 11. ATS/LF を使った定理証明Next

全域関数を使って証明を組み立てる

ATS/LF では、定理は型 (もしくはより正確に命題) によって表現されます。 例えば、次の命題は整数の乗法が可換であると言っています: 

{m,n:int}{p:int} MUL (m, n, p) -<prf> MUL (n, m, p)

ATS/LF において定理に対する証明をコンストラクトすることは、ATS/LF 内にエンコーディングされた定理である型の全域値 (ほぼ全域関数になるでしょう) を実装することを意味します。 ここでの全域とは純粋で停止することを意味しています。 このスタイルの定理証明はまだ体験していない人にはやや風変わりに見えるかもしれません。

はじめに単純で初歩的な例として、次のインターフェイスで与えられる ATS/LF の証明関数をコンストラクトしてみましょう: 

prfun mul_istot {m,n:int} (): [p:int] MUL(m, n, p)

キーワード prfun は (非証明関数ではなく) 証明関数のインターフェイスを示しています。 mul_istot は次の型 (より正確には命題) で宣言されていることに注意してください: 

{m,n:int} () -<prf> [p:int] MUL(m, n, p)

これは本質的に整数の乗法が全域関数であると言っています。 2つのどのような整数 m と n が与えられても、構造的帰納的に定義 MUL に従った m, n, p の関係にあるような整数 p が存在します。 次のコードは mul_istot の実装です: 

primplement
mul_istot{m,n}() = let
//
prfun istot
  {m:nat;n:int} .<m>. (): [p:int] MUL(m, n, p) =
  sif m > 0 then MULind(istot{m-1,n}()) else MULbas()
// end of [istot]
//
in
  sif m >= 0 then istot{m,n}() else MULneg(istot{~m,n}())
end // end of [mul_istot]

(implement ではなく) キーワード primplement は証明の実装の開始です。 内部の証明関数 istot は、与えられたどんな自然数 m と整数 n についても MUL に従った m, n, p の関係にあるような整数 p が存在することを示す証明をエンコードしています。 キーワード sif は条件が静的な式であるような (証明の) 条件式を作るのに使われます。 istot にエンコードされている証明は m についての帰納法によって進みます; もし m > 0 なら、m-1, n, p1 が (m-1 についての) 帰納法の仮定により関係しているような整数 p1 が存在し、したがって m, n, p は関係していて MULind にエンコードされた規則によれば p = p1+n です; もし m = 0 なら、m, n, p は関係していて p = 0 です。 mul_istot の実装にエンコードされている証明は次のようなものです: もし m が自然数なら、istot で 証明された補題が m, n, p が関係していることを示しています; もし m が負の数なら、同じ補題がなんらかの整数 p1 について ~m, n, p1 が関係していることを示していて、したがって m, n, p は関係していて MULneg にエンコードされた規則によれば p = ~p1 です。

ATS/LF における定理証明の別の例として、 次のような mul_isfun という名前の証明関数を見てみましょう: 

prfn mul_isfun
  {m,n:int}{p1,p2:int}
(
  pf1: MUL(m, n, p1), pf2: MUL(m, n, p2)
) : [p1==p2] void = let
  prfun isfun
    {m:nat;n:int}{p1,p2:int} .<m>.
  (
    pf1: MUL(m, n, p1), pf2: MUL(m, n, p2)
  ) : [p1==p2] void =
    case+ pf1 of
    | MULind(pf1prev) => let
        prval MULind(pf2prev) = pf2 in isfun (pf1prev, pf2prev)
      end // end of [MULind]
    | MULbas() => let
        prval MULbas() = pf2 in ()
      end // end of [MULbas]
  // end of [isfun]
in
  case+ pf1 of
  | MULneg(pf1nat) => let
      prval MULneg(pf2nat) = pf2 in isfun (pf1nat, pf2nat)
    end // end of [MULneg]
  | _ (*non-MULneg*) =>> isfun (pf1, pf2)
end // end of [mul_isfun]

キーワード prfn は再帰的ではない証明関数を定義するために使われます。 またキーワード prval は証明の式、つまり命題型の式に関連する名前を束縛します。 網羅的なパターンマッチの範囲では、prval は val+ と等価です (証明はパターンマッチの失敗のような作用を含むことができません)。

mul_isfun が証明しているのは、関係 MUL が最初の2つの引数について関数的だということです: もし m, n, p1 が MUL によって関係していて、m, n, p2 もまた MUL によって関係しているなら、p1 と p2 は等しくなります。 これは、m が自然数であるという仮定で内部の証明関数 isfun によって最初に証明されます。 そしてその後この仮定は破棄されます。 ここで isfun の本体で1番目にマッチする節を見てみましょう。 もしこの節が選択されたら、 pf1 はパターン MULind(pf1prev) にマッチし、従って pf1prev の型は自然数 m1 と 整数 n1, p1 があるとき MUL(m1, n1, q1) になります。 そして m=m1+1, n=n1, p1=q1+n1 であるような整数 p1 が存在します。 これは m2+1=m, n2=n, p2=q2+n2 のような型 MUL(m2, n2, q2) の pf2prev があるとき、 pf2 が MULind(pf2prev) でなければならないことを意味しています。 pf1prev と pf2prev について isfun を呼び出すし、 m-1 における帰納法の仮定を使うと、q1=q2 を証明でき、これは p1=p2 を示しています。 isfun の本体で2番目にマッチする節はたやすく理解できるでしょう。 これは isfun にエンコードされた帰納的証明の基底部に相当します。

PrevHomeNext
ATS/LF を使った定理証明Up例: 乗法の分配法則