The Coq mailing list

[jean-francois.monin AT imag.fr]

Xavier quoted, from the FAQ :
« Extensionality of functions is an axiom in, say set theory, but from
  a programing point of view, extensionality cannot be a priori accepted
  since it would identify, say programs such as mergesort and
  quicksort. »

The relation with time complexity is not very clear here since
mergesort and quicksort are both O(n*log n) "in most practical
cases". They are just completely different algorithms.

  Jean-Francois Monin

Jason Hickey a ecrit :
 > Xavier Leroy wrote:
 > > So, I don't quite see why functional extensionality "cannot be
 > > accepted from a programming point of view", but the above
 > > identification can...
 > 
 > It does seem strange that the argument against function extensionality 
 > would be based on computational complexity.  Another example might be
 > 
 >     fst (e1, e2) = e1
 > 
 > which "forgets" about an arbitrarily complex computation e2.  However, 
 > if evaluation is lazy then the equivalence does hold (and Xavier's two 
 > power functions are also equivalent).
 > 
 > Function extensionality can of course be very useful.  For example, 
 > suppose we interpret records as functions from labels to values.  The 
 > encoding is elegant and has many nice properties.  Without 
 > extensionality, statements like the following become very tedious to prove.
 > 
 >     { { r with x = 1 } with y = 2 } = { { r with y = 2 } with x = 1 }
 > 
 > I think the user might be unhappy to find that he has to account for the 
 > computational complexity of his record operations.  In any case, I would 
 > expect that there are other arguments against function extensionality.
 > 
 > BTW, Constable and Crary have an explicit account of computational 
 > complexity in type theory:
 > 
 >     Computational Complexity and Induction for Partial Computable
 >     Functions in Type Theory, Constable and Crary, 2002.
 >     http://www.nuprl.org/documents/Constable/01complexity.html
 > 
 > Jason
 > 
 > -- 
 > Jason Hickey                  http://www.cs.caltech.edu/~jyh
 > Caltech Computer Science      Tel: 626-395-6568 FAX: 626-792-4257
 > --------------------------------------------------------
 > 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