ATSプログラミング入門:
PrevChapter 12. 定理証明によるプログラミングNext

強化された正確性を使って明記する

整数の加算関数には ATS では次のような依存型を割り当てることができます。 これはこの関数が2つの整数の引数の和を返すことを示しています: 

{i,j:int} (int (i), int (j)) -> int (i+j)

この型は整数の加算に対する完全な仕様です。この型を取るような停止する関数は、整数の加算関数だけです。 けれども、自然数 n に適用すると最初の n 個の正の整数の積を得るような、階乗関数には次のような型を与えることができません: 

{n:nat} int (n) -> int (fact(n))

階乗関数を指す fact は ATS の静的な部分には存在しないからです。 明らかに、大変興味深く適切な疑問は次のようなものでしょう。 fact で明記された関数的関係を完全に捕捉するような型を ATS で作れるのでしょうか？ その答は YES です。 そのような型をコンストラクトできるだけでなく、ATS で実装された停止する関数に適用することもできるのです。

階乗関数は次の2つの等式で定義できることを思い出してみましょう: 

fact(0) = 1
fact(n) = n * fact(n-1) (n > 0 のような全ての n について)

当然これらの等式は、次のように宣言される dataprop FACT に関連したコンストラクタでエンコードできます: 

dataprop
FACT(int, int) =
  | FACTbas(0, 1)
  | {n:nat}{r1,r:int}
    FACTind(n, r) of (FACT(n-1, r1), MUL(n, r1, r))
// end of [FACT]

与えられたどのような自然数 n と 整数 r についても、 fact(n) が r に等しいかどうか証明するために FACT(n, r) を割り当てられることに注意してください。 したがって、次のような型: 

{n:nat} int (n) -> [r:int] (FACT (n, r) | int (r))

は自然数 n に適用されると証明と整数を返すような関数にのみ割り当てることができます。 この証明はその整数が fact(n) に等しいことを立証しています。 例えば、次に定義された関数 ifact にはこの型が割り当てられています: 

//
fun
ifact
{n:nat} .<n>.
(
  n: int(n)
) :<> [r:int] (FACT(n, r) | int r) =
(
//
if
n = 0
then (FACTbas() | 1)
else let
  val (pf1 | r1) = ifact (n-1) // pf1: FACT(n-1, r1)
  val (pfmul | r) = imul2 (n, r1) // pfmul: FACT(n, r1, r)
in
  (FACTind(pf1, pfmul) | r)
end // end of [else]
//
) (* end of [ifact] *)
//

証明が削除されると、ifact は階乗関数の正確な実装になります。

この章で紹介したコードの全体とテストのための追加コードは オンライン から入手できます。

PrevHomeNext
例: 安全な行列の添字演算Up例: もう一つの検証された階乗