再帰関数の停止性検査

ATS には、再帰的に定義された関数の停止性を検査するための停止性メトリクス (termination metrics) をプログラマ自身で提供できるような、メカニズムがあります。 すぐに明らかになることですが、この停止性検査のメカニズムは ATS/LF のデザインにおいて基礎的な役割を果たします。 この ATS/LF は ATS における定理証明サブシステムで、その証明は全域関数プログラムとして構成されます。

停止性メトリクスは自然数の単純なタプルで、 そのタプルの順序には標準の自然数の辞書順が使われます。 次の例では、再帰関数 fact が停止するか検査するために、シングルトンメトリクス (singleton metric) n を与えています。 このとき nfact の整数引数の値です:

fun fact {n:nat} .<n>. (x: int n): int = if x > 0 then x * fact (x-1) else 1 // end of [fact]

再帰呼び出し fact(x-1) に付随したメトリクスは n-1 であり、これは最初のメトリクス n よりも小さいことに注意してください。 本質的に、ATS における停止性検査とは、関数の本体にあるそれぞれの再帰呼び出しに付随するメトリクスが、その関数の当初のメトリクスよりも必ず小さくなること検証することです。

より難しくまた興味深い例は、次のマッカーシーの91関数 (MacCarthy's 91-function) の実装です:

fun f91 {i:int} .<max(101-i,0)>. (x: int i) : [j:int | (i < 101 && j==91) || (i >= 101 && j==i-10)] int (j) = if x >= 101 then x-10 else f91 (f91 (x+11)) // end of [f91]

f91 の停止性を証明するために与えられたメトリクスは max(101-i,0) です。 このとき if91 の整数引数の値です。 このメトリクスが f91 の停止性検証するのに十分であるかどうか、手で検証してみてください。

別の例として、次のコードはアッカーマン関数を実装しています。 この関数は原始再帰関数でない再帰として有名です:

fun acker {m,n:nat} .<m,n>. (x: int m, y: int n): Nat = if x > 0 then if y > 0 then acker (x-1, acker (x, y-1)) else acker (x-1, 1) else y + 1 // end of [acker]

acker の停止性検証のために与えられたメトリックはペア (m,n) です。 このとき mnacker の2つの整数引数の値です。 acker への3つの再帰呼び出しに付随するメトリクスは、左から右に (m-1,k), (m,n-1), (m-1,1) です。 このとき k はなんらかの自然数です。 自然数のペアを辞書順によれば、これらのメトリクスは初期のメトリクス (m,n) よりも小さくなっていることは明白です。

相互再帰関数の停止性検査も同様です。 次の例では、isevnisodd が相互再帰的に定義されています:

fun isevn {n:nat} .<2*n>. (n: int n) : bool = if n = 0 then true else isodd (n-1) and isodd {n:nat} .<2*n+1>. (n: int n) : bool = not (isevn (n))

isevnisodd の停止性を検査するために与えられたメトリクスはそれぞれ 2*n2*n+1 です。 このとき nisevn の整数引数の値であり、さらにまた isodd の整数引数の値です。 isevnisodd(n, 0)(n, 1) のメトリクスを与えれば、これら2つの関数の停止性もまた検査できることは明白です。 相互再帰的に定義された関数のメトリクスは同じ長さのタプルであることが要求されることに注意してください。