Giuseppe Castagna | 28 Mar 2012 15:13
Picon

[TYPES] A question about unification terminology

[ 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

Gmane