WEKO3
アイテム
Compositional Z: Confluence Proofs for Permutative Conversion
http://hdl.handle.net/2237/25573
http://hdl.handle.net/2237/255732275f7e7-b0ff-4263-9ff1-175ab4fad8be
名前 / ファイル | ライセンス | アクション |
---|---|---|
main.pdf ファイル公開:2017/12/01 (201.9 kB)
|
|
Item type | 学術雑誌論文 / Journal Article(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2017-02-15 | |||||
タイトル | ||||||
タイトル | Compositional Z: Confluence Proofs for Permutative Conversion | |||||
言語 | en | |||||
著者 |
Nakazawa, Koji
× Nakazawa, Koji× Fujita, Ken-etsu |
|||||
アクセス権 | ||||||
アクセス権 | open access | |||||
アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||
権利 | ||||||
言語 | en | |||||
権利情報 | The final publication is available at Springer via http://doi.org/10.1007/s11225-016-9673-0 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Lambda calculus | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Lambda-mu calculus | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Confluence | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Permutative conversion | |||||
抄録 | ||||||
内容記述タイプ | Abstract | |||||
内容記述 | 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 calculus with explicit substitutions. For lambda calculi with permutative conversion, naïve parallel reduction technique does not work, and (if we consider untyped terms, and hence we do not use strong normalization) traditional notion of residuals is required as Ando pointed out. This paper shows that the difficulties can be avoided by extending the technique proposed by Dehornoy and van Oostrom, called the Z theorem: existence of a mapping on terms with the Z property concludes the confluence. Since it is still hard to directly define a mapping with the Z property for the lambda calculi with permutative conversions, this paper extends the Z theorem to compositional functions, called compositional Z, and shows that we can adopt it to the calculi. | |||||
言語 | en | |||||
出版者 | ||||||
出版者 | Springer | |||||
言語 | en | |||||
言語 | ||||||
言語 | eng | |||||
資源タイプ | ||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
資源タイプ | journal article | |||||
出版タイプ | ||||||
出版タイプ | AM | |||||
出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||
DOI | ||||||
関連タイプ | isVersionOf | |||||
識別子タイプ | DOI | |||||
関連識別子 | https://doi.org/10.1007/s11225-016-9673-0 | |||||
ISSN | ||||||
収録物識別子タイプ | PISSN | |||||
収録物識別子 | 0039-3215 | |||||
書誌情報 |
en : Studia Logica 巻 104, 号 6, p. 1205-1224, 発行日 2016-12 |
|||||
著者版フラグ | ||||||
値 | author | |||||
URI | ||||||
識別子 | http://doi.org/10.1007/s11225-016-9673-0 | |||||
識別子タイプ | DOI | |||||
URI | ||||||
識別子 | http://hdl.handle.net/2237/25573 | |||||
識別子タイプ | HDL |