The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/28/2016 08:21 AM, Pierre-Marie Pédrot wrote:
> On 28/01/2016 08:40, Guillaume Melquiond wrote:
> > Now I am not saying that there are no models that invalidate functional
> > extensionality. What I am saying is that there are no models of coq's
> > logic that invalidate functional extensionality because of time
> > complexity of functions (that is impossible). So people should just
> > refrain from talking about time complexity whenever the topic of
> > functional extensionality comes around. It is just irrelevant.
> I am actually not quite sure about this stance. Most notably, the
> Dialectica tranlation gives rise to a model of CIC that allows you
> amongst other to count the number of uses of a variable in a function
> and thus breaks functional extensionality, but still interprets
> convertibility as such (modulo some computational implementation of
> multisets). There is an obvious notion of complexity arising from this
> feature, so I would not claim that a first-class notion of « complexity
> » is not achievable in CIC.
>
> PMP

My example of time complexity wasn't intended to imply anything other 
than "some arbitrary interesting property" of functions that would make 
a Coq user not appreciate having functional extensionality forced on 
them by the logic.  Hence, I did not intend to stir up this controversy 
I didn't even know existed.  However, I think we are talking past each 
other in the following way: by "some arbitrary interesting property" of 
a function (and time complexity qualifies), I didn't intend to restrict 
myself to a property that Coq's logic can detect when given the 
functions to analyze.  I was thinking of my own tendency to use Coq to 
develop OCaml functions via extraction.  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.

-- Jonathan