Lambda the Ultimate

Abstract: Array theory combines APL with set theory, transfinite arithmetic, and operationally transformed functions to produce an axiomatic theory in which the theorems hold for all arrays having any finite number of axes of arbitrary countable ordinal lengths. The items of an array are again arrays. The treatment of ordinal numbers and letters is similar to Quine's treatment of individuals in set theory. The theory is developed first as a theory of lists. This paper relates the theory to the eight axioms of Zermelo-Fraenkel set theory, describes the structure of arrays, interprets empty arrays in terms of vector spaces, presents a system of axioms for certain properties of operations related to the APL function of reshaping, deduces a few hundred theorems and corollaries, develops an algebra for determining the behavior of operations applied to empty arrays, begins the axiomatic development of a replacement operator, and provides an informal account of unions. Cartesian products, Cartesian arrays, and outer, positional, separation, and reduction transforms.

Preamble: The intention of the work reported here is to develop a theory of arrays, in terms of standard set theory, that will provide rigorous definitions for programming operations and thereby a logical foundation for the construction of programming languages. The present contribution is a first approach to establishing a comprehensive theory of arrays, and it is anticipated that future papers will extend and refine the concepts presented.

The objects used in programming are represented in a mathematical system of ordered collections as arrays of arrays. Simple axioms define certain primitive operations on the arrays. Most data operations in programming can then be represented by operations built upon the axioms. One of the starting points for the development of the theory is APL. Programs written in APL are used to generate corollaries of the axioms and to check the consistency of the system.

Although the paper was written for the specialist in mathematical logic, it should be of interest to the computer scientist and particularly to one who specializes in programming languages. Its chief contribution is an axiomatic theory for data structures, which includes explicit rules for transforming any operation into a new operation that applies to all items in any array.