ダウンロード数 : ?
ファイル
言語
英語
著者
藤田 憲悦
内容記述(抄録等)
We give a syntactical proof to the statement that a novel CPS translation with surjective pairing is injective for the extensional λ-calculus. The result itself might be preliminary, since the source language (the extensional λ-calculus) of the translation is a sublanguage of the target language (λ-calculus with surjective pairing). However this paper shows that there exists a nontrivial injection from the extensional λ-calculus into the λ-calculus with surjective pairing. In this sense our result can be regarded as an extension of Plotkin, i.e., a call-by-value simulation of call-by-name λ-calculus with η-rule (extensionality). Moreover, the method presented here can be naturally extended to the case of the extensional λη-calculus which is defined from the extensional λ-calculus together with control operators.
主題
Extensional λ-calculus
Surjective Pairing
Church-Rosser Property
Continuation-passing-style Translation
Call-by-name
Call-by-value
掲載誌名
島根大学総合理工学部紀要. シリーズB
36
開始ページ
39
終了ページ
48
ISSN
13427121
発行日
2003-03
NCID
AA11157123
出版者
島根大学総合理工学部
資料タイプ
紀要論文
ファイル形式
PDF
著者版/出版社版
出版社版
部局
(旧組織)大学院総合理工学研究科
他の一覧
このエントリーをはてなブックマークに追加