Folks, (01)
In a note to Matthew and Ali, I promised to translate the formal
terminology in Ali's note to plain English. But I realize that
the task of mapping all the formal notation to English + ordinary
programming terminology is nontrivial. Therefore, I'll start by
explaining one fundamental term: the word 'model'. (02)
That term has many diverse uses, which create a lot of confusion.
Therefore, I'll use the term 'Tarski-style model' or 'TS model' for
the kinds of models that are used in discussions of logic. I don't
deny the value of other uses, but I want to explain TS models. (03)
I also want to explain the distinction between two very important
ways of using logic: (04)
1. Theorem proving, which most logicians talk about and most
programmers rarely, if ever, do. (05)
2. Model checking, which logicians sometimes talk about, and which
relational databases do as a matter of course (but with different
terminology). (06)
Many people (SemWebbers in particular) make the claim that first-order
logic is inefficient because theorem proving (#1 above) can sometimes
be undecidable and can sometimes be intractable (take exponential time
or worse). That is true. But in many important cases, theorem proving
can take polynomial time or even linear time. (07)
However, the SemWebbers don't talk about model checking, which never
takes more than polynomial time. And for many very important cases,
model checking can be done in linear or even logarithmic time. (08)
The DB gang never use the term 'model checking'. But they do it
under the terms 'constraint checking' and 'query answering'. Both
of those practices are efficient and widely used applications of FOL. (09)
For this explanation, I'll use examples of SQL with relational
databases, but I want to emphasize that network DBs are logically
*identical* in expressive power to table DBs. Any information stored
in one can be mapped to a logically equivalent form in the other.
There may be differences in syntax, performance, human factors,
etc., but the logic and the semantics are identical. Although I'll
talk about SQL and relational DBs, these principles also hold for
anything stored in a graph or network form. (010)
To explain the connection between databases and model checking, the
first step is to make the comparison between a relational DB and
a Tarski-style model (TS model). (011)
1. A Tarski-style model for a first-order language L (such as Common
Logic) consists of a domain D of *individuals* and a set R of
*relations* over D. The models for Common Logic also include
a set F of *functions* over D (but some versions of model theory
lump the functions with the relations in a single set R). (012)
2. A relational database also has a set D of all the individuals that
are named by strings in the DB, and a set T of tables, each of
which consists of a set of rows (or n-tuples) of strings that
define some n-adic relation. Since all the tables in T are finite,
they can only define finite relations. However, a DB may also
contain a set VT of *virtual tables*, which are computed instead
of being stored. Since virtual relations are not stored, they
can be infinite -- for example, the greater-than relation over
numbers is trivial to compute, but impossible to store. (013)
The crucial feature of a Tarski-style model M is an evaluation function
Phi(s,M), where s is any sentence in the logic L and M is any model
M=(D,R,F) with domain D, relations R, and functions F. The function
Phi has two possible values: (014)
Phi(s,M) is *true* if the sentence s is true of the TS model M. (015)
Phi(s,M) is *false* if s is false of M. (016)
Note that every relational database has a unique mapping to a TS model: (017)
1. The domain D of individuals named in the DB maps to the domain D
of a TS model. (018)
2. The n-tuples of any table in the DB can be mapped to the n-tuples
of either a relation in R or a function in F of a TS model. (019)
3. The n-tuples that are computed by any virtual relation in the DB
can also be mapped to either a relation in R or a function in F
of a TS model. (020)
Even more important, the WHERE clause of an SQL query can express
full first-order logic: it uses the operators AND, OR, NOT, and
the quantifier EXISTS in all possible combinations. It can
therefore be mapped to Common Logic or other versions of FOL. (021)
Finally, the methods for evaluating an SQL WHERE clause in terms
of a relational DB are *exactly equivalent* to Tarski's definition
of the evaluation function Phi(s,M). (022)
Since Tarski was defining a mathematical system, he didn't worry
about computational efficiency in his definition. But the methods
for evaluating an SQL WHERE clause use various optimizations,
including indexes over the names in various columns of the tables.
Even without indexing, every sentence s derived from an SQL WHERE
clause can be evaluated for truth or falsity in at most polynomial
time (where the exponent of the polynomial is less than or equal
to the number of quantifiers in the sentence s). With indexing,
the amount of computation can often be drastically reduced. (023)
Given this mapping, we can distinguish three applications of model
checking that use a relational DB: (024)
1. Updates. Any theory expressed in first-order logic can be
translated to a collection of *constraints* on permissible
updates to a database. Each update u converts a DB that
represents a model M to an updated DB that represents a model M'
in which the new assertion u is true. But before the update u
is completed, each constraint is checked against the new model M'.
If any constraint evaluates to *false* then the update is blocked,
and the DB remains unchanged. (025)
2. True-false questions. The truth of any statement s in FOL can
evaluated in terms of a given DB by translating s to an SQL WHERE
clause. The SELECT clause for the query does not ask for any data
to be retrieved; it just checks whether the WHERE clause is true. (026)
3. WH-questions. Any question that begins with 'who', 'what', 'when',
'where', or 'which' can answered by an SQL query in which the
SELECT clause requests the data that make the WHERE clause true. (027)
These are applications of model checking to check constraints
and to answer questions. Both the constraints and the questions
can use full expressive power of first-order logic. (028)
No matter how complex the FOL statements, the model checking is
decidable and efficient. In fact, the entire world economy
depends on these applications of model checking. (029)
For a tutorial on math and logic, including a brief introduction
to first-order logic and model theory, see (030)
http://www.jfsowa.com/logic/math.htm (031)
Section 6 of this tutorial shows how relations can be mapped
to graphs. Sections 8 to 10 survey propositional and predicate
logic. Section 13 surveys model theory. (032)
For further discussion of some of the points discussed in this
note, see (033)
http://www.jfsowa.com/pubs/fflogic.pdf
Fads and fallacies about logic (034)
John Sowa (035)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (036)
|