ATS におけるいくつかの形式の証明をこれまで紹介してきました。けれども、そのような証明を構築することは、ATSにおいて最重要ではありません。もし私が Isabelle や Coq のような定理証明システムと ATS を比較するとしたら、ATS における定理証明のデザインは定理証明に対する視点が根本的に異なることを指摘したいと思います。特に、ATS における定理証明は、定理を公理や法則の最小集合の正当性に変換することで、その正当さを立証するような基礎的なアプローチを取りません。その代わりに、ATS での定理証明は準形式的な作法で行なわれ、その主眼は、間違った仮定や要求をプログラマが使ってしまう可能性を大きく減少させることです。この点において、ATS の定理証明は (数学その他における) 紙とペンによる非形式的な証明の構築に似ています。私は ATS における定理証明のこのスタイルをプログラマ中心であると呼んでいます。このような定理証明のスタイルがどのようなものなのか、読者により具体的な実感を得てもらうために、この章では単純かつ有用なプログラマ中心の定理証明の例を示します。
有理数の二乗が2に等しくないことを証明することを想像してみましょう。この表明は、2の平方根が有理数でない表明より少し弱いことに注意してください。後者は2の平方根の存在を仮定しています。はじめに、次のような非形式的な証明をスケッチしてみましょう。
なんらかの正の数 m と n について、(m/n)2=2 を考えます。これは (m)2=2(n)2 を意味し、m は偶数であることを暗示しています。m=2m2 としてみると、(2m2)2=2(n)2 が得られ、これは (n/m2)2=2 を暗示しています。明確に、m > n > m2 ということになります。なんらかの n について (m/n)2=2 を満たすような最小の正の数を m と仮定すると、n は m と同じ特性を持つことになり、矛盾が生じます。従って、二乗が2に等しくなる有理数は存在しません。数2を別の素数で置き換えてもこの証明は成立することも明確です。
上記の非形式的な証明における主な論拠は、ATS では次のようにエンコードできます:
// extern prfun mylemma_main {m,n,p:int | m*m==p*n*n}(PRIME(p)): [m2:nat | n*n==p*m2*m2] void // primplmnt mylemma_main {m,n,p}(pfprm) = let prval pfeq_mm_pnn = eqint_make{m*m,p*n*n}() prval () = square_is_nat{m}() prval () = square_is_nat{n}() prval () = lemma_PRIME_param(pfprm) prval pfmod1 = lemma_MOD0_intr{m*m,p,n*n}() prval pfmod2 = mylemma1{m,p}(pfmod1, pfprm) prval [m2:int] EQINT() = lemma_MOD0_elim(pfmod2) prval EQINT() = pfeq_mm_pnn prval () = __assert{p}{p*m2*m2,n*n}() where { extern prfun __assert{p:pos}{x,y:int | p*x==p*y}(): [x==y] void } (* end of [where] *) // end of [prval] in #[m2 | ()] end // end of [mylemma_main] //
2つの整数 m と p が与えられたとき、MOD0(m,p) はなんらかの自然数 q について、m が p と q の積に等しいことを意味するとします。この意味は次の2つの証明関数にエンコードできます:
// prfun lemma_MOD0_intr{m,p,q:nat | m==p*q}(): MOD0(m, p) // prfun lemma_MOD0_elim{m,p:int}(MOD0(m, p)): [q:nat] EQINT(m, p*q) //
// prfun lemma_PRIME_param{p:int}(PRIME(p)): [p >= 2] void // prfun mylemma1{n,p:int}(MOD0(n*n, p), PRIME(p)): MOD0(n, p) //
mylemma_main の実装において次の宣言が不可解だ、という人がいるかもしれません:
pfeq_mm_pnn は命題 EQINT(m*m, p*(n*n)) であることに注意してください。また、上記の宣言が型検査された時点で、なんらかの自然数 m2 について m が p*m2 に等しいことになります。これは、上記の宣言が型検査された後で、(p*m2)2 と p*(n)2 が等しいことを静的な仮定に追加することを意味しています。二乗が2に等しくなる有理数が存在しないことをエンコードした証明全体は オンライン から入手できます。