-
Notifications
You must be signed in to change notification settings - Fork 236
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
Conversation
(x1 == x2 /\ squash ((r_b x1) y1 y2)) | ||
|
||
|
||
/// Provide a mapping from a point in lex_sq to a squashed point in lex |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, fixed!
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:
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! |
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. |
Overview
This PR adds support for internalizing accessibility predicates based termination checking in F*. For a recursive function:
we can now write:
where
|- rel:FStar.WellFounded.well_founded_relation a
andx_i |- e:a
for some typea
. For a recursive callf arg_i
, F* adds the following termination check in the VC:i.e. expression
e
when substituted byarg_i
forx_i
should be related toe
byrel
.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 aGTot
version of accessibility (theGTot
version is useful when writing squashed relations, see below). For example, see here for a proof of well-foundedness of<
relation onnat
.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:
To prove
Valid (lex_t e e')
, we need a termt: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:rather than as an inductive formulation:
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
{:well-founded
to the parser and lexer, and parsing it as well-founded relation baseddecreases
clause.WFOrdering (rel, e)
in the parser AST (the decreases clause is eitherDecreases (LexList l)
orDecreases (WFOrdering (rel, e))
decreases_order
as a separate type inFStar.Syntax.Syntax
. It has two cases:Decreases_lex of list<term>
andDecreases_wf of term * term
. TheDECREASES
flag is thenDECREASES of decreases_order
Typechecker changes
Decreases_wf (rel, e)
, we generate a fresh uvar?u:Type ?uu
and check thatrel : well_founded_relation<?uu> ?u
ande : ?u
(tc_comp
inTcTerm.fs
)mk_precedes
function, which adds termination check to the VC, branches ondecreases_order
and either adds lexicographic ordering check or the well-founded relation check (guard_letrec
inTcTerm.fs
).ulib
changesFStar.WellFounded
: expanding on the utilities for building well-founded relationsFStar.LexicographicOrdering
: proving admissibility of the lexicographic ordering based terminationFStar.IndefiniteDescription
: added a helper functionsquash p -> GTot p
Some references