Zobrazeno 1 - 10
of 50
pro vyhledávání: '"Ken-etsu Fujita"'
Autor:
Ken-etsu Fujita
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 235, Iss Proc. WPTE 2016, Pp 16-31 (2017)
The Church-Rosser theorem in the type-free lambda-calculus is well investigated both for beta-equality and beta-reduction. We provide a new proof of the theorem for beta-equality with no use of parallel reductions, but simply with Takahashi's transla
Externí odkaz:
https://doaj.org/article/46ac63bef3704ad6927bc6ead053924a
Publikováno v:
Mathematical Structures in Computer Science. 32:1015-1027
This paper gives a new proof of confluence for Carraro and Guerrieri’s call-by-value lambda calculus λvσ with permutation rules. We adapt the compositional Z theorem to λvσ.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::33666f23f989520998a422b94144eecc
https://doi.org/10.1017/s0960129522000408
https://doi.org/10.1017/s0960129522000408
Publikováno v:
Studia Logica. 109:917-936
This paper applies Dehornoy et al.’s Z theorem and its variant, called the compositional Z theorem, to prove confluence of Parigot’s $$\lambda \mu $$ -calculi extended by the simplification rules. First, it is proved that Baba et al.’s modified
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4ec788b4054b660277245b676f22a0d1
https://doi.org/10.1007/s11225-020-09931-0
https://doi.org/10.1007/s11225-020-09931-0
Autor:
Ken-etsu Fujita
Publikováno v:
Theoretical Computer Science. 813:327-340
We introduce a formal system of reduction paths as a category-like structure induced from a digraph. Our motivation behind this work comes from a quantitative analysis of reduction systems based on the perspective of computational cost and computatio
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1c401a193e501c7e214203e9cf33754d
https://doi.org/10.1016/j.tcs.2020.01.002
https://doi.org/10.1016/j.tcs.2020.01.002
Autor:
Ken-etsu Fujita, Toshihiko Kurata
Publikováno v:
Fundamenta Informaticae. 170:223-240
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c1a3edad57a8ef304528478cc0302da3
https://doi.org/10.3233/fi-2019-1861
https://doi.org/10.3233/fi-2019-1861
Autor:
Ken-etsu Fujita
Publikováno v:
Information and Computation. 263:52-56
We show that an upper bound function for the Church–Rosser theorem of type-free λ-calculus with β-reduction must be in the fourth level of the Grzegorczyk hierarchy, i.e., the smallest Grzegorczyk class properly extending the class of elementary
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ee7442bd87777ff3f6a226b11c109653
https://doi.org/10.1016/j.ic.2018.09.002
https://doi.org/10.1016/j.ic.2018.09.002
Autor:
Koji Nakazawa, Ken-etsu Fujita
Publikováno v:
Studia Logica. 104(6):1205-1224
This paper gives new confluence proofs for several lambda calculi with permutation-like reduction, including lambda calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions, and a lambda cal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0ac17c64e7e7feb17c2da828f7440dad
https://nagoya.repo.nii.ac.jp/records/23378
https://nagoya.repo.nii.ac.jp/records/23378
Publikováno v:
Studia Logica. 103:1225-1244
The third author gave a natural deduction style proof system called the $${{\lambda}{\rho}}$$??-calculus for implicational fragment of classical logic in (Komori, Tsukuba J Math 37:307---320, 2013). In (Matsuda, Intuitionistic fragment of the $${{\la
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::62c6072177f219bd64988f1aee4f2354
https://doi.org/10.1007/s11225-015-9616-1
https://doi.org/10.1007/s11225-015-9616-1
Autor:
Aleksy Schubert, Ken-etsu Fujita
Publikováno v:
Theoretical Computer Science. 549:17-35
We study type checking, typability, and type inference problems for second-order existential systems in type-free style. The type-free style is an intermediate representation of terms between the Curry style and the Church style. Terms in the type-fr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b3a5fdf3c6b31828e542cfeaf57cbdc0
https://doi.org/10.1016/j.tcs.2014.05.019
https://doi.org/10.1016/j.tcs.2014.05.019
Autor:
Ken-etsu Fujita, Aleksy Schubert
Publikováno v:
Information Processing Letters. 114:72-75
We prove subject reduction of the Curry style existential system ( ? , ? ) with regard to complete developments. We use here a remote adaptation of the technique of Barbanera et al. used before for systems with union types. The type system with exist
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::06c11e667f35b84ccb0d0b670fd5330d
https://doi.org/10.1016/j.ipl.2013.07.027
https://doi.org/10.1016/j.ipl.2013.07.027