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

例: 安全な行列の添字演算

内部では、次元 m x n の行列はサイズ m*n の配列として表現されます。 行列の添字演算のために、次のインターフェイスの関数テンプレートを実装する必要があります: 

fun{
a:t@ype
} matrix_get
  {m,n:int}{i,j:nat | i < m; j < n}
  (A: arrayref (a, m*n), col: int n, i: int i, j: int j): (a)
// end of [matrix_get]

行列が行優先スタイルで表現されていると仮定しましょう。 すると、その行列の i と j で指定された要素は、その行列を表現する配列では i*n + j で指定されることになります。 ここで、i と j はそれぞれ m と n より小さい自然数です。 けれども、次の実装の型検査には失敗します: 

implement
{a}(*tmp*)
matrix_get (A, n, i, j) = A[i*n+j] // it fails to typecheck!!!

この推論失敗の簡単な理由は、i*n+j が m*n より正確に小さい自然数であることを、 ATS の制約ソルバが自動的に検査できないためです。 型検査を通る matrix_get の実装は次のようになります: 

implement
{a}(*tmp*)
matrix_get
  {m,n}{i,j}
  (A, n, i, j) = let
//
  val (pf | _in_) = imul2 (i, n)
//
  prval ((*void*)) = mul_elim(pf)
  prval ((*void*)) = mul_nat_nat_nat(pf)
  prval ((*void*)) = mul_gte_gte_gte{m-1-i,n}()
//
in
  A[_in_+j]
end // end of [matrix_get]

matrix_get の本体から呼び出される関数には次のインターフェイスが割り当てられています: 

//
fun
imul2{i,j:int}
  (int i, int j):<> [ij:int] (MUL(i, j, ij) | int ij)
//
prfun
mul_elim
  {i,j:int}{ij:int} (pf: MUL(i, j, ij)): [i*j==ij] void
//
prfun
mul_nat_nat_nat
  {i,j:nat}{ij:int} (pf: MUL(i, j, ij)): [ij >= 0] void
//
prfun
mul_gte_gte_gte
  {m,n:int | m >= 0; n >= 0} ((*void*)): [m*n >= 0] void
//

m と n が自然数で、i と j がそれぞれ m と n より小さい自然数であると仮定します。 i*n+j < m*n を示すために matrix_get の実装で用いられている証明コードは、 (m-1-i)*n >= 0 を証明しています。 これは明確に m*n >= i*n+n > i*n+j を暗示しています。

様々な証明関数が arith_prf.sats で宣言されていることに注意してください。 これらの証明は算術演算を含む定理を証明するのに役に立ちます。 ATSにおける証明の構成例として、arith_prf.dats にある証明関数の実装を参照してください。

この章のコード全体は オンライン から入手できます。

PrevHomeNext
定理証明によるプログラミングUp強化された正確性を使って明記する