Readme
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
Repository
Clone this repository using: git clone http://chriswarbo.net/git/powerplay.git
Branches
- master: Tweaks Chris Warburton <chriswarbo@gmail.com> Fri Oct 9 12:57:35 AM UTC 2015
Generated by git2html.