Dipartimento di Informatica e Scienze dell'Informazione
Relationships between Logical Frameworks
M. Cerioli .
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
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
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
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