The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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

Attachment: signature.asc
Description: OpenPGP digital signature