The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I think the compiler should be free to replace subterms with definitionally equal ones because Coq programs/proofs cannot make any distinction finer than definitional equality. However, is it possible to build a compiler that optimally exploits this freedom?

More concretely, has there been work on the theoretical/practical feasibility of finding a "best" definitionally-equal sibling of a given Coq term?

I understand that defining "best" in a useful way may be challenging. 

In Guillaume's example below, f2 is clearly better for anyone interested in running their Coq programs.

To begin with, I am curious about the case where a term x is better than y iff when applied to 0 or more arguments of the right types, x takes fewer or same # of steps to achieve a weak-head normal form under call-by-need (lazy) evaluation.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Jan 28, 2016 at 11:58 AM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> 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