Matrix Transpose - FAQ

Matrix Representation
For the purposes of this project, matrices will be represented by lists of lists. To be more specific, a matrix will be a represented list in which each element represents a row of the matrix. Each row in the representation will be the list of elements in the corresponding row of the matrix. The (i,j)-th element of a matrix is the j-th element in the i-th list in the representation of the matrix.

Examples
     a matrix with three rows and four columns and its representation
    1  2  3  4
    5  6  7  8     ((1 2 3 4) (5 6 7 8) (9 12 11 12))
    9 10 11 12

     a matrix with four rows and three columns and its representation
    1  5  9
    2  6 10      ((1 5 9) (2 6 10) (3 7 11) (4 8 12))
    3  7 11
    4  8 12

A matrix with m rows and n columns is said to be an m-by-n matrix. This project will deal only with rectangular matrices -- that is, matrices in which all rows have the same number of elements. In an m-by-n matrix, all m rows contain exactly n elements. The number of lists in the representation of a matrix is, of course, the number of rows in the matrix. So, there are m lists in the representation of an m-by-n matrix, and each of those lists has exactly n elements.

By convention, we allow 0-by-0 matrices, but we do not allow 0-by-n matrices or n-by-0 matrices where n is not zero. That is, an m-by-n matrix exists if and only if neither m nor n is zero or both m and n are zero.

A 0-by-0 matrix is represented by NIL (the empty list). One consequence of the convention that prohibits non-empty matrices with empty rows is that NIL cannot be a member of a non-empty list representing a matrix. However, the list ((NIL NIL) (NIL NIL) (NIL NIL)) represents a 3-by-2 matrix in which all elements have the value NIL. Any ACL2 atom or cons-pair can be an element of a matrix.

Matrix Transpose
The rows of a matrix are the columns of its transpose. That is, the (j,i)-th element of the transpose of a matrix A is the (i,j)-th element of A. In the above examples, the 3-by-4 matrix is the transpose of the 4-by-3 matrix, and vice versa.

Requirements

1. matrix?   The formula (matrix? X) delivers something other than NIL if X represents a matrix and NIL if X does not represent a matrix.
2. num-rows   The formula (num-rows X) delivers the number of rows in the matrix represented by X.
3. num-cols   The formula (num-cols X) delivers the number of columns in the matrix represented by X.
4. transpose   The formula (transpose X) delivers the representation of the transpose of the matrix that X represents.

Properties
State the following theorems in ACL2 notation, and use "The Method" to get ACL2 to prove at least one of them.

1. The value delivered by (transpose X) is a matrix whenever X is a matrix.
2. The number of rows in  (transpose X)  is the number of columns in X.
3. The number of columns in  (transpose X)  is the number of rows in X.

Performance
Demonstrate that transpose can successfully deliver the transpose of a 400-by-400 matrix in a reasonable time (under a minute, say, and you may be able to do much better than that), and of course without a mechanical breakdown, such as a stack overflow.

Don't display the transpose of a large matrix. Just invoke the operation and extract a small piece to display. Don't enter the matrix by hand, either. Find some other way to generate the representation of a 400-by-400 matrix.

You may be interested to know that functions meeting the performance requirements can be written in either nested or tail recursive form. It is, of course, also possible to write functions in either nested or tail recursive form that fail to meet the performance requirements.