03.28.2019 Pac-Man Specification and Synthesis Milestone Report

This demo shows generalized loop inference. In the Pac-man animation system, a palette is a collection of four color id's. A color id is a 4 bit integer that maps to an 8 bit RGB color (as shown in a prior demo), and a palette is identified by a 5-bit palette id. In this demo, a palette id 0-31 is selected by the user in the bottom right bits (which invokes the program) and four RGB display pixels are colored with the four colors of the palette. The construction of the program involves synthesizing a loop over the inner colorIdToRgbColor function, by applying rules to the type-graph. The yellow-red-blue pallete contains the yellow of pac-man himself!

Loop Inference and the AST. The previous version of the path-compiler had an implementation of loop inference and synthesis that was hackish and limited, just barely good enough to construct the previous demos. In this sprint, I upgraded the capability significantly, generalizing it to work in a greater variety of contexts. I did this by constructing a mathematical model of the situation, finding a simple algorithm that solves the problem on the model, and then updating the code to implement the model and the algorithm. The model is inspired by some basic category theory involving projection and inclusion functions. An analogy is that if we have five people with two feet each and five pairs of socks, most likely we want to put one sock on each foot, as opposed to putting seven socks on one foot and launching the other three into space, or any other Turing-complete possibility...

Once a path is found on the type graph, now called a program path, if the path matches a certain pattern of projection and inclusion, it is inferred that a loop is required over the intervening subpath, and this loop is constructed analogously to a map function in a functional language such as Haskell. This approach further crystalizes the view that the path-compiler is essentially constructing an AST for a functional language that has no textual representation.

In this demo, the mathematical model of the synthesized loop with map rule reduction is

$$ P \rightarrow Q \rightarrow C^m \xrightarrow{proj} C \xrightarrow{f} R \xrightarrow{inc} R^m \\ \\ \Bigg \Downarrow \\ \\ P \rightarrow Q \rightarrow C^m \xrightarrow{map(f)} R^m, \\ $$ with \(P = \mathit{PaletteId}\), \(Q = \mathit{Palette}\), \(C = \mathit{ColorId}\), \(R = \mathit{RgbColor}\), and \(m = 4\).

Computational Models and Human Expression. I've been studying the traditional models of computation such as finite state automata, pushdown automata and Turing machines, and in particular reading about connections between these models and group theory. A lot of it is rather confusing as it pertains to actual practical computing devices, or the flip machine model, or the binary vector space model (below). What I do know is that a flip machine with a fixed number of bits and program length is equivalent to a finite state automata. This is true for everyday computers and programs as well, but things get murky; people tend to think of their computers as approximating Turing machines, due to the overwhelming number of states and lengths of programs. My hunch is that for the purposes of expressing human ideas in computational phenomena (to borrow a phrase from Frank Pfenning), more computationally powerful and open ended methods may be the last thing we want, that in fact it's quite nice and valuable to think of coordinated dimensions of restricted computational models where finiteness and algebraic structure enable advanced levels of synthesis. That very notion is the overall driving force of this project.

Future Directions.