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
the initial state of the world
the preconditions under which an action can be taken, and
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
All birds fly
Tweety is a bird
All broken-winged creatures cannot fly, and
Tweety has a broken wing
can prove both
Tweety can fly, and
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:
1234567891011
typeMultiSet=MapStringNat-- | grandTotal counts the number of elements in each set and adds themgrandTotal::MultiSet->MultiSet->NatgrandTotalxsys=fold(+)0(mergexsys)where-- Imported:fold::(Nat->Nat->Nat)->Nat->MultiSet->Nat(+)::Nat->Nat->Nat0::Natmerge::MultiSet->MultiSet->MultiSet
-- The derivative of a natural number is an integer, since-- the natural number can either increase or decrease.typeNat'=InttypeMultiSet'=MapStringNat'grandTotal'::MultiSet->MultiSet'->MultiSet->MultiSet'->Nat'grandTotal'xsxs'ysys'=fold'(+)(+') 0 (derive 0) (merge xs ys) (merge'xsdxsysdys)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::Natderive::Nat->Nat'merge::MultiSet->MultiSet->MultiSetmerge'::MultiSet->MultiSet'->MultiSet->MultiSet'->MultiSet
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:
moduleDifferentiatewheretypeId=StringdataTermp=Primitivep|LambdaId(Termp)|App(Termp)(Termp)|VarIdderiving(Eq,Ord,Read,Show)differentiate::MonadIdm=>(p->m(Termp))->Termp->m(Termp)differentiatedifferentiatePrimitive=diffwherediffterm=casetermofPrimitivep->differentiatePrimitivepLambdavarterm->doletdvar="d"++varrememberIdvarvar$generateIddvar$\var'->doterm'<-rememberIddvarvar'$difftermreturn(Lambdavar(Lambdavar'term'))Appst->dos'<-diffs-- t and t' will often share common sub-expressions.-- A better implementation would factor their commonalities out,-- to avoid redundant computation at runtime.t'<-difftreturn(App(Apps't)t')Varvar->dovar'<-recallIdvarreturn(Varvar')classMonadm=>MonadIdmwhere-- Return a unique string that starts with the given string.generateId::String->(String->ma)->ma-- Add mapping from old variable name to new variable namerememberId::String->String->ma->ma-- Lookup the new variable name that was mapped to the given old variable name.recallId::String->mString
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.
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).
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
typeSeta=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
dataListab=(Ordb)=>List(a->b)(Seta)
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 LimitedLists 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.
1
dataMaybea=Nothing|Justa
The monoidal operation is to pick Just over Nothing, but with the restriction
that both arguments cannot be Justs.
12345
instanceMonoidMaybewhereNothing`mappend`Nothing=NothingNothing`mappend`(Justx)=Justx(Justx)`mappend`Nothing=Justx(Justx)`mappend`(Justy)=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.
-- QO = Query OperationdataQOinputoutputwhere-- 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(colla)(colla)Count::QO(colla)SumSum::QO(collInteger)Sum-- 'The' takes a collection which is expected to have no more than one element-- and extracts the element.The::QO(colla)(Maybea)-- SortBy converts any kind of collection into a List.SortBy::(Ordb)=>Expr(a->b)->QO(colla)(Lista)-- Limit, First, and Last, are defined for any (seq)uence:-- Lists, LimitedLists, Firsts, and Lasts.Limit::Integer->QO(seqa)(LimitedLista)First::QO(seqa)(Firsta)Last::QO(seqa)(Lasta)-- Mapping only works on Set!Select::Expr(a->b)->QO(Seta)(Setb)-- Well technically Select also works on Maybe, but we'll make a separate-- query operation for Maybes.Apply::Expr(a->b)->QO(Maybea)(Maybeb)-- Lists contain their sorting function, so we cannot allow arbitrary-- mapping on lists. We can, however, support monotonic mappings.SelectMonotonic::Expr(a->b)->QO(seqa)(seqb)-- 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(seqa)(seqb)
A few more data structures and we will have all the pieces necessary for
an application developer to define a cache schema.
1234567891011121314
dataTablet=TableString-- A Query is a sequence of query operations that begins with a tabledataQueryoutputwhereFrom::Tablet->Query(Sett)Compose::Queryinput->QOinputoutput->Queryoutput-- convenience constructor(+>)=ComposedataCacheKeyDefinition=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.
typeTaskId=StringtypeUserId=StringdataTask={taskId::TaskId,ownerId::UserId,title::String,completed::Boolean,dueDate::Integer}deriving(Eq,Ord,Read,Show)taskTable=Table"tasks"::TableTaskschema=do-- The task objects.-- type: String-- expected redis commands on insert:-- SET"task.{taskId}"$=\tid->FromtaskTable+>Where(\t->taskIdt==tid)+>The+>Applyshow-- 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->FromtaskTable+>Where(\t->ownerIdt==uid&¬(completedt))+>SortBydueDate+>Limit100+>SelectReversible(\t->(dueDatet,taskIdt))fst-- The number of tasks a user has successfully completed.-- type: integer-- expected redis commands on insert:-- INCR"numCompleted.{userId}"$=\uid->FromtaskTable+>Where(\t->ownerIdt==uid&&completedt)+>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:
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.
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:
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.
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).
In the false case, userId remains unbound, but that’s ok, because the expression reduces to a no-op:
12345678910
taskIds_'userId'_new=taskIds_'userId'++(maptaskId(iffalsethentask:filter(\t->t.owner==userId)[]elsefilter(\t->t.owner==userId)[]))taskIds_'userId'_new=taskIds_'userId'++(maptaskId(filter(\t->t.owner==userId)[]))taskIds_'userId'_new=taskIds_'userId'++(maptaskId[])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.
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:
Debugging
Writing code
Helping other people
Learning and evaluating libraries, frameworks, and tools
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:
Using languages that have very strong type systems (e.g. haskell)
Using smart editors (e.g. IntelliJ) that give me immediate feedback when I make mistakes
Writing code in short, quick iterations instead of large batches
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.
1234567891011121314151617181920
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:
1234567
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:
12345678
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.
1234
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:
123456
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:
123456789101112131415161718
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.
123456789101112131415
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.
12345
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?
/- 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.
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.
The hundred year function
1
solve::(a->Bool)->Size->Random(Maybea)
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:
It satisfies the predicate.
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:
“Put down fahrenheit,” said the explorer. “I don’t expect it to matter.”
defthe_obvious_max_subarray(A):answer=0forstartinrange(0,len(A)-1):forendinrange(start+1,len(A)):answer=max(answer,sum(A[start:end]))returnanswerdefthe_fast_max_subarray(A):max_ending_here=max_so_far=0forxinA:max_ending_here=max(x,max_ending_here+x)max_so_far=max(max_so_far,max_ending_here)returnmax_so_fardefdifferentiates(input):returnthe_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.printsolve(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.
My computer is smarter than Kadane, if you’ll just be patient.
123456789101112131415
defsteps(algorithm,input):(_result,steps)=eval_with_steps(algorithm,input)returnstepsdefis_fast_max_subarray(algorithm):# Check that algorithm is equivalent to the_obvious_max_subarrayifsolve(lambdainput:the_obvious_max_subarray(input)!=eval(algorithm,input),4*5):returnFalse# Check that algorithm is faster than the_obvious_max_subarrayforexampleinexample_inputs:ifsteps(algorithm,input)>steps(the_obvious_max_subarray,input):returnFalsereturnTrueprintsolve(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.
Ten years too late for Uncle Petros
1234567891011
goldbach=parse("forall a > 2: exists b c: even(a) => prime(b) && prime(c) && b + c == a")defproves_goldbach(proof):ifproof[-1]!=goldbach:returnFalseforstepinrange(0,len(proof)-1):ifnotproof[step].follows_from(proof[0:step]):returnFalsereturnTrueprintsolve(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 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?
Beck’s revenge
12345678
defpasses_tests(patches):returnunit_tests.pass(partial_program.with(patches))patches=solve(passes_tests,10000)ifpatches:printpartial_program.with(patches)elseprint"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!
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.
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.
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.
Assign values to some of the variables in a way that corresponds to the first processor containing
the machine code of the predicate.
Likewise, assign values so that the accumulator register of the last processor contains the value True.
Apply a sat solver to the variables and their constraints.
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:
The formula given to the sat solver is enormous, even for small predicates and input sizes. (It’s
polynomial, but the coefficient is large.)
The formula is highly symmetrical, which means the sat solver will perform a lot of redundant computation.
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.
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).
One approach is to unroll the loop a finite number of times.
A six is a six is a six is a
1234567891011121314151617181920
defis_palindrome(str):i=0j=len(str)-1ifi<j:ifstr[i]!=str[j]:returnFalsei+=1j-=1ifi<j:ifstr[i]!=str[j]:returnFalsei+=1j-=1ifi<j:ifstr[i]!=str[j]:returnFalsei+=1j-=1ifi<j:_longer_loop_needed=Truei=arbitrary_value()# in case rest of function depends on i or jj=arbitrary_value()# (It doesn't in this example.)returnTrue
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:
Solver for a predicate with one loop
1234567891011121314151617
defsolve(predicate,size):unroll_count=1sat_solver=SatSolver()limit=max_unroll_count(predicate,size)whileTrue:unrolled=unroll_loop(predicate,unroll_count)formula=compile(unrolled)sat_solver.push(formula)sat_solver.push("_longer_loop_needed == 0")sol=sat_solver.solve()ifsol:returnsolsat_solver.pop()sol=sat_solver.solve()ifsol==None:returnNone# even unrolling more iterations won't help ussat_solver.pop()ifunroll_count==limit:returnNoneunroll_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.
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 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