Dipartimento di Informatica e Scienze dell'Informazione
A sound and equationally complete deduction system
for partial conditional (higher-order) types
(Extended Abstract)
M. Cerioli .
In Proceedings of the 3rd Italian Conference of Theoretical
Computer Science. World Scientific, 1989.
Higher-order algebraic specifications of partial functions lead naturally to
consider partial conditional specifications, ie partial specifications with
axioms that are implications with a (possibly infinite) set of equalities
in the premises and one equality as consequence, where on the left-hand
side the equality is strong (the equality holds iff either both sides are
defined and equal (existential equality) or both are undefined).
Contrary to the well explored case of positive conditional axioms (only
existential equalities on the left) those specifications do not always admit
free models (the related theory is much more subtle and still unsettled).
Relying on and completing some our previous results, we present in this paper
a deduction system which is complete w.r.t. strong equalities between open terms,
with an application to the existence of free objects.
Since positive conditional partial specifications and conditional total
specifications are special cases of the paradigm investigated here, the
presented theory generalizes the related Birkhoff-like deduction theory.
The system we exhibit here looks nice since it handles also the case of
infinitary conjunctions on the left of the axioms; it reduces to a classical
one for the positive conditional case just dropping one rule, and finally
solves the empty carrier problem, noticed by Huet and Goguen-Meseguer,
without using explicit quantification.
The compressed postscript version of this paper is available through anonymous ftp
at ftp.disi.unige.it, in
/person/CerioliM/EATCS89.ps.z
(29807 Kb)