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:

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]

Assume that the matrix is represented in the row-major style. 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}(*tmp*) matrix_get (A, n, i, j) = A[i*n+j] // it fails to typecheck!!!

The simple reason for this failure is due to the ATS constraint solver not being able to automatically verify that i*n+j is a natural number strictly less than m*n. An implementation of matrix_get that typechecks can be given as follows:

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]

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

// 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 //

Assume that m and n are natural numbers and i and j are natural numbers less than m and n, respectively. The proof code employed in the implementation of matrix_get to show i*n+j < m*n proves (m-1-i)*n >= 0, which clearly implies m*n >= i*n+n > i*n+j.

Note that there are a variety of proof functions declared in arith_prf.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 arith_prf.dats.

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