Logic In Action

Exponential-time algorithms running on large data

Moshe Vardi is perhaps the world’s foremost expert on the application of logic to practical computations. His paper “Reasoning about Infinite Computations” with Pierre Wolper won the 2000 Gödel Prize. Infinite computations may not seem practical, but the magic is in the finite machines that perform them, and how requirements expressed in various logics translate into machine operations.

Today we wish to describe this logic-automata correspondence, and the larger issue of what distinguishes a “practical” algorithm.

Vardi gave three lectures on July 11–13 in this year’s H.M.S. Coxeter Lectures of the University of Toronto Fields Institute. They were also part of the Institute’s Summer Thematic Program on the Mathematics of Constraint Satisfaction.

I (Ken) had the pleasure of attending them while playing in the 2011 Canadian Open Chess Championship July 9–17. I wrote a tournament report for the prominent Susan Polgar chess blog. Besides reuniting with some old chess friends as described there, I spent other time at the university meeting visitors there I hadn’t seen in some years.

Audio and slides of the lectures are available here (scroll down). A running theme was that once we know a task is `elementary’, can we get it down to single-exponential time? So that we can actually run it on large data? That may seem quixotic to our understanding of the class as standing for “Practical” but life goes on, and so do processor cycles.

The Lectures

The titles of his three lectures hint at the humorous but earnest spirit in which they were delivered:

1. And Logic Begat Computer Science: When Giants Roamed the Earth
2. From Philosophical to Industrial Logics
3. Logic, Automata, Games, and Algorithms.

The first lecture was also called, “From Aristotle to Pentium.” Although much of this story is familiar, Vardi supplied historical details deeper than the beaten track, and unexpected angles of approach.

For instance, we all know that computers are based on Boolean logic, 0 and 1, and that circuits use logic gates. Thus it may seem strange to hear that in 1901, mathematical logic as a field seemed to have the least of any branch of mathematics to offer humanity. As Cosma Shalizi begins this note quoted by Vardi, the highlight of its previous 30-or-so years had been only the development of infinite cardinal numbers. Moreover the next 30 years were to seem a total car wreck:

• Bertrand Russell finds a gaping hole in Gottlob Frege’s formal set theory.
• Russell’s own programme to formalize mathematics in a strong logic requires 379 dense pages before it can derive , and only with the assistance of Alfred North Whitehead, who later denounces it as what this Wikipedia page terms “an overarching ontological mistake.”
• Though David Hilbert passionately championed the same programme, it is due to be blind-sided by Kurt Gödel’s incompleteness theorems, Hilbert himself recognizing this as defeat. [Update 4/1/13: not sure about this last sentence]

Indeed, as he noted, the lives of all the luminaries up through Gödel, Alan Turing, and John von Neumann would be punctuated by tragedy. Yet within 50 more years, the “defeated” programme was up and running industrially-vital applications all over the world. Our take on the “Classification Project” at the beginning of Vardi’s second lecture is that the key to success for logic was seeing weakness rather than strength as a virtue.

Is it True? Can it be True?

Every system of logic provides a formal language in which to express certain assertions and properties. The language can be tailored to the kind of structure one wishes to analyze and the particular relations one needs to formulate. Here are three kinds of structures:

Strings: Let denote that the character in position is . Then

is a logical assertion about (particular) strings. It says that between every two ‘s there is at least one .

Graphs: Let stand for the edge relation. Then

is an assertion about graphs. It says that every edge is involved in a triangle.

Time Series: Now let denote that happens at a given time; we are suppressing the index of the time. Then

is an assertion of temporal logic—in fact, LTL for linear temporal logic. It says that whenever a happens, a happens next and a happens sometime in the future. Here the logic suppresses the index .

Given an assertion and a structure , we can ask the following questions:

• Model Checking: Is true for the structure ?
• Satisfiability: Can there be a structure in which is true? (Maybe where is a small change from ?)

We can translate an ordinary Boolean formula into a formula over binary strings so that is satisfiable if and only if belongs to . Thus logical satisfiability is “usually” -hard. Model-checking in the Boolean case just means seeing whether a given truth assignment evaluates to true, but in the presence of quantifiers it can become harder.

When encodes conditions for a skyscraper or nuclear reactor to be managing its environment, or for a processor’s gate array to give correct results, these are more than 64 million dollar questions. If you weaken the logics to just what you need to express these conditions, you have a better chance of answering the questions.

Mechanizing Formulas

For every formula , we can define the language of structures in which is true. In the case of Strings this is an ordinary formal language. For other structures we can identify the language with some means of encoding the structures. Thus our questions become the familiar ones of whether a given string belongs to the language, or whether the language is (non-)empty.

If has free variables, we can incorporate them into the structures. For example, consider strings of some length over some alphabet , and an index variable that ranges over places . We can make “double-decker” strings over alphabet in which the components indicate value(s) of .

For a free first-order variable , we can impose the restriction that exactly one double-character in has as on the second deck. For representing a set of index variables, we need no such restriction. This is intuitively why second-order logics that are monadic, meaning they allow quantifying over relations—but only unary relations which denote sets—play a distinguished role.

What began to be realized in the late 1950’s is that by restricting the logics, the languages have forms that we already know how to handle via machines. Over strings, monadic second-order logic gives exactly the regular languages. First-order logics give important subclasses of the regular languages. Thus finite automata, NFA’s as well as DFA’s, become the machines to consider.

Over other structures, you have to consider other kinds of machines. And when you’re considering open-ended time intervals or sequences of events, it is actually an impediment to have a symbol “” standing for a finite length of string or size of structure. For mathematical reasons as well, it became surprisingly natural and necessary to consider machines with infinite words as input, and an acceptance cirterion that involved entering a “good” state infinitely often.

The problem finally became, how to build the right machine from the formula ?

It’s Elementary…Or Not

The useful fact about formulas is that they are built up inductively from smaller formulas. For instance, we may have . Suppose we have a deterministic machine for .

Now deals with strings that have a “deck” for values of . , however, involves strings without this deck. Instead, a machine for has to be built to “guess” possible values on this deck, before employing . Thus we are led to being nondeterministic. In the case of finite automata on finite strings we can use the sets-of-states construction to convert to a DFA . However:

• For automata on infinite words, the sets-of-states construction doesn’t work, and something more involved is needed;
• For a universal quantifier you need complementation or something else, which is even more involved; and
• Even so, the step can blow up the state space by an exponential.

If we have quantifiers, we may iterate for -many times. If depends on the size of the formula, then the blowup may be an unbounded stack of exponentiated ‘s.

This means a function that fails to be elementary. There is a formal notion of elementary in logic. A neat theorem shows that the languages definable in elementary logic are exactly those decided in time -to-the--to-the-…-to-the- power, for some finite stack of ‘s. That is, a language is elementary if and only if it is decidable in elementary time.

Non-elementary time is “hopeless”—and for some logic problems, non-elementary lower bounds show that we cannot do better. But for others there is a smarter way to cut down the state space when managing quantifiers in a formula, yielding an elementary-time algorithm. But generally always there is some exponential in the time, so is this still hopeless?

Running…

Again we are telling the story in shortcutted form, and hence cutting off some of Vardi’s carefully-told points. We invite you to follow his slides, and the audio if you have time—for many deft bits of humor in the lectures drew appreciation from the packed room at the Fields Institute. But let us make an analogy:

• In polynomial complexity, the real import of the Cobham-Edmonds thesis is that once some polynomial-time algorithm is found, the gangway is opened for combinatorial mavens to set about reducing the exponent, and (hopefully) the other constants on the running time. Once you know the exponent is finite, you can grab it and work on it.
• In computational logic, the same role is played by the stack of exponentials. Once you know it is finite, you can work on reducing it.

In one example, a double-exponential time construction was reduced in a series of eight papers to , where the “” is mysteriously tight in worst-case.

Another example showed how choice of logic can be a game-changer. Linear temporal logic (LTL) has the same expressive power as first-order logic with natural-number variables. The satisfiability problem for first-order logic extended to include computation traces—in some way analogous to our “decks” example above—has a non-elementary lower bound. The corresponding satisfiability problem for LTL, however, belongs to single-exponential time, and is in fact -complete.

Something about LTL enables building branching tableaus that help control the blowup in eventual machines. The third lecture detailed how the translation from LTL to machines on infinite words involves another game-changing element, namely games themselves, to create alternating machines that wind up being more succinct than what you’d get by insisting on nondeterministic, let alone deterministic, machines.

Isn’t -complete supposed to be bad news? Apparently not. The second lecture ended with a “Reduction to Practice” for LTL, with three implementations from 1983 to 1995. The third lecture ended by reiterating the importance of

Games/alternation as a high-level algorithmic construct,

with the

Bottom line: Alternation is a key algorithmic construct in automated reasoning — used in industrial tools.

Open Problems

Why do these exponential-time algorithms run tolerably well in practice? How do you know when they aren’t doing the job well or quickly enough?

I wound up asking just one very particular question of this kind, about shortcuts in hash-table representations of big machine state spaces that sometimes compromise the logic itself so that some erroneous conditions (such as bugs in gate arrays) don’t get detected—before having to dash downtown for my chess game.

If computational logic seems to have retreated again as a field, what new boon may it have to offer? This was Vardi’s first general question.

[Update 4/1/13: I am unable to trace a source I recall as saying Hilbert graciously congratulated Gödel—more the opposite appears to be the case, with Hilbert decrying “excessive finitism” in Gödel’s setup.]