Project topics and materials
Get Complete Project Material File(s) Now! »
Introduction : Constraint Systems
In this chapter we introduce the notion of constraint systems (cs’s) that is central for this dissertation. Constraint systems is one of the main notions of the concurrent constraint programming (ccp), a well known formalism in concurrency theory. Most of the material in this chapter was taken from [BDPP95, KPPV12, HPRV15, ORV13]. For more details on constraint systems and ccp we strongly recommend you to see [SRP91, PSSS93].
This chapter is organized as follows. First, we shall start by giving some definitions for posets, maps and lattices which were taken from [Vic96, DP02]. Then we shall move to the basic notion of constraint systems. We shall also introduce in this chapter the notions of spatial constraint systems (scs’s) and spatial constraint systems with extrusion (scse’s), which can be seen as extensions of the basic cs’s in order to account for space and mobility, respectively. We shall describe the differences between scs’s and its predecessor cs’s.
Posets and Maps
Definition 2.1.1 (Preorder). A preorder is a set P which is equipped with a binary relation v that is reflexive and transitive.
Posets
A poset or a partially ordered set can be seen as a set of elements together with a binary relation stating the order of the elements in the set.
Definition 2.1.2 (Poset). A partially ordered set (poset) is a set P equipped with a binary relation v satisfying, for every x, y, z 2 P the following prop-erties:
1. ( reflexivity) x v x for all x 2 P
2. ( transitivity) if x v y and y v z then x v z
3. ( antisymmetry) if x v y and y v x then x = y
Definition 2.1.3 (Directed Set). Consider the poset (P, v) and D ✓ P . We say that D is an upward directed set (resp. downward directed set) if for every a, b 2 D there exists c 2 D such that a v c and b v c (resp. c v a and c v b).
Maps
We shall now introduce some formal definitions for maps on posets. Definition 2.1.4 (Maps). Let (P, v) and (Q, v) be posets. A map f : P !
Q is
1. order-preserving if a v b in P then f(a) v f(b) in Q,
2. order-reflecting if f(a) v f(b) in Q then a v b in P,
3. order-embedding if it is both, an order-preserving and order-reflecting map,
4. order-isomorphism if it is an order-embedding and surjective map.
In addition, we shall say that a map is a self-map if P = Q.
Lattices
We define the meet (greatest lower bound or glb) of a set as an element which is below every element in that set, formally
Definition 2.2.1 (Meet (glb)). Let P be a poset, X ✓ P and y 2 P. Then y is a glb for X iff
• ( lower bound) If x 2 X then y v x, and
• If z is any other lower bound for X then z v y
We shall write y = d X whenever y is the glb of X.
The next proposition states that for every subset of a poset we can have at most one meet.
Proposition 2.2.1. Let P be a poset and X ✓ P . Then X can have at most one glb.
Now we introduce the definition of join (least upper bound or lub) of a set as an element which is above every element in that set, that is
Definition 2.2.2 (Join (lub)). Let P be a poset, X ✓ P and y 2 P. Then y is a lub for X iff
• ( upper bound) If x 2 X then y w x, and
• If z is any other upper bound for X then z w y
We shall write y = FX whenever y is the lub of X.
By the duality principle we shall use P OP to denote the same elements in P with the order reversed.
Proposition 2.2.2. Let P be a poset, X ✓ P and y 2 P. Then y is a lub for X iff y is a glb for X in P OP
Now we formally define when a function between two posets preserves meets.
Definition 2.2.3. Let P and Q be two posets, and f be a function f : P ! Q. Then we say that f preserves glbs iff whenever X ✓ P has a glb y, then f(y) is a glb for {f(x) | x 2 X}.
Given that posets only can guarantee the order of the elements in a given set, then we need to make use of the notion of lattices which, in addition to preserve the order, they have all finite meets (glbs) and joins (lubs).
Definition 2.2.4 (Lattice). Consider the poset P . Then P is called
• a lattice if for all x, y 2 P then x t y and x u y exists.
• a complete lattice iff for every subset X ✓ P , we have d X and FX.
We shall call a meet (join) preserving function between two lattices a lattice homomorphism. An important property on maps that will be very useful through this dissertation is that of being able to preserve all lub (or glb). This property on maps is called continuity and can be defined as follows :
Definition 2.2.5 (Continuous Maps). Consider the lattices L and L0, a map between the lattices f : L ! L0 and and a set S 2 L. We say that
1. f is upward-continuous if f(FS) = Ff(S) and S is directed. If S is not directed then f is join-complete.
2. f is downward-continuous if f(d S) = d f(S) and S is downward directed. If S is not downward directed then f is meet-complete.
Algebraic Lattice
Another important definition that we shall introduce is that of algebraic lattices. Intuitively, we say that a lattice is algebraic whenever every element of the lattice can be approximated by the finite elements below it. These elements are knows as compact elements.
Definition 2.2.6 (Compact Elements). Let L be a lattice and k 2 L. We say that k is compact if for every subset S ✓ L G G
k v S implies k v S0 for some finite S0 ✓ S
The set of compact elements in L is denoted by K(L)
Definition 2.2.7 (Algebraic Lattices). Let L be a complete lattice. We say that L is an algebraic lattice if for each element x 2 L we have
G c = {y 2 K(L) | y v x}
where K(L) represents the set of compact elements in L.
Distributive lattices
Many applications in order theory require lattices in which meets (glb) distributes over the joins (lub). These lattices are know in the literature as distributive lattices.
Definition 2.2.8 (Distributive Lattices). A lattice L is distributive iff for every x, y and z 2 L we have that x u (y t z) = (x u y) t (x u z).
In this section we shall talk about frames and Heyting algebras. We recom-mend to see [Vic96] for more details and proofs about this two notions.
We can intuitively define a frame as a distributive lattice in which every arbitrary subset has a join and every finite subset has a meet. Formally.
Definition 2.3.1 (Frame). Let A be a poset, Y ✓ A and x 2 Y. We say that A is a frame iff
1. Every subset has a join
2. Every finite subset has a meet
3. Binary meets distribute over joins:
x u Y = {x u y : y 2 Y } (frame distributivity)
We shall call a function between two frames preserving arbitrary joins and finite meets a frame homomorphism.
Heyting algebras
In this dissertation we shall often mention the notion of Heyting implica-tion. We can intuitively define a Heyting implication c ! d as the weakest constraint e you should join c with in order to be able to entail d. Heyt-ing implications are the standard implication operation in Heyting algebras. Formally.
Definition 2.3.2 (Heyting algebra). Consider the lattice A = (Con, v). We say that A is a Heyting algebra iff for every c, d 2 Con we can build one element c ! d such that
def l c ! d = {e 2 Con | c t e w d }.
The element c ! d is known as a Heyting implication. We shall define a Heyting negation as s def ! Recall that is the greatest ele-
c = c false. false ment in the constraint system representing the join of possible inconsistent information.
We shall call a function f between Heyting algebras preserving finite joins, finite meets and the operation ! (i.e. f(a ! b) = f(a) ! f(b)) a Heyting algebra homomorphism. Additionally, we shall say that a Heyting algebra is a complete Heyting algebra (cHa) iff it is a complete lattice.
The following proposition states the relation between frames and cHa.
Proposition 2.3.1. Consider the lattice A. Then we say that A is a frame iff it is a cHa.
Table of contents :
1 Introduction
1.1 Introduction
1.1.1 The Extrusion Problem
1.1.2 Knowledge in Terms of Space
1.1.3 Distributed Spaces
I Constraint Systems and Modal Logics
2 Introduction: ConstraintSystems
2.1 Posets and Maps
2.1.1 Posets
2.1.2 Maps
2.2 Lattices
2.2.1 Lattices
2.2.2 Algebraic Lattice
2.2.3 Distributive lattices
2.3 Frames
2.3.1 Frames
2.3.2 Heyting algebras
2.4 Constraint Systems
2.5 Spatial Constraint Systems
2.6 Spatial Constraint Systems with Extrusion
3 Introduction: ModalLogics
3.1 Modal Logics
3.1.1 Modal Language
3.1.2 Kripke Model
3.2 Normal Modal Logics
3.2.1 Normal Modal Logics
II The Extrusion Problem
4 Introduction
4.1 Background: Spatial Constraint Systems
4.2 Constraint Frames and Normal Self-Maps
4.2.1 Normal Self-Maps
4.3 Extrusion Problem for Kripke Constraint Systems
4.3.1 KS and Kripke SCS
4.3.2 Complete Characterization of the Existence of Right Inverses
4.3.3 Deriving Greatest Right-Inverse
4.4 Deriving Normal Right-Inverses
4.4.1 Deriving Greatest Normal Right Inverse
4.4.2 Deriving Minimal Normal-Right Inverses
4.5 Applications
4.5.1 Right-Inverse Modalities
4.5.2 Normal Inverses Modalities
4.5.3 Inconsistency Invariance
4.5.4 Bisimilarity Invariance
4.5.5 Temporal Operators
4.6 Summary
III Knowledge in Terms of Space
5 Introduction
5.1 S4 Knowledge as Global Information
5.1.1 Knowledge Constraint System
5.1.2 Knowledge as Global Information
5.2 Summary
IV Distributed Information in Terms of Space
6 Introduction
6.1 Background
6.2 Spatial Constraint Systems
6.2.1 Extrusion and utterance
6.3 Distributed Spaces
6.3.1 Properties of Distributed Spaces
6.3.2 Views and Distributed Spaces
6.4 Summary
7 Conclusions andRelatedWork 9
7.1 Concluding Remarks
7.2 Related and Future Work
Bibliography
