License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.190
URN: urn:nbn:de:0030-drops-40629
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4062/
Go to the corresponding LIPIcs Volume Portal

Fujita, Ken-etsu ; Schubert, Aleksy

Decidable structures between Church-style and Curry-style

pdf-format:
15.pdf (0.5 MB)

Abstract

It is well-known that the type-checking and type-inference problems are undecidable for second order lambda-calculus in Curry-style, although those for Church-style are decidable. What causes the differences in decidability and undecidability on the problems? We examine crucial conditions on terms for the (un)decidability property from the viewpoint of partially typed terms, and what kinds of type annotations are essential for (un)decidability of type-related problems. It is revealed that there exists an intermediate structure of second order lambda-terms, called a style of hole-application, between Church-style and Curry-style, such that the type-related problems are decidable under the structure. We also extend this idea to the omega-order polymorphic calculus F-omega, and show that the type-checking and type-inference problems then become undecidable.

BibTeX - Entry

@InProceedings{fujita_et_al:LIPIcs:2013:4062,
  author =	{Ken-etsu Fujita and Aleksy Schubert},
  title =	{{Decidable structures between Church-style and Curry-style}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{190--205},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4062},
  URN =		{urn:nbn:de:0030-drops-40629},
  doi =		{10.4230/LIPIcs.RTA.2013.190},
  annote =	{Keywords: 2nd-order lambda-calculus, type-checking, type-inference, Church-style and Curry-style}
}

Keywords: 2nd-order lambda-calculus, type-checking, type-inference, Church-style and Curry-style
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI