Intersection type matching with subtyping

Boris Düdder; Moritz Martens; Jakob Rehof

doi:10.1007/978-3-642-38946-7_11

Intersection type matching with subtyping

Boris Düdder, Moritz Martens, Jakob Rehof

2 Citations (Scopus)

Abstract

Type matching problems occur in a number of contexts, including library search, component composition, and inhabitation. We consider the intersection type matching problem under the standard notion of subtyping for intersection types: Given intersection types τ and σ, where σ is a constant type, does there exist a type substitution S such that S(τ) is a subtype of σ? We show that the matching problem is NP-complete. NP-hardness holds already for the restriction to atomic substitutions. The main contribution is an NP-algorithm which is engineered for efficiency by minimizing nondeterminism and running in Ptime on deterministic input problems. Our algorithm is based on a nondeterministic polynomial time normalization procedure for subtype constraint systems with intersection types. We have applied intersection type matching in optimizations of an inhabitation algorithm.

Original language	English
Title of host publication	Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
Number of pages	15
Publication date	27 Sept 2013
Pages	125-139
ISBN (Print)	9783642389450
DOIs	https://doi.org/10.1007/978-3-642-38946-7_11
Publication status	Published - 27 Sept 2013
Event	11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Netherlands Duration: 26 Jun 2013 → 28 Jun 2013

Conference

Conference	11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013
Country/Territory	Netherlands
City	Eindhoven
Period	26/06/2013 → 28/06/2013

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7941 LNCS
ISSN	0302-9743

Access to Document

10.1007/978-3-642-38946-7_11

Cite this

Düdder, B., Martens, M., & Rehof, J. (2013). Intersection type matching with subtyping. In Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings (pp. 125-139). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 7941 LNCS https://doi.org/10.1007/978-3-642-38946-7_11

Intersection type matching with subtyping. / Düdder, Boris; Martens, Moritz; Rehof, Jakob.

Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. 2013. p. 125-139 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7941 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Düdder, B, Martens, M & Rehof, J 2013, Intersection type matching with subtyping. in Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7941 LNCS, pp. 125-139, 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013, Eindhoven, Netherlands, 26/06/2013. https://doi.org/10.1007/978-3-642-38946-7_11

Düdder B, Martens M, Rehof J. Intersection type matching with subtyping. In Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. 2013. p. 125-139. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7941 LNCS). doi: 10.1007/978-3-642-38946-7_11

@inproceedings{f5caaa71a4cb4b818317c380c0492d6d,

title = "Intersection type matching with subtyping",

abstract = "Type matching problems occur in a number of contexts, including library search, component composition, and inhabitation. We consider the intersection type matching problem under the standard notion of subtyping for intersection types: Given intersection types τ and σ, where σ is a constant type, does there exist a type substitution S such that S(τ) is a subtype of σ? We show that the matching problem is NP-complete. NP-hardness holds already for the restriction to atomic substitutions. The main contribution is an NP-algorithm which is engineered for efficiency by minimizing nondeterminism and running in Ptime on deterministic input problems. Our algorithm is based on a nondeterministic polynomial time normalization procedure for subtype constraint systems with intersection types. We have applied intersection type matching in optimizations of an inhabitation algorithm.",

author = "Boris D{\"u}dder and Moritz Martens and Jakob Rehof",

year = "2013",

month = sep,

day = "27",

doi = "10.1007/978-3-642-38946-7_11",

language = "English",

isbn = "9783642389450",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "125--139",

booktitle = "Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings",

note = "11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 ; Conference date: 26-06-2013 Through 28-06-2013",

}

TY - GEN

T1 - Intersection type matching with subtyping

AU - Düdder, Boris

AU - Martens, Moritz

AU - Rehof, Jakob

PY - 2013/9/27

Y1 - 2013/9/27

N2 - Type matching problems occur in a number of contexts, including library search, component composition, and inhabitation. We consider the intersection type matching problem under the standard notion of subtyping for intersection types: Given intersection types τ and σ, where σ is a constant type, does there exist a type substitution S such that S(τ) is a subtype of σ? We show that the matching problem is NP-complete. NP-hardness holds already for the restriction to atomic substitutions. The main contribution is an NP-algorithm which is engineered for efficiency by minimizing nondeterminism and running in Ptime on deterministic input problems. Our algorithm is based on a nondeterministic polynomial time normalization procedure for subtype constraint systems with intersection types. We have applied intersection type matching in optimizations of an inhabitation algorithm.

AB - Type matching problems occur in a number of contexts, including library search, component composition, and inhabitation. We consider the intersection type matching problem under the standard notion of subtyping for intersection types: Given intersection types τ and σ, where σ is a constant type, does there exist a type substitution S such that S(τ) is a subtype of σ? We show that the matching problem is NP-complete. NP-hardness holds already for the restriction to atomic substitutions. The main contribution is an NP-algorithm which is engineered for efficiency by minimizing nondeterminism and running in Ptime on deterministic input problems. Our algorithm is based on a nondeterministic polynomial time normalization procedure for subtype constraint systems with intersection types. We have applied intersection type matching in optimizations of an inhabitation algorithm.

UR - http://www.scopus.com/inward/record.url?scp=84884509674&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-38946-7_11

DO - 10.1007/978-3-642-38946-7_11

M3 - Article in proceedings

AN - SCOPUS:84884509674

SN - 9783642389450

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 125

EP - 139

BT - Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings

T2 - 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013

Y2 - 26 June 2013 through 28 June 2013

ER -

Intersection type matching with subtyping

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this