Re: [TYPES] A question about unification terminology

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I want to thank François Fages, Christian Skalka, Paweł Urzyczyn and
Fritz Henglein for their answers, references, and corrections [I love
the types-list]

As they pointed me:

>> the problem of finding a substitution σ such that tσ=s is NOT
>> called semi-unification but matching. Semi-unification is to find σ
>> such that tσ matches sσ, i.e. there is another substitution σ' with
>> tσσ'=sσ.

For what concerns the problem I asked about:

>> how is it called the problem of finding a substitution σ such that
>> tσ≤sσ where ≤ denotes a generic subtyping relation?

Paweł wrote:

> If you write ≤ for matching that would be semi-unification. But I
> guess you mean other kinds of subtyping.

Indeed. I am finishing to write a paper on type inference for
polymorphic higher-order functions with union, intersection and negation
types where instantiation and subsumption are kept separated. I use the
subtyping relation to define and subsume intersections, unions and
negations of types while the polymorphic variables have a specific
instantiation rule. So ≤ denotes just "classic" monomorphic type
containment and it is extended to polymorphic types by a universal