% $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.