On a Generalization of the Curry Correspondence

• Item type: Trans(1)
• 公開日: 2021-05-12
• タイトル: On a Generalization of the Curry Correspondence
• タイトル / 言語: en
• タイトル: On a Generalization of the Curry Correspondence
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要, Unrefereed Presentatin Abstract]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: STAIR Lab, Tsudanuma Campus, Chiba Institute of Technology／Graduate School of Informatics, Kyoto University
• 著者所属(英): en
• 著者所属(英): STAIR Lab, Tsudanuma Campus, Chiba Institute of Technology / Graduate School of Informatics, Kyoto University
• 著者名: Yosuke, Fukuda
• 著者名(英): Yosuke, Fukuda
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Combinatory logic discovered by Schönfinkel (1924) and Curry (1930) is a formal system of computation that does not explicitly make use of bound variables. Unlike λ-calculus, which uses bound variables as primitive concepts in its function notation, combinatory logic realizes various computations by means of “combinators” (e.g., using SKI combinators), and this framework was often used as an implementation technique for functional programming languages since the late 1970s. An interesting aspect of it is its relation to proof theory. As Curry observed (1958), a typed-version of combinatory logic corresponds to a Hilbert-style deductive system (i.e., a kind of formal system of proof theory) in the sense that there is a one-to-one correspondence between well-typed programs and well-formed proofs. Thanks to this Curry correspondence, we can investigate the proof-theoretical meaning of computations and the computational meaning of proofs. However, although the correspondence is famous as the origin of the Curry-Howard correspondence, it is often mentioned in the context of the implicational fragment of intuitionistic propositional logic. Its extensions to other logical fragments are not widely known. In this presentation, we review related work that mentions some extensions of the Curry correspondence, and then discuss its generalization. If time permits, we also discuss a connection to the logical abstract machine developed by Ohori (1999).
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Combinatory logic discovered by Schönfinkel (1924) and Curry (1930) is a formal system of computation that does not explicitly make use of bound variables. Unlike λ-calculus, which uses bound variables as primitive concepts in its function notation, combinatory logic realizes various computations by means of “combinators” (e.g., using SKI combinators), and this framework was often used as an implementation technique for functional programming languages since the late 1970s. An interesting aspect of it is its relation to proof theory. As Curry observed (1958), a typed-version of combinatory logic corresponds to a Hilbert-style deductive system (i.e., a kind of formal system of proof theory) in the sense that there is a one-to-one correspondence between well-typed programs and well-formed proofs. Thanks to this Curry correspondence, we can investigate the proof-theoretical meaning of computations and the computational meaning of proofs. However, although the correspondence is famous as the origin of the Curry-Howard correspondence, it is often mentioned in the context of the implicational fragment of intuitionistic propositional logic. Its extensions to other logical fragments are not widely known. In this presentation, we review related work that mentions some extensions of the Curry correspondence, and then discuss its generalization. If time permits, we also discuss a connection to the logical abstract machine developed by Ohori (1999).
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 14, 号 2, p. 32-32, 発行日 2021-05-12
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会