% $Id: RDFUtil.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
%
% 2.2. Utility Relations; "Layer 1"
% http://www.w3.org/RDF/Group/1998/02/WD-rdf-syntax-19980216/#model

RDFUtil: trait

   includes
      RDFCore,
      Positive(Ord) % for ordinals

   introduces
      ok: Set[Arc] → Bool            % meets the constraints in the spec

      [ __ ]: Arc → Node       % reification
      reify: Arc → Set[Arc]

      [ __ ]: Ord → Node          % ordinals

      Property: → Node % RDF:Property
      InstanceOf: → Node
      PropName: → Node
      PropObj: → Node
      Value: → Node

      Seq: → URI
      Bag: → URI
      Alt: → URI

   asserts
     ∀ n:Ord, r, r2, t, t2, typ: Node, v, v2: Value,
        ps, d: Set[Arc]

        isPropertyType(InstanceOf);
          isPropertyType(PropName);
          isPropertyType(PropObj);
          isPropertyType(Value);

% reification

        ¬ isPropertyType(Property);

        reify([ t, r, v ]) =
          insert([InstanceOf,  [ [ t, r, v ] ], ref(Property)],
            insert([PropName,  [ [ t, r, v ] ], ref(t)],
              insert([PropObj, [ [ t, r, v ] ], ref(r)],
                insert([Value, [ [ t, r, v ] ], v], {}))));

% "Elements of Triples that have RDF:InstanceOf as the first item in
% the triple must have elements of Nodes as their second item and third
% item. "

        ok(ps) ⇒ ([ InstanceOf, r, v ] ∈ ps ⇒ tag(v) = ref);

% Collections

        ¬ isPropertyType([Seq]);
        ¬ isPropertyType([Bag]);
        ¬ isPropertyType([Alt]);

% "There may be at most one arc from a single collection node labeled
% with each element of Ord and the elements of Ord must be used in
% sequence starting with RDF:1."

        ok(ps) ∧ (typ = [Seq] ∨ typ = [Bag] ∨ typ = [Alt])
          ∧ [ InstanceOf, r, ref(typ) ] ∈ ps ⇒
          (([ t, r, v ] ∈ ps ∧
            [ t2, r, v2 ] ∈ ps) ⇒ (t = t2 ∧ v = v2));

% "and the elements of Ord must be used in sequence starting with
% RDF:1."

        ok(ps) ∧ (typ = [Seq] ∨ typ = [Bag] ∨ typ = [Alt])
          ∧ [ InstanceOf, r, ref(typ) ] ∈ ps ⇒
           ([ [ n+1 ], r, v ] ∈ ps ⇒ [ [ n ], r, v ] ∈ ps);

% "For nodes that are instances of the RDF:Alt collection type, there
% must be exactly one member whose arc label is RDF:1 "

        ok(ps) ∧ [InstanceOf, r, ref([Alt])] ∈ ps ⇒
          ∃ v ([[1], r, v] ∈ ps)


% Review Notes, 1998-03-04
% suggestion: "Elements of Triples that have RDF:InstanceOf as the
% first item in the triple must have elements of Nodes as their second
% item and third item."
% change it so Triples is the whole cross product, and property
% is the subset that satisfies constraints such as this.
% hmm... I have in stead added an "ok" predicate on Models

% "all that is done is to add to the data model" which data model?

% What does this constraint apply to? suggest: model
% (hmm... examples section uses "graph." Choose one or the other.)
% "There may be at most one arc from a single collection node labeled
% with each element of Ord and the elements of Ord must be used in
% sequence starting with RDF:1."

[Index]

HTML generated using lsl2html.