library Calculi/Space/RCC8 version 0.3 %% author: S. Woelfl %% date: 23-06-2005 %% %left_assoc __cup__,__cap__ %prec {__cup__} < {__cmps__} %( The RCC8 Calculus (resp. Containment Algebra) Literature: TODO )% 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 RCC8, i.e., the set of base relations and the composition table. Arbitrary relations of RCC8 are represented as sets of base relations. In turn base relations are represented by their respective singleton sets. The spec RelationBaseOfRCC8 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 RCC8, namely spec RCC8. )% %( RCC8 has 8 base relations, namely, dc ("disconnected"), ec ("externally connected"), po ("partially overlaps"), tpp ("tangential proper part"), ntpp ("non-tangential proper part"), tppi ("tangential proper part inverse"), ntppi ("non-tangential proper part inverse"), and eq ("equals"). )% spec RCC8BaseRelations = %mono free type BaseRel ::= dc | ec | po | tpp | ntpp | tppi | ntppi | eq end %( The following spec encodes the composition table of RCC8 as well as the information on the converses of base relations. )% spec RCC8CompositionTable = sort BaseRel ops dc ,ec ,po ,tpp ,ntpp ,tppi ,ntppi ,eq: BaseRel and CompositionTable with op id |-> eq then . inv(dc) = dc %(sym_dc)% . inv(ec) = ec %(sym_dc)% . inv(po) = po %(sym_po)% . inv(tpp) = tppi %(inv_tpp)% . inv(tppi) = tpp %(inv_tppi)% . inv(ntpp) = ntppi %(inv_ntpp)% . inv(ntppi) = ntpp %(inv_ntppi)% . inv(eq) = eq %(sym_eq)% . dc cmps dc = 1 %(cmps_dcdc)% . dc cmps ec = dc cup ec cup po cup tpp cup ntpp %(cmps_dcec)% . dc cmps po = dc cup ec cup po cup tpp cup ntpp %(cmps_dcpo)% . dc cmps tpp = dc cup ec cup po cup tpp cup ntpp %(cmps_dctpp)% . dc cmps ntpp = dc cup ec cup po cup tpp cup ntpp %(cmps_dcntpp)% . dc cmps tppi = dc %(cmps_dctppi)% . dc cmps ntppi = dc %(cmps_dcntppi)% . ec cmps dc = dc cup ec cup po cup tppi cup ntppi %(cmps_ecdc)% . ec cmps ec = dc cup ec cup po cup tpp cup tppi cup eq %(cmps_ecec)% . ec cmps po = dc cup ec cup po cup tpp cup ntpp %(cmps_ecpo)% . ec cmps tpp = ec cup po cup tpp cup ntpp %(cmps_ectpp)% . ec cmps ntpp = po cup tpp cup ntpp %(cmps_ecntpp)% . ec cmps tppi = dc cup ec %(cmps_ectppi)% . ec cmps ntppi = dc %(cmps_ecntppi)% . po cmps dc = dc cup ec cup po cup tppi cup ntppi %(cmps_podc)% . po cmps ec = dc cup ec cup po cup tppi cup ntppi %(cmps_poec)% . po cmps po = 1 %(cmps_popo)% . po cmps tpp = po cup tpp cup ntpp %(cmps_potpp)% . po cmps ntpp = po cup tpp cup ntpp %(cmps_pontpp)% . po cmps tppi = dc cup ec cup po cup tppi cup ntppi %(cmps_potppi)% . po cmps ntppi = dc cup ec cup po cup tppi cup ntppi %(cmps_pontppi)% . tpp cmps dc = dc %(cmps_tppdc)% . tpp cmps ec = dc cup ec %(cmps_tppec)% . tpp cmps po = dc cup ec cup po cup tpp cup ntpp %(cmps_tpppo)% . tpp cmps tpp = tpp cup ntpp %(cmps_tpptpp)% . tpp cmps ntpp = ntpp %(cmps_tppntpp)% . tpp cmps tppi = dc cup ec cup po cup tpp cup tppi cup eq %(cmps_tpptppi)% . tpp cmps ntppi = dc cup ec cup po cup tppi cup ntppi %(cmps_tppntppi)% . ntpp cmps dc = dc %(cmps_ntppdc)% . ntpp cmps ec = dc %(cmps_ntppec)% . ntpp cmps po = dc cup ec cup po cup tpp cup ntpp %(cmps_ntpppo)% . ntpp cmps tpp = ntpp %(cmps_ntpptpp)% . ntpp cmps ntpp = ntpp %(cmps_ntppntpp)% . ntpp cmps tppi = dc cup ec cup po cup tpp cup ntpp %(cmps_ntpptppi)% . ntpp cmps ntppi = 1 %(cmps_ntppntppi)% . tppi cmps dc = dc cup ec cup po cup tppi cup ntppi %(cmps_tppidc)% . tppi cmps ec = ec cup po cup tppi cup ntppi %(cmps_tppiec)% . tppi cmps po = po cup tppi cup ntppi %(cmps_tppipo)% . tppi cmps tpp = po cup eq cup tpp cup tppi %(cmps_tppitpp)% . tppi cmps ntpp = po cup tpp cup ntpp %(cmps_tppintpp)% . tppi cmps tppi = tppi cup ntppi %(cmps_tppitppi)% . tppi cmps ntppi = ntppi %(cmps_tppintppi)% . ntppi cmps dc = dc cup ec cup po cup tppi cup ntppi %(cmps_ntppidc)% . ntppi cmps ec = po cup tppi cup ntppi %(cmps_ntppiec)% . ntppi cmps po = po cup tppi cup ntppi %(cmps_ntppipo)% . ntppi cmps tpp = po cup tppi cup ntppi %(cmps_ntppitpp)% . ntppi cmps ntpp = po cup tpp cup tppi cup ntpp cup ntppi cup eq %(cmps_ntppintpp)% . ntppi cmps tppi = ntppi %(cmps_ntppitppi)% . ntppi cmps ntppi = ntppi %(cmps_ntppintppi)% end view RCC8CompositionTable_as_GroundingCompositionTable : GroundingCompositionTable to RCC8CompositionTable = id |-> eq end spec BooleanAlgebraOfRCC8Relations = SetRepresentationOfRelations[RCC8BaseRelations] end view BooleanAlgebraOfRCC8Relations_as_AtomicBooleanAlgebra : {AtomicBooleanAlgebra hide preds __<__, __<=__, __>__, __>=__} to BooleanAlgebraOfRCC8Relations = Elem |-> Rel, AtomElem |-> BaseRel end spec RCC8 = ConstructPseudoRelationAlgebra[RCC8BaseRelations] [RCC8CompositionTable fit op id:BaseRel |-> eq] end spec RichRCC8 = ConstructExtPseudoRelationAlgebra[RCC8BaseRelations] [RCC8CompositionTable fit op id:BaseRel |-> eq] end view RCC8_as_AtomicRelationAlgebra : AtomicRelationAlgebra to RichRCC8 = AtomRel |-> BaseRel, id |-> eq end %[ Needs to be checked: view RCC8_as_IntegralRelationAlgebra : IntegralRelationAlgebra to RichRCC8 end view RCC8_as_SymmetricRelationAlgebra : SymmetricRelationAlgebra to RichRCC8 end ]% %( Part II: Semantic Level Following we describe how models of RCC8 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 RCC8BaseRelationModel_OpenDisc[MetricSpace] = %def BaseRelationModel[Discs[MetricSpace] fit Elem |-> OpenDisc] then %def ops dcRel,ecRel,poRel,tppRel,ntppRel,tppiRel,ntppiRel,eqRel:Relation free type BaseRel ::= dcRel | ecRel | poRel | tppRel | ntppRel | tppiRel | ntppiRel | eqRel forall x,y:OpenDisc . (x,y) isIn rep(dcRel) <=> clDisc(rad(x),cen(x)) disjoint clDisc(rad(y),cen(y)) . (x,y) isIn rep(ecRel) <=> x disjoint y /\ not clDisc(rad(x),cen(x)) disjoint clDisc(rad(y),cen(y)) . (x,y) isIn rep(poRel) <=> not x subset y /\ not y subset x /\ not x disjoint y . (x,y) isIn rep(tppRel) <=> x subset y /\ not clDisc(rad(x),cen(x)) subset y . (x,y) isIn rep(ntppRel) <=> clDisc(rad(x),cen(x)) subset y . (x,y) isIn rep(tppiRel) <=> y subset x /\ not clDisc(rad(y),cen(y)) subset x . (x,y) isIn rep(ntppiRel) <=> clDisc(rad(y),cen(y)) subset x . (x,y) isIn rep(eqRel) <=> x = y end spec LargeMetricSpace = MetricSpace %[ to be done ]% end spec UnboundedMetricSpace = MetricSpace then forall r:Real . exists x,y:S . d(x,y) > r end view v_ToBeDone : LargeMetricSpace to UnboundedMetricSpace %( A metric space provides a JEPDBaseRelationModel only if it contains at least ??? elements )% view JEPDBaseRelationModel_From_RCC8BaseRelationModel_OpenDisc[LargeMetricSpace]: JEPDBaseRelationModel to RCC8BaseRelationModel_OpenDisc[LargeMetricSpace] = sort Elem |-> OpenDisc end view CompositionClosedBaseRelationModel_From_RCC8BaseRelationModel_OpenDisc[UnboundedMetricSpace]: CheckCompositionClosedBaseRelationModel to { ConstructPseudoModelFromBaseRelationModel[ RCC8BaseRelationModel_OpenDisc[MetricSpace] fit Elem |-> OpenDisc] then %def ops id:Rel; inv__:BaseRel -> Rel; __cmps__:BaseRel * BaseRel -> Rel } = Elem |-> OpenDisc end spec RCC8Model_OpenDisc[UnboundedMetricSpace] = %def ConstructModelFromBaseRelationModel[ RCC8BaseRelationModel_OpenDisc[MetricSpace] fit Elem |-> OpenDisc] then %def ops inv__ : BaseRel -> BaseRel; __cmps__: BaseRel * BaseRel -> Rel end view RCC8Model_OpenDisc_ExtModels_RCC8CompositionTable[UnboundedMetricSpace] : RCC8CompositionTable to RCC8Model_OpenDisc[UnboundedMetricSpace] = ops dc |-> dcRel, ec |-> ecRel, po |-> poRel, tpp |-> tppRel, ntpp |-> ntppRel, tppi |-> tppiRel, ntppi |-> ntppiRel, eq |-> eqRel end view MetricSpace_induces_AlgebraOfBinaryRelations_OpenDisc[UnboundedMetricSpace] : AlgebraOfBinaryRelations to RCC8Model_OpenDisc[UnboundedMetricSpace] = Elem |-> OpenDisc end view MetricSpace_induces_ModelOfRCC8_OpenDisc[UnboundedMetricSpace] : RCC8 to RCC8Model_OpenDisc[UnboundedMetricSpace] = ops dc |-> dcRel, ec |-> ecRel, po |-> poRel, tpp |-> tppRel, ntpp |-> ntppRel, tppi |-> tppiRel, ntppi |-> ntppiRel, eq |-> eqRel end %( Special Models )% view EuclideanSpace2D_Is_EvenLarger : UnboundedMetricSpace to EuclideanSpace2D = S |-> Point, d |-> dist end spec RCC8EuclideanSpace2D_OpenDisc = %def RCC8Model_OpenDisc[view EuclideanSpace2D_Is_EvenLarger] end view RCC8EuclideanSpace2D_OpenDisc_models_RCC8 : RCC8 to RCC8EuclideanSpace2D_OpenDisc = ops dc |-> dcRel, ec |-> ecRel, po |-> poRel, tpp |-> tppRel, ntpp |-> ntppRel, tppi |-> tppiRel, ntppi |-> ntppiRel, eq |-> eqRel end