Search Results

Documents authored by Fujita, Ken-etsu

Found 2 Possible Name Variants:

Fujita, Ken-Etsu

Document
DOI: 10.4230/LIPIcs.RTA.2013.190
Decidable structures between Church-style and Curry-style

Authors: Ken-etsu Fujita and Aleksy Schubert

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

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.
Cite as

Ken-etsu Fujita and Aleksy Schubert. Decidable structures between Church-style and Curry-style. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 190-205, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fujita_et_al:LIPIcs.RTA.2013.190,
  author =	{Fujita, Ken-etsu and Schubert, Aleksy},
  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 =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.190},
  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}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.103
The Undecidability of Type Related Problems in Type-free Style System F

Authors: Ken-Etsu Fujita and Aleksy Schubert

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We consider here a number of variations on the System F, that are predicative second-order systems whose terms are intermediate between the Curry style and Church style. The terms here contain the information on where the universal quantifier elimination and introduction in the type inference process must take place, which is similar to Church forms. However, they omit the information on which types are involved in the rules, which is similar to Curry forms. In this paper we prove the undecidability of the type-checking, type inference and typability problems for the system. Moreover, the proof works for the predicative version of the system with finitely stratified polymorphic types. The result includes the bounds on the Leivant’s level numbers for types used in the instances leading to the undecidability.
Cite as

Ken-Etsu Fujita and Aleksy Schubert. The Undecidability of Type Related Problems in Type-free Style System F. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 103-118, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{fujita_et_al:LIPIcs.RTA.2010.103,
  author =	{Fujita, Ken-Etsu and Schubert, Aleksy},
  title =	{{The Undecidability of Type Related Problems in Type-free Style System F}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{103--118},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.103},
  URN =		{urn:nbn:de:0030-drops-26475},
  doi =		{10.4230/LIPIcs.RTA.2010.103},
  annote =	{Keywords: Lambda calculus and related systems, type checking, typability, partial type inference, 2nd order unification, undecidability, Curry style type system}
}

Fujita, Ken-etsu

Document
DOI: 10.4230/LIPIcs.RTA.2013.190
Decidable structures between Church-style and Curry-style

Authors: Ken-etsu Fujita and Aleksy Schubert

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

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.
Cite as

Ken-etsu Fujita and Aleksy Schubert. Decidable structures between Church-style and Curry-style. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 190-205, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fujita_et_al:LIPIcs.RTA.2013.190,
  author =	{Fujita, Ken-etsu and Schubert, Aleksy},
  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 =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.190},
  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}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.103
The Undecidability of Type Related Problems in Type-free Style System F

Authors: Ken-Etsu Fujita and Aleksy Schubert

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We consider here a number of variations on the System F, that are predicative second-order systems whose terms are intermediate between the Curry style and Church style. The terms here contain the information on where the universal quantifier elimination and introduction in the type inference process must take place, which is similar to Church forms. However, they omit the information on which types are involved in the rules, which is similar to Curry forms. In this paper we prove the undecidability of the type-checking, type inference and typability problems for the system. Moreover, the proof works for the predicative version of the system with finitely stratified polymorphic types. The result includes the bounds on the Leivant’s level numbers for types used in the instances leading to the undecidability.
Cite as

Ken-Etsu Fujita and Aleksy Schubert. The Undecidability of Type Related Problems in Type-free Style System F. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 103-118, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{fujita_et_al:LIPIcs.RTA.2010.103,
  author =	{Fujita, Ken-Etsu and Schubert, Aleksy},
  title =	{{The Undecidability of Type Related Problems in Type-free Style System F}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{103--118},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.103},
  URN =		{urn:nbn:de:0030-drops-26475},
  doi =		{10.4230/LIPIcs.RTA.2010.103},
  annote =	{Keywords: Lambda calculus and related systems, type checking, typability, partial type inference, 2nd order unification, undecidability, Curry style type system}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact