Introduction to Programming in ATS:
<<< PreviousProgramming with Theorem-ProvingNext >>>

Example: Safe Matrix Subscripting

Internally, a matrix of the dimension m by n is represented as an array of the size m*n. For matrix subscripting, we need to implement a function template of the following interface: 

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

Assume that the matrix is row-major. Then the element indexed by i and j in the matrix is the element indexed by i*n + j in the array that represents the matrix, where i and j are natural numbers less than m and n, respectively. However, the following implementation fails to pass typechecking: 

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

as the ATS constraint solver cannot automatically verify that i*n+j is a natural number strictly less than m*n. An implementation of matget that typechecks can be given as follows: 

implement{a}
matget {m,n} {i,j} (A, n, i, j) = let
//
  val (pf_in | _in) = i imul2 n // pf_in: MUL (i, n, _in)
  prval () = mul_nat_nat_nat (pf_in) // _in >= 0
//
  prval pf_mn = mul_istot {m,n} () // pf1_mn: MUL (m, n, _mn)
  prval () = mul_elim (pf_mn) // _mn = m*n
  prval MULind (pf_m1n) = pf_mn // _m1n = (m-1)*n = m*n-n
//
  stadef i1 = m-1-i
  prval pf_i1n = mul_istot {i1,n} () // pf_i1n: MUL (i1, n, _i1n)
  prval () = mul_nat_nat_nat (pf_i1n) // _i1n >= 0
//
  prval pf2_m1n = mul_distribute2 (pf_in, pf_i1n) // _m1n = _in + _i1n
  prval () = mul_isfun (pf_m1n, pf2_m1n) // _mn - n = _in + _i1n 
//
in
  A[_in+j]
end // end of [matget]

where the functions called in the body of matget are assigned the following interfaces: 

fun imul2 {i,j:int}
  (i: int i, j: int j): [ij:int] (MUL (i, j, ij) | int ij)

prfun mul_istot {i,j:int} (): [ij:int] MUL (i, j, ij)

prfun mul_isfun {i,j:int} {ij1, ij2: int}
  (pf1: MUL (i, j, ij1), pf2: MUL (i, j, ij2)): [ij1==ij2] void

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_distribute2
  {i1,i2:int} {j:int} {i1j,i2j:int}
  (pf1: MUL (i1, j, i1j), pf2: MUL (i2, j, i2j)): MUL (i1+i2, j, i1j+i2j)

Note that the keyword stadef is for introducing a binding between a name and a static term (of any sort). Assume that m and n are natural numbers and i and j are natural numbers less than m and n, respectively. The method employed in the implementation of matget to show i*n+j < m*n essentially proves that m*n = (m-1)*n + n, (m-1)*n = i*n + (m-1-i)*n and (m-1-i)*n >= 0, which in turn imply that m*n >= i*n+n > i*n+j.

Note that there are a variety of proof functions declared in prelude/SATS/arith.sats for helping prove theorems involving arithmetic operations. For examples of proof construction in ATS, please find the implementation of some of these proof functions in prelude/DATS/arith.dats.

The entirety of the above presented code is available on-line.

<<< PreviousHomeNext >>>
Programming with Theorem-ProvingUpSpecifying with Enhanced Precision