Get Complete Project Material File(s) Now! »
Extrusion as the right inverse of Space
In spatially distributed systems an agent can transfer information from its space to the outside. We shall refer to this kind of transmission as extrusion. The extruded information is posted outside, possibly addressed to some other agent. Our epistemic view of extrusion is what we shall call utterance. An agent may utter information which will then be available to others. The uttered information may be inconsistent with the agent’s own beliefs, in particular it could be a lieLet us now extend spatial constraint systems with extrusion. First recall that given a function f : X ! Y , we say that g : Y ! X is a right inverse (or section) of f iff f(g(y)) = y for every y 2 Y . Similarly, given g : Y ! X we say that f : X ! Y is a left inverse (or retraction) of g iff f(g(y)) = y for every y 2 Y:
Limit Preservation
In the following sections we will often refer to preservation of some limits by space functions. Let C be an scs with constraints Con. A space function []i of C preserves the supremum of a set S Con iff [ F S]i = F f[c]i j c 2 Sg. The preservation of the infimum of a set is defined analogously. Notice that S.2 and the associativity of t imply that the space functions preserve the lub of any finite subset of Con. Recall (by Definition 2.1.14) that a space function that preserves the supremum/infimum of any arbitrary subset of Con is said to be join-complete/meet-complete. Also recall that a space function in C is continuous/ downward continuous if it preserves the supremum/infimum of any directed set/filtered set.
The join-completeness of space functions trivially implies their (Scott) continuity, a central concept in domain theory. From S.2 and the fact that constraint systems are complete lattices, the reverse implication is also true: Space continuity implies space completeness. Proposition 3.3.1. Let []i be a space function of an scs. If []i is continuous then []i is join-complete. Proof. The above proposition follows from the fact that any function from a poset in which every non-empty finite supremum exists preserves arbitrary suprema if and only if it preserves both directed suprema and finite suprema [GHK+03].
The Extrusion Problem
Given an scs a legitimate question is whether it can be extended to an scse. In this section we would like to identify conditions that guarantee the existence of extrusion functions « 1; : : : ; « n for spaces []1; : : : ; []n of any given n-scs. From set theory we know that there is an extrusion function (i.e., a right inverse) « i for []i iff []i is surjective. Recall that the fiber of y 2 Y , or pre-image of the singleton fyg, under f : X ! Y is the set f1(y) = fx 2 X j y = f(x)g.
Thus the extrusion « i can be defined as a function, called choice function, that maps each element c to some element from the (non-empty because of surjectivity) fiber of c under []i: The existence of this choice function assumes, however, the Axiom of Choice. Nevertheless, we are interested in an explicit construction for extrusion. This is possible for continuous space functions due to the following lemma stating that the fibers of space functions are directed sets. In fact, we can prove the lemma by showing something stronger: fibers are closed under finite joins.
Table of contents :
Résumé
Abstract
Acknowledgments
Contents
1 Introduction
2 Background on Constraint Systems
2.1 Order Theory
Posets and Maps
Lattices
2.2 Constraint Systems
Spatial Constraint Systems
2.3 Summary
3 Spatial Constraint Systems with Extrusion
3.1 Extrusion as the right inverse of Space
3.2 Derived Notions and Applications
Heyting Implication
Lying Agents
Communicating Agents
Process Mobility
Outermost Extrusion
3.3 Limit Preservation
3.4 The Extrusion Problem
Local/Subjective Distribution
Global/Objective Distributed Extrusion
3.5 Properties of Space and Extrusion
Consistent and Contradicting Agents Orders
3.6 Galois Connections
3.7 Summary
4 Opinions & Lies: A Bimodal Logic
4.1 Modal Logics
4.2 Kripke Spatial Constraint Systems
A modal language
4.3 A Logic of Belief and Utterance
Left-total left-unique Kripke Structures
The BUn logic
4.4 Summary
5 Knowledge in Terms of Global Space
5.1 Epistemic Logic
5.2 Knowledge Constraint System
5.3 Knowledge as Global Information
5.4 Summary
6 Algebraic view of LTL
6.1 Linear Temporal Logic
Future
Past
6.2 Constraint systems for LTL models
6.3 Constraint system semantics for LTL
6.4 Summary
7 Conclusions and Related Work
7.1 Related and Future Work
7.2 Correspondence between operators
Bibliography