Syntax and semantics of logic programming

Declarative logic programs consist entirely of rules of the form

<span id="mwEA"></span><span class="nv" id="mwEQ">H</span> <span class="p" id="mwEg">:-</span> <span class="nv" id="mwEw">B1</span><span class="p" id="mwFA">,</span> <span class="p" id="mwFQ">...,</span> <span class="nv" id="mwFg">BN</span><span class="p" id="mwFw">.</span>

Each such rule can be read as an implication:

${\displaystyle B_1\wedge \dots \wedge B_n\to H}$

meaning "If each ${\displaystyle B_i}$ is true, then ${\displaystyle H}$ is true". Logic programs compute the set of facts that are implied by their rules.

Many implementations of Datalog, Prolog, and related languages add procedural features such as Prolog's cut operator or extra-logical features such as a foreign function interface. The formal semantics of such extensions are beyond the scope of this article.

Datalog

Datalog is the simplest widely-studied logic programming language. There are three major definitions of the semantics of Datalog, and they are all equivalent. The syntax and semantics of other logic programming languages are extensions and generalizations of those of Datalog.

Syntax

A Datalog program consists of a list of rules (Horn clauses). If constant and variable are two countable sets of constants and variables respectively and relation is a countable set of predicate symbols, then the following BNF grammar expresses the structure of a Datalog program:

<span id="mwOQ"></span><span class="p" id="mwOg"><</span><span class="nc" id="mwOw">program</span><span class="p" id="mwPA">></span> <span class="o" id="mwPQ">::=</span> <span class="p" id="mwPg"><</span><span class="nc" id="mwPw">rule</span><span class="p" id="mwQA">></span> <span class="p" id="mwQQ"><</span><span class="nc" id="mwQg">program</span><span class="p" id="mwQw">></span> | "" <span class="p" id="mwRA"><</span><span class="nc" id="mwRQ">rule</span><span class="p" id="mwRg">></span> <span class="o" id="mwRw">::=</span> <span class="p" id="mwSA"><</span><span class="nc" id="mwSQ">atom</span><span class="p" id="mwSg">></span> ":-" <span class="p" id="mwSw"><</span><span class="nc" id="mwTA">atom-list</span><span class="p" id="mwTQ">></span> "." <span class="p" id="mwTg"><</span><span class="nc" id="mwTw">atom</span><span class="p" id="mwUA">></span> <span class="o" id="mwUQ">::=</span> <span class="p" id="mwUg"><</span><span class="nc" id="mwUw">relation</span><span class="p" id="mwVA">></span> "(" <span class="p" id="mwVQ"><</span><span class="nc" id="mwVg">term-list</span><span class="p" id="mwVw">></span> ")" <span class="p" id="mwWA"><</span><span class="nc" id="mwWQ">atom-list</span><span class="p" id="mwWg">></span> <span class="o" id="mwWw">::=</span> <span class="p" id="mwXA"><</span><span class="nc" id="mwXQ">atom</span><span class="p" id="mwXg">></span> | <span class="p" id="mwXw"><</span><span class="nc" id="mwYA">atom</span><span class="p" id="mwYQ">></span> "," <span class="p" id="mwYg"><</span><span class="nc" id="mwYw">atom-list</span><span class="p" id="mwZA">></span> | "" <span class="p" id="mwZQ"><</span><span class="nc" id="mwZg">term</span><span class="p" id="mwZw">></span> <span class="o" id="mwaA">::=</span> <span class="p" id="mwaQ"><</span><span class="nc" id="mwag">constant</span><span class="p" id="mwaw">></span> | <span class="p" id="mwbA"><</span><span class="nc" id="mwbQ">variable</span><span class="p" id="mwbg">></span> <span class="p" id="mwbw"><</span><span class="nc" id="mwcA">term-list</span><span class="p" id="mwcQ">></span> <span class="o" id="mwcg">::=</span> <span class="p" id="mwcw"><</span><span class="nc" id="mwdA">term</span><span class="p" id="mwdQ">></span> | <span class="p" id="mwdg"><</span><span class="nc" id="mwdw">term</span><span class="p" id="mweA">></span> "," <span class="p" id="mweQ"><</span><span class="nc" id="mweg">term-list</span><span class="p" id="mwew">></span> | ""

Atoms are also referred to as literals. The atom to the left of the :- symbol is called the head of the rule; the atoms to the right are the body. Every Datalog program must satisfy the condition that every variable that appears in the head of a rule also appears in the body (this condition is sometimes called the range restriction).

Rules with empty bodies are called facts. For example, the following rule is a fact:

<span id="mwjg"></span><span class="nf" id="mwjw">r</span><span class="p" id="mwkA">(</span><span class="s s-Atom" id="mwkQ">x</span><span class="p" id="mwkg">)</span> <span class="p" id="mwkw">:-</span> <span class="p" id="mwlA">.</span>

Syntactic sugar

Many implementations of logic programming extend the above grammar to allow writing facts without the :-, like so:

<span id="mwmg"></span><span class="nf" id="mwmw">r</span><span class="p" id="mwnA">(</span><span class="s s-Atom" id="mwnQ">x</span><span class="p" id="mwng">).</span>

Many also allow writing 0-ary relations without parentheses, like so:

<span id="mwog"></span><span class="nf" id="mwow">p</span> <span class="o" id="mwpA">:-</span> <span class="s s-Atom" id="mwpQ">q</span><span class="p" id="mwpg">.</span>

These are merely abbreviations (syntactic sugar); they have no impact on the semantics of the program.

Example

The following program computes the relation path, which is the transitive closure of the relation edge.

<span id="mwsA"></span><span class="nf" id="mwsQ">edge</span><span class="p" id="mwsg">(</span><span class="s s-Atom" id="mwsw">x</span><span class="p" id="mwtA">,</span> <span class="s s-Atom" id="mwtQ">y</span><span class="p" id="mwtg">).</span> <span class="nf" id="mwtw">edge</span><span class="p" id="mwuA">(</span><span class="s s-Atom" id="mwuQ">y</span><span class="p" id="mwug">,</span> <span class="s s-Atom" id="mwuw">z</span><span class="p" id="mwvA">).</span> <span class="nf" id="mwvQ">path</span><span class="p" id="mwvg">(</span><span class="nv" id="mwvw">A</span><span class="p" id="mwwA">,</span> <span class="nv" id="mwwQ">B</span><span class="p" id="mwwg">)</span> <span class="p" id="mwww">:-</span> <span class="nf" id="mwxA">edge</span><span class="p" id="mwxQ">(</span><span class="nv" id="mwxg">A</span><span class="p" id="mwxw">,</span> <span class="nv" id="mwyA">B</span><span class="p" id="mwyQ">).</span> <span class="nf" id="mwyg">path</span><span class="p" id="mwyw">(</span><span class="nv" id="mwzA">A</span><span class="p" id="mwzQ">,</span> <span class="nv" id="mwzg">C</span><span class="p" id="mwzw">)</span> <span class="p" id="mw0A">:-</span> <span class="nf" id="mw0Q">path</span><span class="p" id="mw0g">(</span><span class="nv" id="mw0w">A</span><span class="p" id="mw1A">,</span> <span class="nv" id="mw1Q">B</span><span class="p" id="mw1g">),</span> <span class="nf" id="mw1w">edge</span><span class="p" id="mw2A">(</span><span class="nv" id="mw2Q">B</span><span class="p" id="mw2g">,</span> <span class="nv" id="mw2w">C</span><span class="p" id="mw3A">).</span>

Semantics

There are three widely-used approaches to the semantics of Datalog programs: model-theoretic, fixed-point, and proof-theoretic. These three approaches can be proven to be equivalent.

An atom is called ground if none of its subterms are variables. Intuitively, each of the semantics define the meaning of a program to be the set of all ground atoms that can be deduced from the rules of the program, starting from the facts.

Model theoretic

A rule is called ground if all of its atoms (head and body) are ground. A ground rule R₂ is a ground instance of another rule R₁ if R₂ is the result of a substitution of constants for all the variables in R₁.

The Herbrand base of a Datalog program is the set of all ground atoms that can be made with the constants appearing in the program. An interpretation (also known as a database instance) is a subset of the Herbrand base. A ground atom is true in an interpretation I if it is an element of I. A rule is true in an interpretation I if for each ground instance of that rule, if all the atoms in the body are true in I, then the head of the rule is also true in I.

A Herbrand model of a Datalog program P is an interpretation I of P which contains all the ground facts of P, and makes all of the rules of P true in I. Model-theoretic semantics state that the meaning of a Datalog program is its minimal Herbrand model (equivalently, the intersection of all its Herbrand models).

For example, this program:

<span id="mwAUQ"></span><span class="nf" id="mwAUU">edge</span><span class="p" id="mwAUY">(</span><span class="s s-Atom" id="mwAUc">x</span><span class="p" id="mwAUg">,</span> <span class="s s-Atom" id="mwAUk">y</span><span class="p" id="mwAUo">).</span> <span class="nf" id="mwAUs">edge</span><span class="p" id="mwAUw">(</span><span class="s s-Atom" id="mwAU0">y</span><span class="p" id="mwAU4">,</span> <span class="s s-Atom" id="mwAU8">z</span><span class="p" id="mwAVA">).</span> <span class="nf" id="mwAVE">path</span><span class="p" id="mwAVI">(</span><span class="nv" id="mwAVM">A</span><span class="p" id="mwAVQ">,</span> <span class="nv" id="mwAVU">B</span><span class="p" id="mwAVY">)</span> <span class="p" id="mwAVc">:-</span> <span class="nf" id="mwAVg">edge</span><span class="p" id="mwAVk">(</span><span class="nv" id="mwAVo">A</span><span class="p" id="mwAVs">,</span> <span class="nv" id="mwAVw">B</span><span class="p" id="mwAV0">).</span> <span class="nf" id="mwAV4">path</span><span class="p" id="mwAV8">(</span><span class="nv" id="mwAWA">A</span><span class="p" id="mwAWE">,</span> <span class="nv" id="mwAWI">C</span><span class="p" id="mwAWM">)</span> <span class="p" id="mwAWQ">:-</span> <span class="nf" id="mwAWU">path</span><span class="p" id="mwAWY">(</span><span class="nv" id="mwAWc">A</span><span class="p" id="mwAWg">,</span> <span class="nv" id="mwAWk">B</span><span class="p" id="mwAWo">),</span> <span class="nf" id="mwAWs">edge</span><span class="p" id="mwAWw">(</span><span class="nv" id="mwAW0">B</span><span class="p" id="mwAW4">,</span> <span class="nv" id="mwAW8">C</span><span class="p" id="mwAXA">).</span>

has this Herbrand universe: x, y, z

and this Herbrand base: edge(x, x), edge(x, y), ..., edge(z, z), path(x, x), ..., path(z, z)

and this minimal Herbrand model: edge(x, y), edge(y, z), path(x, y), path(y, z), path(x, z)

Fixed-point

Let I be the set of interpretations of a Datalog program P, that is, I = P(H), where H is the Herbrand base of P and P is the powerset operator. The immediate consequence operator for P is the following map T from I to I: For each ground instance of each rule in P, if every clause in the body is in the input interpretation, then add the head of the ground instance to the output interpretation. This map T is monotonic with respect to the partial order given by subset inclusion on T. By the Knaster–Tarski theorem, this map has a least fixed point; by the Kleene fixed-point theorem the fixed point is the supremum of the chain ${\displaystyle T(\mathrm{\varnothing }),T(T(\mathrm{\varnothing })),\dots ,T^n(\mathrm{\varnothing }),\dots }$. The least fixed point of M coincides with the minimal Herbrand model of the program.

The fixpoint semantics suggest an algorithm for computing the minimal Herbrand model: Start with the set of ground facts in the program, then repeatedly add consequences of the rules until a fixpoint is reached. This algorithm is called naïve evaluation.

Proof-theoretic

Given a program P, a proof tree of a ground atom A is a tree with a root labeled by A, leaves labeled by ground atoms from the heads of facts in P, and branches with children ${\displaystyle A_1,\dots ,A_n}$ labeled by ground atoms G such that there exists a ground instance

G :- A1, ..., An.

of a rule in P. The proof-theoretic semantics defines the meaning of a Datalog program to be the set of ground atoms that can be derived from such trees. This set coincides with the minimal Herbrand model.

One might be interested in knowing whether or not a particular ground atom appears in the minimal Herbrand model of a Datalog program, perhaps without caring much about the rest of the model. A top-down reading of the proof trees described above suggests an algorithm for computing the results of such queries, such a reading informs the SLD resolution algorithm, which forms the basis for the evaluation of Prolog.

Other approaches

The semantics of Datalog have also been studied in the context of fixpoints over more general semirings.