2.5.1 Using J for Proofs

Iverson and others have written several books which use J to describe a number of computing related topics. One of these [Iv 95] uses J in a rather formal way to express algorithms and proofs of topics covered in [Gr 89]. Following is an example from the introduction of [Iv 95].

A theorem is an assertion that one expression l is equivalent to another r. We can express this relationship in J as:

t=: l -: r

This is the same as saying that l must match r, that is, t must be the constant function 1 for all inputs. T is sometimes called a tautology. For example, suppose

l =: +/ @ i.     NB. Sum of integers
r =: (] * ] - 1:) % 2:

If we define n =: ] , the right identity function, the we can rewrite the last equations as:

r =: (n * n - 1:) % 2:

Next,

t =: l -: r

Notice that by experimentation, t seems to always be 1 no matter what input argument is used.

   t 1 2 3 4 5 6 7 8 9
1 1 1 1 1 1 1 1 1

A proof of this theorem is a sequence of equivalent expressions which leads from l to r.

l
+/ @ i.                            Definition of l
+/ @ |. i.                         Sum is associative and commutative
                                   (|. is reverse)
((+/ @ i.) + (+/ @ |. @ i.)) % 2:  Half sum of equal values
+/ @ (i. + |. @ i.) % 2:           Summation distributes over addition
+/ @ (n # n - 1:) % 2:             Each term is n -1; there are n terms
(n * n - 1:) % 2:                  Definition of multiplication
r                                  Definition of r

Of course, each expression in the above proof is a simple program and the proof is a sequence of justifications which allow transformation of one expression to the next.