This document defines the model-theoretic semantics of Notation3 Logic based on its abstract syntax.
This specification was published by the Notation 3 (N3) Community Group. It is not a W3C Standard nor is it on the W3C Standards Track. Please note that under the W3C Community Contributor License Agreement (CLA) there is a limited opt-out and other conditions apply. Learn more about W3C Community and Business Groups.
GitHub Issues are preferred for discussion of this specification. Alternatively, you can send comments to our mailing list. Please send them to public-n3-dev@w3.org (subscribe, archives).
This document defines the model-theoretic semantics of Notation3 Logic. We define the semantics of Notation3 (N3) on an abstract syntax. We will provide the mapping from explicit N3 Syntax to abstract syntax in an extra document. By doing so we separate the handling of implicit quantification from the model.
N3 is an extension of RDF. We use the following concepts from the [[[RDF11-CONCEPTS]]]: IRI, RDF triple, RDF graph, subject, predicate, object, node, blank node, and literal.
Notation3 supports implicit quantification. When blank nodes are used in triples, they implicitly stand for existentially quantified variables. When universals (i.e., variables starting with a question mark in the concrete syntax) are used, they implicitly stand for universally quantified variables. Implicit universal quantification is always global; that is, implicit universal quantification always spans over the full graph. Implicit existential quantification is always local; that is, it spans the local graph (i.e., if implicit existential quantification occurs in a graph term, it spans only that graph term). To simplify the definitions in this document, we assume all quantification to be explicit and introduce an abstract syntax to better express that.
In order to help the reader to make a connection between Notation3 concrete syntax and abstract syntax, we will provide example translations together with the concepts we introduce. We will provide a formal definition of the mapping in a separate document.
The set of atomic terms consists of:
A term can be
In this specification we follow the original terminology of Notation3 Logic used in the team submission where a sequence of terms is called a list. An N3 list is very similar to an RDF-collection with the difference that N3 treats lists as special terms in the language and not only as syntactic sugar. In this and its related documents created by the N3 group, we will sometimes also use the term N3 collection or just collection for N3 lists. These terms should be understood as synonyms.
Terms form triples:A triple is made of
:s _:x :o.
is valid in N3.
Even lists or graph terms can appear in the predicate position of a triple.
A graph is a tuple $(U, E, F)$ where
A graph $G=(U, E, F)$ is finite if the sets $U$, $E$ and $F$ are finite.
As we will see in the semantics section below, the sets $U$ and $E$ act like quantifiers with variables for the graph and its subgraphs. We therefore call these sets also quantification sets.To provide some intuition on the correspondence between concrete N3 syntax and abstract N3 syntax, we provide some examples below. We always write a graph in concrete N3 syntax followed by its counterpart in abstract N3 syntax.
()
") for all graph terms here and in the remainder of the document. That is, for example, we will write:socrates :knows _:x.
{?x a :Human} => {?x a :Mortal}.
:socrates :says {_:x a :Mortal}.
:socrates :says {_:x a :Mortal}. _:y :knows :socrates.
{?x a :Human} => {?x :hasMother _:y}.
_:y :says {?x a :Mortal}.
We will re-use these examples in the following sections.
:socrates :says {_:x a :Mortal}.
:socrates :says {_:x a :Mortal}.
Note that the definition makes a difference between graphs and graph terms. A graph term is a direct constituent of the graph ("containing graph") in which it occurs as a triple component. However, the direct constituents of the graph term's graph, and their direct constituents (and so on), are not direct constituents of the containing graph. Rather, they are constituents of the containing graph. This difference is crucial for the definitions below: a graph is not the same as a graph term.
With that definition, we now introduce free variables: these are variables which occur directly or nested in the graph but which are not covered by a quantification set.
The set of free variables ($FV$) of a term or a set of triples is defined as follows:
Examples:
This enables us to introduce the notion of closed graphs and ground terms.
We denote the set of ground terms as $T_G$.
A triple is ground if all of its direct constituents are ground.
A graph $G=(U,E,F)$ is ground if $E=U=\emptyset$ and all triples in $F$ are ground.
An abstract N3 graph which is constructed from a graph in the direct N3 syntax cannot contain free variables.
However, when considering a specific graph term in isolation,
all variables that are quantified outside that graph term will appear to be free in that graph term.
For instance, the following N3 concrete syntax:
`_:y :says { ?x :knows :bob }.`
corresponds to
$\qquad (\{x\}, \{y\}, \{( \text{:y}, \text{:says}, <\{\},\{\},\{(x, \text{:knows}, \text{:bob})\}>)\})$
When considering the graph term's graph in isolation:
`({},{},{(x, :knows, :bob)})`
the variable $x$ will be a free variable (as it was quantified in the containing N3 graph).
An abstract graph $G=(U,E,F)$ can also contain quantified variables $v\in U\cup E$ which do not occur in any triple of $F$. These variables do not contribute to the interpretation of the graph. In order to simplify our considerations for the following sections, we introduce the notion of normalised graphs:
For each graph $G=(U,E,F)$, we call $G^N=(U\cap (FV(F)), E\cap(FV(F)), F)$ the normalisation of $G$.
Examples:For two mappings $M$ and $N$ from terms to terms, we define their combination as follows:
In this document, combinations will mainly be used to handle nested scoped variables. It is therefore no coincidence that this "overriding" behavior is very similar to how quantifiers behave in first order logic: when the same variable is quantified at different levels, the left-most quantifier is overridden by the right-most one.
With combinations of mappings we can define isomorphisms between abstract N3 graphs:
Let $M$ be a bijection between the variables of $V$, we define:
We call a graph $G_1$ isomorphic to a graph $G_2$, written as $G_1\simeq G_2$, if there exists some $M$ such that $G_1$ is isomorphic to $G_2$ under $M$.
If $G_1$ is isomorphic to $G_2$ then $G_2$ is also isomorphic to $G_1$.
Consider the following graphs:
_:x :knows :p. :p :says {_:x a :Genius}.
_:y :knows :p. :p :says {_:z a :Genius}.
}
_:y :knows :p. :p :says {_:x a _:z}.
}
Then $G_1$ is isomorphic to $G_2$:
$x$ as the subject of the first triple is replaced with $M(x)=y$, while $x$ as the subject of the unique triple in the graph term is replaced with $M\bullet P(x) = z$ (P overrides M).
On the other hand, G1 is not isomorphic to G3.
A basic interpretation $I$ is defined by:
This definition is generally "compatible" with RDF simple interpretations, with the following superficial changes:
Note that the images of $Q_I$ are syntactic elements (graph terms), but they can (and most likely will) also be elements of the domain $Δ_I$. Note however that not all interpretations are required to have graph terms in their domain, because $Q_I$ is allowed to be the empty mapping. Such interpretations could still satisfy a graph that has no graph term constituent.
The basic interpretation maps graph terms to an isomorphic copy of themselves. As a consequence, two non-isomorphic graph terms cannot have the same meaning. For the abstract versions of the graph terms {_:x :p :o}
, {_:y :p :o}
and {_:x :p :o. _:y :p :o}
, we thus get:
However, as we will see below, N3 provides mechanisms to unquote graph terms (that is, to transform them into graphs), and to compare them based on the meaning of the formulae they quote.
Given $I$ a basic interpretation, we recursively define $I(x) =$
Note that the interpretation function $Q_I(x)$ maps ground graphs into the domain of discourse without interpreting their content separately. This choice was made to guarentee referential opacity (see also referential opacity in RDF-star ). To illustrate this idea consider the superman example expressed in N3:
:superman owl:sameAs :clarkKent.
:loisLane :believes {:superman :can :fly}.
Even if we assume that our logic is extended by an interpretation for owl:sameAs
which assures that the function $D_I$ maps the IRIs
:superman
and :clarkKent
to the same resource, it should still not yield the following conclusion:
:loisLane :believes {:clarkKent :can :fly}.
?x :says {?x :is :wise}.
everyone says about themselves that they are wise. In abstract syntax, the formula would be expressed as:
$G = (\{x\}, \{\}, \{(x, \text{:says}, <\{\}, \{\}, \{(x, \text{:is}, \text{:wise})\}>)\})$.
This formula is interesting because the universally quantified variable appears once as a direct constituent in the triple and once as only a constituent. If we replace the variable $x$ by, for example:bob
, we get:
$G_{bob} = (\{\}, \{\}, \{(\text{:bob}, \text{:says}, <\{\}, \{\}, \{(\text{:bob}, \text{:is}, \text{:wise})\}>)\})$
The semantics for ground graphs maps IRIs to not further specified domain elements, while ground graph terms are mapped to an isomorphic version of themselves. The interpretation of the above example $I(G_{bob})$ will be true if $(D_I(\text{:bob}), D_I(\text{:says}), Q_I(<\{\}, \{\}, \{(\text{:bob}, \text{:is}, \text{:wise})\}>)\in EXT_I$.
If we revert back to our original example with variables, a regular valuation function (such as the mapping A used for blank nodes in [[RDF11-MT]]) will simply replace both occurrences of variable $x$ with a domain element $\delta_i$ from $\Delta_I$. In that case, $Q_I$ will have to map the graph term $<\{\}, \{\}, \{(\delta_i, \text{:is}, \text{:wise})\}>$ to an isomorphic copy. However, the isomorphism is only defined for concrete N3 terms, and not domain elements. If not applying the valuation function to the graph term, $Q_I$ will have to map the graph term $<\{\}, \{\}, \{(x, \text{:is}, \text{:wise})\}>$, which is however no longer ground as its graph is no longer closed ($x$ is quantified outside of the graph). In our basic interpretation, the mapping $Q_I$ is only defined for ground graph terms. We thus need to first ground these kinds of leaked variables, i.e., variables that become free when considering the graph term in isolation (as is required when determining isomorphisms).
We need to extend RDF's classical semantic condition for blank nodes and use a so-called assignment, which, instead of simply mapping variables to resources, maps variables to pairs of resources and term representations:
Given a basic interpretation $I$ and a set of variables $V_1$. We call a mapping $A$ from $V_1$ to $Δ_I\times T_G$ such that $A(v)=(A_1(v),A_2(v))$ and $I(A_2(v))=A_1(v)$ an assignment for $V_1$.
We can consider both values $A_1$ and $A_2$ of an assignment $A(v)=(A_1(v), A_2(v))$ as separate mappings. The mapping $A_2$ assigns variables to terms, and will be used to ground free variables within graph terms. Note that given an interpretation $I$ and two assignments $A$ for a set $V_1$, and $B$ for a set $V_2$ of variables, the combination $A\bullet B$ is again an assignment for $V_1\cup V_2$.
In order to apply mapping $A_2$ on graphs, we introduce the notion of total application.Let $G=(U,E,F)$ be a graph and let $M$ be a mapping from a set of variables $V$ into a set $S$. A total application $M^t(G)$ of $M$ is defined as follows:
$M^t(G) = (U, E, \{ (M^t(s), M^t(p), M^t(o)) | \; (s, p, o) \in F \})$ such that:
$M^t($$<\{\},\{y\},\{(x, \text{:hasMother}, y)\}>$$)$ $=$$<\{\},\{y\},\{(tom, \text{:hasMother}, y)\}>$
Variable $x$ is replaced by $M(x)$ as it is a free variable, while $y$ does not get replaced since it is scoped (i.e., quantified in the nested graph). This results in a ground graph term, which can be mapped by $Q_I$.The definition of total applications enables us to define interpretations with assignment:
For a closed graph $G=(U,E,F)$, a basic interpretation $I$ and an assignment $A$ on the set of variables $U\cup E$, we define $I[A](x)$ as:
For a closed graph $G=(U, E, F)$ and a basic interpretation $I$, we say $I(G)=\textit{true}$ or interpretation $I$ satifies $G$, if for all assignments $A$ for $U$ (universal variables) there exist an assignment $B$ for $E$ (existential variables) such that $I[A\bullet B](F)=\textit{true}$. We also write that as $I\models G$.
Note that the interpretation of a variable $x$ depends on its position in a graph. In the expression $(\emptyset, \emptyset,\{(x, \text{:p}, <\emptyset, \emptyset, \{(x, \text{:q}, \text{:r})\}>)\})$, the first $x$ is interpreted as $A_1(x)$ while the second is interpreted as $A_2(x)$. The connection between these two values is established by the condition that $I(A_2(v))=A_1(v)$.
For instance:
$I(\{x\}, \{\}, \{(x, \text{:says}, < \{\}, \{\}, \{( x, \text{:is}, \text{:wise} )\} >)\})$
will be true if for all assignments $A:\{x\}\rightarrow Δ_I\times T_G$, the following is true:
$I(\{(A_1(x), \text{:says}, < \{\}, \{\}, \{ (A_2(x), \text{:is}, \text{:wise}) \} >)$
For assignments and free variables we define:Let $G=(U,E,F)$ be a graph. We say that $G$ is true under the interpretation $I$ and the assignment $A$ if $I[A]\models G$. That is, for each assignment $A^1$ for the variables in $U$ there exists an assignment $B^1$ for the variables in $E$ such that $I[A\bullet A^1\bullet B^1](F)=true$.
This last definition handles all variables occurring freely in a graph as universally quantified.
Let $G$ and $H$ be two graphs, we say that $G$ b-entails $H$, noted $G ⊨ H$, if and only if every interpretation $I$ that satisfies $G$ $(I ⊨ G)$ also satisfies $H$ $(I ⊨ H)$.
In order to illustrate the properties of basic entailment, we give a few examples::socrates :knows :plato.
:socrates :knows _:x.
?x :knows :plato.
:socrates :knows :plato.
{?x a :Human} => {?x a :Mortal}.
{:socrates a :Human} => {:socrates a :Mortal}.
:socrates :says {:socrates a :Mortal}.
@forSome :x. :x :says { :x a :Mortal}.
:socrates a :Human. {:socrates a :Human} => {:socrates a :Mortal}.
:socrates a :Mortal.
:socrates :says {:socrates a :Mortal}.
:socrates :says {_:x a :Mortal}.
_:x :says {_:x a :Mortal}.
log:implies
or as a short-cut =>
)
is covered through an addition: log-interpretations which we introduce in the following section.
This section defines an extension of base semantics providing the specific meaning of (some of) the builtins in the N3-logic namespace, short `log:` namespace.
For the definitions below, we assume that the set of literals $L$ contains the two boolean literals `true` and `false`. The literal `true` stands for the graph term $<\emptyset, \emptyset, \emptyset>$.
The set of logical predicates $LP$ contains the predicate `log:implies`.
The list of predicates in LP is planned to be extended by more predicates. The goal here is to cover all (or at least most of) the predicates in the `log:` namespace. For the other namespaces we plan to provide similar definitions.
Below, we give specify how log interpretations extend basic interpretations:
Let $I$ be a basic interpretation for a graph $G=(U, E, F)$. Then $G$ is true under log-interpretation or $I$ log satisfies $G$ ($I\models_{log} G$) if for each assignment $A$ for $U$ there exists an assignment $B$ for $E$ such that:
We define the meaning of $I[A\bullet B]\models_{log}(s,p,o)$ depending on the concrete $p\in LP$ below.
Note that if there are no logical predicates used in a graph, then the log-interpretation coincides with the basic interpretation. We call a graph $G=(U, E, F)$ log-free, if $p\not\in LP$ for all triples $(s,p,o)\in F$. All log-free graphs which are true under the basic interpretation are thus also true under log-interpretation.
The aim of the predicate log:implies
is to provide a form of logical implication.
This interpretation acts on the ground terms which are true under basic interpretations.
If $t = (s, \text{log:implies}, o )$ is a triple, then $I[A\bullet B]\models_{log} t$ if:
The first bullet of the above definition clarifies how implications with graph terms $< G_1>$ and $<G_2>$ in subject and object position are interpreted. Note that under the simple interpretation these graph terms are ground, that is, $I[A\bullet B](G_1)$ and $I[A\bullet B](G_2)$ are closed graphs. To determine the meaning of the implications these closed graphs are further interpreted using $I[A\bullet B]$ as an interpretation. The log-interpretation thus interprets the basic interpretation of a graph term.
The second bullet covers implications with
the boolean literal false
in the consequence.
In log-semantics this literal is understood as truth constant "false" (or $\bot$).
Note that the interpretation process here consists of two steps: we first consider the basic interpretation
of the implication triple which needs to be true and then we test whether
- using the same interpretation as a log interpretation - the premise is false.
However, the mere fact that a closed graph $G_1$ is false under an interpretation $I$
($I\not\models_{log} G_1$), does not allow us to conclude that
$I\models_{log} (\{\}, \{\}, \{ (< G_1>, \text{log:implies}, \text{false})\})$.
The last bullet ensures that the truth value of triples having log:implies
in predicate position but no graph term or truth value in subject or object position like
for example :socrates log:implies :plato.
is only determined by the basic interpretation of the triple. That is,
log:implies
only has a special meaning when used with graph terms and/or truth values.
Let $G$ and $H$ be two graphs, we say that $G$ log-entails $H$, written as $G ⊨_{log} H$, if and only if every interpretation $I$ that log satisfies $G$ ($I ⊨_{log} G$) also log satisfies $H$ ($I ⊨_{log} H$).
To illustrate the definition, we discuss some examples of entailment and non-entailment in the sections below.log:implies
we observe the following examples of log entailment:
:socrates a :Human.
{:socrates a :Human} => {:socrates a :Mortal}.
:socrates a :Mortal.
:socrates a :Human. {?x a :Human} => {?x a :Mortal}.
:socrates a :Mortal.
:socrates a :Human. {_:x a :Human} => {_:x a :Mortal}.
_:x a :Mortal.
:socrates :says {:socrates a :Mortal}.
{?x :says {?x a :Mortal}}=>{?x a :WisePerson}
:socrates a :WisePerson.
:socrates a :Human. :socrates a :Mortal.
{:socrates a :Human} => {:socrates a :Mortal}.
:socrates :says {:socrates a :Mortal}.
{:socrates :says {_:x a :Mortal}}=>{:socrates a :WisePerson}
:socrates a :WisePerson.
:socrates :says {_:x a :Mortal}.
{:socrates :says {?y a :Mortal}}=>{:socrates a :WisePerson}
:socrates a :WisePerson.
As above, these examples follow the last agreement on the interpretation of N3 concrete syntax which might be implemented differently in some reasoners. The difference does not effect the meaning of abstract formulas. The community group is currently working on a solution for this problem.
A special form of entailment enabled by our semantics is the so-called unquoting. By that, we mean the entailment which enables us to make the graph contained in a graph term true. To illustrate the idea, we give an example.
Let's assume that simon says that birds can fly. In abstract N3, we can express that as:
simon :says {:birds :can :fly}.
In N3 we can write a rule stating that everything Simon says is true. We do that as follows:
{:simon :says ?x}=>?x
From this last rule we can derive via b-entailment:
{:simon :says {:birds :can :fly}}=>{:bird :can :fly}.
Via log-entailment we get:
:birds :can :fly.
The example above showed us the basic idea of unquoting. The feature is supported by N3 semantics using the two step-interpretation. The b-interpretation treats the universally quantified variable in premise and conclusion of the rule as terms. We can replace the variable by graph terms if these (or graphs isomorphic to these) form part of $\Delta_I$ (which needs to be the case if $I$ is an interpretation of the first triple of this example). The log-interpretation now interprets these terms which allows us to come to our conclusion.