powerplay

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

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

Repo

View repository

View issue tracker

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:

• The PowerPlay implementation is formally verified
• We can build PowerPlay’s proof machinery on top of Coq’s

The repository is layed out as follows:

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

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

• Simple.v A simple, standalone PowerPlay specification

• SimpleTests.v Unit tests and theorems about Simple.v

• SK.v A Coq implementation of SK combinatory logic

• SKTests.v Unit tests and theorems about SK.v

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

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

• Util.v Generic utility functions and theorems

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