An inference engine for extensional untyped λ-calculus
C++ Python CMake Protocol Buffer Jupyter Notebook Makefile Other
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
bootstrap
doc
include
src
.clang-format
.gitignore
.travis.yml
Brewfile
CMakeLists.txt
LICENSE
Makefile
README.md
configure-analyst.sh
diff.py
install.sh
pomagma
requirements.txt
setup.py
vet.py
vetted_hashes.csv

README.md

Pomagma

Build Status PyPI Version

Pomagma is an inference engine for extensional untyped λ-join-calculus, a simple model of computation in which nondeterminism gives rise to an elegant gradual type system.

Pomagma can:

  • simplify code fragments expressed in λ-join-calculus
  • validate codebases of programs and assertions
  • solve systems of inequalities and horn clauses
  • synthesize code from sketches and inequality constraints

Pomagma's base theory is being formally verified in the Hstar project.

Pomagma's architecture follows a client-server model, where a Python client library performs high-level syntactic tasks, and a shared C++ database server performs low-level inference work.

Installing

The server targets Ubuntu 14.04 and 12.04, and installs in a python virtualenv.

git clone https://github.com/fritzo/pomagma
cd pomagma
. install.sh
make small-test     # takes ~5 CPU minutes
make test           # takes ~1 CPU hour

The client library supports Python 2.7.

pip install pomagma

Quick Start

Start a local analysis server with the tiny pre-built atlas

pomagma analyze             # starts server, Ctrl-C to quit

Then in another terminal, start an interactive python client session

$ pomagma connect           # starts a client session, Ctrl-D to quit
>>> simplify(['APP I I'])
[I]
>>> validate(['I'])
[{'is_bot': False, 'is_top': False}]
>>> solve('x', 'EQUAL x APP x x', max_solutions=4)
['I', 'BOT', 'TOP', 'V']
>>> validate_facts(['EQUAL x TOP', 'LESS x BOT'])
False

Alternatively, connect using the Python client library

python
from pomagma import analyst
with analyst.connect() as db:
    print db.simplify(["APP I I"])
    print db.validate(["I"])
    print db.solve('x', 'EQUAL x APP x x', max_solutions=4)
    print db.validate_facts(['EQUAL x TOP', 'LESS x BOT'])

Get an Atlas

Pomagma reasons about large programs by approximately locating code fragments in an atlas of 103-105 basic programs. The more basic programs in an atlas, the more accurate pomagma's analysis will be. Pomagma ships with a tiny pre-built atlas of ~2000 basic programs.

To get a large pre-built atlas, put your AWS credentials in the environment and

export AWS_ACCESS_KEY_ID=...        # put your id here
export AWS_SECRET_ACCESS_KEY=...    # put your hey here
pomagma pull                        # downloads latest atlas from S3

To start building a custom atlas from scratch

pomagma make max_size=10000         # kill and restart at any time

Pomagma is parallelized and needs lots of memory to build a large atlas.

Atlas Size Compute Time Memory Space Storage Space
1 000 atoms ~1 CPU hour ~10MB ~1MB
10 000 atoms ~1 CPU week ~1GB ~100MB
100 000 atoms ~1 CPU year ~100GB ~10GB

License

Copyright (c) 2005-2017 Fritz Obermeyer.
Pomagma is licensed under the Apache 2.0 License.

Pomagma ships with the Google Farmhash library, licensed under the MIT license.