# The History of the Frame Problem

This is my synopsis of the paper, “The History of the Frame Problem”.

In 1969, McCarthy and Hayes tackled the problem of making agents that can formulate strategies to complete goals. The problem has two parts: representing the state of the world at various moments in time, and searching for a sequence of actions whose final world state satisfies the goal. Like good software engineers, they aspired to decouple the parts, and had a clever idea. They formalized in first-order logic

1. the initial state of the world
2. the preconditions under which an action can be taken, and
3. the state-to-next-state transformation an action produces on the world.

This solved the first half of the problem, and now the second problem could be solved by a generic theorem prover. Unfortunately, in practice, formalization #3 ended up being really large.

We were obliged to add the hypothesis that if a person has a telephone, he still has it after looking up a number in the telephone book. If we had a number of actions to be performed in sequence, we would have quite a number of conditions to write down that certain actions do not change the values of certain fluents [fluent = a proposition about the world which changes over time]. In fact, with `n` actions and `m` fluents, we might have to write down `n*m` such conditions.

They called this problem of `n*m`-blowup the frame problem, but made the mistake of including the word philosophical in the title of their paper, provoking AI doomsayers to cite it as yet another example of why computers could never think like humans. The discussion became more interesting when Daniel Dennett directed the attack away from the AI researches and toward the philosophers. He caricatured epistemology as a comically profound but very incomplete theory, because for thousands of years, no one had ever noticed the frame problem.

… it is turning out that most of the truly difficult and deep puzzles of learning and intelligence get kicked downstairs by this move [of leaving the mechanical question to some dimly imagined future research]. It is rather as if philosophers were to proclaim themselves expert explainers of the methods of a stage magician, and then, when we ask them to explain how the magician does the sawing-the-lady-in-half trick, they explain that it is really quite obvious: the magician doesn’t really saw her in half; he simply makes it appear that he does. ‘But how does he do that?’ we ask. ‘Not our department’, say the philosophers – and some of them add, sonorously: ‘Explanation has to stop somewhere.’

Some philosophers and AI researches argued that the original mistake leading to the frame problem was McCarthy and Hayes choosing first-order logic for world representation. Their case is easily made with the Tweety Bird problem: The premises

1. All birds fly
2. Tweety is a bird
3. All broken-winged creatures cannot fly, and
4. Tweety has a broken wing

can prove both

1. Tweety can fly, and
2. Tweety cannot fly

Clearly premise 1 is too strong, but attempting to modify first-order logic to support most statements instead of all statements breaks monotonicity: Under most-enabling logic, premises 1, 2, 3 would prove 5, but premises 1, 2, 3, 4 would prove 6. An agent learning premise 4 would change its mind from conclusion 5 to conclusion 6. This is, of course, the desired behavior, but dropping the stability of truth means the agent can no longer use a generic theorem prover. The agent is using a modified logic system, and so it must use a specialized theorem prover. The question becomes: which logic system to use?

In standard first-order logic, every proposition is either true, false, or unknown. Learning new information can only ever change the status of unknown statements. To solve the tweety bird problem, a logic must enable assuming unknowns as false until proven otherwise (closed-world assumption). The symbolic AI community eventually converged on circumscription, which is a logic that assumes particular propositions to be false until proven otherwise.

McCarthy updated his situation calculus by circumscribing the proposition Abnormal, allowing him to formalize Most birds fly as All birds fly unless they are abnormal and adding the premise Broken-winged creatures are abnormal. Since the Abnormal proposition is assumed to be false until proven otherwise, Tweety is assumed to be a normal flying bird until the agent learns that Tweety has a broken wing.

Shanahan took a time-oriented approach instead. In his circumscriptive event calculus, he circumscribed Initiates and Terminates, so he could formalize Most birds fly as All birds can fly at birth and he could replace All broken-winged creatures cannot fly with Breaking a wing Terminates the flying property. Since the Terminates proposition is assumed to be false until proven otherwise, Tweety’s birth state (capable of flight) is assumed to persist until the agent learns that Tweety’s wing was broken.

Personally I find circumscription unsatisfying. To me, the most obvious answer for “How do you turn ‘all’ into ‘most’?” is probability theory. As E. T. Jaynes showed, logic is merely a special case of probability theory (in which all of the probabilities are 0 or 1), so the jump from logic to probability theory seems more natural to me than circumscription. I am not alone in thinking this, of course. Many people attempted to solve the frame problem using probability theory, but as Pearl showed in 1988 regarding the Yale Shooting Problem, probability theory can never be enough, because it cannot describe counterfactuals, and thus cannot describe causality.

But that limitation disappeared in 1995, when Pearl figured out how to generalize probability theory. He discovered a complete set of axioms for his “calculus of causality”, which distinguishes between observed conditional variables and intervened conditional variables.

``````Logic -> Probability Theory -> Calculus of Causality (wow!)
``````

According to the linked paper, the circumscriptive event calculus and Thielscher’s fluent calculus have adequately solved the frame problem. But I still wonder, has anyone re-attempted a solution using the calculus of causality?﻿

# Automatic Redis Through Static Differentiation

A new project, “Incremental λ-Calculus”, obviates my previous posts on automatic redis. The team has created an algorithm, called static differentiation, which performs a source to source translation on functions in the simply typed lambda calculs. The resulting function takes twice as many arguments as the previous program, with every other argument being a diff, or derivative, on the previous argument. When further optimizations are applied to the source, such as constant reduction and dead code elimination, the non-derivative arguments can sometimes be removed entirely. Here is an example from the paper:

After static differentiation, the code becomes:1

When optimizations are applied, `grandTotal'` becomes the implementation that a programmer would have written:

In this case, the resulting `grandTotal'` makes no reference to the original multisets at all. The authors of the paper call this “self-maintainability”, by analogy to self-maintainable views in databases.

The problem of infering redis update operations from database update operations, then, is simply a matter of differentiating and then optimizing the cache schema. (“Cache schema” is the mapping from redis keys to the database queries that populate those keys.) The mappings whose derivatives are self-maintainable can be translated into redis commands.

Here is the source transformation described in the paper:

Returning to an example from the first post:

The derivative is

In the case of an insert, we have

which means that `userIds'` can be reduced to

1: I’m being a little imprecise when I define the derivative of a type as another type, since the type of the derivative can vary depending on the value. The derivative of 3 is all integers from -3 to positive infinity, not all integers.

# Using unsafeInterleaveIO to Lift Haskell’s Lazy Semantics Into a Toy Interpreter

The main challenge of writing a lazy interpreter is sharing structure: in particular, making sure that an individual closure is not evaluated more than once. Obvious but tedious solutions in Haskell include using `IORef`s and monadic state. The interpreter below uses a completely different tactic: exploiting `unsafeInterleaveIO`. All function arguments are evaluated “right away”, but in the context of an `unsafeInterleaveIO` (so, in fact, they are actually not evaluated right away). With this hack, we get to write an interpreter which looks like an interpreter for a strict functional language, but actually behaves lazily (by lifting haskell’s own lazy semantics into our interpreter).

Interpreter.hs

# Partial Evaluation of Fat Languages

Language theory has always been my favorite part of computer science, and recently I have been playing around with partial evaluation. Creating an optimal, self-applicable specializer is really tricky. I thought that I was helping myself by working in a very minimal language, but this turned out to be counter-productive. It is easier to write a specializer in a language that has a large number of unnecessary primitives. The additional complexity of each primitive is very localized: just add another case to the giant switch statement, which does nothing more than “lift” the container language’s primitive into the contained language, and is a small price to pay for easing the coding of the rest of the specializer.

But that was not the only benefit! It turns out that having extra constructs also makes the binding-time analysis easier. (Binding-time analysis is the task of figuring out which parts of a program are static and which are dynamic for a given partial input.) An obvious example is booleans. Using church-encoded booleans is more minimal than having primitive booleans and an if-then-else construct, but analyzing the former is harder, since it requires analysis of higher-order functions, which usually requires writing a type-inference algorithm. Maps are another example. Lisp-style association lists seem like a natural approach, but, unless you do some very sophisticated analysis, the specializer will fail to recognize when the keys are static and the values are dynamic, and so appromixate to marking the entire data structure as dynamic (which usually kills optimality). By making maps a primitive in the language, you can code especially for that scenario.

For anybody interested in partial evaluation, I highly recommend the Jones, Gomard, and Sestoft book. It is extremely lucid in its exposition, not only of partial evaluation, but of many other analysis and transformational techniques. For instance, a year or so ago I was trying to understand abstract interpretation, but I could not find a succinct explanation of the algorithm anywhere. It turns out they provide one in chapter 15. They do it in only five pages, most of which is examples. Another example is supercompilation, which was opaque to me until I read Neil Mitchell’s excellent paper on Supero. But if he hadn’t written it, I could have turned to chapter 17 of the book, which incidentally also covers deforestation in the same breath. I think the only computer science book which I have revisited more frequently than this one is Norvig and Russell’s book on artificial intelligence. Pierce’s Types and Programming Languages is a close 3rd.

# Automatic Redis, Part Two: Sorting and Data Structures

This post is part of a sequence I am calling automatic redis, which is my attempt to solve the cache invalidation problem.

In my previous post, I demonstrated that a library could infer cache update operations from database insert operations by performing algebraic manipulations on the queries that define the cache keys. The algebraic laws needed were the distribution laws between monoids. e.g. `count` distributes over the `Set` monoid to produce the `Sum` monoid. A library could also infer the arguments of the cache keys (e.g. `taskIds.{userId} -> taskIds.65495`) by performing functional logical evaluation on the cache key’s query. If the library’s goal became suspended during evaluation, it could proceed by unifying expressions of low multiplicity with all possible values. For instance, if the goal for a filter query became suspended, the library could proceed by considering the `true` and `false` cases of the filter separately.

In this post I would like to talk about sorting and limiting, as well as flesh out some of the data structures that might be used in an automatic redis library.

##### Set

`Set` is the simplest data structure, and forms the foundation for two of our other collection types.

The monoidal operation for `Set` is simply set union.

##### List

`List` is a `Set` with an embedded sorting function. Tracking the sorting function enables us to compute redis sorted set keys if necessary.

A commonly used sorting function would be `x => x.modifiedDate`.

The monoidal operation for `List` is the merge operation from merge-sort, with one restriction: the sorting functions of both lists must be the same sorting function.

##### LimitedList

`LimitedList` is a `List` with an upper bound on its size.

The length of the contained `List` must be less than or equal to the upper bound. Tracking the length enables us to know how to trim cache entries, e.g. when using the ZREMRANGEBYRANK command.

The monoidal operation for `LimitedList` is to merge-sort the two lists and truncate the result to the limit. Similarly to `List`, the library expects both lists to have the same upper limit.

##### First and Last

`First` and `Last` are essentially `LimitedList`s whose upper bound is `1`. Making specialized types for singleton LimitedLists makes working with non-collection redis data structures easier.

Although `First` and `Last` have the same representation, they have different monoidal operations, namely `(x,y) => x` and `(x,y) => y`.

##### Maybe

The `Maybe` type is useful for queries that always generate a unique result (such as lookup by primary key), and as such the `Maybe` type does not need to contain a sorting function.

The monoidal operation is to pick `Just` over `Nothing`, but with the restriction that both arguments cannot be `Just`s.

Collision of `Just`s can happen if the application developer misuses the `The` operation (defined below). Unfortunately this error cannot be caught by an automatic redis library, because the library never actually computes the value of `mappend`. The library only tracks monoidal types so that it can know what the final redis commands will be.

Speaking of query operations, it’s about time I defined them. But first… one more monoid.

## Query operations

Query operations are parameterized over an input type and an output type.

A few more data structures and we will have all the pieces necessary for an application developer to define a cache schema.

Putting it all together, we can showcase the cache schema for a simple task management website.

It’s important to keep in mind that although I have made the above code look like haskell, no library in haskell could actually use the above code. The variables occuring after the `\$=` sign are logic variables, not function parameters. An EDSL could get close to something like the above, but the normal types for `==` and `&&` are unusable, and the lambdas inside the `Where` clauses would need to be reified anyway.

Still to come: deletes, updates, uniqueness constraints (maybe?), and psuedo-code for the generation of redis commands.

# Automatic Redis, Part One: Inserts and Cache Key Extraction

This post is part of a sequence I am calling automatic redis, which is my attempt to solve the cache invalidation problem.

These are some initial thoughts on how to automate cache updates. The question I want to answer is this: given a mapping from redis keys to the queries that produce their values, how can I infer which redis commands should be run when I add, remove, and update items in the collections which are my source of truth?

The code in this post is psuedo-haskell. What appears to the left of an `=` sign is not always a function, and the `.` is used for record field lookup as well as function composition.

I’ll start with a simple example. Suppose I run a website which is a task manager, and I want to display on my website the number of users who have signed up for an account. i.e. I want to display `count users`. I don’t want to count the entire collection every time I add an item to it, so instead I keep the count in redis, and increment it whenever a new account is created. Proving that INCR is the right command to send to redis is straightforward:

Notice that when `count` distributes, it changes the plus operation from union (`++`) to addition (`+`).

Here is a similar example, this time storing the ids instead of a count.

Obviously the appropriate redis command to use in this case is SADD.

Filtering is also straightforward.

Obviously a pipeline of `SADD`s will be correct, and the expression to the right of the `++` gives my automatic cache system a procedure for determining which `SADD` operations to perform. When the cache system gets the user object to be added, it will learn that the number of `SADD` operations is either zero or one, but it doesn’t have to know that ahead of time.

A computer can easily verify the above three proofs, as long as they are properly annotated. But can I get the computer to create the proof in the first place?

Rewriting the activeUserIds example to use function composition suggests one approach.

In general, it seems that queries of the form

become

provided f, g, h, etc. all distribute over `mappend`. The actual value of `mappend` will determine which redis operation to perform. Integer addition becomes `INCR`, set union becomes `SADD`, sorted set union becomes ZADD, list concatenation becomes LPUSH or RPUSH, etc. An important monoid which may not be obvious is the Last monoid (`mappend x y = y`), which becomes SET.

So much for updates on constant cache keys. Parameterized cache keys are much more interesting.

On my task manager website, I want to have one cache entry per user. The user’s id will determine the cache key that I use.

It’s tempting to think of this definition as a function:

But an automatic caching system will not benefit from this perspective. From it’s perspective, the input is a task object, and the output is any number of redis commands. The system has to implicitly discover the `userId` from the task object it receives. The `userId` parameter of `taskIds.{userId}` is therefore more like a logic variable (e.g. from prolog) than a variable in imperative or functional languages.

The monoidal shortcut rule is still valid for parameterized redis keys.

The caching system does not need to reduce this expression further, until it receives the task object. When it does, it can evaluate the addend as an expression in a functional-logical language (similar to Curry).

Unfortunately at this point the goal becomes suspended. The cache system can cheat a little by unifying `task.owner == userId` with `True` and `False`.

In the true case, `userId` unifies with `task.owner`, which I’ll say is 65495:

In the false case, `userId` remains unbound, but that’s ok, because the expression reduces to a no-op:

In general, whenever the cache system’s goals become suspended, it can resume narrowing/residuation by picking a subexpression with low multiplicity (e.g. booleans, enums) and nondeterministically unifying it with all possible values.

Most of the time, each unification will result in either a no-op, or a redis command with all parameters bound. An exception (are there others?) is queries which affect an inifinite number of redis keys, e.g. caching all tasks that do NOT belong to a user.

This is clearly a bug, so the caching system can just log an error and perform no cache updates. It may even be possible for the caching system to catch the bug at compile time by letting the inserted entity (e.g. a task) be an unbound variable, and seeing if a non-degenerate redis command with unbound redis key parameters can be produced.

This post has focused mostly on inserts and queries that fit the monoidal pattern. In another post I’ll take a look at deletes and queries which are not so straightforward.

# Rubber-duck Logging

I often ask myself, “How can I be a more productive software engineer?” I can answer this question better if I break it down into pieces.

In my day to day work, there are approximately five things that take up most of my time. Ordered from most time consuming to least time consuming, they are:

1. Debugging
2. Writing code
3. Helping other people
4. Learning and evaluating libraries, frameworks, and tools
5. Designing solutions

So the obvious place to start is reducing my time spent debugging. The best way to reduce debugging time is to avoid doing it in the first place, and I’ve accomplished this a number of ways. From best to worst:

1. Using languages that have very strong type systems (e.g. haskell)
2. Using smart editors (e.g. IntelliJ) that give me immediate feedback when I make mistakes
3. Writing code in short, quick iterations instead of large batches
4. Writing unit tests

(To the weenies who are angry at me for putting unit tests at the bottom: it’s only because I hit the point of diminishing returns once I’ve applied the other approaches. I found writing unit tests in ruby to be enormously helpful, because ruby is neither statically typed nor does it have smart editors. But when I’m writing scala in IntelliJ, the type system and the editor catch so many of my bugs that there’s usually nothing left for the unit tests to find. I still write unit tests, but they provide more value in discovering regressions than in discovering bugs the first time around.)

Despite using all these approaches, debugging still takes up more of my time than the actual writing of the code. The only exception has been haskell, but I don’t use haskell at work.

My approaches are fairly standard, but a few days ago I discovered an approach that I haven’t heard described elsewhere. I was practicing the habit of “noticing when I’m surprised”. Being frequently surprised is bad because it means I’m not learning. I noticed that sometimes when I ran my programs, they did not behave the way I expected. i.e. I was surprised.

How could I stop being surprised? I decided to start documenting my surprises. I created a document with a table of two columns. In the left column I would record each surprise: what I did, what I expected to happen, and what actually happened. In the right column I would record the resolution (once I had finished debugging it), and why my expectations were wrong in the first place.

I was hoping that after doing this for a few days, I would have enough data to find the persistent errors in my thinking. But something pleasant happened before I got that far!

I have not been very disciplined about this. I have only remembered to document my surprises twice since I started this experiment, and I almost missed the second one. I was about to bust out the printlns and the debugger before I caught myself. Although it felt tedious, I opened up my document and wrote down what I did, what I expected to happen, and what actually happened. When I added that last part, it suddenly hit me what my mistake was. No debugging necessary! Apparently the very act of articulating the difference between my expectations and reality was sufficient for me to recognize the error in my thinking (and my coding).

Perhaps it was a fluke. Perhaps the reason would have come to me anyway. But I am now definitely motivated to continue this experiment.

# A Data Representation Language

I have an idea for a language, and I want to know if it already exists. The language is a data representation language. It encodes rules about how data is represented in a store (e.g. MySQL, HBase, Riak, Neo4J, MongoDB, Redis, flat files). The language would have four directives: `entity`, `predicate`, `operation`, and `realize`. The `entity` directive gives the “platonic” description of a type.

The `predicate` directive tells how these types are represented. For example, to represent the user object in a relational database:

or in a key value store:

You can also use predicates to specify how types are embodied in classes.

Notice that I left out `userName`; classes do not have to be perfectly aligned with the platonic entities. You can even combine different entities into a single class. For example, imagine a Java class like this:

Even though tasks and comments are separate entites, you can still map between them and the task class:

It’s a little crazy, but it could be made simpler with a library function and/or syntactic sugar saying “this embodied list matches this list of entites”. I just wanted to give you some idea of how flexible I want this language to be.

The `operation` directive gives names to operations that might be performed on the entities.

The `realize` directive indicates how operations will be realized using concrete classes.

Compiling would generate a code block for each `realize` directive. It would fail if any of the operations were impossible. (e.g. `getTasksForUser` would be impossible for a key-value store if you had stored only `Task => [User]` pairs and forgotten the `User => [Taks]` pairs. It would generate a warning if any of the operations were slow. (e.g. `getCommentsForTask` on an ordered key-value store when the comments were indexed by `commentId` and not by `\$taskId:\$commentId`)

So, does a language like this already exist? I know there are several things that come close, ORMs being the obvious example. Most ORMs require you to build schemas according to THEIR rules, not your own rules, and the exceptional ones require you to write custom code, usually 4 different times, for the get, set, update, and delete cases, when the representation is anything non-standard.

I want something that can handle

• multiple stores simultaneously, e.g. memcache and MySQL.
• denormalized data. e.g. if I have a User-to-Task and a Task-to-User representation of `UserTask` in a sharded database, the code generated for `createUserTask` should do two inserts.
• other really crazy representations, such as
• In a column family database, storing the first comment of a task in the `comment1` column of the row for that task, the second comment in the `comment2` column, etc.
• Putting a sentinel value in a redis list so I can tell the difference between an empty list and `unknown`.

Since it seems really useful, I would love to write this language, but honestly, I don’t even know where to begin. Conceptually, how do you translate quantified logic into imperative code? What would abstraction look like in this language? (e.g. Can I make a `listEqualsList` function?) Outside of the `entity`/`predicate`/`operation`/`realize` directives, what primitives would I need to provide so that other people can write modules for their favorite pet database?

# Symmetric Constraint Learning

Suppose I have the following graph:

And I’m trying to find a two-coloring for it. (i.e. I want to color each of the nodes black or white in such a way that directly connected nodes have opposite colors.) Obviously any realistic constraint solver is going to solve this problem in linear time, since any assignment causes a propagation to the rest of the graph. (e.g. `A` being black causes `B`, `C`, and `D` to be white which causes `E` to be black, `F` to be white, `G`, `H`, and `I` to be black, and `J` to be white.)

But suppose (since this is just an illustration) my constraint solver doesn’t maintain arc consistency, but it does do some kind of constraint learning. Also, suppose that I already know some of the symmetry in this problem. In particular, I know that `[A, B, C, D, E]` is symmetric with `[F, G, H, I, J]`. (The constraint solver doesn’t have to discover this symmetry; I know it in advance.)

The constraint solver might learn at some point that `A == E`, because it combines the constraint `A != B` with `B != E`. It would be a shame if the constraint solver later also learned that `F == J`. It would be nice if it could learn `F == J` at the same time that it learns `A == E`, since I have told it about the symmetry of the problem.

Notice that the learning is valuable even though the two halves of the problem have different assignments. (If `A` is black, then `F` is white.)

How can a constraint solver make these kind of inferences?

Here’s my current solution:

A constraint satisfaction problem is a collection of variables and constraints. We declare an ordered subset `X` of variables as isomorphic to a subset `Y` of variables if for every constraint involving only variables in X there is an identical constraint involving the corresponding variables in `Y`. (Constraints involving variables both in `X` and around `X` are not required to have a corresponding constraint.)

It follows that if `X` and `Y` are isomorphic, then their corresponding subsets must also be isomorphic.

Whenever a constraint solver learns a constraint, it can add all of the isomorphic constraints to its collection of learned constraints. There might even be a space optimization here, if I can find an appropriate lazy data structure, e.g. by allowing “abstract” constraints in the solver’s collection of learned constraints. The hard part is figuring out how to do watched literals.

Has this problem already been tackled?

# The Hundred-Year Function

What will programming languages look like one hundred years from now? Where will all of those wasted cycles end up going?

I think it is safe to say that the programming language of the future, if it exists at all, will involve some kind of artificial intelligence. This post is about why I think that theorem provers will be standard in languages of the future.

This simple function takes two arguments. The first is a predicate distinguishing between desirable (`True`) and undesirable (`False`) values for A. The second is a size restriction on A (e.g. number of bytes).

The function returns a random value of A, if one exists, meeting two constraints:

1. It satisfies the predicate.
2. It is no larger than the size constraint.

Also, the `solve` function is guaranteed to terminate whenever the predicate terminates.

First I will try to convince you that the `solve` function is more important than any of your petty opinions about syntax, object-orientation, type theory, or macros. After that I will make a fool of myself by explaining how to build the `solve` function with today’s technology.

## Why it matters

It can find fix-points:

It can invert functions:

It can solve Project Euler problems:

It can check that two functions are equal:

So it’s useful for detecting the introduction of bugs when you are optimizing things.

In fact, the solve function can find a more efficient implementation on your behalf.

The speed check is crude, but the idea is there.

Keeping the size constraint reasonable prevents the `solve` function from just creating a giant table mapping inputs to outputs.

Curry and Howard tell us that programs and proofs are one and the same thing. If our `solve` function can generate programs, then it can also generate mathematical proofs.

If the proof is ugly, we can decrease the search size, and we will get a more elegant proof.

The `solve` function can find bugs:

The `solve` function will never get people to stop arguing, but it will at least change the dynamic vs static types argument from a pragmatic one to an artistic one.

One last example:

Test-driven development advocates writing tests which are sufficient to construct the missing parts of a program. So why write the program at all?

In fact, unit_tests can be replaced with any assertion about the desired program: e.g. that it type checks under Hindley-Milner, that it terminates within a certain number of steps, that it does not deadlock within the first X cycles of the program’s execution, and so on.

Are you excited yet? Programming in the future is awesome!

## Implementation

Correct, but useless. If the predicate consisted of only one floating point operation, the Sequoia supercomputer would take 17 minutes to solve a mere 8 bytes.

The complexity of `solve` is clear. The variable `num` can be non-deterministically chosen from the range in linear time (`size * 8`), decode takes linear time, and predicate takes polynomial time in most of our examples from above. So `solve` is usually in NP, and no worse than NP-complete as long as our predicate is in P.

It’s a hard problem. Were you surprised? Or did you get suspicious when the programmers of the future started exemplifying godlike powers?1

Thankfully, a lot of work has been put into solving hard problems.

Today’s sat solvers can solve problems with 10 million variables. That’s 1.2 megabytes of search space, which is large enough for almost all of the examples above, if we’re clever enough. (The Kadane example is the definite exception, since the predicate takes superpolynomial time.)

The Cook-Levin theorem gives us a procedure for writing the `solve` function more efficiently.

1. Imagine a large number of processors, each with its own memory, lined up and connected so that the output state of each processor and memory becomes the input state of the next processor and memory. The state of the entire assembly is determined solely by the state of the first processor. The state of the whole system is static.
2. Represent each (unchanging) bit in the assembly with a boolean variable, and generate constraints on those variables by examining the logic gates connecting the bits.
3. Assign values to some of the variables in a way that corresponds to the first processor containing the machine code of the predicate.
4. Likewise, assign values so that the accumulator register of the last processor contains the value `True`.
5. Apply a sat solver to the variables and their constraints.
6. Extrapolate a solution by examining the first processor’s total state.

I call this approach “solving the interpreter trace” because the imaginary processors act as an interpreter for the predicate, and we ask the sat solver to trace out the processor execution.

The approach is elegant, but it has three major problems:

1. The formula given to the sat solver is enormous, even for small predicates and input sizes. (It’s polynomial, but the coefficient is large.)
2. The formula is highly symmetrical, which means the sat solver will perform a lot of redundant computation.
3. The meaning of bits in later processors is highly dependent on the value of bits in earlier processors (especially if the predicate starts off with a loop). This will force our sat solver to work a problem from beginning to end, even when a different order (such as end to beginning) would be more intelligent.

We can get rid of these problems if we compile our predicate directly into a boolean formula. Compilation is easy enough if our predicate contains neither loops nor conditionals.

becomes

Actually conditionals aren’t that hard either

becomes

A sat solver would immediately assign `w2` the value `0`. If we were solving over an interpretational trace, `w2` wouldn’t be a single variable, but would be one of two variables depending on whether `b` was `True` or `False`.

By compiling the predicate, we have enabled the solver to work from end to beginning (if it so chooses).

Can we handle loops?

One approach is to unroll the loop a finite number of times.

With branching and conditionals, we are turing complete. Function calls can be in-lined up until recursion. Tail recursive calls can be changed to while loops, and the rest can be reified as loops around stack objects with explicit push and pop operations. These stack objects will introduce symmetry into our sat formulas, but at least it will be contained.

When solving, we assume the loops make very few iterations, and increase our unroll depth as that assumption is violated. The solver might then look something like this:

`max_unroll_count` does static analysis to figure out the maximum number of unrolls that are needed. The number of unrolls will either be a constant (and so can be found out by doing constant reduction within the predicate), or it will somehow depend on the size of the predicate argument (and so an upper bound can be found by doing inference on the predicate).

The solver is biased toward finding solutions that use fewer loop iterations, since each loop iteration sets another boolean variable to `1`, and thus cuts the solution space down by half. If the solver finds a solution, then we return it. If not, then we try again, this time allowing `_longer_loop_needed` to be true. If it still can’t find a solution, then we know no solution exists, since `i` and `j` were set to arbitrary values. By “arbitrary”, I mean that, at compilation time, no constraints will connect the later usages of `i` and `j` (there are none in this example) with the earlier usages.

I admit that this approach is ugly, but the alternative, solving an interpreter trace, is even more expensive. The hacks are worth it, at least until somebody proves P == NP.

Some of the examples I gave in the first section used eval. Partial evaluation techniques can be used to make these examples more tractable.

I’ve only talked about sat solvers. You can probably get better results with an smt solver or a domain-specific constraint solver.

In thinking about this problem, I’ve realized that there are several parallels between compilers and sat solvers. Constant reduction in a compiler does the same work as the unit clause heuristic in a sat solver. Dead code removal corresponds to early termination. Partial evaluation reduces the need for symmetry breaking. Memoization corresponds to clause learning. Is there a name for this correspondance? Do compilers have an analogue for the pure symbol heuristic? Do sat solvers have an analogue for attribute grammars?

## Today

If you want to use languages which are on the evolutionary path toward the language of the future, you should consider C# 4.0, since it is the only mainstream language I know of that comes with a built-in theorem prover.

Update (2013-11-24):

I am happy to report that I am not alone in having these ideas. “Search-assisted programming”, “solver aided languages”, “computer augmented programming”, and “satisfiability based inductive program synthesis” are some of the names used to describe these techniques. Emily Torlak has developed an exciting language called Rosette, which is a dsl for creating solver aided languages. Ras Bodik has also done much work combining constraint solvers and programming languages. The ExCAPE project focuses on program synthesis. Thanks to Jimmy Koppel for letting me know these people exist.

1: Even many computer scientists do not seem to appreciate how different the world would be if we could solve NP-complete problems efficiently. I have heard it said, with a straight face, that a proof of P = NP would be important because it would let airlines schedule their flights better, or shipping companies pack more boxes in their trucks! One person who did understand was Gödel. In his celebrated 1956 letter to von Neumann, in which he first raised the P versus NP question, Gödel says that a linear or quadratic-time procedure for what we now call NP-complete problems would have “consequences of the greatest magnitude.” For such a procedure “would clearly indicate that, despite the unsolvability of the Entscheidungsproblem, the mental effort of the mathematician in the case of yes-or-no questions could be completely replaced by machines.” But it would indicate even more. If such a procedure existed, then we could quickly find the smallest Boolean circuits that output (say) a table of historical stock market data, or the human genome, or the complete works of Shakespeare. It seems entirely conceivable that, by analyzing these circuits, we could make an easy fortune on Wall Street, or retrace evolution, or even generate Shakespeare’s 38th play. For broadly speaking, that which we can compress we can understand, and that which we can understand we can predict. — Scott Aaronson