Information Frames

Dieter Spreen

(Universitaet Siegen)

In 1982 Dana Scott introduced information systems as a logic-based approach to domain theory. An information system consists of a set of tokens to be thought of as atomic statements about a computational process, a consistency predicate telling us which finite sets of such statements contain consistent information, and an entailment relation saying what atomic statements are entailed by which consistent sets of these. Theories of such a logic, also called states, i.e. finitely consistent and entailment-closed sets of atomic statements, form a bounded-complete domain with respect to set inclusion, and, conversely, every such domain can be obtained in this way, up to isomorphism. This gives Scott's idea that domain elements represent information about states of a computation a precise mathematical meaning.

The role of bounded completeness becomes also clear in this context: States represent consistent information. So, any finite collection of substates must contain consistent information as well, and this fact is witnessed by any of its upper bounds.

Whereas in Scott's approach the consistency witnesses are hidden, in this paper we present an approach that makes them explicit. This allows to consider the more general situation in which there is no longer a uniform global consistency predicate. Instead there is consistency predicate for each atomic statement telling us which finite sets of atomic statements express information that is consistent with the given statement. As it turns out the theories, or states, of such a more general information system form an L-domain, and, up to isomorphism, each L-domain can be obtained in this way.

Since every token in the just delineated kind of information system has its own consistency predicate, we can also think of each such system as a family of logics, or a Kripke frame.

Wednesday 5th March 2014, 14:00
Robert Recorde Room
Department of Computer Science