In this article, I present two styles of theorem-proving in ATS, illustrating through concrete examples the key relation between the two fundamentally different sorts bool and prop. For the entirety of the code used in this presentation, please see the file bool-vs-prop.dats.
Let us start with an example. A function fib can be specified as follows for computing Fibonacci numbers:
fib(0) = 0 fib(1) = 1 fib(n+2) = fib(n) + fib(n+1) for n >= 0The following code gives a direct implementation of this specified function in ATS:
fun fib ( n: int ) : int = if n >= 2 then fib (n-2) + fib (n-1) else n // end of [fib]Clearly, this is a terribly inefficient implementation of exponential time-complexity. An implementation of fib in C is given as follows that is of linear time-complexity:
int
fibc (int n) {
int tmp, f0 = 0, f1 = 1 ;
while (n-- > 0) { tmp = f1 ; f1 = f0 + f1 ; f0 = tmp ; } ; return f0 ;
} // end of [fibc]
If translated into ATS, the function fibc can essentially be
implemented as follows:
fun fibc ( n: int ) : int = let fun loop (n: int, f0: int, f1: int) = if n > 0 then loop (n-1, f1, f0+f1) else f0 // end of [loop] in loop (n, 0, 1) end // end of [fibc]There is obviously a logic gap between the definition of fib and its implementation as is embodied in fibc.
In ATS, an implementation of fib can be given that completely bridges this gap. In order to do so, the specification of fib needs to be encoded into ATS, which is fulfilled by the declaration of the following dataprop:
// dataprop fib_p(int, int) = | fib_p_bas0(0, 0) of () | fib_p_bas1(1, 1) of () | {n:nat}{r0,r1:int} fib_p_ind2(n+2, r0+r1) of (fib_p(n, r0), fib_p(n+1, r1)) //Note that fib_p is a prop constructor, where prop means type for proofs. Given two static integer terms N and R, fib_p forms the prop fib_p(N, R), which basically means that fib(N) equals R.
There is a predicate fib_b corresponding to fib_p:
// stacst fib_b : (int, int) -> bool //Given two static integer terms N and R, the boolean term fib_b(N, R) corresponds to the prop fib_p(N, R). Also, the following three proof functions correspond to the three proof constructors associated with fib_p:
// // Note: unit_p is the unit prop // extern praxi fib_b_bas0() : [fib_b(0, 0)] unit_p extern praxi fib_b_bas1() : [fib_b(1, 1)] unit_p extern praxi fib_b_ind2 {n:nat}{r0,r1:int}(): [fib_b(n, r0)&&fib_b(n+1, r1) ->> fib_b(n+2, r0+r1)] unit_p //The syntax for the interface assigned to fib_b_ind2 may need some explanation here: It basically states fib_b_ind2 being a proof function that asserts the conjunction of fib_b(n, r0) and fib_b(n+1, r1) implying fib_b(n+2, r0+r1) for any natural number n and integers r0 and r1.
The following code gives a verified implementation of the fib function specified above:
// extern fun f_fib_p {n:nat} (n: int(n)): [r:int] (fib_p(n, r) | int(r)) // implement f_fib_p{n}(n) = let // fun loop { i:nat | i < n } { r0,r1:int } ( pf0: fib_p(i, r0) , pf1: fib_p(i+1, r1) | i: int(i) , r0: int(r0), r1: int(r1) ) : [r:int] (fib_p(n,r) | int(r)) = let // in // if i+1 < n then loop(pf1, fib_p_ind2(pf0, pf1) | i+1, r1, r0+r1) else (pf1 | r1) // end // end of [loop] // prval pf0 = fib_p_bas0() prval pf1 = fib_p_bas1() // in if n >= 1 then loop(pf0, pf1 | 0, 0, 1) else (pf0 | 0) end // end of [f_fib_p] //The interface assigned to f_fib_p indicates that f_fib_p takes a natural number n to return an integer r paired with a proof of the prop fib_p(n, r). In other words, the integer returned from a call to f_fib_p on the natural number n always equals the value of fib defined on the number.
The style of theorem-proving in the implementation of f_fib_p is often labeled as being explicit as it makes explicit use of proofs. There is another style of theorem-proving supported in ATS that may be labeled as being implicit (due to its making no use of explicit proofs). For instance, the following code gives another verified implementaion of the fib function, where theorem-proving is done implicitly:
// extern fun f_fib_b {n:nat} (n: int(n)) : [r:int] (fib_b(n, r) && int(r)) // implement f_fib_b{n}(n) = let // prval() = $solver_assert(fib_b_bas0) prval() = $solver_assert(fib_b_bas1) // fun loop { i:nat | i < n } { r0,r1:int | fib_b(i,r0); fib_b(i+1,r1) } ( i: int(i) , r0: int(r0), r1: int(r1) ) : [r:int | fib_b(n,r)] int(r) = let // prval() = $solver_assert(fib_b_ind2{i}) // in // if i+1 < n then loop(i+1, r1, r0+r1) else r1 // end // end of [loop] // in if n >= 1 then loop(0, 0, 1) else 0 end // end of [f_fib_b] //Applying the keyword $solver_assert to a proof indicates the need to turn the prop of the proof into a static boolean term (of the same meaning) and then add the term as an assumption (to be used by the underlying constraint-solver for solving the subsequent constraints generated in the same scope). The first and second calls to $solver_assert add fib_b(0, 0) and fib_b(1, 1), respectively. The third one adds the following assumption:
{r0,r1:int} fib_b(i, r0)&&fib_b(i+1, r1) ->> fib_b(i+2, r0+r1)
which states that the conjunction of fib_b(i, r0) and
fib_b(i+1, r1) implies fib_b(i+2, r0+r1) for
every pair of integers r0 and r1. Please note that
i is a free variable and it is not quantified here.
Currently, the constraints generated from typechecking the implementation of f_fib_b cannot be solved by the built-in constraint-solver of ATS/Postiats. One option is to first export these constraints and then invoke the command patsolve_z3 to solve them, where patsolve_z3 is a utility for employing Z3 to solve constraints generated from typechecking ATS source. Please find more details in the provided Makefile.
Which style of theorem-proving is preferred: explicit or implicit? It really depends on what needs to be proven. My personal opinion is to use the latter for "easy" stuff while the former for more "difficult" stuff. I strongly encourage a non-expert to first try theorem-proving of explicit style.
This article is written by Hongwei Xi.