[Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]

[Frédéric Blanqui]

Le 31/08/2020 à 11:44, Víctor López Juan a écrit :
> Hi Frédéric,
>
> I hope someone comes up with a better reference for this…
>
> As far as I know, there are two works which also address the issue of 
> "recursive" functions on Booleans.
>
> - Adam Gundry's PhD thesis (§4.2.5, ¶"Rigid-rigid decomposition"; see 
> also Figure 4.12) [1], which considers the issue in a setting where 
> terms are fully normalized, the recursor on Booleans is an eliminator, 
> and terms contain twin variable annotations to facilitate dynamic 
> pattern unification.
>
> - My own licentiate thesis (§4.5.8) [2], building upon the former and 
> with a theory which is closer to Agda, but relies on inconsistent 
> assumptions (Type : Type). The formulation of uniqueness (here, 
> completeness of rules) is done using the usual judgmental equality.
>
> As noted, both differ somewhat from the variant MLTT used in Agda.
>
> I wish I could be of more help.
>
> But, do you have some way in mind in which user recursive definitions 
> could affect uniqueness?
>
Well, modulo the definitions of addition and multiplication on natural 
numbers, some polynomials have several solutions.

Thank you for your interesting references anyway.

Best regards,

Frédéric.


> — Víctor
>
> [1]: 
> https://adam.gundry.co.uk/pub/thesis/thesis-2013-12-03.pdf#subsection.4.2.5
> [2]: https://lopezjuan.com/project/licentiate/licentiate-printer.pdf#42
>
> Den 2020-08-28 kl. 14:24, skrev Frédéric Blanqui:
>> Thank you for these references.
>>
>> However, if I understand correctly, in both cases, it is about 
>> unification in LF modulo beta, eta and projections only. So, this 
>> does not include user recursive definitions...
>>
>>
>> Le 27/08/2020 à 11:55, Víctor López Juan a écrit :
>>> Den 2020-08-25 kl. 15:36, skrev Neel Krishnaswami:
>>> >
>>> > I didn't know that solutions remained unique even if you solved
>>> > constraints lazily. Is there a reference for this?
>>>
>>> Den 2020-08-25 kl. 14:54, skrev Frédéric Blanqui:
>>>>
>>>> Le 25/08/2020 à 12:49, András Kovács a écrit :
>>>>> Frédéric: by solving only pattern unification problems, which have 
>>>>> definitionaly unique solutions,
>>>>
>>>> Could you provide a reference please?
>>>
>>> A good one would be Jason Reed's 2009 paper [1], which shows this 
>>> for the λΠ calculus.
>>> Andreas Abel and Brigitte Pientka generalize it to the λΠΣ calculus 
>>> [2].
>>>
>>> [1]: https://www.cs.cmu.edu/~jcreed/papers/lfmtp2009.pdf
>>> [2]: https://link.springer.com/chapter/10.1007/978-3-642-21691-6_5