ATS プログラミング言語システムには、(対話的な) 定理証明をサポートする ATS/LF という名前の部品あります。 ATS/LF では、全域関数のプログラムとして証明をコンストラクトすることで定理証明は行なわれます。 この定理証明のスタイルは、関数型プログラミングと組み合わさってあるプログラミングパラダイムを産み出すことがすぐに明確になるでしょう。 このようなパラダイムを ATS では 定理証明を使ったプログラミング と呼んでいます。 その上、ATS/LF は様々な演繹システムとそれらのメタな性質をエンコードすることができます。
この章で解説するコードとテストのための追加コードは オンライン から入手できます。
ATS の静的な部分には、証明の型を表わす静的な項のためのビルトインの種 prop があります。 種 prop の静的な項は、型もしくはより正確に命題型や、単に命題と呼ばれます。 データ命題はデータ型の宣言とよく似た作法で宣言できます。 例えば、FIB をコンストラクトする証明は次のデータ命題宣言で導入できます:
dataprop FIB(int, int) = | FIB0(0, 0) of () // [of ()] can be dropped | FIB1(1, 1) of () // [of ()] can be dropped | {n:nat}{r0,r1:int} FIB2(n+2, r0+r1) of (FIB(n, r0), FIB(n+1, r1)) // end of [FIB]
FIB0: () -> FIB (0, 0)
FIB1: () -> FIB (1, 1)
FIB2: {n:nat}{r0,r1:int} (FIB(n, r0), FIB(n+1, r1)) -> FIB(n+2, r0+r1)
fib(0) = 0, and
fib(1) = 1, and
fib(n+2) = fib(n+1) + fib(n) for n >= 2.
データ命題の別の例として、次の宣言は命題コンストラクタ MUL と関連する3つの証明コンストラクタを導入しています:
dataprop MUL(int, int, int) = | {n:int} MULbas(0, n, 0) of () | {m:nat}{n:int}{p:int} MULind(m+1, n, p+n) of MUL(m, n, p) | {m:pos}{n:int}{p:int} MULneg(~(m), n, ~(p)) of MUL(m, n, p) // end of [MUL]
全ての整数 n について 0*n = 0 、かつ
整数 m と n のペアそれぞれについて (m+1)*n = m*n + n 、かつ
整数 m と n のペアそれぞれについて (~m)*n = ~(m*n)
関数的な関係 (例: 関数を表わす関係) をデータ命題にエンコードする過程は Prolog のような論理型プログラミング言語における関数の実装に類似していることにすぐに気が付くでしょう。