DISI 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)