Logic for Computer Science/Querying

From Wikibooks, open books for an open world
< Logic for Computer Science
Jump to: navigation, search

Query and Definability[edit]

The problem of satisfiability is central to mathematical logic: for a logic L on a domain D of structures try to find a model in D for a given formula φ from L. The more special problem of model-checking on a logic L and a domain D of structures tries to answer, does \mathfrak A \vDash \psi\ hold for a given structure \mathfrak A \in D and a formula \psi\ \in L. Model-checking is an important area in computer science. The concept of querying is leading beyond these 'true-false' evaluations, it introduces the result set as it's outcome.

Query[edit]

Motivation

Think of a customer-database. Now one can query such a database e.g. "All Customers in Africa" that results in a list of all customers in Africa. In case of a query like "All customers and their countries" the result consists of 2-ary tuples of a customer and a country, whereas the query "(Do) we have a customer in Rwanda" leads to either yes or no. Similarly one can define queries on structures that deliver a set of elements of the universe, where the universe relates to the data in the database.

Notion

First recapture the notion of bound and free variables: whereas a sentence (no free variables) like \forall_x \exists_y xRy computes to either true or false the formula's \forall_x xRy truth-value is relative to the free variable y and thus implies a set of values for y for which it is true. In general for a formular with n free variables we get a set of n-tuples (that may also be empty). In this sense sentences deliver 0-ary tuples in case they are true.

Definition

Let \mathfrak A be a S-structure with universe A, m a nonegative integer and Q a mapping from S-structures to sets of subsets of Am, s.t. each \mathfrak A maps to a subset of Am.

Q is said to be a m-ary Query on S-structures iff Q is closed under isomorphism,

where closed (or preserved) under isomorphism is: if \mathfrak A \cong \mathfrak B by an isomorphism f then f(Q(\mathfrak A)) = Q(\mathfrak B).

Remarks

  • A 0-ary Q is also called a boolean query. In this case Q maps to A0, that is a 0-tuple, or the empty set. The former result is also called TRUE the latter FALSE.
  • For a boolean query Q a subset C of S-structures can be defined by: \mathfrak A \in C iff Q(\mathfrak A) = true
  • the closedness condition ensures that only the 'shape' of structures is queried, i.e. it is unimportant what the universe consists of as long as its related in the same way. Thus questions on the kind of elements of the universe cannot be answered by a query.
  • From a unary query a substructure \mathfrak B of the queried structure \mathfrak A can be obtained with
    R^\mathfrak B = R^{\mathfrak A} \cap Q^m, for an m-ary R and with an 1-1 mapping of constants.

Examples

Simple

Take S = {<}. We query 'all elements that have no smaller element'. This gives for a universe of {10, 11, 12} the result {(10)} (A set of 1-ary tuples). The query for 'all elements that have a smaller element' gives {(11), (12)}. A query for 'all directly succeeding elements' gives {(10, 11), (11, 12)} (A set of 2-ary tuples). The query 'there is a biggest element' results in {()} (The 0-ary element), whereas 'there is no biggest element' gives {} (false).

Graphs

Typical queries on graphs G = (V, E) are:

  • transitive closure (smallest transitive extension) is a 2-ary query:
    \big\{(x, y ) \in V^2 |\mbox{ there is a path from x to y }\big\}
  • isolated nodes is a 1-ary query:
    \{(x) \in V |\mbox{ there is no node connected with x }\}
  • planarity is a 0-ary (boolean) query:
    \begin{cases} \{()\} & \mbox{if G is planar} \\ \{\} & else \end{cases}


Definability[edit]

On one hand we have queries that can be more or less 'complicated'. Just think of a database-query simply for all customers with name = 'Ubuntu' compared to a query for customers named Ubuntu that are not situated in Africa or middle east. On the other hand we have languages of different expressive power like FO and MFO (monadic first oder logic). So one can ask if the expressive power of a language is strong enough to express (define) a certain query.

Definition for classes of structures

Let C be a class of finite structures and L be a logic. C is said to be definable in the logic L iff there is a sentence φ in L s.t. C is the set of all finite models of φ.

Definition for queries

Let Q be a query, L a logic

Q is said to be definable in L iff it exists a formular φ(x1, ..., xm) of L in S s.t. for all \mathfrak A all elements of Q(\mathfrak A) are an assignment on φ s.t. \mathfrak A \vDash \varphi

Examples

Simple

On a finite graph the query 'there is an element that is adjacent with all others' can be written in FO as \exists_x \forall_y x R y. The language can even be restricted further, e.g. by allowing only 2 variable per formula (and thus is definable in the logic FO2).

Negative

Single step connectivity for graphs can be defined in FO as

\forall_{x y} E(x, y)

So we get 2-step connectivity as

\forall_{x z} \exists_y E(x, y) \land E(y, z)

This can be continued to n-step connectivity for a fixed n, but not for arbitrary n since FO formluas are always of fixed length. It would take some 'infinite conjunction' to expand the above approach to arbitrary length. And since there is no other way to express arbitrary connectivity in FO (what is omitted show here) we say the connectivity query is not definable in FO. It can be shown that it is expressible in UMSO (Universal Monadic Second Order Logic).

Graphs

The definability of the queries considered above is:

  • the transitive closure query is not definable in FO
  • the isolated node query is definable in FO as
    \forall_y \neg E(x, y)
  • planarity is not definable in FO

Propositions[edit]

Query-Safety

TODO

The impact of Order

TODO

Finite Structures[edit]

Concept[edit]

Definition

A Structure is said to be finite iff it's Universe is finite.

Examples


The unusual effectiveness of finite structures in computer science[edit]

Data structures in computer science are usually finite, e.g. a Database always holds finitely many entries. But by restricting to finite structures we have to issues:

  • We still have to deal with structures of arbitrary size, e.g. to sum from 1 to 3 one can write 1 + 2 + 3, from 1 to 4: 1 + 2 + 3 + 4, but from 1 to an arbitrary natural number we must use a special operator like 'Σ' that extends our simple '+' language (Also the '...' notation doesn't help since it extends our language as well).
  • We now have to deal with complexity issues, that we haven't had before. Example ...


Finite Model Theory[edit]

So the Theory dealing with finite structures (Finite Model Theory (FMT)) is not just a simplification of the theory also covering infinite ones (Model Theory (MT)). It has it's own character. This is especially an issue when it comes to instruments for proofing. One of the most important of such tools in MT is the compactness theorem, but it is completely useless when we deal with finite structures exclusively:

Consider the following sentence σ3

\exists_x \exists_y \exists_z (x\ne y \and y\ne z \and x\ne z)

that says that there are at least 3 different elements in a universe. One can expand σ3 easily for n other than 3. So, let Σ = {σ1, σ2, σ3, ...} be the infinite set of all these sentences. Now Σ is obviously not satisfiable by a finite model, although every finite subset of Σ is. Ok, but why does that matter? One of the most useful tools in general Model theory is the Compactness theorem, stating: "Let Σ be a set of FO sentences. If every finite subset of Σ is satisfiable, then Σ is satisfiable." But as just shown this doesn't hold for the finite case, thus there is no Compactness theorem in Finite Model Theory!

And (unfortunately) this is the case for many other important theorems as well (actually the very most of them) like e.g. Gödel's Completeness theorem. Moreover important definitions of MT must be adopted for the finite case. For example the concept of types is a very central one in MT. But applied to FMT it turns out to be quite useless since it already characterises finite structures up to isomorphism. So the definition of types has to be refined in FMT (to a type concept in FO[k], depending on an integer k).

So Finite Model Theorists can not simply adopt the classic instruments from Model theory, they have to find their own. The basic ones are presented in the 'Proofs' section.

The Property of Elementary Equivalence[edit]

Querying is about discrimination of structures. So the basic question is "Can i discriminate a structure from all different structures?", where different means not equal up to isomorphy. This can be done for finite structures (but not for infinite ones). E.g. ...

Properties for a finite Number of Structures[edit]

So being of a certain structure can be seen as an elementary property, that discriminates a class of isomorphic structures from all others. Now we can think of properties that discriminate 2 different (nonisomorphic) structures from the rest. They can also be descriminated by simply connecting the properties, like e.g. ...

This can be extended to properties for a finite number of structures, like e.g. ...

Properties for an infinite Number of Structures[edit]

Also properties that hold for an infinite number of structures can be thought of. But these are not discriminatable in the above way. E.g. ...

There are Logics that allow this sort of infinite disjunction, like ...

So, are there other ways to discriminate these structure in FO? Sometimes, like in the case of ...

So we need a decision tool (method) that decides if structures with a certain property can be discriminated or not, i.e. responds either "yes" or "no" for all possible properties, i.e. is sound and complete.

The special roles of First-Order and Infinitary Logics[edit]

TODO

Some Definability Results[edit]

FO on Graphs[edit]

Fragments of SO[edit]

MSO and EMSO on Graphs[edit]

MSO and FO on Strings[edit]

Fixed-Point Logics[edit]