[Agda] «Extensionally but not definitionally equal» — can I say that?

[Thorsten Altenkirch]

How does this matter?

Get Outlook for iOS<https://aka.ms/o0ukef>
________________________________
From: Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis at gmail.com>
Sent: Monday, September 5, 2022 8:35:28 PM
To: Thorsten Altenkirch (staff) <psztxa at exmail.nottingham.ac.uk>
Cc: Ignat Insarov <kindaro at gmail.com>; agda at lists.chalmers.se <agda at lists.chalmers.se>
Subject: Re: [Agda] «Extensionally but not definitionally equal» — can I say that?

I think that one missing piece of information here is that the fact that you cant prove that two things are equal doesnt not mean that they are not equal.

On Mon, Sep 5, 2022 at 12:38 PM Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk<mailto:Thorsten.Altenkirch at nottingham.ac.uk>> wrote:

No you cannot distinguish extensionally equal object in type theory. Otherwise extensionality as provided by cubical agda would be inconsistent. This is a feature, not a bug.



If you want to talk about intensional aspects of functions you need to talk about function codes not functions. That is you need to implement a representation of functions that reveals the intensional aspects you want to talk about. In your case you may want to use a monad (I think it is called the writer monad) which counts the number of steps and then work in this monad.



Cheers,

Thorsten



From: Agda <agda-bounces at lists.chalmers.se<mailto:agda-bounces at lists.chalmers.se>> on behalf of Ignat Insarov <kindaro at gmail.com<mailto:kindaro at gmail.com>>
Date: Saturday, 3 September 2022 at 10:45
To: agda at lists.chalmers.se<mailto:agda at lists.chalmers.se> <agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>>
Subject: [Agda] «Extensionally but not definitionally equal» — can I say that?

Hello!

Suppose I have two definitions of addition — one works on Peano
numbers and the other works in binary representation. Can I express in
Agda that these two definitions are extensionally equal but
definitionally distinct?

Ideally in the future I want to proceed to reasoning about their
asymptotic performance (linear versus logarithmic). So, I want to have
several notions of equality, finer than the commonly postulated
functional extensionality.

The way I imagine this could go is by reifying the definition of said
functions as a syntactic tree or another appropriate encoding of the
way Agda sees them. Then I should say «these two functions are
extensionally equal × their representation as syntactic trees is
distinct». Is this realistic? Are there other approaches?

See also on Zulip:
<https://agda.zulipchat.com/#narrow/stream/238741-general/topic/Extensionally.20but.20not.20definitionally.20equal.20.E2.80.94.20can.20I.20say.20that.3F/near/296889550>
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.





_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220905/3f05359e/attachment-0001.html>