PhD Thesis

Dipartimento di Informatica e Scienze dell'Informazione

Relationships between Logical Frameworks

PhD thesis, Universities of Genova, Pisa and Udine, 1993. Available as internal report of Pisa University, TD-4/93.

Formal specifications are widely considered an important tool in software specification, design and implementation. As a result both of theoretical investigations and of preliminary attempts at applications, a variety of specification formalisms have been considered. This fragmentation of frames is conflicting with some essential requirements of any specification formalism, ie the ability of supporting modularity and refinement, which are clearly related to the problem of reuse of specifications. The central theme of this thesis is the independence of specifications and results from the logical formalisms in which they are formulated.
A concrete motivating example of the need for a formal tool allowing translation and comparison of specifications defined in different frameworks is the debate about the algebraic specification of partial (higher-order) functions. Indeed the relevance of such a problem is made obvious by the wide use of partial operations in programming languages and their data types and not only the scientific community didn't agree on what formalism is better, but also the criteria for such a judgment are still under investigation.
After presenting a parade of different formalisms proposed to define partial functions and in particular some recent results about the partial paradigm, the concept of simulation of a framework by another is introduced, adopting the notion of institution as a synonym for logical formalism. The basic idea of simulation is encoding the syntax, ie signatures and sentences, of a new frame by that of an already known formalism in a way consistent with the semantics, in order to transfer back results and tools.
Then simulations are used to investigate the relationships between frames, first using the relationships between specifications of partiality in different formalisms as a guide, and then applying the same technique to the analogous problem of defining non-strict functions (like the ubiquitous if_then_else). Three levels can be distinguished (and formalize using simulations): the``set-theoretic'', where the individual models are related disregarding their categorical and logical interconnection, the ``categorical'', where the relation is between the categories of models, and the ``logical'', where the relation is between specifications (or theories).
Moreover a general categorical construction is introduced, that allows ``borrowing'' the logical tools of a framework to enrich another framework lacking them, provided that an appropriate mapping between the frameworks exists. This technique applies, in particular, to the translation of inference systems along simulations (in a way that soundness and completeness are preserved) and of proofs along maps of the underlying institutions (entailment systems). An instance of this technique builds an equationally complete inference system for the partial higher-order specifications starting from an equationally complete inference system for the first-order case.
Finally the notion of institution independent metalanguage, by Sannella and Tarlecki, is refined in simulation independent metalanguage, allowing specification defined in different institutions to be assembled to build new specifications, and the concept of implementation is generalized, involving models in two institutions; in this way specifications may be related that belongs to different frames.

The compressed postscript version of the thesis is available through anonymous ftp at ftp.disi.unige.it, in /person/CerioliM/thesis92.ps.z (488578 Kb)