Jos De Roo

A Canonical-Expansion Theorem for Basic N3 Entailment

Draft status. Candidate text for a publication section.
Scope. Basic N3 entailment only. This does not cover the additional semantics of log: built-ins such as log:implies.

Abstract

We give a syntactic characterisation of basic entailment for finite, closed, normalised abstract N3 graphs. The result is an N3 analogue of the RDF simple-entailment interpolation lemma. Because N3 includes explicit universal variables and quoted graph terms, the appropriate object is not the premise graph itself but its canonical expansion: the union of all ground universal instances of the premise, with fresh witnesses for existential variables. Basic N3 entailment is then equivalent to containment of every universal instance of the conclusion, after a suitable existential instantiation, in this canonical expansion.

Background and notation

The N3 semantics defines an abstract graph as a triple:

G = (U, E, F)

where:

N3 terms include IRIs, literals, variables, lists, and graph terms. Ground graph terms are compared modulo the N3 graph-term isomorphism relation.

The semantics of variables uses assignments that provide both:

  1. a denotation in the semantic domain; and
  2. a ground term representation.

This second component is essential because variables may occur freely inside quoted graph terms. The semantic operation of total application grounds such occurrences recursively, while respecting variable scope inside nested graph terms.

Throughout this section, entailment means basic N3 entailment.

Normalisation assumptions

Let

G = (UG, EG, FG)    and    H = (UH, EH, FH)

be finite, closed, normalised abstract N3 graphs.

We assume:

  1. variables of G and H have been renamed apart;
  2. free variables, if any occur in a concrete syntax presentation, have first been added to the appropriate universal-variable set;
  3. graph terms are considered modulo graph-term isomorphism;
  4. equality of triples containing graph terms is taken modulo that isomorphism.

These assumptions are standard hygiene conditions and do not affect entailment.

Ground terms with witnesses

Let

GT*

be the set of ground N3 terms over the language, extended with a countably infinite supply of fresh witness names.

These witness names play the same role as labelled nulls in canonical-model constructions.

Ground instances

For a graph

K = (UK, EK, FK)

and a map

μ : UK ∪ EK → GT*

write

μ[K]

for the ground instance of K obtained by applying μ to FK.

The application is total:

Equivalently, if ⟨L⟩ is a graph term, then its instance is:

⟨ μt(L) ⟩

where μt denotes total application.

Canonical expansion

For every assignment

σ : UG → GT*

choose fresh witness names

we,σ

for every

e ∈ EG.

Define

σ̂ = σ ∪ { e ↦ we,σ | e ∈ EG }.

The canonical expansion of G, written C(G), is:

C(G) = ⋃σ : UG → GT* σ̂[FG].

Membership in C(G) is taken modulo graph-term isomorphism.

Intuitively, C(G) contains every ground universal instance of G, with fresh witnesses for the existential variables of each such instance.

Theorem

Canonical expansion characterisation of basic N3 entailment. Let
G = (UG, EG, FG)    and    H = (UH, EH, FH)
be finite, closed, normalised abstract N3 graphs. Then
G ⊨ H
if and only if, for every assignment
α : UH → GT*
there exists an assignment
β : EH → GT*
such that
(α ∪ β)[FH] ⊆ C(G).
In words: G basic-entails H exactly when every universal instance of H has an existential instance contained in the canonical expansion of G.

Proof

Soundness

Assume that for every assignment

α : UH → GT*

there exists

β : EH → GT*

such that

(α ∪ β)[FH] ⊆ C(G).

We prove that

G ⊨ H.

Let I be an arbitrary basic interpretation such that

I ⊨ G.

We must show that

I ⊨ H.

Let A be an arbitrary assignment for the universal variables UH. For each u ∈ UH, write

A(u) = (A1(u), A2(u)),

where A1(u) is the denotation and A2(u) is a ground term representation satisfying

I(A2(u)) = A1(u).

Define

α(u) = A2(u).

By the syntactic assumption, there exists

β : EH → GT*

such that

(α ∪ β)[FH] ⊆ C(G).

Only finitely many triples of C(G) are used in this inclusion. Each such triple belongs to some canonical instance of G, generated by some universal assignment

σ : UG → GT*.

For every such σ, define an assignment Aσ for the universal variables of G in I by

Aσ(u) = (I(σ(u)), σ(u)).

Since

I ⊨ G,

there exists an assignment Bσ for EG such that

I[Aσ • Bσ](FG) = true.

Now replace each canonical witness name

we,σ

occurring in the selected finite fragment by the corresponding ground term representation

Bσ,2(e).

Call this replacement map ρ, and extend ρ recursively to lists and graph terms. The replacement preserves sharing: the same witness name is always replaced by the same witness term.

Because each selected triple came from an instance of G that is true in I, every triple in

ρ((α ∪ β)[FH])

is true in I.

Define an existential assignment B for EH by

B(e) = (I(ρ(β(e))), ρ(β(e))).

Then

I[A • B](FH) = true.

Since A was arbitrary, we have

I ⊨ H.

Since I was arbitrary among models of G, it follows that

G ⊨ H.

This proves soundness.

Completeness

Assume that the syntactic condition fails.

Then there exists an assignment

α : UH → GT*

such that, for every assignment

β : EH → GT*,

we have

(α ∪ β)[FH] ⊄ C(G).

We construct a basic interpretation IG such that

IG ⊨ G

but

IG ⊭ H.

Let the domain of IG be

ΔIG = GT* / ≃,

the set of ground N3 terms modulo graph-term isomorphism.

For every IRI or literal a, define

DIG(a) = [a].

For every ground graph term ⟨K⟩, define

QIG(⟨K⟩) = [⟨K⟩].

Thus graph terms are interpreted as representatives of their own isomorphism classes, and isomorphic graph terms receive the same value.

Define the extension relation by

EXTIG = { ([s], [p], [o]) | (s, p, o) ∈ C(G) }.

We first show that

IG ⊨ G.

Let A be any assignment for UG. Put

σ(u) = A2(u).

By construction of C(G), the canonical instance of G corresponding to σ is contained in C(G). For every existential variable e ∈ EG, choose the canonical witness

we,σ.

This gives an existential assignment B such that every triple in

(A • B)[FG]

belongs to EXTIG. Hence

IG[A • B](FG) = true.

Since A was arbitrary,

IG ⊨ G.

We now show that

IG ⊭ H.

Use the assignment for UH determined by the failing α:

A(u) = ([α(u)], α(u)).

Suppose, for contradiction, that

IG ⊨ H.

Then there would exist an existential assignment B for EH. Define

β(e) = B2(e).

Since truth in IG is exactly membership in C(G), this would imply

(α ∪ β)[FH] ⊆ C(G),

contradicting the choice of α.

Therefore

IG ⊭ H.

Thus there exists a model of G that is not a model of H, so

G ⊭ H.

This proves completeness.

Relation with the RDF interpolation lemma

The RDF interpolation lemma states that, for simple RDF entailment, a graph S entails a graph E exactly when some subgraph of S is an instance of E.

The theorem above is the corresponding statement for basic N3 entailment.

In the RDF fragment:

The condition

there exists β : EH → GT* such that β[FH] ⊆ C(G)

then says precisely that an instance of H is contained in G. Thus the N3 theorem conservatively generalises the RDF interpolation lemma.

The essential extra feature in N3 is the presence of explicit universal variables. Because of them, a conclusion may be supported by several different universal instances of the premise.

For example, the graph

({x}, ∅, {P(x), Q(x)})

entails

({u, v}, ∅, {P(u), Q(v)}).

However, the two triples in the conclusion may come from two different instances of the premise. This is why a direct “subgraph of G” formulation is insufficient; the correct object is the canonical expansion C(G).

Scope and limitations

This theorem concerns basic N3 entailment only.

It does not cover the additional semantics of predicates such as log:implies. The N3 draft treats log interpretation separately from basic interpretation, adding special semantic conditions for predicates in the log: namespace.

Thus the theorem should be read as the N3 analogue of simple RDF entailment, not as a completeness theorem for full N3 reasoning with logical built-ins.

References