Tabular Expressions and Total Functional Programming

Our research Group is developing methods of producing practical reference documentation for software products and components. Our document contents are defined by a relational model in which each document is required to be a representation of a specified relation. In effect, we are using mathematical descriptions of relations to provide specifications and descriptions of programs written in conventional languages. Key to making these documents readable is a multidimensional form of expressions, which we call tabular expressions. These parse complex expressions into arrays of simpler expressions allowing readers to “look up ” the information that they seek without understanding the whole expression. Tools that check and evaluate these expressions would be very useful when these methods are applied and we are looking for efficient implementations of such functions. Typed lambda calculus has been used as a foundational model of general mathematical expressions in early mechanized mathematics systems such as Automath, and in theorem provers such as Coq, HOL and Isabelle. We explore the application of this approach to interpret tabular expressions. Our approach is based on a simple functional definition language for tables, thei