The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/28/2016 11:58 AM, Guillaume Melquiond wrote:
> On 28/01/2016 17:15, Jonathan Leivent wrote:
>
> > If the output of extraction
> > from two extensionally-equivalent functions would behave differently in
> > OCaml, then I would prefer that they are not treated within Coq as
> > substitutionally identical.
> But that is already the case, even without any functional extensionality!
>
> Axiom g : nat -> nat -> nat.
> Fixpoint f1 (n : nat) :=
>    match n with S n => g (f1 n) (f1 n) | O => g O O end.
> Fixpoint f2 (n : nat) :=
>    match n with S n => let v := f2 n in g v v | O => g O O end.
> Goal f1 = f2. reflexivity. Qed.
>
> While f1 and f2 are convertible, their behavior is entirely different
> when extracted to Ocaml. One performs an exponential number of calls to
> g, the other one is only linear. Sure, you could devise an Ocaml
> optimization so that f1 also has linear complexity once compiled. But
> where do you set the limit of what a compiler is allowed to?
>
> Best regards,
>
> Guillaume

What's funny about this is that initially in my reply I had the 
parenthetical "(modulo reduction)", and then removed it just before 
hitting send ;)

-- Jonathan