Abstract: Type class polymorphism in an institutional framework

Type class polymorphism in an institutional framework

Lutz Schröder, Till Mossakowski, Christoph Lüth
FB 3 - Mathematik und Informatik, Universität Bremen

Higher-order logic with ML-style type class polymorphism is widely
used as a specification formalism. Its polymorphic entities (types,
operators, axioms) can easily be equipped with a `naive' semantics
defined in terms of collections of instances. However, this semantics
has the unpleasant property that while model reduction preserves
satisfaction of sentences, model expansion generally does not. In
other words, unless further measures are taken, type class
polymorphism fails to constitute a proper institution, being only a
so-called rps preinstitution; this is unfortunate, as it means that
one cannot use institution-independent or heterogeneous structuring
languages, proof calculi, and tools with it.

Here, we suggest to remedy this problem by modifying the notion of
model to include information also about its potential future
extensions. Our construction works at a high level of generality in
the sense that it provides, for any preinstitution, an institution in
which the original preinstitution can be represented. The semantics of
polymorphism used in the specification language HasCASL makes use of
this result. In fact, HasCASL's polymorphism is a special case of a
general notion of polymorphism in institutions introduced here, and
our construction leads to the right notion of semantic consequence
when applied to this generic polymorphism. The appropriateness of the
construction for other frameworks that share the same problem depends
on methodological questions to be decided case by case. In particular,
it turns out that our method is apparently unsuitable for
observational logics, while it works well with abstract state machine
formalisms such as state-based CASL.