文章基本信息

标题：Pregrammars and Intersection Types
本地全文：下载
作者：Sabine Broda
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2021
卷号：183
页码：14:1-14:22
DOI：10.4230/LIPIcs.CSL.2021.14
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：A representation of intersection types in terms of pregrammars is presented. Pregrammar based rewriting relations, corresponding respectively to type checking and inhabitation are defined and the latter is used to implement a Wajsberg/Ben-Yelles style alternating semi-decision algorithm for inhabitation. The usefulness of the framework is illustrated by revisiting and partially extending standard inhabitation related results for intersection types, as well as establishing new ones. It is shown how the notion of bounded multiset dimension emerges naturally and the relation between the two settings is clarified. A meaningful rank independent superset of the set of rank 2 types is identified for which EXPSPACE-completeness for inhabitation as well as for counting is proved. Finally, a standard result on negatively non-duplicated simple types is extended to intersection types.
关键词：Intersection Types; Pregrammars; Inhabitation