See: Larch home page,
Larch FAQ
RDFCore: trait
includes
Set(Arc),
String(Char)
% "The triple composed of a property type, a resource, and a value is
% an RDF property."
Arc tuple of name: Node, object: Node, value: Value
% "the third item is either an element of Nodes or an atomic value (an
% RDF string). "
Value union of str: String[Char], ref: Node
introduces
isPropertyType: Node → Bool % PropertyTypes is subset of Node
% larch doesn't have subsorts,
% so a characteristic function is
% a handy equivalent of a subset
[ __ ]: URI → Node % make a node from a URI
[ __ ]: Set[Arc] → Node % the node of a Description
isDescription: Set[Arc] → Bool
schema: Node → Node % only specified over property types
__ .. __: Node, Name → Node % schema..name qualification
asserts
∀ r, t: Node, v: Value, p, p2: Arc, ps, d: Set[Arc]
% "The first item of each 3-tuple (triple) is an element of PropertyTypes"
[ t, r, v ] ∈ ps ⇒ isPropertyType(t);
% "A set of triples that all refer to the same node (the second item
% in the triple) can be grouped as a unit called a Description."
% in this case, a description is a non-empty, finite set of triples
¬isDescription({});
isDescription({p});
isDescription(insert(p, insert(p2, ps))) =
(p.object = p2.object ∧ isDescription(insert(p2, ps)))
% Review Notes, 1998-03-04
% @@application?
% @@understand?
% @@Two RDF strings are deemed to be the same ...
% "an RDF data model instance" What's that?
% suggest: a description or a collection
% The use of RDF:Value as a sort of "default value" for structured
% values doesn't seem to be described in the spec.
[Index]