[TYPES] A question about unification terminology

[Giuseppe Castagna]

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
rather than existential quantification. That is, roughly,  t≤s holds
if only if tσ≤sσ for all possible substitutions σ, (and not if there
exists a substitution such that tσ=s) (*).
    I cannot remember other works that  make such a distinction, so
if anybody knows some reference please let me know.


(*) actually these substitutions are semantic substitutions in a
particular class of models (these are just technical details: I can
send references to whoever is interested).



Furthermore François suggests that

>
> "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.
>

My point is that in the literature constraint solving may concern other
kinds of constraints (conditionals, universal, ...) while the one I
asked about is a problem onto which seems so easy to stumble that I
thought it should already be given a name by somebody.

Anyhow, thanks again

---Beppe---