Introduction to Programming in ATS:
PrevChapter 12. Programming with Theorem-ProvingNext

Specifying with Enhanced Precision

The integer addition function can be assigned the following (dependent) type in ATS to indicate that it returns the sum of its two integer arguments: 

{i,j:int} (int(i), int(j)) -> int(i+j)

This type gives a full specification of integer addition as the only (terminating) function that can be given the type is the integer addition function. However, the factorial function, which yields the product of the first n positive integers when applied to a natural number n, cannot be given the following type: 

{n:int | n >= 0} int(n) -> int(fact(n))

as fact, which refers to the factorial function, does not exist in the statics of ATS. Evidently, a highly interesting and relevant question is whether a type can be formed in ATS that fully captures the functional relation specified by fact? The answer is affirmative. We can not only construct such a type but also assign it to a (terminating) function implemented in ATS.

Let us recall that the factorial function can be defined by the following two equations: 

fact(0) = 1
fact(n) = n * fact(n-1) (for all n > 0)

Naturally, these equations can be encoded by the constructors associated with the dataprop FACT declared as follows: 

dataprop
FACT(int, int) =
  | FACTbas(0, 1)
  | {n:nat}{r1,r:int}
    FACTind(n, r) of (FACT(n-1, r1), MUL(n, r1, r))
// end of [FACT]

Note that for any given natural number n and integer r, FACT(n, r) can be assigned to a proof if and only if fact(n) equals r. Therefore, the following type: 

{n:nat} int(n) -> [r:int] (FACT(n, r) | int(r))

can only be assigned to a function that, if applied to a natural number n, returns a proof and an integer such that the proof attests to the integer being equal to fact(n). For instance, the following defined function ifact is assigned this type: 

//
fun
ifact
{n:nat} .<n>.
(
  n: int(n)
) :<> [r:int] (FACT(n, r) | int r) =
(
//
if
n = 0
then (FACTbas() | 1)
else let
  val (pf1 | r1) = ifact (n-1) // pf1: FACT(n-1, r1)
  val (pfmul | r) = imul2 (n, r1) // pfmul: FACT(n, r1, r)
in
  (FACTind(pf1, pfmul) | r)
end // end of [else]
//
) (* end of [ifact] *)
//

After proof erasure, ifact precisely implements the factorial function.

Please find the entirety of the above presented code plus some testing code on-line.

PrevHomeNext
Example: Safe Matrix SubscriptingUpExample: Another Verified Factorial