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.
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
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'])
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 |
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.