library Calculi/Space/RCC5 version 0.3 %% author: S. Woelfl %% date: 22-06-2005 %% %left_assoc __cup__,__cap__ %prec {__cup__} < {__cmps__} %prec {__cmps__} < {__cmpl__} %( The RCC5 Calculus (resp. Containment Algebra) )% from Calculi/Algebra/BooleanAlgebra get BooleanAlgebraWithCompl, ExtBooleanAlgebraByOrderRelations, AtomicBooleanAlgebra from Calculi/Algebra/RelationAlgebra get AtomicRelationAlgebra, IntegralRelationAlgebra, SymmetricRelationAlgebra from Calculi/Algebra/RelationAlgebraSymbolic get CompositionTable, GroundingCompositionTable, SetRepresentationOfRelations, ConstructPseudoRelationAlgebra, ConstructExtPseudoRelationAlgebra from Calculi/Algebra/RelationAlgebraModel get BinaryRelations, AlgebraOfBinaryRelations, JEPDBaseRelationModel, BaseRelationModel, ConstructPseudoModelFromBaseRelationModel, ConstructModelFromBaseRelationModel, CompositionClosedBaseRelationModel, CheckCompositionClosedBaseRelationModel from Calculi/Space/EuclideanSpace get EuclideanSpace2D, EuclideanSpace3D from HasCASL/TopologicalSpaces get RichTopologicalSpace from HasCASL/MetricSpaces get MetricSpace from HasCASL/Set get Set %( Part I: Symbolic Level We start by describing the symbolic level of the region connection calculus RCC5, i.e., the set of base relations and the composition table. Arbitrary relations of RCC5 are represented as sets of base relations. In turn base relations are represented by their respective singleton sets. The spec BooleanAlgebraOfRCC5Relations builds this set of all relations, which obviously forms an atomic Boolean algebra. Via the composition table we then define a relation algebra on the set of all relations. This provides us with a specification of RCC5, namely spec RCC5. )% %( RCC5 has 5 base relations, namely, dr ("disconnected"), po ("partially overlaps"), pp ("proper part"), ppi ("proper part inverse"), and eq ("equals"). )% spec RCC5BaseRelations = %mono free type BaseRel ::= dr | po | pp | ppi | eq end %( The following spec encodes the composition table of RCC5 as well as the information on inverses of base relations. )% spec RCC5CompositionTable = sort BaseRel ops dr,po,pp,ppi,eq: BaseRel and CompositionTable with op id |-> eq then . inv(dr) = dr %(sym_dr)% . inv(po) = po %(sym_po)% . inv(pp) = ppi %(inv_pp)% . inv(ppi) = pp %(inv_ppi)% . inv(eq) = eq %(sym_eq)% . pp cmps pp = pp %(cmps_pppp)% . pp cmps ppi = 1 %(cmps_ppppi)% . pp cmps po = pp cup po cup dr %(cmps_pppo)% . pp cmps dr = dr %(cmps_ppdr)% . pp cmps eq = pp %(cmps_ppeq)% . ppi cmps pp = pp cup po cup ppi cup eq %(cmps_ppipp)% . ppi cmps ppi = ppi %(cmps_ppippi)% . ppi cmps po = ppi cup po %(cmps_ppipo)% . ppi cmps dr = ppi cup po cup dr %(cmps_ppidr)% . ppi cmps eq = ppi %(cmps_ppieq)% . po cmps pp = po cup pp %(cmps_popp)% . po cmps ppi = ppi cup po cup dr %(cmps_poppi)% . po cmps po = 1 %(cmps_popo)% . po cmps dr = ppi cup po cup dr %(cmps_podr)% . po cmps eq = po %(cmps_poeq)% . dr cmps pp = pp cup po cup dr %(cmps_drpp)% . dr cmps ppi = dr %(cmps_drppi)% . dr cmps po = pp cup po cup dr %(cmps_drpo)% . dr cmps dr = 1 %(cmps_drdr)% . dr cmps eq = dr %(cmps_dreq)% . eq cmps pp = pp %(cmps_eqpp)% . eq cmps ppi = ppi %(cmps_eqppi)% . eq cmps po = po %(cmps_eqpo)% . eq cmps dr = dr %(cmps_eqdr)% . eq cmps eq = eq %(cmps_eqeq)% end view RCC5CompositionTable_as_GroundingCompositionTable : GroundingCompositionTable to RCC5CompositionTable = id |-> eq end spec BooleanAlgebraOfRCC5Relations = SetRepresentationOfRelations[RCC5BaseRelations] end view BooleanAlgebraOfRCC5Relations_as_AtomicBooleanAlgebra : {AtomicBooleanAlgebra hide preds __<__, __<=__, __>__, __>=__} to BooleanAlgebraOfRCC5Relations = Elem |-> Rel, AtomElem |-> BaseRel end spec RCC5 = ConstructPseudoRelationAlgebra[RCC5BaseRelations] [RCC5CompositionTable fit op id:BaseRel |-> eq] end spec RichRCC5 = ConstructExtPseudoRelationAlgebra[RCC5BaseRelations] [RCC5CompositionTable fit op id:BaseRel |-> eq] end view RCC5_as_AtomicRelationAlgebra : AtomicRelationAlgebra to RichRCC5 = AtomRel |-> BaseRel, id |-> eq end %[ Needs to be checked: view RCC5_as_IntegralRelationAlgebra : IntegralRelationAlgebra to RichRCC5 end view RCC5_as_SymmetricRelationAlgebra : SymmetricRelationAlgebra to RichRCC5 end ]% %( Part II: Semantic Level Following we describe how models of RCC5 can be constructed from metric spaces. )% logic HasCASL spec Discs[MetricSpace] = %def local Set within op opDisc(r:Real;x:S) : Set S = \y:S . d(x,y) 0 /\ X=opDisc(r,x)} type ClosedDisc = {X:Set S . exists r:Real;x:S . r > 0 /\ X=clDisc(r,x)} preds __disjoint__,__subset__: Set S * Set S ops cen: OpenDisc -> S; rad: OpenDisc -> Real forall X:OpenDisc; r:Real; x:S . X = opDisc(r,x) <=> cen(X) = x /\ rad(X) = r end spec RCC5BaseRelationModel_OpenDisc[MetricSpace] = %def BaseRelationModel[Discs[MetricSpace] fit Elem |-> OpenDisc] then %def ops ppRel,ppiRel,poRel,drRel,eqRel:Relation free type BaseRel ::= ppRel | ppiRel | poRel | drRel | eqRel forall x,y:OpenDisc . (x,y) isIn rep(ppRel) <=> x subset y /\ not x = y . (x,y) isIn rep(ppiRel) <=> y subset x /\ not x = y . (x,y) isIn rep(poRel) <=> not x subset y /\ not y subset x /\ not x disjoint y . (x,y) isIn rep(drRel) <=> x disjoint y . (x,y) isIn rep(eqRel) <=> x = y end spec LargeMetricSpace = MetricSpace %[ to be done ]% end spec EvenLargerMetricSpace = MetricSpace %[ to be done , presumably unbounded metric spaces ]% end view v_ToBeDone : LargeMetricSpace to EvenLargerMetricSpace %( A metric space provides a JEPDBaseRelationModel only if it contains at least ??? elements )% view JEPDBaseRelationModel_From_RCC5BaseRelationModel_OpenDisc[LargeMetricSpace]: JEPDBaseRelationModel to RCC5BaseRelationModel_OpenDisc[LargeMetricSpace] = sort Elem |-> OpenDisc end view CompositionClosedBaseRelationModel_From_RCC5BaseRelationModel_OpenDisc[EvenLargerMetricSpace]: CheckCompositionClosedBaseRelationModel to { ConstructPseudoModelFromBaseRelationModel[ RCC5BaseRelationModel_OpenDisc[MetricSpace] fit Elem |-> OpenDisc] then %def ops id:Rel; inv__:BaseRel -> Rel; __cmps__:BaseRel * BaseRel -> Rel } = Elem |-> OpenDisc end spec RCC5Model_OpenDisc[EvenLargerMetricSpace] = %def ConstructModelFromBaseRelationModel[ RCC5BaseRelationModel_OpenDisc[MetricSpace] fit Elem |-> OpenDisc] then %def ops inv__ : BaseRel -> BaseRel; __cmps__: BaseRel * BaseRel -> Rel end view RCC5Model_OpenDisc_ExtModels_RCC5CompositionTable[EvenLargerMetricSpace] : RCC5CompositionTable to RCC5Model_OpenDisc[EvenLargerMetricSpace] = ops pp |-> ppRel, ppi |-> ppiRel, po |-> poRel, dr |-> drRel, eq |-> eqRel end view MetricSpace_induces_AlgebraOfBinaryRelations_OpenDisc[EvenLargerMetricSpace] : AlgebraOfBinaryRelations to RCC5Model_OpenDisc[EvenLargerMetricSpace] = Elem |-> OpenDisc end view MetricSpace_induces_ModelOfRCC5_OpenDisc[EvenLargerMetricSpace] : RCC5 to RCC5Model_OpenDisc[EvenLargerMetricSpace] = ops pp |-> ppRel, ppi |-> ppiRel, po |-> poRel, dr |-> drRel, eq |-> eqRel end %( Special Models )% view EuclideanSpace2D_Is_EvenLarger : EvenLargerMetricSpace to EuclideanSpace2D = S |-> Point, d |-> dist end spec RCC5EuclideanSpace2D_OpenDisc = %def RCC5Model_OpenDisc[view EuclideanSpace2D_Is_EvenLarger] end view RCC5EuclideanSpace2D_OpenDisc_models_RCC5 : RCC5 to RCC5EuclideanSpace2D_OpenDisc = ops pp |-> ppRel, ppi |-> ppiRel, po |-> poRel, dr |-> drRel, eq |-> eqRel end