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

[Tarik ÖZKANLI]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220906/cc3ef192/attachment-0001.html>