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

Tue Sep 6 13:37:53 CEST 2022

Yes, Nicolai, that is a very good explanation.

On Tue, Sep 6, 2022 at 2:29 PM Tarik ÖZKANLI <tozkanli2023 at gmail.com> wrote:

> Hi,
>
> Is it possible to think about a formal system in which one can develop its
> own notion of equality across object level & higher levels?
>
> Best Regards.
>
> Tarik
>
> On Tue, 6 Sept 2022 at 14:06, Nicolai Kraus <nicolai.kraus at gmail.com>
> wrote:
>
>> 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.
>> 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.
>> Nicolai
>>
>>
>>
>> On Tue, Sep 6, 2022 at 11:45 AM Apostolis Xekoukoulotakis <
>> apostolis.xekoukoulotakis at gmail.com> wrote:
>>
>>> 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)
>>>
>>> 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.
>>>
>>> Thus we would be able to show that a function f is intensionally
>>> distinct with itself.
>>>
>>>
>>> On Tue, Sep 6, 2022 at 12:36 AM Thorsten Altenkirch <
>>> Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>>>
>>>> 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> 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> on behalf of Ignat
>>>> Insarov <kindaro at gmail.com>
>>>> *Date: *Saturday, 3 September 2022 at 10:45
>>>> *To: *agda at lists.chalmers.se <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
>>>> 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
>>>> 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
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220906/bee7af66/attachment.html>