12.16.2018  Pac-Man Specification and Synthesis Milestone Report

This milestone was reached: in a workbench demo UI, a user can toggle four input bits which triggers execution of a pre-synthesized flip program that translates the four input bits into 8 output bits, following the original Namco Pac-Man color table design.  The workbench UI monitors the output bits and draws a display "pixel" div in the corresponding RGB color.  The work primarily consisted of:

Concessions: The workbench UI is intentionally geared toward the purpose of producing the constituent parts of the overal pac-man experience, and not very flexible or suitable for other purposes. There is a bug in the color table spec that causes some colors to be slightly off.  This can be corrected in the next set of demos which will need tools to extract data from the original pac-man roms, for the palette table, tile table, and sprite table.

Observations

Reversible branching.  I couldn't get the Axelsen[2007] trace-free approach to work, most likely because I misunderstand it, or it doesn't directly translate to the flip architecture.  I opted for a trace approach, where with the addition of a single bit per instruction in the program, we can record two execution traces.  This is good enough for the moment, especially since we aren't actually utilizing reverse execution yet for any real purpose.  The implemenation of reversible branching in the flip virtual machine ultimately lead to adding another higher-level language, called the level-1 flip language which gets translated to the original level-0 flip language.  This was done to make it sane to produce programs that meet the requisite constraints for reversibility, e.g. jump source and desination pairs need to be unique.  A short example:

Level-1 Program

Level-0 Program

flip 0

if 0

  flip 0

  if 1

    flip 1

if 0

  flip 1

  if 1

    flip 1

  flip 1

FLIP 0

JUMPTO 0 4

FLIP 0

JUMPTO 1 1

FLIP 1

JUMPFROM 1 1

JUMPFROM 0 4

JUMPTO 0 5

FLIP 1

JUMPTO 1 1

FLIP 1

JUMPFROM 1 1

FLIP 1

JUMPFROM 0 5

Program space, function space and the group action.  It's not crystal clear yet how to describe the group action, nor how to produce a closed non-recursive formula for the size of the level-1 program space.  A formula for the size of the function space is known; it is hyper-exponential. And it is known that there is not a bijection between level-1 program space and the multi-boolean function space.  It also remains to be seen if one can always derive a level-1 program for any given multi-boolean function (i.e. is the mapping surjective onto the function space?).  Additionally, it is interesting to consider whether a textual language could be constructed that does biject with the multi-boolean function space.

Program compression.  Already, the level-1 flip language programs being produced by the simple IO-spec generator contain some redundancies.  Some work could be done to compress them into smaller equivalent programs, even before adding support for loops or recursion.

Program search and pruning.  No actual search of level-1 program space has been implemented yet, because the IO-case synthesizer doesn't need it -- it can simply derive the required flip code directly from the specification.  Going forward, if we do end up searching level-1 space, we may be able to proceed by "pruning rules", i.e. rules that avoid certain branches of the space based on theorems about the group structure and the computed function.  This potentially starts to lend some weight to the original hypothesis that the group structure is advantageous for synthesis.

Types, human meaning and the Path Compiler.  It seems as though a type system is a way to bridge human meaning to bit patterns.  The next step appears to be clear: create a database of types and function type signatures.  This can be used to generate a graph. For example, for the color table demo the types are bit[4], bit[8], colorId, RgbColor, and the only function is colorIdToRgbColor(colorId): RgbColor .  Then, assuming, each function is accompanied by flip program code that implements it, given a desired source type and destination type, if a path can be found on the graph from the source type to the destination type, this path can be directly translated into a chain of the corresponding flip programs, i.e. compiled together, with some minimal additional flip code to glue the output of one function to the input of the next.

Powers of two.  It feels as though the explosive number of groups of order two (aka the "GNU number") could be related to the present situation, since the order of the total acting group seems to be 2^(n+L).   It also raises the question of whether it might be advantageous to use, instead of bits, granular stores with orders of 3 or 5 or other instead of 2?  i.e. tribits etc.  Also, we could consider adding other reversible operations that significantly change the group structure -- i.e. a "swap" operation that swaps two bit positions, which would generate a symmetric group, I think.  It's not clear whether the more mundane existing group, which is the cartesian product of many order-two groups is better or worse to use than a richer, symmetric (or other) group, since we really aren't utilizing the algebraic group structure yet.

Bugs.  If a program has a bug, it is still a member of the total group (and may generate an interesting subgroup?). Thus the desired program and buggy program are related through the group structure -- is this useful?  How can we describe this relation?  (Example: consider the bug in the IO-case synthesizer where due to a design flaw the synthesizer was producing a program that was partially incorrect.  As a group element, how is that program related to the correct program?)