Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for accessibility predicates based termination checking #2307

Merged
merged 38 commits into from
Jun 3, 2021

Conversation

aseemr
Copy link
Collaborator

@aseemr aseemr commented Jun 1, 2021

Overview

This PR adds support for internalizing accessibility predicates based termination checking in F*. For a recursive function:

let rec f x_i : Tot t = ...

we can now write:

let rec f x_i : Tot t (decreases {:well-founded rel e}) = ...

where |- rel:FStar.WellFounded.well_founded_relation a and x_i |- e:a for some type a. For a recursive call f arg_i, F* adds the following termination check in the VC:

rel (e[arg_i/x_i]) e

i.e. expression e when substituted by arg_i for x_i should be related to e by rel.

Proof of well-foundedness

To prove a relation to be well-founded, we need to exhibit a proof that every element is accessible. Module ulib/FStar.WellFounded.fst provides the basic setup of accessibility predicates and utilities to prove a relation to be well-founded.

It defines a Tot and a GTot version of accessibility (the GTot version is useful when writing squashed relations, see below). For example, see here for a proof of well-foundedness of < relation on nat.

The library also shows that well-foundedness commutes with subrelation and inverse image (from Constructing Recursion Operators in Type Theory, L. Paulson JSC (1986) 2, 325-355).

Proof for well-foundedness of lexicographic ordering

The PR also contains a proof that the lexicographic ordering relation is well-founded (see this). (Hence justifying its admissibility in F*.)

Squashed vs constructive relations

The termination check that F* adds to the VC is by-default sent to the SMT solver (as usual). So the VC may contain obligations like:

phi ==> Valid (lex_t e e')

To prove Valid (lex_t e e'), we need a term t:lex_t e e'. In general, it is hard for SMT to come up with this proof term by itself.

Therefore, it helps to work with squashed relations. For lex, for example, a more SMT-friendly way is to define the relation as:

let lex (x1, y1) (x2, y2) = r_a x1 x2 \/ (x1 == x2 /\ r_b y1 y2)

rather than as an inductive formulation:

type lex_t ... = | Left : ... | Right : ...

However, this is at odds with the fact that accessibility proofs are easier (at least for me) to grok at when done in the constructive fragment. For example, dealing with squash etc. in the middle of lex accessibility proof would be an additional baggage.

To deal with this, the library provides a way to move between squashed and non-squashed versions of a relation. Essentially the library allows the programmer to do their accessibility proofs on the constructive version of a relation, define a squashed version that's more SMT friendly, define a map from squashed version of the relation to the constructive version, and then reuse the well-foundedness proof of the constructive version: see this.

Using this we define a squashed version of lex and prove it is well-founded. Ultimately, we use it to prove termination of ackermann here.

Code changes

Syntax changes

  • A new token {:well-founded to the parser and lexer, and parsing it as well-founded relation based decreases clause.
  • New node WFOrdering (rel, e) in the parser AST (the decreases clause is either Decreases (LexList l) or Decreases (WFOrdering (rel, e))
  • Hoisting decreases_order as a separate type in FStar.Syntax.Syntax. It has two cases: Decreases_lex of list<term> and Decreases_wf of term * term. The DECREASES flag is then DECREASES of decreases_order

Typechecker changes

  • To typecheck Decreases_wf (rel, e), we generate a fresh uvar ?u:Type ?uu and check that rel : well_founded_relation<?uu> ?u and e : ?u (tc_comp in TcTerm.fs)
  • The mk_precedes function, which adds termination check to the VC, branches on decreases_order and either adds lexicographic ordering check or the well-founded relation check (guard_letrec in TcTerm.fs).
  • For mutually recursive let bindings, we enforce that the decreases check is consistently lex ordering based or well-founded relation based, and if the latter, uses the same relation (syntactically).

ulib changes

  • FStar.WellFounded: expanding on the utilities for building well-founded relations
  • FStar.LexicographicOrdering: proving admissibility of the lexicographic ordering based termination
  • FStar.IndefiniteDescription: added a helper function squash p -> GTot p

Some references

@aseemr aseemr requested review from nikswamy and tahina-pro June 1, 2021 06:31
(x1 == x2 /\ squash ((r_b x1) y1 y2))


/// Provide a mapping from a point in lex_sq to a squashed point in lex
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: I guess you mean lex_aux rather than lex_sq

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, fixed!

@nikswamy
Copy link
Collaborator

nikswamy commented Jun 3, 2021

This is really great work, Aseem. Congratulations! I'm delighted to see it all working so well together. The part where you transition between squashed and constructive relations is really nice---I hadn't seen that earlier.

A couple of remarks:

  • I was expecting to see a change in FStar.Parser.ToDocument to handle the Decreases (WFOrder _) case, but I don't see it there (unless I missed it). We need it otherwise fstar --print etc. will crash. Please check this one before merging.

  • I see that the WFOrder is not yet exposed in the reflection API. That's ok for now, I think. But someone will ask for it sooner or later.

A curiosity: I wonder in what scenario one would prefer to use the symmetric product over the lex ordering. I guess you could have proven it well-founded using the sub-relation infrastructure you have set up, as opposed to proving it WF from scratch?

Anyway, super stuff. I really liked your PR notes too, describing all of this very clearly. Do add a brief note in CHANGES.md too.

Thanks!

@aseemr aseemr merged commit 181c9cd into master Jun 3, 2021
@aseemr
Copy link
Collaborator Author

aseemr commented Jun 3, 2021

Thanks for the review Nik! Indeed I was missing the case in resugaring, I added it, with a pretty-printing testcase. Also added a note in CHANGES.md. For the reflection API, I was wondering if we should change the API to expose comp flags properly, instead of adding another case in comp. We can discuss more.

Interesting bit about symmetric ordering. You are right, we can define it as a subrealtion of lex, but it needed a non-dependent lex. I re-worked the library to do it so.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants