<div dir="ltr">Hi,<div><br></div><div>Is it possible to think about a formal system in which one can develop its own notion of equality across object level & higher levels?</div><div><br></div><div>Best Regards.</div><div><br></div><div>Tarik</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 6 Sept 2022 at 14:06, Nicolai Kraus <<a href="mailto:nicolai.kraus@gmail.com">nicolai.kraus@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Apostolis, what you wrote is right, but here's how I suggest looking at this: There are two levels, the object theory and the meta-theory. In our case, the object theory is Agda. Everything you implement lives on that level. The meta-theory is the level "above" (say, the level at which we live), which allows you to reason about how Agda behaves. "Definitionally equal" and "type-checks" are concepts of the meta-level. The object theory doesn't know about them and can't talk about them. Thus, the object theory can't say whether two implementations are definitionally distinct.<div>Thorsten's solution essentially shifts everything by one level. The function codes become the new "object level", and Agda can now serve as meta-theory to that new level. That's why Agda can suddenly talk about intensional features of the addition function codes.<br></div><div>Nicolai</div><div><br><div><div><br></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 6, 2022 at 11:45 AM Apostolis Xekoukoulotakis <<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>I was thinking that something that can not be shown definitionally equal by the type checker does not tell us anything about whether it is propositionally equal or not. ( I was assuming that this would be the way to encode "definitional" equality in Agda)<br></div><div><br></div><div>But now I understand your point. Any data structure that would indicate that two functions are intensionally distinct would be impossible since extensionally equal functions are equal in cubical theory.</div><div><br></div><div>Thus we would be able to show that a function f is intensionally distinct with itself.<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 6, 2022 at 12:36 AM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<div>
<div>
<div dir="ltr">How does this matter?</div>
</div>
<div id="gmail-m_-5717094920792596147m_-3724275545374116398m_8699128748558656276ms-outlook-mobile-signature">
<div><br>
</div>
Get <a href="https://aka.ms/o0ukef" target="_blank">Outlook for iOS</a></div>
</div>
<hr style="display:inline-block;width:98%">
<div id="gmail-m_-5717094920792596147m_-3724275545374116398m_8699128748558656276divRplyFwdMsg" dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> Apostolis Xekoukoulotakis <<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>><br>
<b>Sent:</b> Monday, September 5, 2022 8:35:28 PM<br>
<b>To:</b> Thorsten Altenkirch (staff) <<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>><br>
<b>Cc:</b> Ignat Insarov <<a href="mailto:kindaro@gmail.com" target="_blank">kindaro@gmail.com</a>>; <a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a> <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject:</b> Re: [Agda] «Extensionally but not definitionally equal» — can I say that?</font>
<div> </div>
</div>
<div>
<div dir="ltr"><i>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.</i><br>
</div>
<br>
<div>
<div dir="ltr">On Mon, Sep 5, 2022 at 12:38 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br>
</div>
<blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<div lang="EN-GB">
<div>
<p><span>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.<u></u><u></u></span></p>
<p><span><u></u> <u></u></span></p>
<p><span>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.
<u></u><u></u></span></p>
<p><span><u></u> <u></u></span></p>
<p><span>Cheers,<u></u><u></u></span></p>
<p><span>Thorsten<u></u><u></u></span></p>
<p><span><u></u> <u></u></span></p>
<div style="border-color:rgb(181,196,223) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm">
<p style="margin-right:0cm;margin-bottom:12pt;margin-left:36pt">
<b><span style="font-size:12pt;color:black">From: </span></b><span style="font-size:12pt;color:black">Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Ignat Insarov <<a href="mailto:kindaro@gmail.com" target="_blank">kindaro@gmail.com</a>><br>
<b>Date: </b>Saturday, 3 September 2022 at 10:45<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a> <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>[Agda] «Extensionally but not definitionally equal» — can I say that?<u></u><u></u></span></p>
</div>
<div>
<p style="margin-left:36pt">Hello!<br>
<br>
Suppose I have two definitions of addition — one works on Peano<br>
numbers and the other works in binary representation. Can I express in<br>
Agda that these two definitions are extensionally equal but<br>
definitionally distinct?<br>
<br>
Ideally in the future I want to proceed to reasoning about their<br>
asymptotic performance (linear versus logarithmic). So, I want to have<br>
several notions of equality, finer than the commonly postulated<br>
functional extensionality.<br>
<br>
The way I imagine this could go is by reifying the definition of said<br>
functions as a syntactic tree or another appropriate encoding of the<br>
way Agda sees them. Then I should say «these two functions are<br>
extensionally equal × their representation as syntactic trees is<br>
distinct». Is this realistic? Are there other approaches?<br>
<br>
See also on Zulip:<br>
<<a href="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" target="_blank">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</a>><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><u></u><u></u></p>
</div>
</div>
<pre>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.
</pre>
</div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</blockquote>
</div>
</div>
<pre>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.
</pre></div>
</blockquote></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>