headers
Vrijer, R.C. de | 14 Mar 2012 15:44
Picon
Picon

[TYPES] passing away of N.G. de Bruijn

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

Sad to announce the passing away of

N. G. (Dick) de Bruijn                July 9, 1918 - February 17, 2012

We are grateful to this remarkable and inspiring man.
Next to putting his everlasting mark on diverse areas in pure and applied
mathematics, he introduced, in 1967, the pioneering language AUTOMATH
and the idea of automated verification of mathematical proofs after formalization.
This application of type theory and rewriting is both fundamental and high-tech.
The resulting field of formal verification has developed into a major industrial
contribution of mathematics.

Henk Barendregt
Jan Willem Klop
Roel de Vrijer
Permalink | Reply | 0 comments |
headers
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
Permalink | Reply | 0 comments |
headers
Christian Skalka | 28 Mar 2012 20:47
Picon

Re: [TYPES] A question about unification terminology

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

Beppe,

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

In related work, we have been using the terms constraint "closure" and
"consistency" to describe algorithmic techniques for addressing the problem
you describe, which together guarantee the logical property of constraint
"solvability". See especially Section 7 of [skalka-etal-jfp08] (bibtex
below)
which contains pertinent discussion. Note that we use a regular tree
semantics
of (recursive) type constraints in our work, so we are concerned with
*solvability* (proving existence of a solution) rather than obtaining a
solution
in a concrete sense (as with e.g. a unifying substitution). This is because
regular trees may be infinitely large. We adapt this approach
and terminology
from earlier work by Smith et al., especially
[eifrig-etal-mfps95, trifonov-smith-sas96].
(Continue reading)

Permalink | Reply | 0 comments |
headers
Fritz Henglein | 28 Mar 2012 23:09
Picon
Favicon
Gravatar

Re: [TYPES] A question about unification terminology

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

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
Permalink | Reply | 0 comments |
headers
François Fages | 28 Mar 2012 23:16
Picon
Picon
Favicon

Re: [TYPES] A question about unification terminology

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

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,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Giuseppe Castagna | 30 Mar 2012 15:08
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |

Gmane