Programming with Theorem Proving

The paradigm of programming with theorem proving is rich and broad, and it is probably the most innovative feature in ATS. We give an introduction to this paradigm by presenting a few examples, explaining some motivations behind programming with theorem proving as well as demonstrating a means to achieve it in ATS.

The following code implements a function that computes factorials: 

// non-tail-recursive
fun fact {n:nat} (n: int n): Nat =
  if n > 0 then n nmul fact (n-1) else 1
The type assigned to fact is 
{n:nat} int (n) -> Nat
That is, the function fact takes a nature number as its argument and, if it terminates, returns a natural number as its result.

Now suppose we want to be more accurate. We want to verify that the code indeed implements the factorial functions. One possibility is to specify the factorial function in the statics of ATS, and then try to assign the following type to fact: 

{n:nat} int (n) -> int (fact(n))
Note that the name fact is overloaded here to also refer to the factorial function in the statics of ATS. There is, however, a serious problem with this approach: If functions as complex as the factorial function could be specified in the statics of ATS, then it would no longer be possible to support fully automatic constraint-solving. We take a different approach instead.

With standard mathematical notation, the factorial function can be specified as follows: 

fact (0) = 1 ;
fact (n) = n * fact (n-1) ; if n > 0
In ATS, we can declare a dataprop to encode this specification: 
// [FACT (n, x)] is inhabited if and only if [fact (n) = x]
dataprop FACT (int, int) =
  | FACTbas (0, 1)
  | {n:int | n > 0} {r,r1:int}
    FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r))
The prop constructor MUL is already defined: Given integers p, q, and pq, MUL(p, q, pq) is inhabited if and only if the product of p and q is pq. The constructors FACTbas (base case) and FACTind (inductive case) correspond to the first and the second clauses in the above specification, respectively. Given integers n and r, the prop FACT(n, r) is inhabited if and only if the factorial of n equals r. Clearly, if a terminating function can be assgined the following type: 
{n:nat} int n -> [r:int] (FACT (n, r) | int r)
then this function must compute factorials. The code below implements such a function fact1: 
// [fact1] implements the factorial function in a non-tail-recursive manner
fun fact1 {n:nat} .< n >.
  (n: int n): [r:int] (FACT (n, r) | int r) =
  if n > 0 then
    let
       val (pf_fac_n1_r1 | r1) = fact1 (n-1)
       val (pf_mul_n_r1_r | r) = n imul2 r1
    in
       (FACTind (pf_fac_n1_r1, pf_mul_n_r1_r) | r)
    end
  else (FACTbas () | 1)
When applied to a natural number n, fact1 is guaranteed to return a pair (pf, r), where pf is a proof stating that the factorial of n is r. A crucial property of ATS is the irrelevance of proofs to program evaluation: The dynamic semantics of a program cannot be altered by erasing the proofs in it. So proofs are all erased after compilation and thus are not constructed at run-time.

This example clearly gives some impression of code duplication as the specification (FACT) and the implementation (fact1) are of great similarity to each other. We now present another example, where the specification and the implementation are far different from each other.

The following code gives another implementation of the factorial function, where only tail-recursion is involved: 

// tail-recursive
fn fact {n:nat} (n: int n): Nat =
  let
    fun loop {n:nat} (n: int n, res: Nat): Nat =
      if n > 0 then loop (n-1, n nmul res) else res
  in
    loop (n, 1)
  end
Base on this tail-recursive implementation, we implement as follows a function fact2 that is verified to compute factorials. 
// Some lemmas on multiplication are stated (without proofs)
extern prval MULlem00 : {x,y:int} () -<prf> [xy:int] MUL (x, y, xy)

// 1 * x = x
extern prval MULlem10 : {x,y:int} MUL (1, x, y) -<prf> [x==y] void
// x * 1 = x
extern prval MULlem11 : {x,y:int} MUL (x, 1, y) -<prf> [x==y] void

// multiplication is associative: (xy)z = x(yz)
extern prval MULlem20 : {x,y,z,xy,yz,xyz:int}
  (MUL (x, y, xy), MUL (y, z, yz), MUL (xy, z, xyz)) -<prf> MUL (x, yz, xyz)

// [fact2] implements the factorial function in a tail-recursive style
fn fact2 {n:nat} (n: int n): [r0: int] (FACT (n, r0) | int r0) =
  let
    // [loop] is tail-recusive
    fun loop {n:nat; x:int} .< n >. (n: int n, x: int x)
      : [r,r0:int] (FACT (n, r), MUL (x, r, r0) | int r0) =
      if n > 0 then let
        val (pf_mul_x_n_xn | xn) = x imul2 n
        val (pf_fac_n1_r1, pf_mul_xn_r1_r0 | res) = loop (n-1, xn)
        prval pf_mul_n_r1_nr1 = MULlem00 ()
        prval pf_mul_x_nr1_r0 = MULlem20 (pf_mul_x_n_xn, pf_mul_n_r1_nr1, pf_mul_xn_r1_r0)
        prval pf_fac_n_nr1 = FACTind (pf_fac_n1_r1, pf_mul_n_r1_nr1)
      in
        (pf_fac_n_nr1, pf_mul_x_nr1_r0 | res)
      end else let
        prval pf_mul_x_1_y = MULlem00 () // x * 1 = y
        prval () = MULlem11 (pf_mul_x_1_y) // x = y
      in
        (FACTbas (), pf_mul_x_1_y | x)
      end

    val (pf_fac, pf_mul | res) = loop (n, 1)
    prval () = MULlem10 (pf_mul)
  in
    (pf_fac | res)
  end
In practice, programming with theorem proving is commonly employed to capture program invariants that would otherwise not be possible in ATS. For instance, aided by programming with theorem proving, we can program a complex data structure like doubly-linked list or doubly-linked tree while having no fear of misusing pointers. This is considered a great strength of ATS.

The code used for illustration is available here.