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

[Víctor López Juan]

Den 2020-08-31 kl. 21:09, skrev Frédéric Blanqui:
 > Well, modulo the definitions of addition and multiplication on natural
 > numbers, some polynomials have several solutions.

I see! This got me thinking.

I think that those cases where this would be an issue are outside the 
scope of what the Agda unifier tries to achieve. Here is some detailed 
analysis for the setting you mention, with polynomials on the natural 
numbers:

--------

Take a constraint · ⊢ p ?α ≈ q ?α : Nat, where p and q are polynomials, 
and ?α is a metavariable of type Nat. After normalizing both sides of 
the constraint, there are six possibilities:

(i) p and q are constants. Then the constraint does not give information 
about (?α).

(ii) both sides are headed by a suc contructor.
E.g. · ⊢ suc (p ?α) ≈ suc (q ?α) : Nat. Then the suc constructor can be 
removed.

(iii) Both sides are headed by a incompatible constructors.
E.g. · ⊢ suc (p ?α) ≈ zero : Nat. Then the constraint has no solution.

(iv) one of p or q is the identity, and the other is a constant.
E.g · ⊢ ?α ≈ 2 : Nat. Then the constraint can be solved, as it
is in the pattern fragment.

(v) p or q is the identity, the other is a function of (?α)
E.g · ⊢ ?α ≈ ?α * ?α : Nat.
Then the constraint does not pass the occurs check, as the head 
metavariable of the LHS (?α) occurs rigidly on the RHS. Therefore Agda 
will not use this constraint to gain information about ?α.

(vi) Either p or q are non-trivial polynomials.
E.g · ⊢ ?α * 1 ≈ ?α * ?α : Nat (with multiplication defined by recursion 
on the first argument).
Then at least one of the sides is an irreducible term, but which could 
possibly reduce if ?α were  to be instantiated. That is, it is not a 
"strongly neutral" term. Agda will thus not use this constraint to glean 
information about ?α.

---

To sum up, the equational theory behind the user-defined functions 
should not affect uniqueness, as those constraints with terms that could 
reduce after a metavariable instantiation will not be used in order to 
obtain solutions.

(There is some form of injectivity analysis of user definitions which 
may allow more constraints to be used, but this does not change the 
general picture).

— Víctor

Den 2020-08-31 kl. 21:09, skrev 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