[Agda] [Open normalization] Re: Pattern matching on irrelevant types with only one constructor?

Thu May 2 10:48:46 CEST 2019

On 2019-05-02 10:40, Andrea Vezzosi wrote:
> Is there an established term for "normalizing in an open context"
> because often I end up saying strong normalization for that, even if
> the part about _every_ reduction path is not quite relevant.

I tend to do the same, using SN for what correctly could be called 
"normalization of open terms" or maybe "open normalization".  But even 
"open terms" is not understood by everyone.

Maybe "normalization under binders" would be an alternative, assuming 
folks know what a "under a binder" means.  But somehow "normalization 
under binders" is too long already.

> On Wed, May 1, 2019 at 4:34 PM Jon Sterling <jon at jonmsterling.com> wrote:
>>
>> Just to clarify, strong normalization (SN) is irrelevant here --- what is relevant is that there exists _some_ normalization strategy. Strong normalization is a property of an abstract rewriting system, a methodology which generally is not even considered for type theories which have strong type-directed equational rules, which tend to disrupt confluence. Modern Swedish-style type theories rely on techniques beyond abstract rewriting systems for their metatheory, and SN is therefore not coming into the picture. It is likely that Agda's core language is normalization in the general sense (there is a way to choose canonical representatives of definitional equivalence classses), and this is really orthogonal to SN/WN/etc (since "normalization" in the sense that I just described can be expressed without even mentioning an abstract rewriting system).
>>
>> To respond to Thorsten's comments a bit further down the thread, I tried really hard to make proof assistants without a complete decision procedure for typing practical, and I determined that it is not likely to work out. Decidable type checking is good.
>>
>> Best,
>> Jon
>>
>>
>> On Wed, May 1, 2019, at 6:33 AM, Jesper Cockx wrote:
>>> Well, if we don't have strong normalization we also lose decidability
>>> of typechecking, which is kind of an important design goal of Agda IMO.
>>>
>>> -- Jesper
>>>
>>> On Wed, May 1, 2019 at 12:17 PM Thorsten Altenkirch
>>> <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>>>> I am just wondering with normalisation under inconsistent assumptions is such an important feature? Is this the only thing that goes wrong?____
>>>
>>>> __ __
>>>
>>>> Thorsten____
>>>
>>>> __ __
>>>
>>>> *From: *Agda <agda-bounces at lists.chalmers.se> on behalf of Jesper Cockx <Jesper at sikanda.be>
>>>> *Date: *Wednesday, 1 May 2019 at 08:48
>>>> *To: *Matthew Daggitt <matthewdaggitt at gmail.com>
>>>> *Cc: *Agda mailing list <agda at lists.chalmers.se>
>>>> *Subject: *Re: [Agda] Pattern matching on irrelevant types with only one constructor?____
>>>
>>>> __ __
>>>
>>>> Hi Matthew,____
>>>
>>>> __ __
>>>
>>>> In our paper on definitional proof irrelevance (https://hal.inria.fr/hal-01859964) we give a criterion for when it is allowed to pattern match on an irrelevant argument. As we argue in the paper, the condition that the datatype has a single constructor is neither sufficient nor necessary. The criterion we give is not yet implemented in Agda, but I hope to add it in the not-too-distant future (it depends on my PR https://github.com/agda/agda/pull/3589 being merged first). Unfortunately, the Acc datatype does not satisfy this criterion. In fact, allowing pattern matching on irrelevant Acc would break strong normalization of the theory, as you can always have an absurd hypothesis of type Acc but evaluation would not be blocked on this argument because it's irrelevant. So the best you can do is get propositional (instead of definitional) irrelevance by proving irrelevance of Acc by hand (or postulate it).____
>>>
>>>> __ __
>>>
>>>> A historical note: Agda used to allow matching on single-constructor datatypes under the --experimental-irrelevance flag, but this was completely broken so I decided to remove it last year (https://github.com/agda/agda/commit/b5f8b509bbe362c4bbb14612a6666e720cabf26a)____
>>>
>>>> __ __
>>>
>>>> -- Jesper____
>>>
>>>> __ __
>>>
>>>> On Wed, May 1, 2019 at 8:33 AM Matthew Daggitt <matthewdaggitt at gmail.com> wrote:____
>>>
>>>>>   In the Agda  documentation <https://agda.readthedocs.io/en/v2.6.0/language/irrelevance.html> it is pretty clear that the only time you can pattern match against irrelevant arguments is when the type is empty. My own reasoning for this has always been that this is to stop decisions being made depending on the result of the pattern match. This leads me to wonder if there are any theoretical reasons why it's not possible to also mark a type irrelevant when it only has a single constructor?____
>>>
>>>>> __ __
>>>
>>>>> Consider the motivating example below. Clearly the `Acc` argument is never actually used in the computation of the final value, and no decisions can be based on its value as it only has a single constructor. It seems like it should be possible to mark it irrelevant. If this were possible then we would immediately get rid of a whole bunch of annoying congruence lemmas.____
>>>
>>>>> ```____
>>>
>>>>> gcd : (m n :  ℕ) → Acc _<_ m → n < m → ℕ____
>>>
>>>>> gcd m zero _ _ = m____
>>>
>>>>> gcd m (suc n) (acc rec) n<m = gcd′ (suc n) (m % suc n) (rec _ n<m) (a%n<n m n)____
>>>
>>>>> ```____
>>>
>>>>> Many thanks,____
>>>
>>>>> Matthew____
>>>
>>>>> _______________________________________________
>>>>>   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
> 