Bayesian induction of programs, à la Solomonoff
Johann
Bayesian induction of programs, à la Solomonoff
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
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.
| 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 | |
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 |
| 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 |
| 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. | ||
