{"created":"2021-03-01T06:31:14.027500+00:00","id":23378,"links":{},"metadata":{"_buckets":{"deposit":"191b6dc2-8eda-4a62-84e0-46899c6639aa"},"_deposit":{"id":"23378","owners":[],"pid":{"revision_id":0,"type":"depid","value":"23378"},"status":"published"},"_oai":{"id":"oai:nagoya.repo.nii.ac.jp:00023378","sets":["312:313:314"]},"author_link":["69308","69309"],"item_10_biblio_info_6":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2016-12","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"6","bibliographicPageEnd":"1224","bibliographicPageStart":"1205","bibliographicVolumeNumber":"104","bibliographic_titles":[{"bibliographic_title":"Studia Logica","bibliographic_titleLang":"en"}]}]},"item_10_description_4":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_language":"en","subitem_description_type":"Abstract"}]},"item_10_identifier_60":{"attribute_name":"URI","attribute_value_mlt":[{"subitem_identifier_type":"DOI","subitem_identifier_uri":"http://doi.org/10.1007/s11225-016-9673-0"},{"subitem_identifier_type":"HDL","subitem_identifier_uri":"http://hdl.handle.net/2237/25573"}]},"item_10_publisher_32":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"Springer","subitem_publisher_language":"en"}]},"item_10_relation_11":{"attribute_name":"DOI","attribute_value_mlt":[{"subitem_relation_type":"isVersionOf","subitem_relation_type_id":{"subitem_relation_type_id_text":"https://doi.org/10.1007/s11225-016-9673-0","subitem_relation_type_select":"DOI"}}]},"item_10_rights_12":{"attribute_name":"権利","attribute_value_mlt":[{"subitem_rights":"The final publication is available at Springer via http://doi.org/10.1007/s11225-016-9673-0","subitem_rights_language":"en"}]},"item_10_select_15":{"attribute_name":"著者版フラグ","attribute_value_mlt":[{"subitem_select_item":"author"}]},"item_10_source_id_7":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"0039-3215","subitem_source_identifier_type":"PISSN"}]},"item_1615787544753":{"attribute_name":"出版タイプ","attribute_value_mlt":[{"subitem_version_resource":"http://purl.org/coar/version/c_ab4af688f83e57aa","subitem_version_type":"AM"}]},"item_access_right":{"attribute_name":"アクセス権","attribute_value_mlt":[{"subitem_access_right":"open access","subitem_access_right_uri":"http://purl.org/coar/access_right/c_abf2"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Nakazawa, Koji","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"69308","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Fujita, Ken-etsu","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"69309","nameIdentifierScheme":"WEKO"}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2017-12-01"}],"displaytype":"detail","filename":"main.pdf","filesize":[{"value":"201.9 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"main.pdf ファイル公開：2017/12/01","objectType":"fulltext","url":"https://nagoya.repo.nii.ac.jp/record/23378/files/main.pdf"},"version_id":"cb245fef-1cab-480a-8dc6-c45ab22a620e"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"Lambda calculus","subitem_subject_scheme":"Other"},{"subitem_subject":"Lambda-mu calculus","subitem_subject_scheme":"Other"},{"subitem_subject":"Confluence","subitem_subject_scheme":"Other"},{"subitem_subject":"Permutative conversion","subitem_subject_scheme":"Other"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"journal article","resourceuri":"http://purl.org/coar/resource_type/c_6501"}]},"item_title":"Compositional Z: Confluence Proofs for Permutative Conversion","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Compositional Z: Confluence Proofs for Permutative Conversion","subitem_title_language":"en"}]},"item_type_id":"10","owner":"1","path":["314"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2017-02-15"},"publish_date":"2017-02-15","publish_status":"0","recid":"23378","relation_version_is_last":true,"title":["Compositional Z: Confluence Proofs for Permutative Conversion"],"weko_creator_id":"1","weko_shared_id":-1},"updated":"2023-01-16T04:13:03.502896+00:00"}