Program separation and definitional higher order programming

We describe a program separation scheme based on the notions of form and content of an algorithm. The content of an algorithm consists of all local operations needed to compute the algorithm on the basis of a given definition. Separating an algorithm can thus be described as the process of finding definitions such that the algorithm is locally definable. The form of the algorithm then gives the global structure of the algorithm.

The scheme is given in a definitional context, and we show how this type of program separation can be used as a basis for definitional higher order programming.