% $Id: RDFSemantics.lsl,v 1.2 2001/03/30 18:42:44 connolly Exp $
%
%
%html <p><a href="http://www-diglib.stanford.edu/diglib/ginf/WD/rdf-alg/rdf-alg.ps">Algebraic Specification for RDF Models</a>, Sergey Melnik, meknik@db.stanford.edu July 1999.
%html from <a href="http://www-diglib.stanford.edu/diglib/ginf/">GINF</a></p>

RDFSemantics: trait
  includes
    FormalSystem,
    RDFAbSyn,
    Relation(Resource, Rel[Resource]),
    RelSet(Object, Set[Object])

  introduces
    universe, resources, literals, properties: Interpretation -> Set[Object]
    statement: Interpretation, Object, Object, Object -> Bool
    reify: Interpretation, Object, Object, Object -> Object

    % melnik 2: basic resources
    % leaving containers out for now: Seq, Bag, Alt, N'
    Statement, type, predicate, subject, object, value: Interpretation -> Object

    RDF1: -> System
    andI: -> Rule
    andE: -> Rule
    exI:  -> Rule

    ind: URI, Interpretation -> Resource
    pred: URI, Interpretation -> Rel[Resource]

  asserts
    forall x: Object, m: Interpretation, fls: Set[Formula],
	p, s, o, r, p2, s2, o2: Object

    % melnik 1: "Resources and literals are disjunct"
    model(RDF1, m, fls) =>
      (x \in universe(m) => ((x \in resources(m)) <=> (x \notin literals(m))));

    % skipping melnik 2; I don't see where Kappa is used

    % melnik 3: properties are resources [leaving out ordinals for now]
    model(RDF1, m, fls) =>
      ((x \in properties(m)) => (x \in resources(m)));

    % melnik 4: set of statements
    model(RDF1, m, fls) =>
      (statement(m, p, s, o) => (p \in properties(m)
				  /\ s \in resources(m)
				  /\ o \in universe(m)) );

    % melnik 5: [skipping containers for now]

    % melnik 6: a resource cannot be typed using a literal
    model(RDF1, m, fls) =>
      (statement(m, type(m), s, o) => o \in resources(m));

    % melnik 7: constants for basic resources
    % [leaving out Seq, Bag, Alt for now]
    model(RDF1, m, fls) =>
      (Statement(m) \in (resources(m) - properties(m)));

    % melnik 8: constants for basic properties
    model(RDF1, m, fls) =>
      (type(m) \in properties(m)
      /\ predicate(m) \in properties(m)
      /\ subject(m) \in properties(m)
      /\ object(m) \in properties(m)
      /\ value(m) \in properties(m));

    % melnik 9: Rf is a partial one-to-one function
    model(RDF1, m, fls) =>
    ( reify(m, p, s, o) = r <=> (  statement(m, type(m), r, Statement(m))
				/\ statement(m, predicate(m), r, p)
				/\ statement(m, subject(m), r, s)
				/\ statement(m, object(m), r, o) ) );

    % melnik 10: uniqueness of reificiation
    model(RDF1, m, fls) =>
    ( reify(m, p, s, o) = reify(m, p2, s2, o2)
      => (p=p2 /\ s=s2 /\ o=o2));


    forall
	f, g: Formula,
	a, b: Atomic,
	i: Interpretation,
	p, s, o: URI

    wff(RDF1, f); %hmm... separate sorts for RDF formula and formula in general?
                  % i.e. wff(RDF1, asFormula(m))?

    direct_consequence(RDF1, andI, insert(f, {g}), f \U g);
    direct_consequence(RDF1, andE, {insert(a, f)}, {a});

    interpret(RDF1, i, insert(a, f)) = interpret(RDF1, i, {a})
					 /\ interpret(RDF1, i, f);
    interpret(RDF1, i, {[const(p), const(s), const(o)]}) = ind(s, i) \langle pred(p, i) \rangle ind(o, i);

    %@@more: interpretation of formulas with existentials

% Acks/Fodder:
% rm508 meeting: soundness under deletion of arcs; aka erasure

% Semantics of Predicate Calculus
% http://www.cee.hw.ac.uk/courses/3pe1/20/9.htm
% Thu, 16 Nov 2000 17:19:02 GMT

% http://www.google.com/search?q=first+order+predicate+calculus
% http://directory.google.com/Top/Science/Math/Logic_and_Foundations/Computational_Logic/Combinatory_Logic_and_Lambda_Calculus/Formulae-as-Types_Correspondence/