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

[Víctor López Juan]

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?

— 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