Chore: Tutorial on proven fixpoints combinators

[MikaelMayer]

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.

[cpitclaudel]

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:

1. You want to be able to call f, so you must have PartialFix.requires(f, n) ==> f.requires(PartialFix', n)
2. Abstracting over PartialFix' to remove the recursion, you want PartialFix.requires(f, n) ==> forall g | ??? :: f.requires(g, n), where ??? is a restriction on g (the stronger the ??? the better, because it will lead to weaker restrictions on PartialFix)
3. You need to be able to plug PartialFix' into g, so ??? can be as strong as the requires of PartialFix'. In other words, the strongest ??? can be is forall n' | PartialFix'.requires(n') ==> g.requires(n')
4. The requires of PartialFix' is n' => n' < n, so the condition simplifies to forall 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?

[cpitclaudel]

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 and abs by giving the equations plusOne(n) = n + 1, or abs(n) == if n >= 0 then n else -n, for all integers n.

Sometimes, we want to define a function recursively: in these cases, the function f may appear on both side of the equations. For example:

1. f(n) == if n < 0 then 0 else f(n - 1) + 1, or
2. f(n) == 2 * n - f(n), or
3. f(n) == f(n) + 1, or
4. f(n) == f(n).

When f appears only on one side of the equation, then the equation admits just one solution, and f is unambiguously defined. In other cases, the equation may admit a single solution (as in cases 1 and 2 above, which are equivalent to f(n) = if n < 0 then 0 else n and f(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:

1. eqn := f' => n => if n < 0 then 0 else f'(n - 1) + 1, or
2. eqn := f' => n => 2 * n - f'(n), or
3. eqn := f' => n => f'(n) + 1, or
4. eqn := f' => n => f'(n).
   Each of these lines describes how to compute f(n) given a function f' to be used for recursive calls and a value n.

With these definitions, a fixpoint combinator FIX is a function that takes one of these eqns and returns a function f such that eqn(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 a FIX 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 integers n' strictly smaller that the input n). 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 (!)

[cpitclaudel]

This is a bit cryptic. I think it only makes sense if you know the details already.

[cpitclaudel]

I would start with the curried version (which makes it clear why it's a "fixpoint"), and then introduce the uncurried version

[cpitclaudel]

Suggested change

	/// 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

[cpitclaudel]

Missing backticks in a number of places here

[cpitclaudel]

Missing periods at the end of the entences.

[cpitclaudel]

I'm a bit confused about the names comb and callback. Isn't fixpoint itself the combinator?