The optimal fixed point combinator

I developed a new approach to the formalization of recursive and co-recursive functions, called the optimal fixed point combinator. This combinator enables one to non-constructively build the fixed point of any functional in higher-order logic, without specifying neither its domain nor its termination relation at the time of definition. Then, a fixed point equation can be derived through the proof of an equality called contraction condition. Such a condition can be established through conventional interactive proofs that need not involve dependently-typed values.

Optimal fixed points, like greatest fixed points, capture the maximal amount of non-ambiguous information contained in a circular definition. However, greatest-fixed points only apply to domain theory, where one can have equalities of the form "\bottom = F(\bottom)". On the contrary, optimal fixed points are defined and used directly in a logic of total functions. Technically, the optimal fixed point is defined as the generally-consistent fixed point with the largest domain, where "generally consistent" means "consistent with any other fixed point".

The optimal fixed point combinator offers a proper treatment of partial functions, in the sense that domains need not be hardwired in the definitions of functionals (this is similar to Krauss' function package for Isabelle, 2006). The combinator supports higher-order recursion, nested recursion, and recursive calls inside continuations (which Krauss' approach cannot handle). Moreover, the optimal fixed point combinator also supports the definition of co-recursive value and co-recursive functions, as well as of functions mixing recursion with co-recursion. Partial co-recursive functions are here supported directly, whereas in earlier work they needed to be encoded as total functions (Matthews 1999).

This work builds on the notion of optimal fixed point of a recursive program, introduced by Manna and Shamir (1975) and relies on the notion of contraction condition for establishing the existence of a unique fixed point. In this work, I formalized the notion optimal fixed point in Coq and I proposed a unified and generalized presentation of earlier results on contraction conditions (Harrison, 1995, Krstic and Matthews, 2003) and on complete ordered families equivalences, which are used to express contraction conditions for co-fixed point (Matthews, 1999, Di Gianantonio and Miculan 2002). I have shown how the optimal fixed point combinator can be used to relatively easily formalize all the nontrivial examples of recursive and corecursive definitions that have appeared in the litterature.

Publication

The Optimal Fixed Point Combinator

International Conference on Interactive Theorem Proving (ITP), July 2010

paper - abstract - bib - long version

Formal developments

The optimal fixed point combinator is distributed as a Coq library, as part of the TLC library. The formalization of the combinator is accompanied with a collection of example fixed points.

Example: McCarthy's 91 function

This example involves nested recursion and requires the use of an invariant for proving termination. With the Program feature of Coq, the formalization of this function requires assigning it a dependent type capturing its specification. With the optimal fixed point, however, the proofs of termination and of the specification can be conducted through interactive proofs that avoid such technicalities.

Definition F McCarthy n :=
  If n > 100 then n - 10
             else McCarthy (McCarthy (n + 11)).

Definition McCarthy := FixFun F.

Definition McCarthy_inv n r :=
  If n > 100 then r = n - 10 else r = 91.

Lemma McCarthy_fix_post : 
     (forall n, McCarthy n = F McCarthy n)
  /\ (forall n, McCarthy_inv n (McCarthy n)).
Proof.
  sets meas: (fun n => If n > 100 then 0 else 101 - n).
  applys~ (FixFun_fix_inv (measure meas)). introv IH. 
  unfold F. unfold McCarthy_inv. case_if~.
  forwards [K1 K2]: IH (x+11). unfold measure, meas.
  case_if; case_if*. rewrite <- K1 in *. sets y: (f1(x+11)). 
  unfolds in K2. forwards [L1 L2]: IH y. unfold measure, meas. 
  case_if; case_if*. case_if*. rewrite <- L1 in *. 
  sets z: (f1 y). unfolds in L2. split~. case_if*. case_if*.
Qed.

(** Corrolaries *)

Lemma McCarthy_fix : forall n,  McCarthy n = F McCarthy n.
Proof. apply (proj1 (McCarthy_fix_post)). Qed.

Lemma McCarthy_spec_gt100 : forall n,
  n > 100 -> McCarthy n = n - 10.
Proof. intros. destruct (McCarthy_fix_post n). case_if*. Qed.

Lemma McCarthy_spec_le100 : forall n,
  n <= 100 -> McCarthy n = 91.
Proof. intros. destruct (McCarthy_fix_post n). case_if*. Qed.

Example: the filter function on streams

This example is a partial co-recursive function that can make a bounded number of recursive calls before producing a head constructor. Other approaches to formalizing this function require the domain to be hard-wired in the definition. With the optimal fixed point, the domain of the function can be provided after the fact and thus does not pollute the definition.

Definition Filter filter s :=
  let '(x:::t) := s in 
  If P x then x:::(filter t) else (filter t).

Definition filter := FixFunMod (@bisimilar A) Filter.

Lemma filter_fix : forall s,
  infinitely_often P s ->        
  filter s === Filter filter s.  (* stream bisimilarity *)
Proof.
  applys~ (FixFunMod_mixed_partial 
    (stream_family A)  
    (measure (dist_to_next P))
    (infinitely_often P)
    (@bisimilar A)).
  intros i s f1 f2 Ps H. simpls.
  destruct s. simpl. unfolds. destruct i. simple~.
   inverts Ps as Ps' Ev. case_if as C.
     simpl. constructor~. apply~ H. left*.
     inverts Ev as Ev.
       false.
       apply~ H. right. split~. apply~ eventually_dist_cons.
Qed.

Example: a parser with recursive calls in continuations

This example shows an example of recursive calls located inside a closure. Here again, alternative approaches to formal fixed point are not able to accommodate such a definition without polluting it with dynamic tests or dependent types.

Definition arg := (regexp * text * (text -> bool))%type.

Definition Parse (parse : arg -> bool) (p : arg) : bool := 
  let '(r,s,k) := p in
  match r with
  | regexp_null => false
  | regexp_empty => k s
  | regexp_char c => 
     match s with 
     | nil => false
     | c'::s' => If c = c' then k s' else false
     end
  | regexp_alt r1 r2 => parse (r1,s,k) || parse (r2,s,k)
  | regexp_seq r1 r2 => parse (r1,s,(fun s' => parse (r2,s',k)))
  | regexp_star r1 => k s 
                   || parse (r1,s,(fun s' => parse (r,s',k)))
  end.

Definition parse := FixFun Parse.

(** See file [LibFixDemos.v] of the TLC library for the proofs *)

Earlier work: a constructive fixed point combinator

Before developing the optimal fixed point combinator in a non-constructive logic, I had tried to set up a similar combinator but through fully-constructive definitions. The main difference is that one needs to provide, at the time of constructing the fixed point, a well-founded decidable relation. In order to derive the fixed point equation, one needs to consider a particular domain and prove a contraction condition on this domain for the particular well-founded relation used in the definition.

Proof Pearl: A Constructive Fixed Point Combinator for Recursive Functions

Report, March 2009

paper - abstract - bib

A non-constructive fixed point combinator appeared to be more appealing because it does not need to take the termination relation at the time of construction, and because it generalizes to co-recursion and mixed recursion.