Prof. Dieter Spreen at NII Logic Seminar
Date: March 22, 2016, 14:00--16:00
Place: National Institute of Informatics, Room 1901 (19th floor) 場所: 国立情報学研究所 19階 1901室 (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/)
Speaker: Prof. Dieter Spreen (Siegen University)
Ttile: Information Frames
Abstract: In 1982, Dana Scott introduced information systems as a logic-based approach to domain theory. Here, a domain is a bound-complete algebraic complete partial order with least element. 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 algebraic complete partial order 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 stages 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 infor- mation 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 a 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.
問合せ先: 龍田 真 (国立情報学研究所) e-mail: tatsuta@nii.ac.jp http://research.nii.ac.jp/~tatsuta