-
Notifications
You must be signed in to change notification settings - Fork 256
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
Chore: Tutorial on proven fixpoints combinators #2789
base: master
Are you sure you want to change the base?
Conversation
This PR adds a tutorial on how to prove that fixpoint combinators can finish in Dafny.
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.
I left a few comments in the intro. I think the tutorial starts a bit too fast, and it's not completely clear from the beginning what we're trying to do. It would be great, before we can start looking at code, to clearly say "we would like to define a function fix
such that for all f, n
, fix(f)(n) == f(fix(f))(n)
.
Beyond this, I wonder if things could be made more intuitive by starting with total functions instead of partial ones. You could start with this, which I think is both reasonable and simple:
function method TotalFix(f: (nat -> nat, nat) -> nat, n: nat): nat {
var TotalFix' := (n': nat) => if n' < n then TotalFix(f, n') else 0;
f(TotalFix', n)
}
By bottoming out at 0
, we avoid all termination concerns. Then, you would ask: how do I eliminate the default case? The natural way to do this would be:
function method UnusablePartialFix(f: (nat --> nat, nat) -> nat, n: nat): nat {
var PartialFix' := (n': nat) requires n' < n => UnusablePartialFix(f, n');
f(PartialFix', n)
}
… but of course this doesn't let you define any interesting f
, since f
doesn't know when it can call the function you pass it, so you would refine it into this:
function method UsablePartialFix(f: (nat --> nat, nat) --> nat, n: nat): nat
requires ???
{
var PartialFix' := (n': nat) requires n' < n => UsablePartialFix(f, n');
f(PartialFix', n)
}
From there on it's mostly equational reasoning:
- You want to be able to call
f
, so you must havePartialFix.requires(f, n) ==> f.requires(PartialFix', n)
- Abstracting over
PartialFix'
to remove the recursion, you wantPartialFix.requires(f, n) ==> forall g | ??? :: f.requires(g, n)
, where???
is a restriction ong
(the stronger the???
the better, because it will lead to weaker restrictions onPartialFix
) - You need to be able to plug
PartialFix'
intog
, so???
can be as strong as therequires
ofPartialFix'
. In other words, the strongest???
can be isforall n' | PartialFix'.requires(n') ==> g.requires(n')
- The
requires
ofPartialFix'
isn' => n' < n
, so the condition simplifies toforall n' | n' < n ==> g.requires(n')
From that you get the final definition:
function method PartialFix(f: (nat --> nat, nat) --> nat, n: nat): nat
requires forall g: nat --> nat, n: nat ::
(forall n': nat | n' < n :: g.requires(n')) ==> f.requires(g, n)
{
var PartialFix' := (n': nat) requires n' < n => PartialFix(f, n');
f(PartialFix', n)
}
This version feels less magical to me. WDYT?
/// | ||
/// Fixpoints are functions combinators such that, if they exist, | ||
/// then we don't need to define recursion or mutual recursion at all, | ||
/// only use fixpoints when we need recursion. |
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.
This is hard to read. I would try to start with something more high-level. Maybe something like the following, but it needs to be revised for clarity:
Mathematical functions on are typically defined by means of an equation that relates the functions inputs and outputs. For example, we may define the functions
plusOne
andabs
by giving the equationsplusOne(n) = n + 1
, orabs(n) == if n >= 0 then n else -n
, for all integersn
.
Sometimes, we want to define a function recursively: in these cases, the function
f
may appear on both side of the equations. For example:
f(n) == if n < 0 then 0 else f(n - 1) + 1
, orf(n) == 2 * n - f(n)
, orf(n) == f(n) + 1
, orf(n) == f(n)
.
When
f
appears only on one side of the equation, then the equation admits just one solution, andf
is unambiguously defined. In other cases, the equation may admit a single solution (as in cases 1 and 2 above, which are equivalent tof(n) = if n < 0 then 0 else n
andf(n) == n
, respectively), or no solutions at all (as in case 3 above), or multiple solutions (as on case 4 above, which is true for all functions).
Fixpoint combinators are classes of solutions to functional equations: given an equation, a fixpoint combinator returns a unique function definition that satisfies this equation, if one exists.
Typically, this is done by describing the equation itself as a function:
eqn := f' => n => if n < 0 then 0 else f'(n - 1) + 1
, oreqn := f' => n => 2 * n - f'(n)
, oreqn := f' => n => f'(n) + 1
, oreqn := f' => n => f'(n)
.
Each of these lines describes how to computef(n)
given a functionf'
to be used for recursive calls and a valuen
.
With these definitions, a fixpoint combinator
FIX
is a function that takes one of theseeqn
s and returns a functionf
such thateqn(f)(n) == f(n)
. In other words,FIX(eqn) == eqn(FIX(eqn))
(hence the name "fixpoint")
As we have seen, not all functional equations have solutions, so
FIX
cannot be defined for all inputs. In this tutorial, we'll see how we can define aFIX
combinator in Dafny that works for all equations that describe functions on natural numbers and that are "well-founded" (all recursive calls on the right of the equation made with integersn'
strictly smaller that the inputn
). This matches the kind of functions that Dafny allows, which means that we will be able to define recursive Dafny functions without explicitly using recursion (!)
/// This is nice, but mathematically speaking, we are still defining a function in terms of itself, | ||
/// which is not obvious. | ||
/// Besides a while loop and a stack to implement recursive functions, | ||
/// there is also another way , using fixpoint combinators. |
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.
This is a bit cryptic. I think it only makes sense if you know the details already.
fixpoint2(comb, n) | ||
} | ||
|
||
/// The signature of this fixpoint combinator could typically be: |
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.
I would start with the curried version (which makes it clear why it's a "fixpoint"), and then introduce the uncurried version
comb(callback, u) | ||
} | ||
|
||
/// So let's fix that. Fix, we need to realize that, in order for fixpoint to finish, we need to |
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.
/// So let's fix that. Fix, we need to realize that, in order for fixpoint to finish, we need to | |
/// So let's fix that. First, we need to realize that, in order for fixpoint to finish, we need to |
Too much fix
! :D
|
||
/// So let's fix that. Fix, we need to realize that, in order for fixpoint to finish, we need to | ||
/// that u' is less than u. But doing so changes the type of the first argument of comb from nat -> nat | ||
/// to nat --> nat (see [arrow subset types](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-arrow-subset-types)) |
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.
Missing backticks in a number of places here
|
||
/// Everything looks great, but when it comes to defining our fibonacci function, things fail | ||
/// It says our `comb` function does not satisfy the subset constraints | ||
/// This is because `comb` is only taking `nat -> nat` as first argument, a total function, |
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.
Missing periods at the end of the entences.
decreases u | ||
{ | ||
var callback := (u': nat) requires u' < u => fixpoint3(comb, u'); | ||
comb(callback, u) |
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.
I'm a bit confused about the names comb
and callback
. Isn't fixpoint
itself the combinator?
This PR adds a tutorial on how to prove that fixpoint combinators can finish in Dafny.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.