[TYPES] A question about unification terminology

[Fritz Henglein]

Hi Beppe:

On Wed, Mar 28, 2012 at 3:13 PM, Giuseppe Castagna <gc at pps.jussieu.fr> wrote:
>  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;

I'd call that matching.  Semi-unification is the problem of finding σ
such that tσσ' = sσ for some σ'.
If one defines t <= s if  tσ' = s for some σ', semi-unification is a
particular subtyping relation in the sense you're looking for, since
it is reflextive and transitive:

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

Regards,
Fritz