powerplay

Last updated: 2015-10-09 01:57:35 +0100

Upstream URL: git clone http://chriswarbo.net/git/powerplay.git

Contents of README follows

This is an implementation of Jürgen Schmidhuber’s PowerPlay[1] architecture for ‘Universal Artificial Intelligence’, implemented in the dependently-typed language Coq[2]. Using a system like Coq gives us two things:

<ul> <li>The PowerPlay implementation is formally verified</li> <li>We can build PowerPlay’s proof machinery on top of Coq’s</li> </ul>

The repository is layed out as follows:

build.hs Haskell script to build *.v files in order of dependencies

</li> <li>

Expr.v Initial attempt at defining a reflective Coq-in-Coq implementation (not finished yet)

</li> <li>

Simple.v A simple, standalone PowerPlay specification

</li> <li>

SimpleTests.v Unit tests and theorems about Simple.v

</li> <li>

SK.v A Coq implementation of SK combinatory logic

</li> <li>

SKTests.v Unit tests and theorems about SK.v

</li> <li>

SKUtil.v Utility functions, theorems and proof tactics for SK.v

</li> <li>

Sqrt.v Straightforward implementation of the Simple.v specification for finding square roots in lookup tables

</li> <li>

Util.v Generic utility functions and theorems

</li> </ul>

[1] http://www.idsia.ch/~juergen/interest.html [2] http://coq.inria.fr