[TYPES] A question about unification terminology

[François Fages]

Hi Beppe

"finding a substitution σ such that tσ≤sσ where ≤ denotes a generic 
subtyping relation"
is indeed the problem of solving subtyping constraints over (type) terms,
just like unification is the problem of solving equality constraints 
over terms.
To my opinion, there should not be specific names.

We studied this problem in a slightly more general setting than lattices in:
<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/c/Coquery:Emmanuel.html>Emmanuel 
Coquery, François Fages: Subtyping Constraints in Quasi-lattices.
FSTTCS 2003 
<http://www.informatik.uni-trier.de/%7Eley/db/conf/fsttcs/fsttcs2003.html#CoqueryF03>: 
136-148. Springer-Verlag. LNCS 2914. December 2003.
Complete version available as INRIA research report RR4926 ps 
<http://contraintes.inria.fr/%7Efages/Papers/cf03tr.ps>.

Best

François


Giuseppe Castagna a écrit :
> [ The Types Forum, 
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear Typers,
>
>   the problem of finding a substitution σ such that tσ=sσ is called 
> unification;
>
>   the problem of finding a substitution σ such that tσ=s is called 
> semi-unification;
>
>   but how is it called the problem of finding a substitution σ such 
> that tσ≤sσ where ≤ denotes a generic subtyping relation?
>
> I found in the literature the generic name of "subtype constraint 
> resolution" (e.g., Pottier) but I was wondering whether there exists a 
> more specific name.
>
> Thanks in advance for your answers and pointers to related work.
>
>
> Beppe