The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

What about the following two functions (in mathematical notation)?

f : N -> N
f(n) = 0

g : N -> N
g(n) = 10^10 - 10^10

They are definitionally equal, yet I assume that after extraction f
will run much faster than g unless the extraction process optimizes
the definition of g (actually, looking at the doc it seems that it
does optimize g, but the command "Unset Extraction Optimize" disables
this optimization. It’s kind of cheating to optimize g :-) )

2016-01-28 18:11 GMT+01:00 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
>