Johann
Bayesian induction of programs, la Solomonoff

What is Johann

Johann is a toolset for statistically reasoning about computation. At the core of the Johann system is a dynamic database of assumptions and consequences of a theory of computation. The database finitely approximates the semantic space of computations, and provides a language-independent view of computation. Using the database, Johann can answer easy questions about computation and guess answers to difficult questions (and even quantify how sure he is).

The particular model of computation used is inadvertantly-typed concurrent combinatory algebra, i.e., closed-term lambda-calculus with join. The particular theory of computation used is the Hilbert-Post complete theory concurrent-H-star of terms and Scott's information-ordering relation.

For details, see Fritz's Ph.D. thesis or relevant talks

Combinator Databases

Johann builds big databases of combinators --essentially multiplication tables for functional programs. The Johann-DB library is a lightweight tool for reading Johann databases in C++.

To start exploring, either (i) compile your C++ code with the Johann-DB library and download one of the .jdb database files, or (ii) download one of the .csv bundles.

Databases

SKJ - small
.jdb file skj-small.jdb.bz2 (4.2MB)
.csv bundle skj-small.tbz2 (3.2MB)
programs 4288
equations 784728 apply + 442046 compose + 62535 join
basis _, T, I, K, F, B, C, W, S, J, J', Y, U, V, P, prod, div, semi, unit, bool, sum, inr, inl, maybe, some, none, sset, Simple, P_test

SKJ - medium
.jdb file skj-medium.jdb.bz2 (21MB)
.csv bundle skj-medium.tbz2 (17MB)
programs 7977
equations 4182057 apply + 2255140 compose + 219030 join
basis _, T, I, K, F, B, C, W, S, J, J', Y, U, V, P, prod, div, semi, unit, bool, sum, inr, inl, maybe, some, none, sset, Simple, P_test

Maps of program spaces

Viewing Maps

The maps provided here require an OpenGL visualizer jmapper, located in the mapper/ directory of the Johann git repository. You can download a binary for Mac or Windows or source code for linux/unix.
Platform Downloads
Mac/Intel jmapper_mactel.bz2
Mac/PowerPC jmapper_macppc.bz2
Windows mapper_win.zip
Source Code mapper.tbz2
To view a map and run the jmapper command on the unzipped map, as in
> jmapper_macppc untyped.map

Tips on using the jmapper viewer:
up arrow - zoom in and out
+ / - keys - change node size
ESCAPE - exit viewer
SPACE - clear all labels and parse trees
s or S - label simplest terms
1 / 2 / 3 - select label font size
p or P - toggle label style: combinator or lambda-calculus
a or A - show all parse trees
c or C - toggle hiding of irrelevant nodes
right click - show node's parse tree, hide irrelevant node
middle click - toggle node label
left click - toggle between: parse one step down / parse one step up / don't parse


Maps

SK - small
file untyped.map.bz2
file size 5.7MB (22MB uncompressed)
programs 4,803
equations 1,666,701
basis B, C, S, K, W, C I, 0, 1, 2, S B, B', S', S I, Y, W I
This map took about 1 day to build.

SK - medium
file untyped3.map.bz2
file size 19MB (74MB uncompressed)
programs 8,443
equations 5,679,089
basis B, C, S, K, W, C I, 0, 1, 2, S B, B', S', S I, Y, W I
This map took about 4 days to build.

SKJ - large
file typed.map.bz2
file size 30MB (125MB uncompressed)
programs 12,008
equations 8,904,419
basis B, C, J, S, K, W, C I, V, 0, 1, 2, S B, B', S', S I, Y, W I, P
This map took about 4 weeks to build.


Fritz Obermeyer - (Johann) - The Rational Keyboard - Jenn 3d
Fork me on GitHub