OCaml extraction can generate infinite recursion

[akr]

Version

% coqtop -v
The Coq Proof Assistant, version 8.7.2 (March 2018)
compiled on Mar 13 2018 2:25:05 with OCaml 4.05.0

Operating system

% lsb_release -a   
No LSB modules are available.
Distributor ID:	Debian
Description:	Debian GNU/Linux 9.3 (stretch)
Release:	9.3
Codename:	stretch

Description of the problem

I found that Coq extraction can generate a function
which cause infinite recursion in OCaml.

% coqtop
Welcome to Coq 8.7.2 (March 2018)

Coq < Definition fstarg (x y : bool) := x.
fstarg is defined

Coq < Fixpoint f (z : bool) := fstarg true (f z).
f is defined
f is recursively defined (decreasing on 1st argument)

Coq < Require Extraction.
[Loading ML file extraction_plugin.cmxs ... done]

Coq < Require ExtrOcamlBasic.

Coq < Extraction fstarg.
(** val fstarg : bool -> bool -> bool **)

let fstarg x _ =
  x

Coq < Extraction f.
(** val f : bool -> bool **)

let rec f z =
  fstarg true (f z)

% ocaml
        OCaml version 4.05.0

# let fstarg x _ =
  x  ;;
val fstarg : 'a -> 'b -> 'a = <fun>
# let rec f z =
  fstarg true (f z)  ;;
val f : 'a -> bool = <fun>
# f true;;
Stack overflow during evaluation (looping recursion?).

I think this is dangerous because we can prove (f true) is true in Coq.
But the extracted function is infinite recursion.
I.e. the proof doesn't guarantee the extracted function returns true in OCaml.

Goal (f true) = true.
Proof.
  reflexivity.
Qed.

[akr]

Note that the function causes a problem with cbv, vm_compute, native_compute.

Eval cbv in (f true). (* Stack overflow. *)
Eval vm_compute in (f true). (* Out of memory. *)
Eval native_compute in (f true). (* Stack overflow. *)

So the problem is not only for extraction.

[Zimmi48]

FTR even Eval cbn in (f true). gives a stack overflow, while Eval lazy beta delta iota in (f true). succeeds to evaluate to true.

[cmangin]

This is the same as #6487, which did not get a definitive answer.

[Zimmi48]

If I'm not mistaken this is a known issue, but I don't know if there is already an issue opened for this.
Another similar example is:

Fixpoint f (z : bool) := let x := (f z) in true.

Eval cbv in (f true). (* Stack overflow *)

But in this case Eval cbn in (f true). does succeed.

Anyways, the problem comes from some reduction being performed before the guard condition is checked. I don't remember exactly why it is so but I guess there are good reasons which have prevented people to fix this in the past.

In any case, I acknowledge your problem.

[Zimmi48]

@cmangin You were faster than me :D
Should this issue be closed as a duplicate or kept open because this is indeed a specific problem for extraction? I guess there is no good way to solve this only for extraction so probably it should be closed.

[Zimmi48]

In fact, I closed the previous issue instead because this one explains why this is a problem better.

[cmangin]

I think such definitions should be rejected, which would incidentally remove the problem with extraction.

As for the why, some reduction is performed because there are some definitions like this one which would be rejected without any reduction:

Fixpoint f (n m : nat) {struct} : nat :=
  let g := f O in
  match m with
  | O => O
  | S m' => g m'
  end.

This example is contrived of course, but there are some in the stdlib.
A possible fix (credits to @mattam82) would be to restrict the allowed reductions by forbidding beta and iota reductions which erase their argument. This should be enough to solve this problem, right?

EDIT: see below, I meant zeta indeed :)

[akr]

I think the problem is beta and zeta reduction which erase a term.

If the termination checker checks termination condition of the erased term,
they are acceptable, no need to forbid.

Note that iota reduction also erases a term but I think it is not a problem for
call-by-value evaluation.
But if they are also fixed, Coq may have strong normalization again.

I made a simple example to show that there is an infinite reduction sequence
on a term which subterm is erased by iota reduction (both case and fix).

Fixpoint beta_erase (v:bool) := (fun x y => x) 0 (beta_erase v).

Goal beta_erase true = 0.
Fail cbv. (* Stack overflow. *)
Abort.

Fixpoint zeta_erase (v:bool) := let _ := zeta_erase v in 0.

Goal zeta_erase true = 0.
Fail cbv. (* Stack overflow. *)
Abort.

Fixpoint iota_case_erase (v:bool) :=
  match true with
  | true => 0
  | false => iota_case_erase v
  end.

Goal iota_case_erase true = 0.
cbv delta.
cbv fix; cbv beta.
cbv fix; cbv beta.
cbv fix; cbv beta.
(* infinite reduction sequence... *)
Abort.

Fixpoint iota_fix_erase (v:bool) :=
  let g1 := fix g1 (x : nat) := x
            with g2 (x : nat) := iota_fix_erase v
            for g1
  in
  g1 0.

Goal iota_fix_erase true = 0.
cbv delta.
cbv fix; cbv beta.
cbv fix; cbv beta.
cbv fix; cbv beta.
(* infinite reduction sequence... *)
Abort.

[akr]

Oops. The termination of erased terms by iota reduction must be checked.

In the following example, zeta reduction doesn't erase (f y) but moves it into
the second branch of match.
So, if the erased term by iota reduction (second branch of match) is
not checked, this definition would be accepted.

Fixpoint f (x : bool) :=
  let y := f x in
  match true with
  | true => true
  | false => y
  end.

[herbelin]

Fixed in #15434.