[TYPES] A question about unification terminology

[Christian Skalka]

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

-chris

@ARTICLE{skalka-etal-jfp08,
  AUTHOR = {Christian Skalka and Scott Smith and David Van Horn},
  TITLE = {\textcolor{navy}{Types and Trace Effects of Higher Order
  Programs}},
  YEAR = {2008},
  VOLUME = 18,
  NUMBER = 2,
  PAGES = {179-249},
  JOURNAL = {Journal of Functional Programming},
  PDF = {
http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-vanhorn-jfp07.pdf}}

@InProceedings{trifonov-smith-sas96,
  author       = "Valery Trifonov and Scott Smith",
  title        = "Subtyping Constrained Types",
  booktitle    = "Proceedings of the Third International Static Analysis
                 Symposium",
  series       = "LNCS",
  volume       = "1145",
  pages        = "349--365",
  year         = "1996",
  month        = sep,
  publisher    = "SV",
  note         = "\url{http://rum.cs.yale.edu/trifonov/papers/subcon.ps.gz
}",
}

@InProceedings{eifrig-smith-trifonov-94,
  author       = "Jonathan Eifrig and Scott Smith and Valery Trifonov",
  title        = "Type Inference for Recursively Constrained Types and
                 its Application to {OOP}",
  booktitle    = "Mathematical Foundations of Programming Semantics, New
                 Orleans",
  series       = "Electronic Notes in Theoretical Computer Science",
  publisher    = "Elsevier",
  volume       = "1",
  year         = "1995",
  note         = "\url{http://www.elsevier.nl/locate/entcs/volume1.html}",
}



>
>
> Beppe
>



-- 
Christian Skalka
Associate Professor
Department of Computer Science
University of Vermont
http://www.cs.uvm.edu/~skalka