The Coq mailing list

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

On 13/09/2016 20:21, Maxime Dénès wrote:
> Yes, but I don't see any link between complexity and functional
> extensionality since convertible functions (without fun ext) can already
> have different complexity classes.

To keep repeating myself on this topic each time this question is raised
on Coq-club, there exists a model of type theory that negates functional
extensionality by giving you a way to count the uses of a variable (to
be understood in a CBN semantics). And yes, risking to sound monomoniac,
that is the Dialectica translation.

It's not quite a theory of complexity yet, but I believe that if you can
count the uses of something, you're not far from it.

I think that the misunderstanding about this stems from the fact that we
consider complexity on open terms, so that full reduction of the body of
a function is not relevant (that's O(1), otherwise said).

Cheers,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature