Subtyping Functional+Nonempty Record Types

Vorobyov, Sergei

Local TagsRelease HistoryDetailsSummary

Subtyping Functional+Nonempty Record Types

Vorobyov, S. (1999). Subtyping Functional+Nonempty Record Types. In G. Gottlob, E. Grandjean, & K. Seyr (Eds.), Proceedings of the 12th International Workshop on Computer Science Logic (CSL-98), Annual Conference on the EACSL (pp. 285-297). Berlin, Germany: Springer.

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3699-E Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-369B-A

Genre: Conference Paper

Files

show Files

hide Files

:

csl98-final.ps (Any fulltext), 197KB

File Permalink:
-

Name:
csl98-final.ps

Description:
-

OA-Status:

Visibility:
Private

MIME-Type / Checksum:
application/postscript

Technical Metadata:

Copyright Date:
-

Copyright Info:
-

License:
-

Locators

show

Creators

show

hide

Creators:
Vorobyov, Sergei^{1, 2}, Author

Affiliations:
1Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society, ou_40046
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Content

show

hide

Free keywords: -

Abstract: \begin{abstract} \emph{Solving systems of subtype constraints} (or \emph{subtype inequalities}) is in the core of efficient \emph{type reconstruction} in modern object-oriented languages with subtyping and inheritance, two problems known \emph{polynomial time equivalent}. It is important to know how different combinations of type constructors influence the complexity of the problem. We show the \emph{NP-hardness} of the satisfiability problem for subtype inequalities between object types built by using simultaneously both the functional and the non-empty record type constructors, but without any atomic types and atomic subtyping. The class of constraints we address is intermediate with respect to known classes. For pure functional types with atomic subtyping of a special non-lattice (\emph{crown}) form solving subtype constraints is PSPACE-complete \cite{Tiuryn92,Frey97}. On the other hand, if there are no atomic types and subtyping on them, but the largest $\top$ type is included, then both pure functional and pure record (separately) subtype constraints are \emph{polynomial time solvable} \cite{KozenPalsbergSchwartzbach94,Palsberg95ic}, which is mainly due to the lattice type structure. We show that combining the functional and nonempty record constructors yields NP-hardness \emph{without any atomic subtyping}, and the same is true for just a single type constant with a nonempty record constructor. \end{abstract}

Details

show

hide

Language(s): eng - English

Dates: Modified: 2010-03-12Date issued: 1999

Publication Status: Issued

Pages: -

Publishing info: -

Table of Contents: -

Rev. Type: -

Identifiers: eDoc: 519677
Other: Local-ID: C1256104005ECAFC-B535BC26FE7E2720412566FA003F0BE5-Vorobyov1998CSL

Degree: -

Event

show

hide

Title: Untitled Event

Place of Event: Brno, Czech Republic

Start-/End Date: 1999

Legal Case

show

Project information

show

Source 1

show

hide

Title: Proceedings of the 12th International Workshop on Computer Science Logic (CSL-98), Annual Conference on the EACSL

Source Genre: Proceedings

Creator(s):
Gottlob, Georg, Editor
Grandjean, Etienne, Editor
Seyr, Katrin, Editor

Affiliations:
-

Publ. Info: Berlin, Germany : Springer

Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 285 - 297 Identifier: ISBN: 3-540-65922-6

Source 2

show

hide

Title: Lecture Notes in Computer Science

Source Genre: Series

Creator(s):

Affiliations:

Publ. Info: -

Pages: - Volume / Issue: 1584 Sequence Number: - Start / End Page: - Identifier: -