ATS には、再帰的に定義された関数の停止性を検査するための停止性メトリクス (termination metrics) をプログラマ自身で提供できるような、メカニズムがあります。 すぐに明らかになることですが、この停止性検査のメカニズムは ATS/LF のデザインにおいて基礎的な役割を果たします。 この ATS/LF は ATS における定理証明サブシステムで、その証明は全域関数プログラムとして構成されます。
停止性メトリクスは自然数の単純なタプルで、 そのタプルの順序には標準の自然数の辞書順が使われます。 次の例では、再帰関数 fact が停止するか検査するために、シングルトンメトリクス (singleton metric) n を与えています。 このとき n は 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]
別の例として、次のコードはアッカーマン関数を実装しています。 この関数は原始再帰関数でない再帰として有名です:
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]
相互再帰関数の停止性検査も同様です。 次の例では、isevn と isodd が相互再帰的に定義されています:
isevn と isodd の停止性を検査するために与えられたメトリクスはそれぞれ 2*n と 2*n+1 です。 このとき n は isevn の整数引数の値であり、さらにまた isodd の整数引数の値です。 isevn と isodd に (n, 0) と (n, 1) のメトリクスを与えれば、これら2つの関数の停止性もまた検査できることは明白です。 相互再帰的に定義された関数のメトリクスは同じ長さのタプルであることが要求されることに注意してください。