INRIA EA RAPT Report 2012

Publications

Exchanges

 

Internships

Visits

Movements

Workshops and Seminars

Research Activities

The following is a summary of the work done in the RAPT project in 2012

1. Abella development and maintenance

The Abella theorem prover was built by Andrew Gacek (Rockwell Collins) in the University of Minnesota during his Ph.D. and subsequently during his postdoc at Parsifal. Since then, a number of other people have been building on his work in different branches of Abella, but the work has not been centrally co-ordinated. We have undertaken to create a developers and maintainers organisation for the continued future development of Abella.

The key aspects of this new organisation include:

2. Generalising the Abella specification logic

The main product of Yuting Wang’s internship at Parsifal has been a nearly complete branch of Abella that extends the specification logic from second-order hereditary Harrop (HH2) formulas to arbitrary Lambda Prolog formulas (HH-omega). This extension substantially increases the expressive power of the specification logic, allowing a number of computational specifications in a simpler and more natural fashion.

A key ingredient in making the jump from HH2 to HH-omega was a focused treatment for the specification logic. Focusing is a very general mechanism for refining the structure of sequent proofs and thereby controlling the behaviour of proof search. It turns out that in the HH-omega proof theory, it is sometimes essential to reason about program fragments in contexts of object sequents; focusing is critical in representing such reasoning paths. Moreover, all existing HH2 theorems continue to hold in the extension to focused HH-omega, although some proofs have to be slightly modified for the new focused setting.

The HH-omega branch of Abella has been demonstrated at a workshop in LIX in July and then subsequently at the RAPT/Promis workshop in Montreal in October. Several changes were implemented in response to feedback from users and this branch has been scheduled to be incorporated into the mainline of Abella in the upcoming 2.0 release.

Wang and Chaudhuri are in the process of writing a paper documenting this branch of Abella.

3. Polymorphic types in Abella and Bedwyr

Abella has historically supported only a simple type system based on Church’s Simple Theory of Types. While this has been adequate for small problems, it is clear that for larger developments one would require some support for polymorphism. Our colleagues at the University of Minnesota (Gopalan Nadathur, Yuting Wang, Mike Whalen) and at Rockwell Collins (Andrew Gacek) have been using Abella to formally show the correctness of a compiler for a synchronous dataflow programming language used for programming reactive systems in such domains as avionics and nuclear power plants. Their work is greatly hindered by the lack of polymorphism in Abella.

A common example of the need for polymorphism in such large scale projects has to do with composing data. Currently in Abella, if we need two kinds of lists, the only option is to give two different definitions and duplicate all relevant lemmas about lists for these separate definitions. The problem quickly worsens with increasing structure in the data – for instance, a list of pairs of natural numbers would not only require special lemmas about numbers, pairs, and lists, but also lifting lemmas to move the results from numbers to pairs of numbers, and then to lists of pairs of numbers.

We have undertaken to extend the type system of Abella to support polymorphic types and polymorphic lemmas. Our type system is inspired by the parametric polymorphism of programming languages such as ML and Haskell. Most of the development has been straightforward as the issues with polymorphic type-inference are well known. The implementation is scheduled to be included in the mainline 2.0 release of Abella.

The main theoretical issue with polymorphism in Abella has been the treatment of subordination. Consider the following signature:

kind tm, ty  type.

type b   ty.
type arr ty -> ty.

type abs (tm -> tm) -> tm.
type app tm -> tm -> tm.

From this signature, if we were to compute the subordination relation, we would deduce neither that tm is subordinate to ty, nor the converse. That is to say, in normal ground terms of type ty, there can be no occurrences of subterms of type tm. Hence, whenever we have a function of type tm -> ty, we can immediately conclude that it ignores its argument; this can be used to prune dependencies in metavariables and lead to more equations falling into the dynamic L-lambda fragment which is amenable to higher-order unification.

This simple situation is complicated with the introduction of polymorphic types. Consider the following addition to the signature.

type fst  A -> B -> A.

One valid interpretation of such a declaration is that the type of (fst U V) is independent of the type of V. Hence, the following normal term of type ty

arr (fst b (abs x\ x)) b

contains a strict subterm, abs x\ x, of type tm. This means that the complement of the subordination relation becomes empty, making the computation of this relation completely pointless.

As the subordination relation is very useful in practice, we choose to disallow declarations such as fst from signatures. Practically, this amounts to the following restriction: the target type of any signature constant must contain all the type variables in the type of the constant. Since the target type of fst, viz. A, does not contain the variable B, it fails the check and is disallowed. Note that we can still declare polymorphic constants such as the following.

type id      A -> A.
type nil     list A.
type cons    A -> list A -> list A.
type mkpair  A -> B -> pair A B.

Lambda Prolog, which is the basis for the specification logic of Abella, has a very general notion of polymorphism that includes both parametric polymorphism and ad hoc polymorphism. Supporting reasoning about the full generality of the Lambda Prolog type system, especially in the presence of induction, co-induction, and subordination, is essentially an open research problem lacking good answers. Fortunately, supporting the full generality of Lambda Prolog’s type system is not urgent.

4. Towards a more robust proof language for Abella

One of the most questionable aspects of Abella from a trust perspective is that the proof tactics are trusted. That is, there is no independently verifiable proof object for an Abella theorem. During 2011 we investigated the fundamental problem of certifying Abella proofs, but came to the conclusion that producing a truly independent proof output from Abella was difficult because of the open theoretical problem of certifying completeness of a set of unifiers for a higher-order unification problem.

From a pragmatic perspective, we can improve the trustworthiness of Abella proofs with a slightly weaker notion of trust by treating the unification engine of Abella as a trusted component. Indeed, this definition of trust has already been adopted by the ProofCert project at Parsifal. An interesting aspect for this notion of trust is that we can make the proof language of Abella more robust; this will be the major focus of RAPT activities in 2013. Briefly, Abella proofs are now closely linked to the operational semantics of Abella’s unification engine. For case-analysis, the cases in the proof must be in precisely the order that they are generated by the implementation of higher-order unification, which is not fully predictable from the text written by the user. We are instead planning to decouple the presentation of cases as the user writes them from the check that they cover all the possibilities required by unification. This will bring the Abella proof language more in line with coverage-based approaches in systems such as Twelf or Beluga.

5. A theory of contexts

An emerging theme in the work on Abella, Beluga, and some related systems such as Hybrid, is a way to abstract common idioms in the treatment of contexts in computational specifications. Currently, each system has strengths the others lack. In Abella, contexts can be given very general relational specifications, but the user has to repeatedly prove lemmas about elements in contexts. Beluga on the other hand makes reasoning on the structure of contexts mostly automatic, but it can only handle a single regular context, and the meta-theory of contexts tends to be complicated. In an ideal world, we would be able to take the regular context schemas in the Beluga style—together with the automated reasoning about such contexts—to specify contexts in Abella in the cases where they suffice, while allowing the user to fall back to the fully general relational definitions when necessary.

There are both theoretical and practical challenges to this ideal picture. The theory of regular contexts, although well developed, does not yet give a logical account of the structural features of contexts, in particular of subsumption, weakening, and strengthening. The main issue is that some structural rules such as weakening are height-preserving, meaning that they should not affect the applicability of inductions on the structure of derivations, while other rules such as strengthening need not be height-preserving. Currently, all the above systems lack a means of expressing the height-preserving nature of context transformations.

From a practical standpoint, the key question is whether regularity of contexts is something the system detects and then handles transparently, or if it is something the user explicitly annotates in his definitions. Both approaches come with trade-offs. If the system infers regularity, then the implementation becomes more complex (and therefore less trustworthy), and the user might be surprised by the system discharging proof obligations that he had expected to write proofs for explicitly. In the alternative, the system would have two different ways to specify the same things, so the user might be confused about which style is to be used in which situations.

A careful comparison of the three systems with regard to the treatment of contexts is being undertaken by Brigitte Pientka, Amy Felty (professor, Univ. of Ottawa), and Alberto Momigliano (professor, Univ. Milan).

6. The expressive reach of the two-level logic approach

Systems such as Abella and Beluga implement a strict nesting of specification logics inside reasoning logics (or computations, in the case of Beluga). While this strict nesting is usually sufficient, there are some domains where this restriction is too limiting. To illustrate, in Abella it is currently impossible to use negation in the specification logic, so it is not possible to write a definition such as:

normal (abs M) :-
   pi x\ normal x => normal (M x).
normal (app M N) :-
   normal M, normal N,
   (pi U\ not (M = lam U)).

for which normal M would succeed iff M is a normal lambda expression. Unfortunately, Abella does not support the not predicate in the specification logic. Therefore, the normal relation in Abella needs to be written in the following more cumbersome fashion, using an auxiliary predicate neutral.

normal (abs M) :-
   pi x\ neutral x => normal (M x).
normal M :- neutral M.

neutral (app M N) :- 
   neutral M, normal N.

There are essentially two ways to handle this deficiency. One is to augment the two-level logical basis of Abella to admit negation at the specification level, but if done naively then the provability relation in the reasoning logic (the logical basis of the curly-braces of Abella) can become non-stratified. A less drastic approach would be to allow the specification logic to appeal to certain predicate symbols, such as equality and negation, in the reasoning logic. That is to say, the second clause of the above definition might be written as:

normal (app M N) :-
   normal M, normal N,
   (pi U\ [[ M = lam U -> false ]]).

where [[ ]] is used to embed a reasoning-level formula into the specification logic.

There are a number of other examples where a limited amount of appeal to reasoning logic predicates in the specification logic seems to be either necessary or very useful. We are currently exploring the meta-theory of this kind of back-and-forth communication between the two logics.

7. Interactions between Abella and Bedwyr

Bedwyr is a model checker for sophisticated specifications in a logic very similar to the reasoning logic of Abella. Unlike Abella, Bedwyr cannot be used to prove inductive theorems; even trivial theorems such as nat M -> nat M are beyond the scope of Bedwyr because the way it attempts to prove it is by first constructing the full set of terms M for which nat M holds, which is infinite. On the other hand, Bedwyr is very efficient at exhaustively checking a finite search space because it is based on tabled search; Abella, by comparison, has only a rudimentary search engine that does not attempt to reason by unfolding definitions.

A recent effort by Quentin Heath (engineer at Parsifal) and Dale Miller (senior researcher at Parsifal) has been to combine the strengths of the two systems in the following manner: Abella would be used to prove inductive lemmas about a Bedwyr specification, and Bedwyr would then use these lemmas to improve its tabling mechanism and prune the search space further. A simple example of this approach is a specification of Tic Tac Toe, where Bedwyr can find winning strategies fully automatically; unfortunately, it is not possible to ask Bedwyr to prove that when a board is a winning position for a player, then all symmetric versions of the board also are winning positions. Thus, Bedwyr will end up re-deriving that a symmetric board is or is not a winning position. However, symmetry theorems are fairly straightforward to prove in Abella.

The Abella and Bedwyr languages have been modified slightly so that the same file containing a Bedwyr specification and an Abella proof can be accepted by both systems. Abella would only check the inductive proofs in the file, while Bedwyr would use the lemmas to improve its handling of queries. This is part of the focus of the ADT BATT (2011-2013).

Additional Funding

 

INRIA

Canada

USA

2013 Planning

In 2013 we plan to do the following:

We expect to make use of the full budget allocated to third year EAs (10K euros).