Differential Logic Programs: Programming Methodologies and Semantics

We introduce the notion of differential logic programs and we define an operator for composing them in a hierarchical fashion. The semantics of this composition operator is reminiscent of the semantics of inheritance in the object oriented paradigm. Similar to classes in that paradigm, differential programs can be organized in isa schemas where each component inherits or redefines, modifying them, the predicates defined in the components that are placed higher up in the schema. We demonstrate the use of this form of composition as a programming methodology that enhances reusability, code sharing and information hiding. We define a proof theory and a model theory for the composition of differential programs and we prove that the two theories coincide. We also define a compositional and fully abstract semantics for differential programs and we address the importance of this semantics as a formal tool for reasoning on the computational properties of differential programs and their composition. A preliminary version of this paper appeared in Bossi et al. (1993)