rlepigre/pml

New version of the PML language and (classical) proof assistant

The PML₂ programming language and proof assistant

The PML₂ language provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, non-coercive) subtyping. In the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs. Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the type-checker. This means that the user only has to choose which equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern matchings).

Related documents and prototypes:

• https://doi.org/10.4230/LIPIcs.TYPES.2017.4 (introductory paper),
• https://tel.archives-ouvertes.fr/tel-01682908 (R. Lepigre's PhD thesis),
• https://doi.org/10.1007/978-3-662-49498-1_19 (paper related to the model),
• https://doi.org/10.1145/3285955 (paper related to subtyping),
• https://github.com/rlepigre/subml (the SubML language).

Dependencies and compilation

PML₂ requiere a Unix-like system. It should work well on Linux as well as on MacOS. It might also be possible to make it work on Windows with Cygwyn or with "bash on Windows").

List of dependencies:

• GNU make,
• OCaml (at least 4.04.0) with Opam,
• dune (at least 1.7.0),
• bindlib 5.0.1 (https://github.com/rlepigre/ocaml-bindlib),
• earley 2.0.0 (https://github.com/rlepigre/ocaml-earley).

Using Opam, a suitable OCaml environment can be setup as follows.

opam switch 4.05.0
eval `opam config env`
opam install dune>=1.7.0 bindlib.5.0.1 earley.2.0.0

To compile PML₂, just run the command make in the source directory. This produces the main.native binary, which can be run on files with the .pml extension (use ./main.native --help for more informations).

make
make install   # optionally install the program.
make doc       # optionally produce the ocamldoc documentation

Organization of the repository

This folder contains files related to the PML project.

The source files can be found in the following folders:

• src/util contains a set of libraries not directly related to PML,
• src/parser contains a low level AST of the language and the parser,
• src/kernel contains the core of PML (type checking, equivalence, AST...),
• src/pml.ml is the main program.

Other directories:

• editors contains PML modes for editors (vim and emacs only),
• lib contains the PML standard library (very small),
• test contains most of our examples of PML programs,

The directories tmp and attic are not relevant as the contain files used for debugging the newest features including termination checking and old code that we want to keep somewhere.

Support for the Vim (or Neovim) editor

After installing PML (with make install), you will need to add the following lines to you .vimrc file (if they are not already present).

" PML stuff
let g:opamshare = substitute(system('opam config var share'),'\n$','','''')
execute "set rtp+=" . g:opamshare . "/pml/vim"

Note that it may be necessary for these lines to appear before the following line.

filetype plugin indent on

Support for the Emacs editor

After installing PML (with make install), you will need to add the following lines to you .emacs file.

;; PML stuff
(load "pml-mode")

Where to start in the code

My advice to start looking at the code would be to take a look at the three different abstract syntax representations.

• The main abstract syntax is implemented as a GADT in src/kernel/ast.ml,
• The abstract syntax after parsing can be found in src/parser/raw.ml, together with the first level of type checking (sorting),
• The graph representation of terms for the decision of equivalence can be found in src/kernel/equiv.ml.

The implementation of type checking can be found in src/kernel/typing.ml, and the function for comparing expressions (including the unification functions) are in src/kernel/compare.ml.

pml's Issues

Cost of logging and Chrono

In function which are very frequently called, log and chrono can cost a lot.
If I uncomment the log in add_term and add_valu, the cost of log+chorno in Equiv and
Compare is a factor between 2 and 3.

we should create a binary "main.native" where this log/chrono on small function are disabled
(keeping still the main one like typing) and a main.debug with all log and chrono.

Incompleteness of typing/subtyping

Here we put reference to cases were the incompleteness of typing seems not reasonable.
This issue should probably never be closed.

test/fifo.pml: an annotation (x:a) is needed and this seems strange.

Higher order inductive types

This is needed for GADT and will result in a better syntax too:

type rec list = [ Nil ; Cons of a * list ]

will become

type rec list = [ Nil ; Cons of a * list ]

auto cases! use information from typing

Some time, extra information comes from typing which allows to
restrict cases. This information is probably available in the type of the VWit ...
We should try to use it!

See lib/int.pml for a use case.

A minimal user documentation is needed

Currently make doc, is just for developer (ocamldoc of files)

Error managment in Raw module (mantis #46)

various forbidden case due to sorting that have no error generated

Improve type inference

Reference this issue in .pml file when we are not satisfied.

pool optim, toward only head normal term added to the pool

insert_t_node should use a stack to avoid creating node for partially applied function.

For instance, adding [add n p] to the pool also adds [add n] which is a lambda, hence trigger a cloture construction.

This cost is dominating "equiv" when computation are really needed, with
probably a factor much greater that 2 (10 ?) to gain.

Finish printing

Printing has been improved, but is not finished ... quite a few syntactic sugar are missing.
Notably terms in values, cons, nil, infix, ...

Syntaxe revision (mantis #36)

Reexamine the syntax and see if the current choice are the best ...

The Impl construct has no parse rule

Do we need to learn ordinal relations in the pool

Probably not. Moreover, positivity is probably useless, relation o1 < o2 are enough (as it implies o2 > 0)

But still do we need to know in the pool that o1 < o2 is true ... Probably not ?

Theory

The document with the theory should be added to the git repository.

Reinforce completeness of auto and totality

When instantiating a unification variable of sort value with an expression
in the pool which is not a value, this does not trigger trying to prove that this a
value in auto_prove. Moreover, fixing this is not enough because one should
build a term which is a value to perform the instantiation.

Inequivalence clause are not stored in the pool (mantis #51)

Will only be useful when assuming inequivalence, which is not really possible currently.

Probably useless ... wait for a use case.

avoid canonical term in equiv.ml (mantis #41)

after #18 (mantis #40) is done, one should write an equality directly on
the pool, without using canonical term. canonical term should be kept for
debugging purpose only.

Storing of parents in the pool

Parents are only useful for the root of the union-find data structure. We should change the data structure
to only keep the parent of roots in the union-find.

PML loops

See test/infinite.pml

Position bug (mantis #33)

Position absent or wrong to often

Cyclic value should trigger contradiction in the pool.

An equation like x = S[x] learn in the pool does not yield a contradiction. Moreover,
using any function on x is likely to loop after that. We should detect such cycle.

Strangely, such cycle never appears in PML2 while they were frequent in PML1 ...

eq_expr called from leq_ordinal could use the pool oracle (mantis #54)

When 0000032 is solved, we will know ...

Does not seem usefull.

Deal with unification variables after type-checking (mantis #44)

Unification variable that remains after type-checking should
get a default instanciation.

Remark: if later we keep unification constraints, this would become very
important as there could be unsolvable contraints, or preferably, we should ensure all constraints have a default instanciation that we could use.

PML can not always use function equalities that it learned

When we learn that functions are equal, we should keep that information:
VN_LAbs should contain a list of functions.

This would allow to always deduce f x = g x from f = g

Mutually inductive types

Mutually inductive types can be encoded using extra parameters, but this result
in a notion of sized type which is not the one we want, and leads to failure
of the termination checker.

Incompleteness of the termination checker that seems solvable

Here, we put all use case that seems to be solvable (or that even work in subml):
This issue should probably never be closed.

• test/fifo.pml: with a pair of lists as argument
• test/unfold.pml

Printing of epsilons (mantis #53)

Epsilons should be prionted as the name of a bound variable that wes subsituted
with the epsilon. When epsilons are known to be equal, a "best" name should be chosen.

Automated totality (mantis #35)

Managing totality manually is too painful.
Should be annotated on the arrow type.

Contradiction is not always detected.

Use case in test/old_mccarthy91.pml

Use unification variables parametrized by ordinals (mantis #57)

To do as in subml, we need this.

It relies on higher-order ?

Better control of current totality status

When writing
let f = fun x ...
or even applications, or dependant product, we have no short way to indicate the current totality we want.

Do we need something (like more than one keyword for fun ?)

Automatic case analysis (mantis #34)

Perform a case analysis based on blocked case in evaluation. Could also do case analysis convergent/non convergent (pml1 does it)

Add a syntaxtic sugar to extend record.

Minimal syntactic { include r1; include r2; ... } should use typing to know the field that are present.
The same notation for type is just some kind of higher order function performing some computation on type.

The general include for a record of unknown type (or default record value) seems too hard at the moment,
especially for compilation.

managment of unification variable in equivalence Description (mantis #50)

The current implementation seems to work but should be checked.
The risk is to loose some equivalence/normalisation propagation
when a unification variable gets instanciated.

HApp node are also concerned as their head is often an uninstanciated
unification variable.

Subtyping heuristic and auto case

Currently, we use in subtyping a heuristic testing is the term (int t : A < B) is a value.
This heuristic seems in fact to test if we already unrolled fixpoint ... And is
not so clear.

As a side effect, this heuristic forces subtyping of sums to use introduce a term
Preventing to replace the current term in a case anlysis with only one case with
a witness.

But this term with one case produce useless computation in the pool and useless
case analysis in auto_prove.

use closure in the pool Description (mantis #40)

the binder in all pool node (equiv.ml module) should be replaced
by closure.

This will allow to know that

a = b => (fun x y -> y x) a = (fun x y -> y x) b

without using an oracle

We should be able to use constraint ordering on ordinals.

This is needed to write subtyping proof manually (and checking termination giving exact induction hyp).
Need a use case first ?

Checking for singleton type could be more complete (mantis #52)

Only very simple cases are handled by Typing.is_singleton.
Some quantification or Impl could be allowed.

Better handling of mu abstraction and stack in equivalence (mantis #45)

There is a FIXME in the code ... Don't know what should be done

Can add the equations that were proved for mu-abstraction and named terms:

• contraction of mu-abstractions
• elimination of consecutive stack resorations