Revised Syntax

Navigation

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

lite 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:

Reduction lemmas, each showing that an acceptable graph with a certain characteristic is reducible.
Structural lemmas, which combine the reduction lemmas paying special attention to the structure of the blank nodes.
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 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 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:

h is a subgraph of an acceptable graph g
Every non-literal, non-built-in node in h is explicitly typed.
h satisfies the additional structural requirements on blank nodes.

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.

add machine generated table

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 : s ∈ h, s has subject b }
is the same as the set:
{ s : s ∈ g, 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.

add machine generated 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 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 restriction . 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.

add machine generated table

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 .

add machine generated table

Triples with a ground subject and blank object where that object is a restriction 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, or 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.

add machine generated table

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 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 }
{ Super( description ) }

Modifying t by adding the uriref uuu at the beginning of the appropriate matching subtree results in an abstract syntax tree corresponding to g.

add machine generated table

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

Second List Reduction Lemma

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 .
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 { 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 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.

add machine generated table

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 : s ∈ h, s has subject b }
is the same as the set:
{ s : s ∈ g, 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.

add machine generated table

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

add machine generated table

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 allDifferentrestriction; there are no triples with subject n and object being a blank node; n is not the object of any triple. 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.

add machine generated table

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 b_i in g which is the object of a triple tr to the subject of that triple b_i+1.
Since g contains a first blank node b₁, we can form a sequence b₁, b₂ … 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 b_i of explicit type rdf:List that returns the subject b_i+1 of the triple with predicate rdf:rest and object b_i+1.
As before the sequence b₁, b₂ … terminates, furnishing a node b_n 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:

first unnamed individual explicit type reduction lemma
second unnamed individual explicit type reduction lemma
first unnamed individual triple reduction lemma
second unnamed individual triple reduction lemma

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, or restriction. By the unnamed individual lemma the first possibility is excluded. The conditions on b and g now meet the premises of the first structure reduction 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.