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.
< 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.
< 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').In fact the following stronger result is proved:
%%theorem('Correspondence').The structure of the proof is inductive. The initial case from which the induction starts is the empty graph.
%%lemma('Empty Graph').Ontology()
.
The inductive step involves a number of distinct cases. To structure the proof we introduce the concept of reducible.
Usually h is a proper subgraph of g.
The rest of this section gives: