Introduction to Programming in ATS:
<<< Previous		Next >>>

Theorem-Proving in ATS/LF

Within the ATS programming langauge system, there is a component named ATS/LF for supporting (interactive) therorem-proving. In ATS/LF, theorem-proving is done by constructing proofs as total functional programs. It will soon become clear that this style of theorem-proving can be combined cohesively with functional programming to yield a programming paradigm that is considered the signature of ATS: programming with theorem-proving. Moreover, ATS/LF can be employed to encode various deduction systems and their meta-properties.

Please find on-line the code employed for illustration in this chapter plus some additional code for testing.

Encoding Relations as Dataprops

In the statics of ATS, there is a built-in sort prop for static terms that represent types for proofs. A static term of the sort prop can also be referred to as a type or more accurately, a prop-type or just a prop. A dataprop can be declared in a manner that is mostly similar to the declaration of a datatype. For instance, a prop construct FIB is introduced in the following dataprop declaration:

dataprop FIB (int, int) =
  | FIB0 (0, 0) of () // [of ()] can be dropped
  | FIB1 (1, 1) of () // [of ()] can be dropped
  | {n:nat} {r0,r1:nat}
    FIB2 (n+2, r0+r1) of (FIB (n, r0), FIB (n+1, r1))
// end of [FIB]

The sort assigned to FIB is (int, int) -> prop, indicating that FIB takes two static integers to form a prop-type. There are three data (or proof) constructors associated with FIB: FIB0, FIB1 and FIB2, which are assigned the following function types (or more accurately, prop-types):

FIB0: () -> FIB (0, 0)
FIB1: () -> FIB (1, 1)
FIB2: {n:nat} {r0,r1:int} (FIB(n, r0), FIB(n+1, r1)) -> FIB(n+2, r0+r1)

Given a natural number n and an integer r, it should be clear that FIB(n, r) encodes the relation fib(n) = r, where fib is defined by the following three equations:

fib(0) = 0, and
fib(1) = 1, and
fib(n+2) = fib(n+1) + fib(n) for n >= 2.

A proof value of the prop FIB(n, r) can be constructed if and only if fib(n) equals r. For instance, the proof value FIB2(FIB0(), FIB1()) is assigned the prop FIB(2, 1), attesting to fib(2) equaling 1.

As another example of dataprop, the following declaration introduces a prop constructor MUL together with three associated proof constructors:

dataprop MUL (int, int, int) =
  | {n:int} MULbas (0, n, 0) of ()
  | {m:nat} {n:int} {p:int}
    MULind (m+1, n, p+n) of MUL (m, n, p)
  | {m:pos} {n:int} {p:int}
    MULneg (~m, n, ~p) of MUL (m, n, p)
// end of [MUL]

Given three integers m, n and p, the prop MUL(m, n, p) encodes the relation m*n = p. As for MULbas, MULind and MULneg, they correspond to the following three equations, respectively:

0*n = 0 for every integer n, and
(m+1)*n = m*n + n for each pair of integers m and n, and
(~m)*n = ~(m*n) for each pair of integers m and n.

In other words, the dataprop declaration for MUL encodes the relation that represents the standard multiplication function on integers.

It can be readily noticed that the process of encoding a functional relation (i.e., a relation representing a function) as a dataprop is analogous to implementing a function in a logic programming language such as Prolog.

<<< Previous	Home	Next >>>
Example: Functional Red-Black Trees	Up	Constructing Proofs as Total Functions