Introduction Differences Source Lite Syntax Lite Mapping Lite Triples Lite Proof DL Syntax DL Mapping DL Triples DL Proof

## dl Sufficiency Proof

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:

Sufficiency Theorem
Every acceptable graph is mappable.

In fact the following stronger result is proved:

Correspondence Theorem
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.

Empty Graph Lemma
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.

### Initial Lemmas

Before we start on the reduction lemmas, we present three results that are frequently needed.

Description Lemma
If a graph g corresponds to t and contains a description, an unnamedDataRange or a restriction node n that is not the object of any triple then n corresponds to a directive in t
Proof:
n is blank and hence must arise from one of the mapping rules that introduces a blank node. Moreover, by considering the `rdf:type` triples with n as subject, the only mapping rules to consider are those for the description dataRange or restriction construct from the abstract syntax.
These mapping rules can only be invoked in certain contexts [ ... enumerate contexts, automatic needed? ... ]; in all of these the returned node becomes the object of a triple, except for the context transforming a directive within the ontology construct link to mapping rule.

A similar result holds for unnamed individuals.

Unnamed Individual Lemma
If a graph g corresponds to t and contains an unnamedIndividual node n that is not the object of any triple then n corresponds to a directive in t
Proof:
n is blank and hence must arise from one of the mapping rules that introduces a blank node. Moreover, by considering the `rdf:type` triples with n as subject, the only mapping rules to consider are those for the individual construct from the abstract syntax.
These mapping rules can only be invoked in certain contexts [ ... enumerate contexts, automatic needed? ... ]; in all of these the returned node becomes the object of a triple, except for the context transforming a directive within the ontology construct link to mapping rule.

The reduction lemmas all involve taking a subgraph of an acceptable graph. Most subgraphs of acceptable graphs are themselves acceptable. The precise relationship is:

Subgraph Lemma
Given a graph h such that:
Then h is acceptable.
Proof:
Given an acceptable graph g with subgraph h, take the categorization of the nodes of g and restrict it to be a categorization of the nodes of h.

In a typical mapping of an abstract syntax tree, explicit type triples get generated many times over. To avoid complications from this we use the following result.

Explicit Type Lemma
If n is a node in an acceptable graph g then either n is a builtin uriref or when it has a category found in the table below g contains an explicit type triple as shown.
Proof:
By the first condition on acceptable graphs there is some such an explicit type triple, moreover it cannot have object `rdf:Property`, `rdfs:Class`, `owl:FunctionalProperty`, `owl:DeprecatedProperty`, `owl:DeprecatedClass`, and must appear in one of the triple tables. By inspection of the triple tables, many categories have only one such explicit type triple and these are listed below.

### Reduction Lemmas

The typical reduction lemma has an acceptable graph g and a subgraph h. We need to show that h is acceptable, and that given a correspondence involving h we can form a correspondence of g. Using the subgraph lemma we only need to consider whether h is explicitly typed and whether the blank nodes in h meet the structural requirements. Such requirements on a blank node b in h are characterised by the set of triples with b as their subject.

Most nodes in an acceptable graph require explicit type triples. In general, the induction works by first reducing all other triples involving a node, and then by reducing the explicit type triple. This does not work for most blank nodes which are treated differently.

We first consider the case where of a ground explicit type triple.

Ground Explicit Type Reduction Lemma
If g is an acceptable graph containing some ground, explicit type triple tr with subject n which appears in no other triple, except other explicit type triples, then g can be reduced by removing that triple.
Proof:
Let h be g - { tr }. Every node in h is explicitly typed in g and hence also explicitly typed in h (if n is in h, then it has multiple explicit type triples in g and hence has at least one of them in h). For any blank node b in h the set:
{ s : sh, s has subject b }
is the same as the set:
{ s : sg, s has subject b }
Since g is acceptable, this set of triples meets the structural requirements. So by the subgraph lemma , h is acceptable.
We use the table below to look up the triple and find a directive in the abstract syntax. This table has been constructed such that the directives map to the given explicit type triple and possibly other explicit type triples that are required by the explicit type lemma . Given an abstract syntax tree corresponding to h we can form a tree corresponding to g by adding the additional directive found in the table.

We now consider the case where the explicit type is a blank node.

Blank Explicit Type Reduction Lemma
If g is an acceptable graph containing some explicit type triple tr with uriref subject n which appears in no other triple, except for other explicit type triples, and the object of tr is a blank node b, then g can be reduced by removing that triple.
Proof:
As before, h is acceptable.
b must be a description or a restriction (by inspection of the triple tables). We use the table below to find a directive corresponding to tr. Each entry contains one unexpanded nonterminal from the abstract syntax grammar; this being either `restriction` or `description`. Since b is the object of at most one triple in g, and that triple is tr which is not in h, we have that b is not the object of any triple in h. Hence, the description lemma applies and a directive d in any abstract syntax tree corresponding to h corresponds to d. Thus a new abstract syntax tree can be formed, by cutting d from the old tree and pasting it into the partially unexpanded directive, and adding this new directive into the tree.

Other ground triples can be treated similarly.

Ground Triple Reduction Lemma
If g is an acceptable graph containing a ground triple tr, which is not an explicit type triple, then g can be reduced by removing that triple.
Proof:
As before, h is acceptable.
We use the table below, to look up the triple tr and find a directive to be added to an abstract syntax tree corresponding to h, to form an abstract syntax tree corresponding to g.
This table has been constructed such that the directives map to the given ground triple and possibly explicit type triples that are known to be in g by the explicit type lemma .

Triples with a ground subject and blank object where that object is a restriction, description, unnamedDataRange or unnamedIndividual node can be treated failry similarly; using the description lemma or the unnamed individual lemma . We refer to these triples as Ground-Ground-Blank (GGB) triples.

GGB Triple Reduction Lemma
If g is an acceptable graph containing a triple tr, with ground subject, and blank object b, such that: b does not have explicit type `rdf:List`; and tr is not an explicit type triple, then g can be reduced by removing that triple.
Proof:
As before, h is acceptable.
Take an abstract syntax tree t corresponding to h. By inspection of the triple table b must have category unnamedIndividual, unnamedDataRange, descriptionor restriction. Similarly to in the blank explicit type reduction lemma using either the description lemma or the unnamed individual lemma we find a directive d in t corresponding to b. We can form a tree corresponding to g by:
• finding tr in the table below.
• modify the directive found in the table by substituting d appropriately.
• modifying t by deleting d and adding the new directive modified from the table below.

Blank nodes with explicit type `rdf:List` are treated somewhat differently. Instead of forming a subgraph we form a smaller graph by deleting three triples and replacing the object of a fourth triple.

First List Reduction Lemma
If g is an acceptable graph containing a node n of explicit type `rdf:List` such that n is not the object of a triple with predicate `rdf:rest`, and n is the subject of a triple with predicate `rdf:first` and a uriref or literal object uuu, then it is reducible.
Proof:
By the structural constraints on n in g there must be nodes sss, lll and uriref ppp such that the following triples are in g.
```sss ppp n .
n `rdf:type rdf:List` .
n `rdf:first` uuu .
n `rdf:rest` lll .
```
Moreover, there are no other occurrences of n in g. Let h be g with these four triples deleted, and the following triple added:
```sss ppp lll .
```

h is acceptable with the same categorization as g because:

• the node n has been excised completely, and so cannot contribute to non-acceptability,
• ppp is not rdf:type, (since there is no match in the triple tables) and so no explicit type triples, other than for n have been excised.
• lll is either `rdf:nil` or of the same category as n, by considering the triple tables for `rdf:rest`. Either way since
sss ppp n .
is in the triple tables, so is
sss ppp lll .
• Any other contravention of the acceptability of h would not involve the new or deleted triples, and hence also be a contravention of the acceptability of g.
Given an abstract syntax tree t corresponding to h then since the node lll is either of a list category or `rdf:nil`, it must arise from one of the Seq mapping rules. Moreover ppp is not rdf:rest, and so the context in which that mapping rule was invoked is not one of the tail recursion rules add list of rules. Thus the mapping rule that gave lll as a result must have been invoked from add list of rules.
In each of these rules, the sequence construct arises from a repeated construct in an abstract syntax rule one of:
• { individualID }
• { description }
• { Super( description ) }
• { dataLiteral }
Modifying t by adding the uriref or literaluuu at the beginning of the appropriate matching subtree results in an abstract syntax tree corresponding to g.

We now consider the case where the first item in the list is a blank node.

Second List Reduction Lemma
If g is an acceptable graph containing a node n of explicit type `rdf:List` such that n is not the object of a triple with predicate `rdf:rest`, and n is the subject of a triple with predicate `rdf:first` and a blank object bbb, then it is reducible.
Proof:
We construct h similarly to the first list reduction lemma . The triples
```sss ppp n .
n `rdf:type rdf:List` .
n `rdf:first` bbb .
n `rdf:rest` lll .
```
found in g are replaced by the single triple:
```sss ppp lll .
```
in h. h similarly is acceptable. However, since bbb is blank, the node n must be of category listOfDescription. So ppp must be `owl:intersectionOf` or `owl:unionOf` .
Given an abstract syntax tree t corresponding to h As in lemma 1 the mapping rule that invoked the rule that created lll must be one of add smaller list of rules.
In each of these rules, the sequence construct arises from a repeated construct in an abstract syntax rule of { description } or { Super( description ) }.
Since bbb is the object of at most one triple in g and that triple has been deleted, it is not the object of any triple in h and the description lemma applies. Thus we can modify t by cutting the top-level description or restriction that corresponds to bbb and pasting it at the beginning of the appropriate matching subtree, possibly inside a `Super( )` construct. The resulting abstract syntax tree corresponds to g.

We now consider unnamedIndividual nodes. These behave quite similarly to individualID nodes, but need to be treated slightly differently. With individualIDs the uriref can link multiple directives in the abstract syntax; with unnamed individuals it is necessary to ensure that everything that needs to be said about the individual is said in a single directive.

Nearly as before, we first consider a solitary explicit type triple, dividing it into two cases: a named or an unnamed type. Then we consider the other triples (including multiple explicit type triples).

We first consider the case where the type is not a blank node

First Unnamed Individual Explicit Type Reduction Lemma
If g is an acceptable graph containing some explicit type triple tr with subject n which is an unnamed individual, and has a uriref node as object, and n appears in no other triple, then g can be reduced by removing that triple.
Proof:
Let h be g - { tr }. Every node in h is explicitly typed in g and hence also explicitly typed in h (n is not in h). For any blank node b in h the set:
{ s : sh, s has subject b }
is the same as the set:
{ s : sg, s has subject b }
Since g is acceptable, this set of triples meets the structural requirements, and by the subgraph lemma , h is acceptable.
Given an abstract syntax tree corresponding to h we can form a tree corresponding to g by adding the additional directive `Individual(Type(classID))` where `classID` is the object of the `tr`. This new tree corresponds to g.

The case where the type is a blank node is similar.

Second Unnamed Individual Explicit Type Reduction Lemma
If g is an acceptable graph containing some explicit type triple tr with subject n which is an unnamed individual, and has a blank node as object, and n appears in no other triple, then g can be reduced by removing that triple.
Proof:
h is acceptable as before.
Given an abstract syntax tree t corresponding to h, as in the blank explicit type reduction lemma , we can find a directive in t which corresponds to the type of n. We can form a tree corresponding to g from t by deleting that directive and adding the additional directive `Individual(Type(expr))` where `expr` is the restriction or description directive deleted from t. This new tree corresponds to g.

We now consider some other triples with an unnamed individual as subject and a uriref or literal as object

First Unnamed Individual Triple Reduction Lemma
If g is an acceptable graph containing a triple tr with subject n such that: n which is an unnamed individual; there is some other explicit type triple for n in g; tr has a uriref or literal node as object; and n is not the object of any triple, then g can be reduced by removing tr.
Proof:
We show h is acceptable, as in first unnamed individual explicit type reduction lemma , with the following additional considerations. n does have an explicit type in h, moreover since it has category unnamedIndividual, it does not violate the structural constraints.
Given an abstract syntax tree t corresponding to h we can form a tree corresponding to g by:
• finding tr in the table below
• using the unnamed individual lemma to find the directive in t corresponding to n, this has form `Individual( … )`.
• modifying t by adding into the `Individual( … )` expression the syntactic expression found with tr in the table below.

We now consider some other triples with an unnamed individual as subject and a blank node as object

Second Unnamed Individual Triple Reduction Lemma
If g is an acceptable graph containing a triple tr with subject n such that: n is an unnamed individual; there is some other explicit type triple for n in g; tr has a blank node b as object; and n is not the object of any triple, then g can be reduced by removing tr.
Proof:
h is acceptable, as in first unnamed individual triple reduction lemma .
Take an abstract syntax tree t corresponding to h. By inspection of the triple table b must have category unnamedIndividual, description or restriction and so by the description lemma or the unnamed individual lemma we find a directive d in t corresponding to b. We can form a tree corresponding to g by:
• finding tr in the table below.
• modify the syntax expression found in the table by substituting d appropriately.
• using the unnamed individual lemma to find the directive in t corresponding to n, this has form `Individual( … )`.
• modifying t by adding into the `Individual( … )` expression the modified syntactic expression from the table below.

We now consider some other blank nodes.

First Structure Reduction Lemma
If g is an acceptable graph containing a blank node n such that: n is of category allDifferent, unnamedDataRange, description or restriction; there are no triples with subject n and object being a blank node; n is not the object of any triple; n is not the subject of a triple with predicate `owl:equivalentClass` or `owl:disjointWith`. Then g can be reduced by removing all the triples involving n.
Proof:
As before, h is acceptable.
The triple tables impose significant structural requirements on all nodes satisfying the premises of this lemma. The table below gives an exhaustive listing of the possibilties, along with a corresponding directive from the abstract syntax.
As before we can modify an abstract syntax tree corresponding to h by adding the appropriate directive, to get an abstract syntax tree corresponding to g.

We also consider some cases where a restriction or description has a second restriction or description embedded within it.

Second Structure Reduction Lemma
If g is an acceptable graph containing a blank node n such that: n is of category description or restriction; there is exactly one triple with subject n with object being a blank node b; b is of category description or restriction; n is not the object of any triple; n is not the subject of a triple with predicate `owl:equivalentClass` or `owl:disjointWith`. Then g can be reduced by removing all the triples involving n to form h.
Proof:
As before, h is acceptable.
Given an abstract syntax tree t corresponding to h, as in the blank explicit type reduction lemma we can find a directive d that corresponds to b. We use the table below to look up the node n, and find a directive, into which we substitute the directive d appropriately. We then modify t by deleting d and adding the new modified directive from the table. This then corresponds to g.

We finally consider the case of a restriction or description compared with some other node.

Description Comparison Reduction Lemma
If g is an acceptable graph containing a blank node n such that: there is a triple tr with subject n and with predicate `owl:equivalentClass` or `owl:disjointWith`; tr has object b. Then g can be reduced by removing tr to form h.
Proof:
The only triples in the triple tables matching tr are ones in which n is of category description or restriction.
We note that n meets the structural constraints in h, because it meets those constraints in g and the deleted triple is not relevant to those constraints. Thus, as before, h is acceptable.
Given an abstract syntax tree t corresponding to h, as in the blank explicit type reduction lemma we can find a directive d1 in t that corresponds to n. Note, that since g is appropriate, and n is the subject of an `owl:equivalentClass` or `owl:disjointWith` triple, then n is not the object of any triple in neither g nor h. If b is blank, then it is a restriction or description node, and we similarly can find a directive d2 in t that corresponds to b. We use the table below to look up the triple tr, and find a directive, into which we substitute the description or restriction d1 and either the classID uriref b or the description or restriction d2 appropriately. We then modify t by adding the new modified directive and by deleting d1, and if applicable d2. This then corresponds to g.

### Structural Lemmas

This section further explores the constraints on blank nodes in an acceptable graph.

Blank Node Lemma
If an acceptable graph g contains a blank node then it contains either a blank node that is the object of a triple with a uriref subject, or it contains a blank node which is the object of no triples.
Proof:
Define a partial function on the blank nodes of g mapping a blank node bi in g which is the object of a triple tr to the subject of that triple bi+1.
Since g contains a first blank node b1, we can form a sequence b1, b2 … Since g is finite, and does not contain any cycles of blank nodes, this sequence must terminate. The last element of this sequence, must either be a blank node that is not the object of any triple, or a uriref node that is the subject of a triple with a blank node as object.

Lists can always be reduced.

List Lemma
An acceptable graph g containing a node of explicit type `rdf:List` is reducible.
Proof:
We define a partial function from a node bi of explicit type `rdf:List` that returns the subject bi+1 of the triple with predicate `rdf:rest` and object bi+1.
As before the sequence b1, b2 … terminates, furnishing a node bn that has explicit type `rdf:List` and is not the object of an `rdf:rest` triple.
Hence, either the first list reduction lemma or the second list reduction lemma apply to g.

We can also combine the reduction lemmas for unnamed individuals:

Unnamed Individual Reduction Lemma
An acceptable graph with an unnamed individual node that is not the object of any triple can be reduced.
Proof:
One of the following must apply:

### Main Result

The final stages of the proof.

Ground Reducible Graph Lemma
A ground non-empty acceptable graph can be reduced by one of the reduction rules.
Proof:
Either the ground explicit type reduction lemma or the ground triple reduction lemma applies.

Reducible Graph Lemma
A non-empty acceptable graph can be reduced by one of the reduction rules.
Proof:
Suppose not. Then by the ground reducible graph lemma we have that there must be a blank node b. Moreover, by the list lemma b cannot be of type `rdf:List`. Hence, if b were the object of a triple with a uriref subject, we can apply either the ggb triple reduction lemma or the blank explicit type reduction lemma . Thus, by the blank node lemma , without loss of generality, we have that b is not the object of any triple.
Since b is not of type `rdf:List`, it must be of category unnamedIndividual, allDifferent, unnamedDataRange, description, or restriction. By the unnamed individual lemma the first possibility is excluded. Since the description comparison reduction lemma does not apply, b is not the subject of a triple with predicate `owl:disjointWith`, or `owl:equivalentClass`. The conditions on b and g now meet the premises of the structured nodes lemma and so g is, after all, reducible.

We now can prove the main results:

Correspondence Theorem
Every acceptable graph corresponds to an abstract syntax tree.
Proof:
By induction, with initial step furnished by the empty graph lemma and inductive step by the reducible graph lemma .
Corollary: Sufficiency Theorem
Every acceptable graph is mappable.