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

Originalsprog	Engelsk
Titel	Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
Antal sider	15
Publikationsdato	27 sep. 2013
Sider	125-139
ISBN (Trykt)	9783642389450
DOI	https://doi.org/10.1007/978-3-642-38946-7_11
Status	Udgivet - 27 sep. 2013
Begivenhed	11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Holland Varighed: 26 jun. 2013 → 28 jun. 2013

Konference

Konference	11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013
Land/Område	Holland
By	Eindhoven
Periode	26/06/2013 → 28/06/2013

Navn	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind	7941 LNCS
ISSN	0302-9743

Adgang til dokumentet

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

Andre filer og links

Link to publication in Scopus

Citationsformater

Düdder, B., Martens, M., & Rehof, J. (2013). Intersection type matching with subtyping. I Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings (s. 125-139). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bind 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. s. 125-139 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 7941 LNCS).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Düdder, B, Martens, M & Rehof, J 2013, Intersection type matching with subtyping. i 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), bind 7941 LNCS, s. 125-139, 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013, Eindhoven, Holland, 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. I Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings. 2013. s. 125-139. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 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

Konference

Adgang til dokumentet

Andre filer og links

Fingeraftryk

Citationsformater