The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

The comparision between quicksort and bubblesort is often
used to illustrate the fact that sometimes one may want to stick
to an intentional view.

Now, how different are quicksort and bubblesort in Coq ?

* You can run them in Coq, and you will observe different
  running times.

* You cannot prove they are different, since this would
  negate the extentionality axiom for functions, which is
  validated in the simple set-theoretical model.
   (\forall x, f x = g x => f=g )


* With some work, you can formalize a programming language
  in Coq (deep embeding) and prove that quicksort corresponds
  to quicksort in this encoded language and that bubblesort is
  indeed bubblesort. However, you will not be able to prove
  that quicksort is *not* bubblesort, although it is of course not
  provable. So you can build a predicate distinguishing
  between your two programs, but you cannot prove that it
  actually distinguishes them.

  That is we can define a predicate is_quicksort, s.t.

   is_quicksort(quicksort)  provable
   is_quicksort(bubble)  not provable

but

  not(is_quicksort(bubble)) is not provable either


Hope this helps,


Benjamin



Le 7 août 06 à 23:28, Stefan Karrmann a écrit :

> roconnor AT theorem.ca
>  (Mon, Aug 07, 2006 at 03:32:14AM -0400):
> > On Mon, 7 Aug 2006, Fabrice Lemercier wrote:
> > > > You cannot. Eta allows you to identify very similar
> > > > functions but not,
> > > > say, quicksort and bubble sort.
>
> How do we get in Coq a difference between quicksort and bubble sort?
> We cannot observe the runtime of these functions. (Neither the  
> number of
> reductions, matches or applies.)
>
> In Coq you can only compare the values of the applied functions. -  
> These
> are equal, i.e. forall x. quicksort x = bubble_sort x.
>
> > > What about the following argument taken from
> > > Wikipedia?
> > >
> > > if  f a==g a  for all lambda expressions a, then in
> > > particular by taking a to be a variable x not
> > > appearing free in f nor g we have  f x == g x  and
> i.e. forall x. (f x == g x)
> > > hence  ? x. f x == ? x. g x,  and so by eta-conversion
> > > f == g.
>
> Regards,
> --
> Stefan Karrmann
>
> I didn't get sophisticated -- I just got tired.  But maybe that's what
> sophisticated is -- being tired.
>                 -- Rita Gain
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club