View source for Syntax and semantics of logic programming

{{more footnotes|date=March 2023}}

{{Short description|Formal semantics of logic programming languages}}

[[Logic programming]] is a [[programming paradigm]] that includes languages based on formal logic, including [[Datalog]] and [[Prolog]]. This article describes the syntax and semantics of the purely [[Declarative programming|declarative]] subset of these languages. Confusingly, the name "logic programming" also refers to a {{em|specific}} programming language that roughly corresponds to the declarative subset of Prolog. Unfortunately, the term must be used in both senses in this article.

Declarative logic programs consist entirely of ''rules'' of the form

<syntaxhighlight lang="prolog">
H :- B1, ..., BN.
</syntaxhighlight>

Each such rule can be read as an [[Material conditional|implication]]:

:<math>B_1\land\ldots\land B_n\rightarrow H</math>

meaning "If each <math>B_i</math> is true, then <math>H</math> 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 (logic programming)|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 ==
{{main|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 clause]]s).{{sfn|Ceri|Gottlob|Tanca|1989|p=146}} If ''constant'' and ''variable'' are two [[Countable set|countable]] sets of constants and variables respectively and ''relation'' is a countable set of [[Predicate variable|predicate symbols]], then the following [[BNF grammar]] expresses the structure of a Datalog program:

<syntaxhighlight lang="bnf">
<program> ::= <rule> <program> | ""
<rule> ::= <atom> ":-" <atom-list> "."
<atom> ::= <relation> "(" <term-list> ")"
<atom-list> ::= <atom> | <atom> "," <atom-list> | ""
<term> ::= <constant> | <variable>
<term-list> ::= <term> | <term> "," <term-list> | ""
</syntaxhighlight>

Atoms are also referred to as {{dfni|literals}}. The atom to the left of the <code>:-</code> symbol is called the {{dfni|head}} of the rule; the atoms to the right are the {{dfni|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 {{dfni|range restriction}}).{{sfn|Ceri|Gottlob|Tanca|1989|p=146}}<ref>{{Cite conference |last1=Eisner |first1=Jason |last2=Filardo |first2=Nathaniel W. |date=2011 |editor-last=de Moor |editor-first=Oege |editor2-last=Gottlob |editor2-first=Georg |editor3-last=Furche |editor3-first=Tim |editor4-last=Sellers |editor4-first=Andrew |title=Dyna: Extending Datalog for Modern AI |url=https://link.springer.com/chapter/10.1007/978-3-642-24206-9_11 |conference=Datalog Reloaded, First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010 |series=Lecture Notes in Computer Science |volume=6702 |language=en |location=Berlin, Heidelberg |publisher=Springer |pages=181–220 |doi=10.1007/978-3-642-24206-9_11 |isbn=978-3-642-24206-9}}</ref>

Rules with empty bodies are called {{dfni|facts}}. For example, the following rule is a fact:
<syntaxhighlight lang="prolog">
r(x) :- .
</syntaxhighlight>

==== Syntactic sugar ====

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

<syntaxhighlight lang="prolog">
r(x).
</syntaxhighlight>

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

<syntaxhighlight lang="prolog">
p :- q.
</syntaxhighlight>

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

==== Example ====

The following program computes the relation <code>path</code>, which is the [[transitive closure]] of the relation <code>edge</code>.
<syntaxhighlight lang="prolog">
edge(x, y).
edge(y, z).
path(A, B) :- 
  edge(A, B).
path(A, C) :- 
  path(A, B), 
  edge(B, C).
</syntaxhighlight>

=== Semantics ===

There are three widely-used approaches to the semantics of Datalog programs: [[Model theory|model-theoretic]], [[Fixed point (mathematics)|fixed-point]], and [[Proof-theoretic semantics|proof-theoretic]]. These three approaches can be proven to be equivalent.<ref>{{Cite journal |last1=van Emden |first1=M. H. |last2=Kowalski |first2=R. A. |date=1976-10-01 |title=The Semantics of Predicate Logic as a Programming Language |journal=Journal of the ACM |volume=23 |issue=4 |pages=733–742 |doi=10.1145/321978.321991 |s2cid=11048276 |issn=0004-5411|doi-access=free }}</ref>

An atom is called {{dfni|[[Ground atom|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 ====

[[File:Herbrand-model-hasse.png|thumb|[[Hasse diagram]] of Herbrand interpretations of the Datalog program

<syntaxhighlight lang="prolog">
e(x, y).
e(y, z).
p(A, B) :-
  e(A, B).
p(A, C) :- 
  p(A, B),
  e(B, C).
</syntaxhighlight>

The interpretation <math>M</math> is the minimal Herbrand model. All interpretations above it are also models, all interpretations below it are not models.

]]

A rule is called ground if all of its atoms (head and body) are ground. A ground rule ''R''<sub>1</sub> is a ''ground instance'' of another rule ''R''<sub>2</sub> if ''R''<sub>1</sub> is the result of a [[Substitution (logic)|substitution]] of constants for all the variables in ''R''<sub>2</sub>.

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 {{mvar|I}} if it is an element of {{mvar|I}}. A rule is ''true in an interpretation {{mvar|I}}'' if for each ground instance of that rule, if all the clauses in the body are true in {{mvar|I}}, then the head of the rule is also true in {{mvar|I}}.

A ''model'' of a Datalog program ''P'' is an interpretation {{mvar|I}} of ''P'' which contains all the ground facts of ''P'', and makes all of the rules of ''P'' true in {{mvar|I}}. [[Model-theoretic]] semantics state that the meaning of a Datalog program is its minimal model (equivalently, the intersection of all its models).{{sfn|Ceri|Gottlob|Tanca|1989|p=149}}

For example, this program:

<syntaxhighlight lang="prolog">
edge(x, y).
edge(y, z).
path(A, B) :- 
  edge(A, B).
path(A, C) :- 
  path(A, B), 
  edge(B, C).
</syntaxhighlight>

has this Herbrand universe: <code>x</code>, <code>y</code>, <code>z</code>

and this Herbrand base: <code>edge(x, x)</code>, <code>edge(x, y)</code>, ..., <code>edge(z, z)</code>, <code>path(x, x)</code>, ..., <code>path(z, z)</code>

and this minimal Herbrand model: <code>edge(x, y)</code>, <code>edge(y, z)</code>, <code>path(x, y)</code>, <code>path(y, z)</code>, <code>path(x, z)</code>

==== Fixed-point ====

Let {{mvar|I}} be the set of interpretations of a Datalog program ''P'', that is, {{math|''I'' {{=}} '''P'''(''H'')}}, where ''H'' is the Herbrand base of ''P'' and '''P''' is the [[Power set|powerset]] operator. The {{dfni|immediate consequence operator}} for ''P'' is the following map {{mvar|T}} from {{mvar|I}} to {{mvar|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 {{mvar|T}} is [[Monotonic function|monotonic]] with respect to the [[Partially ordered set|partial order]] given by subset inclusion on {{mvar|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 <math>T(\emptyset), T(T(\emptyset)), \ldots, T^n(\emptyset), \ldots </math>. The least fixed point of {{mvar|M}} coincides with the minimal Herbrand model of the program.{{sfn|Ceri|Gottlob|Tanca|1989|p=150}}

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 [[Datalog#Naïve evaluation|naïve evaluation]].

==== Proof-theoretic ====

[[Image:Proof tree for Datalog transitive closure computation.svg|thumb|Proof tree showing the derivation of the ground atom <code>path(x, z)</code> from the program

<syntaxhighlight lang="prolog">
edge(x, y).
edge(y, z).
path(A, B) :- 
  edge(A, B).
path(A, C) :- 
  path(A, B), 
  edge(B, C).
</syntaxhighlight>
]]

Given a program {{mvar|P}}, a {{dfni|proof tree}} of a ground atom {{mvar|A}} is a [[Tree (data structure)|tree]] with a root labeled by {{mvar|A}}, leaves labeled by ground atoms from the heads of facts in {{mvar|P}}, and branches with children <math>A_1, \ldots, A_n</math> labeled by ground atoms {{mvar|G}} such that there exists a ground instance

:<code>G :- A<sub>1</sub>, ..., A<sub>n</sub>.</code>

of a rule in {{mvar|P}}. The proof-theoretic semantics defines the meaning of a Datalog program to be the set of ground atoms that can be defived from such trees. This set coincides with the minimal Herbrand model.<ref>{{Cite book |first=Serge |last=Abiteboul |url=http://worldcat.org/oclc/247979782 |title=Foundations of databases |date=1996 |publisher=Addison-Wesley |isbn=0-201-53771-0 |oclc=247979782}}</ref>

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 [[semiring]]s.<ref>{{Cite arXiv |last1=Khamis |first1=Mahmoud Abo |last2=Ngo |first2=Hung Q. |last3=Pichler |first3=Reinhard |last4=Suciu |first4=Dan |last5=Wang |first5=Yisu Remy |date=2023-02-01 |title=Convergence of Datalog over (Pre-) Semirings |class=cs.DB |eprint=2105.14435 }}</ref>

== Logic programming ==

While the name "logic programming" is used to refer to the entire paradigm of programming languages including Datalog and Prolog, when discussing formal semantics, it generally refers to an extension of Datalog with [[function symbols]]. Logic programs are also called {{dfni|[[Horn clause]] programs}}. Logic programming as discussed in this article is closely related to the "pure" or [[Declarative programming|declarative]] subset of [[Prolog]].

=== Syntax ===

The syntax of logic programming extends the syntax of Datalog with function symbols. Logic programming drops the range restriction, allowing variables to appear in the heads of rules that do not appear in their bodies.{{sfn|Abiteboul|1996|p=299}}

=== Semantics ===

Due to the presence of function symbols, the Herbrand models of logic programs can be infinite. However, the semantics of a logic program is still defined to be its minimal Herbrand model. Relatedly, the fixpoint of the immediate consequence operator may not converge in a finite number of steps (or to a finite set). However, any ground atom in the minimal Herbrand model will have a finite proof tree. This is why Prolog is evaluated top-down.{{sfn|Abiteboul|1996|p=299}} Just as in Datalog, the three semantics can be proven equivalent.

== Negation ==

Logic programming has the desirable property that all three major definitions of the semantics of logic programs agree. In contrast, there are many conflicting proposals for the semantics of logic programs with negation. The source of the disagreement is that logic programs have a unique minimal Herbrand model, but in general, logic programming (or even Datalog) programs with negation do not.

=== Syntax ===

Negation is written <code>not</code>, and can appear in front of any atom in the body of a rule.

<syntaxhighlight lang="bnf">
<atom-list> ::= <atom> | "not" <atom> | <atom> "," <atom-list> | ""
</syntaxhighlight>

=== Semantics ===

==== Stratified negation ====

{{expand section|date=March 2023|with=a formal definition of stratification}}

A logic program with negation is ''stratified'' when it is possible to assign each relation to some ''stratum'', such that if a relation {{mvar|R}} appears negated in the body of a relation {{mvar|S}}, then {{mvar|R}} is in a lower stratum than {{mvar|S}}.<ref>{{Cite journal |last1=Halevy |first1=Alon Y. |last2=Mumick |first2=Inderpal Singh |last3=Sagiv |first3=Yehoshua |last4=Shmueli |first4=Oded |date=2001-09-01 |title=Static analysis in datalog extensions |url=https://doi.org/10.1145/502102.502104 |journal=Journal of the ACM |volume=48 |issue=5 |pages=971–1012 |doi=10.1145/502102.502104 |s2cid=18868009 |issn=0004-5411}}</ref> The model-theoretic and fixed-point semantics of Datalog can be extended to handle stratified negation, and such extensions can be proved equivalent.

Many implementations of Datalog use a bottom-up evaluation model inspired by the fixed point semantics. Since this semantics can handle stratified negation, several implementations of Datalog implement stratified negation.

While stratified negation is a common extension to Datalog, there are reasonable programs that cannot be stratified. The following program describes a two-player game where a player wins if their opponent has no moves:<ref>{{Cite journal |last1=Leone |first1=N |last2=Rullo |first2=P |date=1992-01-01 |title=Safe computation of the well-founded semantics of datalog queries |url=https://dx.doi.org/10.1016/0306-4379%2892%2990003-6 |journal=Information Systems |language=en |volume=17 |issue=1 |pages=17–31 |doi=10.1016/0306-4379(92)90003-6 |issn=0306-4379}}</ref>

<syntaxhighlight lang="prolog">
move(a, b).
win(X) :- move(X, Y), not win(Y).
</syntaxhighlight>

This program is not stratified, but it seems reasonable to think that <code>a</code> should win the game.

==== Completion semantics ====

{{main|Negation as failure#Completion semantics}}

{{empty section|date=March 2023}}

==== Perfect model semantics ====

{{empty section|date=March 2023}}

==== Stable model semantics ====

{{main|Stable model semantics}}

The stable model semantics define a condition for calling certain Herbrand models of a program ''stable''. Intuitively, stable models are the "possible sets of beliefs that a rational agent might hold, given [the program]" as premises.<ref>{{Cite conference |last1=Gelfond |first1=Michael |last2=Lifschitz |first2=Vladimir |date=1988 |entry=The Stable Model Semantics for Logic Programming |url=https://www.cs.utexas.edu/users/ai-lab/?gel88 |title=Proceedings of International Logic Programming Conference and Symposium |editor1=Kowalski, Robert |editor2=Bowen, Kenneth |pages=1070-1080 |publisher=MIT Press}}</ref>

A program with negation may have many stable models or no stable models. For instance, the program

<syntaxhighlight lang="prolog">
p :- not q.
q :- not p.
</syntaxhighlight>

has two stable models <math>\{p\}</math>, <math>\{q\}</math>. The one-rule program

<syntaxhighlight lang="prolog">
p :- not p.
</syntaxhighlight>

has no stable models.

Every stable model is a minimal Herbrand model. A Datalog program without negation has a single stable model, which is exactly its minimal Herbrand model. 
The stable model semantics defines the meaning of a logic program with negation to be its stable model, if there is exactly one. However, it can be useful to investigate {{em|all}} (or at least, several) of the stable models of a program; this is the goal of [[answer set programming]].

==== Well-founded semantics ====

{{main|Well-founded semantics}}

{{empty section|date=March 2023}}

== Further extensions ==

Several other extensions of Datalog have been proposed and studied, including variants with support for [[integer]] constants and functions (including [[DatalogZ]]),<ref>{{Cite arXiv |last1=Kaminski |first1=Mark |last2=Grau |first2=Bernardo Cuenca |last3=Kostylev |first3=Egor V. |last4=Motik |first4=Boris |last5=Horrocks |first5=Ian |date=2017-11-12 |title=Foundations of Declarative Data Analysis Using Limit Datalog Programs |class=cs.AI |eprint=1705.06927 }}</ref><ref>{{Cite journal |last1=Grau |first1=Bernardo Cuenca |last2=Horrocks |first2=Ian |last3=Kaminski |first3=Mark |last4=Kostylev |first4=Egor V. |last5=Motik |first5=Boris |date=2020-02-25 |title=Limit Datalog: A Declarative Query Language for Data Analysis |url=https://doi.org/10.1145/3385658.3385660 |journal=ACM SIGMOD Record |volume=48 |issue=4 |pages=6–17 |doi=10.1145/3385658.3385660 |s2cid=211520719 |issn=0163-5808}}</ref> [[Inequality (mathematics)|inequality]] constraints in the bodies of rules, and [[aggregate function]]s.

[[Constraint logic programming]] allows for constraints over domains such as the [[Real number|reals]] or [[integer]]s to appear in the bodies of rules.

== See also ==

* [[Herbrand structure]]
* [[Logic programming]]
* [[Negation as failure]]
* [[Prolog syntax and semantics]]

== References ==

=== Notes ===
{{Reflist}}

=== Sources ===

*{{Cite journal|last1=Ceri|first1=S.|last2=Gottlob|first2=G.|last3=Tanca|first3=L.|date=March 1989|title=What you always wanted to know about Datalog (and never dared to ask)|url=https://www2.cs.sfu.ca/CourseCentral/721/jim/DatalogPaper.pdf|journal=IEEE Transactions on Knowledge and Data Engineering|volume=1|issue=1|pages=146–166|doi=10.1109/69.43410|issn=1041-4347 | citeseerx = 10.1.1.210.1118}}

[[Category:Programming language syntax]]
[[Category:Logic programming]]