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

5. Tweety can fly, and
6. 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?

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:

1
2
3
4
5
6
7
8
9
10
11

type MultiSet = Map String Nat

-- | grandTotal counts the number of elements in each set and adds them
grandTotal :: MultiSet -> MultiSet -> Nat
grandTotal xs ys = fold (+) 0 (merge xs ys) where

-- Imported:
fold :: (Nat -> Nat -> Nat) -> Nat -> MultiSet -> Nat
(+) :: Nat -> Nat -> Nat
0 :: Nat
merge :: MultiSet -> MultiSet -> MultiSet

After static differentiation, the code becomes:¹

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

-- The derivative of a natural number is an integer, since
-- the natural number can either increase or decrease.
type Nat' = Int

type MultiSet' = Map String Nat'

grandTotal' :: MultiSet -> MultiSet' -> MultiSet -> MultiSet' -> Nat'
grandTotal' xs xs' ys ys' =
  fold' (+) (+') 0 (derive 0) (merge xs ys) (merge' xs dxs ys dys) where

-- Imported:
fold' :: (Nat -> Nat -> Nat)
      -> (Nat -> Nat' -> Nat -> Nat' -> Nat')
      -> Nat -> Nat'
      -> MultiSet -> MultiSet'
      -> Nat'
(+) :: Nat -> Nat -> Nat
(+') :: Nat -> Nat' -> Nat -> Nat' -> Nat'
0 :: Nat
derive :: Nat -> Nat'
merge :: MultiSet -> MultiSet -> MultiSet
merge' :: MultiSet -> MultiSet' -> MultiSet -> MultiSet' -> MultiSet

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

1
2
3
4
5
6
7
8

grandTotal' :: MultiSet' -> MultiSet' -> Int
grandTotal' xs' ys' = fold' (+) 0 (merge' xs' ys')

-- Imported:
fold' :: (Int -> Int -> Int) -> Int -> MultiSet' -> Int
(+) :: Int -> Int -> Int
0 :: Int
merge' :: MultiSet' -> MultiSet' -> MultiSet'

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:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

module Differentiate where

type Id = String

data Term p
  = Primitive p
  | Lambda Id (Term p)
  | App (Term p) (Term p)
  | Var Id
  deriving (Eq, Ord, Read, Show)

differentiate :: MonadId m => (p -> m (Term p)) -> Term p -> m (Term p)
differentiate differentiatePrimitive = diff where
  diff term =
    case term of
      Primitive p -> differentiatePrimitive p

      Lambda var term -> do
        let dvar = "d" ++ var
        rememberId var var $ generateId dvar $ \var' -> do
          term' <- rememberId dvar var' $ diff term
          return (Lambda var (Lambda var' term'))

      App s t -> do
        s' <- diff s

        -- t and t' will often share common sub-expressions.
        -- A better implementation would factor their commonalities out,
        -- to avoid redundant computation at runtime.
        t' <- diff t

        return (App (App s' t) t')

      Var var -> do
        var' <- recallId var
        return (Var var')

class Monad m => MonadId m where
  -- Return a unique string that starts with the given string.
  generateId :: String -> (String -> m a) -> m a
  -- Add mapping from old variable name to new variable name
  rememberId :: String -> String -> m a -> m a
  -- Lookup the new variable name that was mapped to the given old variable name.
  recallId :: String -> m String

Returning to an example from the first post:

1
2
3
4
5
6
7
8

userIds :: RedisSet
userIds = setToRedisSet (mapProjection userId (dbTableToSet usersTable))

setToRedisSet :: Set Id -> RedisSet
mapProjection :: (User -> Id) -> Set User -> Set Id
userId :: User -> Id
dbTableToSet :: DbTable User -> Set User
usersTable :: DbTable User

The derivative is

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

userIds' :: RedisSet'
userIds' = setToRedisSet' (mapProjection userId (dbTableToSet usersTable)) (mapProjection' userId userId' (dbTableToSet usersTable) (dbTableToSet' usersTable usersTable'))

setToRedisSet' :: Set Id -> Set' Id Id' -> RedisSet'

mapProjection  :: (User -> Id) ->                           Set User ->                    Set Id
mapProjection' :: (User -> Id) -> (User -> User' -> Id') -> Set User -> Set' User User' -> Set' Id Id'

userId  :: User ->          Id
userId' :: User -> User' -> Id'

dbTableToSet  :: DbTable User ->                        Set User
dbTableToSet' :: DbTable User -> DbTable' User User' -> Set' User User'

usersTable  :: DbTable User
usersTable' :: DbTable' User User'

data RedisSet' = SAdd String | ...
data DbTable' a a' = Insert a | ...

In the case of an insert, we have

1

usersTable' = Insert user

which means that userIds' can be reduced to

1
2

userIds' :: RedisSet'
userIds' = SAdd (userId user)

¹: 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.

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 IORefs 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

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.

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.

1

type Set a = Data.Set.Set

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.

1

data List a b = (Ord b) => List (a -> b) (Set a)

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.

1

data LimitedList a b = (Ord b) => LimitedList Integer (List a b)

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 LimitedLists whose upper bound is 1. Making specialized types for singleton LimitedLists makes working with non-collection redis data structures easier.

1
2

data First a b = (Ord b) => First (a -> b) (Maybe a)
data Last  a b = (Ord b) => Last  (a -> b) (Maybe a)

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.

1

data Maybe a = Nothing | Just a

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

1
2
3
4
5

instance Monoid Maybe where
  Nothing  `mappend` Nothing  = Nothing
  Nothing  `mappend` (Just x) = Just x
  (Just x) `mappend` Nothing  = Just x
  (Just x) `mappend` (Just y) = error "This should never happen."

Collision of Justs 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.

1
2
3
4

data Sum = Sum Integer

instance Monoid Sum where
  mappend = (+)

Query operations

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

-- QO = Query Operation
data QO input output where
  -- The operations Where, Count, Sum, The, and SortBy are not concerned with the ordering
  -- of their input, so they can work on Sets, Lists, LimitedLists, Firsts, Lasts,
  -- and Maybes. In these constructor definitions, 'coll' can mean any of those types.
  -- A real implementation might have multiples versions of these query operations,
  --   e.g. WhereSet, WhereList, WhereLimitedList, ..., CountSet, CountList, etc.
  Where :: Expr (a -> Boolean) -> QO (coll a)       (coll a)
  Count ::                        QO (coll a)       Sum
  Sum   ::                        QO (coll Integer) Sum

  -- 'The' takes a collection which is expected to have no more than one element
  -- and extracts the element.
  The   :: QO (coll a) (Maybe a)

  -- SortBy converts any kind of collection into a List.
  SortBy :: (Ord b) => Expr (a -> b) -> QO (coll a) (List a)

  -- Limit, First, and Last, are defined for any (seq)uence:
  --   Lists, LimitedLists, Firsts, and Lasts.
  Limit :: Integer -> QO (seq a) (LimitedList a)
  First ::            QO (seq a) (First a)
  Last  ::            QO (seq a) (Last a)

  -- Mapping only works on Set!
  Select :: Expr (a -> b) -> QO (Set a) (Set b)

  -- Well technically Select also works on Maybe, but we'll make a separate
  -- query operation for Maybes.
  Apply :: Expr (a -> b) -> QO (Maybe a) (Maybe b)

  -- Lists contain their sorting function, so we cannot allow arbitrary
  -- mapping on lists. We can, however, support monotonic mappings.
  SelectMonotonic        :: Expr (a -> b)          -> QO (seq a) (seq b)

  -- Mappings which scramble the order are also allowed, as long as we
  -- have a way to recover the order. i.e. 'a -> c' has to be monotonic,
  -- even though 'a -> b' and 'b -> c' do not.
  SelectReversible       :: Expr (a -> b) -> Expr (b -> c) -> QO (seq a) (seq b)

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14

data Table t = Table String

-- A Query is a sequence of query operations that begins with a table
data Query output where
  From :: Table t -> Query (Set t)
  Compose :: Query input -> QO input output -> Query output

-- convenience constructor
(+>) = Compose

data CacheKeyDefinition = CacheKeyDefinition {
  keyTemplate :: String, -- e.g. "taskIds.{userId}"
  query :: Query -- e.g. from tasks where task.userId = userId select task.id
}

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

type TaskId = String
type UserId = String

data Task = {
    taskId :: TaskId,
    ownerId :: UserId,
    title :: String,
    completed :: Boolean,
    dueDate :: Integer }
 deriving (Eq, Ord, Read, Show)

taskTable = Table "tasks" :: Table Task

schema = do
  -- The task objects.
  -- type: String
  -- expected redis commands on insert:
  --   SET
  "task.{taskId}" $= \tid ->
    From taskTable +>
    Where (\t -> taskId t == tid) +>
    The +>
    Apply show

  -- For each user, the ids of her most urgent tasks.
  -- type: Sorted Set, where the keys are the dueDate and the values are the taskIds.
  -- expected redis commands on insert:
  --   ZADD
  --   ZREMRANGEBYRANK
  "activeTaskIds.{userId}" $= \uid ->
    From taskTable +>
    Where (\t -> ownerId t == uid && not (completed t)) +>
    SortBy dueDate +>
    Limit 100 +>
    SelectReversible (\t -> (dueDate t, taskId t)) fst

  -- The number of tasks a user has successfully completed.
  -- type: integer
  -- expected redis commands on insert:
  --   INCR
  "numCompleted.{userId}" $= \uid ->
    From taskTable +>
    Where (\t -> ownerId t == uid && completed t) +>
    Count

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.

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:

1
2
3
4
5

numUsers = count users
numUsers_new = count (users ++ [user])
numUsers_new = count users + count [user]
numUsers_new = numUsers + 1
-- INCR numUsers

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.

1
2
3
4
5
6

userIds = map userId users
userIds_new = map userId (users ++ [user])
userIds_new = map userId users ++ map userId [user]
userIds_new = userIds ++ map userId [user]
userIds_new = userIds ++ [user.userId]
-- SADD userIds 65495

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

Filtering is also straightforward.

1
2
3
4
5
6
7
8
9
10
11
12

activeUserIds = map userId (filter (\x -> x.status == ACTIVE) users)
activeUserIds_new = map userId (filter (\x -> x.status == ACTIVE) $
  (users ++
  [user]))
activeUserIds_new = map userId (
  filter (\x -> x.status == ACTIVE) users ++
  filter (\x -> x.status == ACTIVE) [user])
activeUserIds_new =
  map userId (filter (\x -> x.status == ACTIVE) users) ++
  map userId (filter (\x -> x.status == ACTIVE) [user])
activeUserIds_new = activeUserIds ++ map userId (filter (\x -> x.status == ACTIVE) [user])
-- SADD activeUserIds 65495

Obviously a pipeline of SADDs 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.

1
2

activeUserIds = (map userId . filter (\x -> x.status == ACTIVE)) users
activeUserIds_new = activeUserIds ++ (map userId . filter (\x -> x.status == ACTIVE)) [user]

In general, it seems that queries of the form

1

values = (f . g . h {- ... -}) entities

become

1

values_new = values `mappend` (f . g . h {- ... -}) [entity]

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.

1

taskIds_'userId' = (map taskId . filter (\t -> t.owner == userId)) tasks

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

1

taskIds :: UserId -> [TaskId]

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.

1
2

taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId . filter (\t -> t.owner == userId)) [task]

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).

1
2
3
4
5
6
7
8
9
10
11
12

taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId . filter (\t -> t.owner == userId)) [task]
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (filter (\t -> t.owner == userId) [task]))
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (if (\t -> t.owner == userId) task then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) []))
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (if task.owner == userId then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) []))

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:

1
2
3
4
5
6
7
8
9
10
11
12
13

taskIds_65495_new = taskIds_65495 ++ (map taskId $
  if 65495 == 65495 then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) [])
taskIds_65495_new = taskIds_65495 ++ (map taskId $
  if true then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) [])
taskIds_65495_new = taskIds_65495 ++ (map taskId $
  task : filter (\t -> t.owner == userId) [])
taskIds_65495_new = taskIds_65495 ++ (map taskId [task])
taskIds_65495_new = taskIds_65495 ++ task.id
-- SADD taskIds_65495 ${task.id}

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

1
2
3
4
5
6
7
8
9
10

taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (if false then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) []))
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (filter (\t -> t.owner == userId) []))
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId [])
taskIds_'userId'_new = taskIds_'userId' ++ []
-- nothing to do

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.

1

taskIds_'userId' = (map taskId . (filter (\t -> t.owner != userId))) tasks

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.

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.

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.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

entity User
  Id id
  String userName
  String displayName

entity Task
  Id id
  String name
  Date dueDate

entity UserTask // encodes many-to-many relationship
  Id id
  User user
  Task task

entity Comment
  Id id
  Task parentTask
  String comment
  Date when

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

1
2
3
4
5
6
7

import RDBMS

predicate forall u: User exists r: RelationalRow where
  r.table = 'User' and
  r['id'] = u.id and
  r['userName'] = u.userName and
  r['displayName'] = u.displayName

or in a key value store:

1
2
3
4
5
6
7
8

import KeyValue
import Pickle

predicate forall u: User exists p: KeyValuePair where
  p.key = "User." + u.id.toString() and
  p.value : Pickled<Map<String,String>> and
  p.value['userName'] = u.userName and
  p.value['displayName'] = u.displayName

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

1
2
3
4

predicate forall u: User exists o: Object where
  o.class = 'org.example.myapp.objects.User' and
  o['id'] = u.id and
  o['displayName'] = u.displayName

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:

1
2
3
4
5
6

public class Task {
  public long id;
  public String name;
  public Date dueDate;
  public List<Comment> comments;
}

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

predicate forall t: Task exists o: Object where
  o.class = 'org.example.myapp.objects.Task' and
  o['id'] = t.id and
  o['name'] = t.name and
  o['dueDate'] = dueDate and
  o['comments'] : List and
  o `sortedBy` (c => c['when']) and
  forall c: Comment (c.parentTask = t =>
    exists co: Object where
    co `in` o['comments'] and
    co.class = 'org.example.myapp.objects.Comment' and
    co['id'] = c.id and
    co['when'] = c.when
    co['comment'] = c.comment) and
  forall co: Object (co `in` o['comments'] =>
    exists c: Comment where
    c.parentTask = t and
    c.id = co['id'])

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.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

operation createUser(userName: in String, displayName: in String) where
  exists u: User and
  u.userName = userName and
  u.displayName = displayName and
  u.id `notIn` Before.User and
  After.User = Before.User + u

operation getTasksForUser(userId: in Id, tasks: out Set<Task>) where
  exists u: User where u.id = userId => (
  forall t: Task (exists ut: UserTask where
      ut.user = u and
      ut.task = t =>
    ut.task `in` tasks) and
  forall t: Task (t `in` tasks =>
    exists ut: User where ut.user = u and ut.task = t))

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

1
2
3
4
5

realize createUser as
  void createUser(userName: java.lang.String, displayName: java.lang.String)

realize getTasksForUser as
  java.util.Set<org.example.myapp.objects.Task> getTasksForUser(u: org.example.myapp.objects.User)

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?

Suppose I have the following graph:

1
2
3
4
5

  /- B -\        /- G -\
 /       \      /       \
A -- C -- E -- F -- H -- J
 \       /      \       /
  \- D -/        \- I -/

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?

Original post: https://www.reddit.com/r/artificial/comments/18rttb/symmetric_constraint_learning/

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.

1

solve :: (a -> Bool) -> Size -> Random (Maybe a)

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:

1
2
3
4
5
6
7

def c2f(temp):
  return temp * 9.0 / 5 + 32

def is_fixpoint(temp):
  return temp == c2f(temp)

print solve(is_fixpoint, 8) # outputs -40.0

It can invert functions:

1
2
3
4

def f2c(temp):
  return (temp - 32) * 5 / 9.0

print solve(lambda fahr: 37.0 == f2c(fahr), 8) # 100.0 IS hot!

It can solve Project Euler problems:

1
2
3
4
5
6
7
8
9
10

def is_pythagorean_triple(a, b, c):
  return a*a + b*b == c*c

def is_solution(triple):
  if len(triple) != 3: return False
  if sum(triple) != 1000: return False
  if !is_pythagorean_triple(*triple): return False
  return True

print solve(is_solution, 12)

It can check that two functions are equal:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

def the_obvious_max_subarray(A):
  answer = 0
  for start in range(0, len(A) - 1):
    for end in range(start + 1, len(A)):
      answer = max(answer, sum(A[start:end]))
  return answer

def the_fast_max_subarray(A):
  max_ending_here = max_so_far = 0
  for x in A:
    max_ending_here = max(x, max_ending_here + x)
    max_so_far = max(max_so_far, max_ending_here)
  return max_so_far

def differentiates(input):
  return the_obvious_max_subarray(input) != the_fast_max_subarray(input)

# Prints None if the two functions are equal for all
#   input sequences of length 5 and smaller.
# Otherwise prints a counter-example.
print solve(differentiates, 4 * 5)

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.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

def steps(algorithm, input):
  (_result, steps) = eval_with_steps(algorithm, input)
  return steps

def is_fast_max_subarray(algorithm):
  # Check that algorithm is equivalent to the_obvious_max_subarray
  if solve(lambda input: the_obvious_max_subarray(input) != eval(algorithm, input), 4 * 5):
    return False
  # Check that algorithm is faster than the_obvious_max_subarray
  for example in example_inputs:
    if steps(algorithm, input) > steps(the_obvious_max_subarray, input):
      return False
  return True

print solve(is_fast_max_subarray, 1000) # prints a function definition

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.

1
2
3
4
5
6
7
8
9
10
11

goldbach = parse("forall a > 2: exists b c: even(a) => prime(b) && prime(c) && b + c == a")

def proves_goldbach(proof):
  if proof[-1] != goldbach:
    return False
  for step in range(0, len(proof) - 1):
    if not proof[step].follows_from(proof[0:step]):
      return False
  return True

print solve(proves_goldbach, 10000)

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:

1
2
3
4
5

def does_not_go_wrong(input):
  result = eval(my_program, input)
  return not is_uncaught_exception(result)

print solve(does_not_go_wrong, 10000)

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?

1
2
3
4
5
6
7
8

def passes_tests(patches):
  return unit_tests.pass(partial_program.with(patches))

patches = solve(passes_tests, 10000)
if patches:
  print partial_program.with(patches)
else
  print "Tests not passable within search space"

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

Always start with the obvious approach:

1
2
3
4
5

def solve(predicate, size):
  for num in range(0, 2 ^ (size * 8) - 1):
    val = decode(num)
    if predicate(val):
      return val

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?¹

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.

1
2
3
4
5
6

def isReadableAndWriteable(x):
  y = x & 4
  z = x & 2
  a = y == 4
  b = z == 2
  return a && b

becomes

1
2
3
4
5

(y0 == x0 & 0) & (y1 == x1 & 0) & (y2 == x2 & 1) &
(z0 == x0 & 0) & (z1 == x1 & 1) & (z2 == x2 & 0) &
(a == ((y0 == 0) & (y1 == 0) & (y2 == 1)) &
(b == ((z0 == 0) & (z1 == 1) & (z2 == 0)) &
a && b

Actually conditionals aren’t that hard either

1
2
3
4
5
6
7
8

def predicate(x):
  b = isEven(x)
  if b:
    w = x & 7
  else:
    z = x & 2
    w = z << 1
  return w < 3

becomes

1
2
3
4
5

(b == (x0 == 0)) &
(b -> ((w0 == (x0 & 1)) & (w1 == (x1 & 1)) & (w2 == (x2 & 1)))) &
(~b -> ((z0 == (x0 & 0)) & (z1 == (x1 & 1)) & (z2 == (x2 & 0)))) &
(~b -> ((w0 == 0) & (w1 == z0) & (w2 == z1))) &
(w2 == 0 & (w1 == 0 | w0 == 0))

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?

1
2
3
4
5
6
7
8

def is_palindrome(str):
  i = 0
  j = len(str) - 1
  while i < j:
    if str[i] != str[j]: return False
    i += 1
    j -= 1
  return True

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

def is_palindrome(str):
  i = 0
  j = len(str) - 1
  if i < j:
    if str[i] != str[j]: return False
    i += 1
    j -= 1
    if i < j:
      if str[i] != str[j]: return False
      i += 1
      j -= 1
      if i < j:
        if str[i] != str[j]: return False
        i += 1
        j -= 1
        if i < j:
          _longer_loop_needed = True
          i = arbitrary_value() # in case rest of function depends on i or j
          j = arbitrary_value() # (It doesn't in this example.)
  return True

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:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

def solve(predicate, size):
  unroll_count = 1
  sat_solver = SatSolver()
  limit = max_unroll_count(predicate, size)
  while True:
    unrolled = unroll_loop(predicate, unroll_count)
    formula = compile(unrolled)
    sat_solver.push(formula)
    sat_solver.push("_longer_loop_needed == 0")
    sol = sat_solver.solve()
    if sol: return sol
    sat_solver.pop()
    sol = sat_solver.solve()
    if sol == None: return None # even unrolling more iterations won't help us
    sat_solver.pop()
    if unroll_count == limit: return None
    unroll_count = min(unroll_count * 2, limit)

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.

¹: 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 Gödel. In his celebrated 1956 letter to von Neumann, in which he first raised the P versus NP question, Gö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