General recursive functions

This file explores a way to formalize general recursive functions without worrying about termination proofs, counters or monads.
The definitions are actually defined by well-founded recursion on the total relation (which isn't well-founded). Using fueling of the accessibility proof, we can however compute with these definitions inside Coq and reason on them independently of the termination proof.


The total relation.
Definition total_relation {A : Type} : A → A → Prop := fun x y ⇒ True.

We assume an inconsistent axiom here, one should be added function per function.
Axiom wf_total_init : ∀ {A}, WellFounded (@total_relation A).
#[local]
Remove Hints wf_total_init : typeclass_instances.

We fuel it with some Acc_intro constructors so that definitions relying on it can unfold a fixed number of times still.
#[local]
Instance wf_total_init_compute : ∀ {A}, WellFounded (@total_relation A).
  exact (fun A ⇒ Acc_intro_generator 10 wf_total_init).
Defined.

Now we define an obviously non-terminating function.
Equations? nonterm (n : nat) : nat by wf n (@total_relation nat) :=
  nonterm 0 := 0;
  nonterm (S n) := S (nonterm (S n)).
Proof.
  (* Every pair of arguments is in the total relation: so
     total_relation (S n) (S n) *) red.
  constructor.
Defined.
  Obligation Tactic := idtac.
The automation has a little trouble here as it assumes well-founded definitions implicitely. We show the second equation: nonterm (S n) = S (nonterm (S n)) using the unfolding equation.
  Next Obligation.
    intros. now rewrite nonterm_unfold_eq at 1.
  Defined.

  (* Note this is a dangerous rewrite rule, so we should remove it from the hints *)
  (* Print Rewrite HintDb nonterm. *)

Make nonterm transparent anyway so we can compute with it
  Transparent nonterm.

We can compute with it (for closed natural numbers)
Definition at_least_five (n : nat) : bool :=
  match n with
  | S (S (S (S (S x)))) ⇒ true
  | _ ⇒ false
  end.

Transparent wf_total_init_compute.

Indeed it unfolds enough so that at_least_five gives back a result.

Example check_10 := eq_refl : at_least_five (nonterm 10) = true.
Example check_0 := eq_refl : at_least_five (nonterm 0) = false.

The elimination principle completely abstracts away from the termination argument as well
Lemma nonterm_ge n : n ≤ nonterm n.
Proof.
  funelim (nonterm n).
  reflexivity.
  lia.
Defined.

We can go as far as defining the (call-by-name) Y combinator and computing with it.
Section Y.
  Context {A : Type}.
  Equations? Y (f : A → A) : A by wf f (@total_relation (A → A)) :=
  Y f := f (Y f).
  Proof.
    (* Every pair of arguments is in the total relation: so
     total_relation f f *) red. constructor.
  Defined.

  Obligation Tactic := idtac.
The automation has a little trouble here as it assumes well-founded definitions implicitely. We show the second equation: nonterm (S n) = S (nonterm (S n)) using the unfolding equation.
  Next Obligation.
    intros. now rewrite Y_unfold_eq at 1.
  Defined.
End Y.

Using Y, we can easily define any general recursive function.
Definition fact :=
  Y (fun (fact : nat → nat) (x : nat) ⇒
       match x with
       | 0 ⇒ 1
       | S n ⇒ S n × fact n
       end).
Check eq_refl : fact 8 = 40320.

Y is only good in call-by-name or call-by-need, so we switch to Haskell

Extraction Language Haskell.
Recursive Extraction fact.

(*
y :: (a1 -> a1) -> a1
y x =
  x (y x)

fact :: Nat -> Nat
fact =
  y (\fact0 x -> case x of {
                  O -> S O;
                  S n -> mul (S n) (fact0 n)})

*)

Let's define an efficient version whose termination is not entirely obvious.
Definition factN :=
  Y (fun (fact : N → N) (x : N) ⇒
       match x with
       | N0 ⇒ 1%N
       | Npos n ⇒ (Npos n × fact (Pos.pred_N n))%N
       end).

1001! is pretty large.
Definition fact1001 :=
 402789647337170867317246136356926989705094239074925347176343710340368450911027649612636252695456374205280468598807393254690298539867803367460225153499614535588421928591160833678742451354915921252299285456946271396995850437959540645019696372741142787347450281325324373824456300226871609431497826989489109522725791691167945698509282421538632966523376679891823696900982075223188279465194065489111498586522997573307838057934994706212934291477882221464914058745808179795130018969175605739824237247684512790169648013778158661520384916357285547219660337504067910087936301580874662367543921288988208261944834178369169805682489420504038334529389177845089679546075023305854006141256288633820079940395329251563788399404652902154519302928365169452383531030755684578503851488154092323576150311569325891190105926118761607100286827930472944913272420825078912158741589850136017030887975452922434889688775883386977825215904423682478943313806072144097432418695807412571292308739802481089407002523955080148184062810447564594783139830113821372260474145316521647368313934670783858482781506915288378941348078689691815657785305896912277993200639858696294199549107738635599538328374931258525869323348477334798827676297868823693023377418942304272267800509765805435653787530370118261219994752588866451072715583785495394684524593296728611334955079882857173250037068541860372512693170819259309411027837176612444692649174536429745421086287708588130082168792750697158901737130221751430550976429258055277255676893874108456870904122902259417224707137723406125811549952159629766771063079472679280213882978523785424760309678138268708239764925768714349554665438389311198715040908077757086900159389712443987670244241787904585093011546861502058550090914877900852701619648229332192401075747543562989953271508977501771085759521631427816116191761031257454497039673414248149210836002497114107565960458576525212556159634975715552638678172137468172843066451093984443636560722213668172225585711566558134467392654185460222589723312097599987253417831473939565071006344352518096564427781204200068323913056897090916602712260306869786107237077572445866572945760977721639408338430009976028970539150822336553856613962747814621747092348996915755983464741082000337526945990059365493439921937093368896754791416759604324895514660325913157843796039917819613717350380997781225472000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000%N.

We can still compute with our Y combinator
Time Check (@eq_refl _ (fact1001) <: factN 1001 = fact1001).

It takes 0.8sec using vm_compute.
An alternative is to use the total relation directly.

Equations factN' (n : N) : N by wf n (@total_relation N) :=
| N0 ⇒ 1;
| Npos n ⇒ (Npos n × factN' (Pos.pred_N n)).
Next Obligation. constructor. Defined.

Unsurprisingly, this computes just as well

Time Check (@eq_refl _ (fact1001) <: factN' 1001 = fact1001).

It takes 0.8sec using vm_compute as well.
factN' also makes sense in a strict/call-by-value language like OCaml.

Extraction Language OCaml.
Extraction factN'.

(*

(** val factN' : n -> n **)

let rec factN' = function
| N0 -> Npos XH
| Npos p -> N.mul (Npos p) (let y = Pos.pred_N p in factN' y)

*)
This page has been generated by coqdoc