ATSプログラミング入門:
Prev	Chapter 9. 依存型入門	Next

例: 依存型を使ったデバッグ

x >= 0 の整数が割り当てられた時、x の平方根は i * i <= x を満たすような最大の整数 i になります。次のように平方根関数を二分探索法をもとに実装します:

fun
isqrt
(
  x: int
) : int = let
//
fun
search
(
  x: int, l: int, r: int
) : int = let
  val diff = r - l
in
  case+ 0 of
  | _ when diff > 0 => let
      val m = l + (diff / 2)
    in
      // x < m * m can overflow easily
      if x / m < m
        then search (x, l, m) else search (x, m, r)
      // end of [if]
    end // end of [if]
  | _ (* diff <= 0 *) => l (* the result is found *)
end // end of [search]
//
in
  search (x, 0, x)
end // end of [isqrt]

この実装は型検査を通りますが、実行すると無限ループにおちいってしまいます。一般的なデバッグ手法 (例: プリント関数呼び出しを埋め込む) を使う代わりに、依存型を使って関数 search の停止性を証明して、無限ループの原因を特定してみることにしましょう。関数 search には関数型 (int, int, int) -> int が割り当てられています。これは search が3つの整数を引数に取り、1つの整数を返すことを意味しています。このような非依存型からその他の情報が得られないことは明確です。けれども、もし実装が正しければ関数 search は次の不変条件を持つべきだと、プログラマは思うでしょう:

search(x, l, r) が呼び出された時、l * l <= x かつ x <= r * r です。
整数 x, l, r について l * l <= x < r * r を仮定します。 search(x, l, r) の本体で整数 l1 と r1 について再帰関数 search(x, l1, r1) を呼び出すと、r1-l1 < r-l です。この不変条件は search が停止することを示しています。

1番目の不変条件は ATS の型システムで表現できるにもかかわらず、非線形な制約を取り扱う必要があるためにいくぶん複雑です。その代わりに、次の依存型の関数として search を定義してみましょう:

{x:nat} {l,r:nat | l < r} .<r-l>. (int(x), int(l), int(r)) -> int

search(x, l, r) が呼び出される時、より弱い不変条件である l < r を取ります。関数 search の停止性を検証するために停止性メトリクス .<r-l>. を与えます。 search に依存型の関数型を割り当てると、型検査で見つかるエラーに対して関数本体を修正する必要があります。次のコードは型検査を通るように適切な修正を施したものです:

fun
isqrt
{x:nat}
(
  x: int x
) : int = let
//
fun
search
{x,l,r:nat | l < r} .<r-l>.
(
  x: int x, l: int l, r: int r
) : int = let
  val diff = r - l
in
  case+ 0 of
  | _ when diff > 1 => let
      val m = l + half(diff)
    in
      if x / m < m
        then search (x, l, m) else search (x, m, r)
      // end of [if]
    end // end of [if]
  | _ (* diff <= 1 *) => l (* the result is found *)
end // end of [search]
//
in
  if x > 0 then search (x, 0, x) else 0
end // end of [isqrt]

r-l が 1 等しい時に search(x, l, r) が呼び出されると、以前の search 実装における無限ループが発生するのではないか、ということが明らかになりました。この呼び出しは同じ引数で別の search 呼び出しを引き起こしてしまう可能性があります。けれども、search に前述の依存型の関数型が割り当てた後では、そのような呼び出しは型エラーになります。

正確であろうとし、また効果的に正確さを強制できることで、実行時デバッグの必要性はどんどん小さくなることに、プログラマは確実に気が付くでしょう。

Prev	Home	Next
再帰関数の停止性検査	Up	データ型の改良