% $Id: RDFAbSyn.lsl,v 1.9 2003/01/31 14:51:05 connolly Exp $
%
%html <h2>References</h2>
%html <cite><a href="http://www.w3.org/TR/2003/WD-rdf-concepts-20030123/">Resource Description Framework (RDF): Concepts and Abstract Syntax</a></cite>
%html <hr />

RDFAbSyn: trait
  includes
    NullOpt(URI_reference),
    NullOpt(Language_Identifier),
    FiniteMap(Blank_node, Term),

    % An RDF graph is a set of RDF triples. (6.2)
    % We restrict ourselves to finite sets here.
    Set(triple, Graph for Set[E])

    % 6.1 RDF Triples
    % We introduce an auxiliary sort here, Term.
    % We'll specify constraints such as
    % the fact that a predicate can't be a bnode, in axioms below.
    triple tuple of
      subject: Term,
      predicate: Term,
      object: Term

    % 6.4 RDF URI References
    % 6.5 RDF Literals
    % 6.6 Blank Nodes
    % @@TODO: connect with URI trait. pay attention to IRI issues
    Term union of uref: URI_reference,
	 blank: Blank_node,
	 lit: Literal

    % REVIEW: 6.5 needs to say the datatype URI and lang tags are optional
    Literal tuple of
      lexical_form: UnicodeStringInNormalFormC, % TODO: factor out charmod stuff
      lang: Opt[Language_Identifier], % RFC 3066
      dt: Opt[URI_reference] 

  introduces
    % 6.3 Graph Equality
    graphEquiv: Graph, Graph -> Bool

    plain : Literal -> Bool % 6.5
    typed : Literal -> Bool % 6.5

    __ [ __ ] : Map[Blank_node, Term], Term -> Term
    __ [ __ ] : Map[Blank_node, Term], triple -> triple
    __ [ __ ] : Map[Blank_node, Term], Graph -> Graph
    allBlank : Map[Blank_node, Term] -> Bool


  asserts
    forall s: triple,
           l: Literal, i: URI_reference, b: Blank_node,
	   ts1, ts2: Graph, spo: triple,
	   s, p, o: Term,
	   m: Map[Blank_node, Term]

    % 6.1 RDF Triples
    tag(s.subject) = uref \/ tag(s.subject) = blank;
    tag(s.predicate) = uref;


    % 6.5
    plain(l) = (tag(l.dt) = absent);
    typed(l) = (tag(l.dt) = value);

    % 6.3 Graph Equality
    % I think 'equality' is a misnomer, but
    % let's see if it works this way...
    (allBlank(m) /\ m[ts1] = m[ts2]) => graphEquiv(ts1, ts2);

    % where blank-node maps extend to triple-set maps
    % in the obvious fashion...
    m[blank(b)] = (if defined(m, b) then apply(m,b) else blank(b));
    m[uref(i)] = uref(i);
    m[lit(l)] = lit(l);
    m[[s, p, o]] = [m[s], m[p], m[o]];
    m[{}] = {};
    m[insert(spo, ts1)] = insert(m[spo], ts1);


% historical note...
%html <h2>Acks</h2><p>Pat Hayes suggested, after I explained
%html the RDF Model and Syntax to him, that what
%html is called a <dfn>model</dfn> in the RDF specs
%html is called an abstract syntax, a term coined
%html by McCarthy; see, for example section
%html <a href="http://www-formal.stanford.edu/jmc/towards/node12.html">
%html Abstract Syntax of Programming Languages</a>
%html in <a href="http://www-formal.stanford.edu/jmc/towards/towards.html">
%html Towards a Mathematical Science of Computation</a>
%html (Tue, 14 May 1996 21:10:20 GMT).</p>