Within the ATS programming language 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.

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:int} FIB2(n+2, r0+r1) of (FIB(n, r0), FIB(n+1, r1)) // end of [FIB]

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)

fib(0) = 0, and

fib(1) = 1, and

fib(n+2) = fib(n) + fib(n+1) for n >= 2.

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]

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.

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.