This section shows that the definition of a graph as triples is sufficient to ensure that the graph also falls under the definition of a graph via the abstract syntax and the mapping rules.

We start by defining terms, and then move into the proof.

acceptable
An RDF graph is accceptable if it meets the constraints specified for a graph as triples
mappable
An RDF graph is mappable if there is an abstract syntax tree in the abstract ontology that maps to it.
correspondences between abstract syntax trees and node categorizations
A correspondence is a 3-tuple < g, t, C > where g is a graph which is both acceptable and mappable, t is an abstract syntax tree that maps to g, and C is a categorization of the nodes of g which shows that it is acceptable. Moreover, in a correspondence, every uriref has the same categorization in the abstract syntax as in C.
corresponds
An acceptable graph g, with categorization C corresponds to an abstract syntax tree t if there is a correspondence < g, t, C >. Under such a correspondence a subtree u of t corresponds to a node n in g if the mapping of t involves mapping u and returning n.

The goal of this section is to show that a graph is acceptable iff it is mappable. However, due to time pressure, I omit showing that mappable graphs are acceptable: this is the easier direction since the triple tables have been generated from the mapping rules. Hence, we aim to show the following:

%%theorem('Sufficiency').
Every acceptable graph is mappable.

In fact the following stronger result is proved:

%%theorem('Correspondence').
Every acceptable graph corresponds to an abstract syntax tree.

The structure of the proof is inductive. The initial case from which the induction starts is the empty graph.

%%lemma('Empty Graph').
The empty graph corresponds to Ontology().

The inductive step involves a number of distinct cases. To structure the proof we introduce the concept of reducible.

reducibility
An acceptable graph g is reducible, if there is a related graph h with fewer triples, which is also acceptable, such that if h corresponds to t then g corresponds to some defined transformation of t.

Usually h is a proper subgraph of g.

The rest of this section gives:

  1. Reduction lemmas, each showing that an acceptable graph with a certain characteristic is reducible.
  2. Structural lemmas, which combine the reduction lemmas paying special attention to the structure of the blank nodes.
  3. The proof of the main theorem, which simply combines the structural lemmas with the reduction lemmas into an inductive argument.