Pomagma is a extensional programming environment for developing computational behaviors. Extensionality is the idea that two programs can be considered equal if their input-output pairs are all equal, in particular ignoring resource usage, run-time complexity, and space. The opposite of extensionality is intensionality, the idea that programs should be considered equal only if they convey the same concept intended by the programmer. Modern programming is mired in far-too intensional practices, where incidental artifacts of code (whitespace, style, line order, local variable names, arbitrary imperitives) frustrate many actions that would be easier with an extensional view (code-search, verification, optimization, automatic parallelization). Better programming practice might start with syntax-directed editors, tools for code refactoring, purely functional and declarative languages, and precise type systems. But a key missing concept is the use of extensionality. Pomagma is an experiment to see how far extensionalty can be pushed.
Pomagma is founded on a simple untyped pure functional programming language, the non-deterministic λ-calculus [1], and a "maximally-coarse" semantics [2] where as many programs as possible are considered equal. At the core of the Pomagma system is an equation prover that is used for verification and search/suggestion.
The λ-join-calculus is a λ-calculus with a join operation,
written x|y indicating nondeterministic or concurrent choice.
Nondeterminism allows one to specify what doesn't matter in a program:
symmetry, order of decoupled operations, etc.
Naively, two programs might be considered equal if their outputs agree at all inputs.
However, in a space where programs can be applied to programs,
and where programs may sometimes halt,
one needs to define this equational semantics carefully by coinduction.
It turns out to be be enough to say that two programs x and y are equal
iff for every program f, f x halts iff f y halts.
Pomagma provides a rich type system by simulating types within the base system.
The first idea, due to Dana Scott [3], is to define a term x to have type t
iff x is a fixed-point of t, i.e., x:t iff t x = x.
The second idea, from [4], is to use the combination of non-determinism and
observational equivalence to define higher-order polymorhic types t
inside the untyped base language.
Pomagma takes an extensional approach to quoting.
Opposite to Kleene's intensional quoting convention,
where codes x are considered intensional and were evaluated {x}
to produce functions, Pomagma's language treats codes x as
extensional and requires quoting {x} to prevent evaluation.
Moreover by consistently extending the λ-join-calculus,
we can achieve the rule: if it is provable that x = y, then also {x} = {y}.
In Pomagma, quoting serves to flatten the information ordering,
rather than preserve intension.
Pomagma consistently extends λ-join-calculus with a partial equation-deciding oracle. This allows equations to be interpreted back into the language as terms. Iterating, we can thus write equations of strength all the way up the hyperarithmetic hierarchy to Δ11, and provide a foundation for all of Sol Feferman's predicative mathematics.
Pomagma's coding interface minimizes intensional data. Rather than a file of lines of code, Pomagma stores a database of unordered lines of code. Each line is either a definition (an explicit declaration) or an assertion (an implicit declaration). All defined variables are globally visible. The behavior of a line of code as a function of its referenced global variables is treated extensionally. Lines are stored in "compiled" form and are "decompiled" on the fly while editing. Multi-line views of code are also generated on the fly by querying the line database. (Contrast this with the archaic tree-of-files-of-lines-of-code format that this very repo is stored in.)
- [1] the λ-join-calculus in terms of Scott's information ordering.
- [2] the λ-theory H-star of observational equivalence.
- [3] "Datatypes as Lattices" -Dana Scott (1976)
- [4] Pomagma began as a PhD thesis and codebase.
- /src - source code (C++, python, javascript)
- /doc - developer documentation
- /data - generated data, mirroring an S3 bucket
- /build - destination of C++ builds
- /pomagma - a symbolic link to appease
pip install -e
The editor front end runs a local server, and can be run without the theorem-prover.
# install using pip
easy_install pip
mkvirtualenv pomagma
workon pomagma
git clone git@github.com:fritzo/pomagma
cd pomagma
pip install -r requirements.txt
pip install -e .
# run the server
python -m pomagma.editor serve
chromium-browser http://localhost:34934 &
The theorem-proving back end currently targets Ubuntu 12.04 LTS.
git clone git@github.com:fritzo/pomagma
cd pomagma
./install.sh # If mkvirtualenv fails, run manually. FIXME
make test
To run a distributed system, pomagma needs Amazon AWS credentials, an S3 bucket, an SWF domain, and optionally an email address to receive errors. These are specified by environment variables
AWS_ACCESS_KEY_ID=...
AWS_SECRET_ACCESS_KEY=...
POMAGMA_BUCKET=Example-Amazon-S3-bucket
POMAGMA_DOMAIN=Example-Amazon-SWF-domain
POMAGMA_EMAIL=example.user@example.com
To run in debug mode, define an environment variable
POMAGMA_DEBUG=
Copyright 2005-2013 Fritz Obermeyer.
All code is licensed under the MIT license unless otherwise noted.