AI Planning for Program Synthesis

Nota: Este post está en inglés, ya que es mi intención compartirlo en un curso sobre Planificación que estuve realizando, como parte de su evaluación.

Since January 13th, I had the opportunity to refresh and deepen my knowledge of Artificial Intelligence Planning, with an awesome course from The University of Edinburgh, through Coursera, by professors Austin Tate and Gerhard Wickler.

Edinburgh's: Artificial Intelligence Planning

Austin Tate and Gerhard Wickler

Coursera

It is now coming to an end, haven proved to be a challenging and fun experience. I particularly enjoyed implementing my own graphplan planner, albeit without mutex verifications. Other programming assignments were actually quite easy if one used Prolog, but none the less very fun!

One of the assignments (the Creative Challenge) was to come up with some application that benefits from planning techniques, or o particular technology for planning. I decided to take the first option and attempt to make a link between planning and my own work. I am currently working on formal semantics and program verification techniques.

A plan can be viewed as a sequence (or possibly a directed acyclic graph) of steps that takes an environment in a given initial state and transforms it in a way that it ends in a given final state. A program is actually a very similar concept. A program, particularly in imperative languages, is a series of steps needed to take a given input and produce a desired output. This input and output can be expressed in terms of conditions that express what things are true at the start and end of a program respectively. This precondition and postcondition together form the specification or contract for the program.

What if you only had the contract but not the program that implements it? A POP planner could be used to take the contract and expand it into several, more simple, tasks. A plan in which all steps are known to have a direct implementation would be the desired program (one that actually implements the proposed contract). A possible way of expanding tasks into simpler subtasks could be through Morgan & Vicker's refinement calculus. This planner would actually be like an automatization of the refinement process they proposed.

And maybe we could think of a crossover in the other direction. Some planning problems, as well as programs, are limited by resources. These resources might be spatial, temporal, for energy, etc. The logic of bunched implications of O'Hearn and Pym presents a framework for specifying resource dependant reasoning. Particularly, Reynold's separation logic allows reasoning with limited resources and exclusive ownership (mainly memory, but other applications are possible). This kind of reasoning could be exported to planners in order to treat with their own resource constraints. Separation logic has a very nice frame axiom that allows local reasoning, and fits perfectly with the analogous notion of a frame in knowledge representation. I have not found any reference for such a crossover, but I think it could definitely be investigated further.

And this was my small contribution and submission to the creative challenge. Thank you very much for reading! Hope you liked it. :)