On the Representation of Data Structures in LCF with Applications to Program Generation.

摘要

In this paper techniques of exploiting the obvious relationship between program structure and data structure for program generation are discussed. Methods of program specification are developed that are derived from a representation of recursive data structures in the Logic for Computable Functions (LCF). As a step towards a formal problem specification language we define definitional extensions of LCF. These include a calculus for (computable) homogeneous sets and restricted quantification. Concepts that are obtained by interpreting data types as algebras are used to derive function definition schemes from a LCF term representing a data structure; they also lead to techniques for the simplification of expressions in the extended language. The specification methods are illustrated with a detailed example. (Author)