型検査中での制約解決

ATS における型検査は制約の生成と解決を引き起こします。 例えば、次のコードはよく知られた階乗関数を実装しています:

この実装では、関数 fact には次の型が割り当てられています: これは、fact は自然数 n に適用されると自然数 r を返すことを意味しています。 このコードが型検査されるとき、次の制約が解決される必要があります:

• それぞれの自然数 n について、n > 0 が n - 1 >= 0 の意味を含む

• それぞれの自然数 n とそれぞれの自然数 r₁ について、n > 0 が n * r₁>= 0 の意味を含む

• それぞれの自然数 n について、常に 1 >= 0 である

1番目の制約は、呼び出し fact(x-1) によって生成されています。 x-1 が自然数であることが要求されているからです。 2番目の制約は、 fact(x-1) が自然数であるという仮定の下で、x * fact(x-1) が自然数であるかどうか検証することで生成されています。 3番目の制約は、1 が自然数であるかどうか検証することで生成されています。 1番目と3番目の制約は ATS の制約ソルバによってたやすく解決できます。 この手法は Fourier-Motzkin 変数消去法にもとづいています。 けれども、2番目の制約は線形ではないため制約ソルバで取り扱うことができません。 この制約は、線形でない項 (n*r₁) が存在するために、線形整数プログラミングの問題に変形できないのです。 ATS の制約ソルバは非線形の制約を自動的に取り扱うことはできませんが、証明を明示的に構築することでプログラマはそれらを検証することができます。 精巧にそして明示的に構築する証明については別の章で紹介します。

初期設定では、ATS/Postiats で実装されている制約ソルバは標準の任意精度演算を用いています。 効率の理由で、整数の制約の解決にマシンレベル演算を使うこともまた選択できます。 演算のオーバーフローの可能性があるため、 マシンレベル演算を使う制約ソルバが返す結果は不正確である可能性があります。 (しかし今までのところ実際にはそのような状況に遭遇したことはありません。)