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]