B枚hm theorem and B枚hm trees for the -calculus
- 作者：Alexis Saurin alexis.saurin@pps.jussieu.fr
- 关键词：位渭-calculus ; Bö ; hm theorem ; Bö ; hm trees ; Classical 位-calculi ; (Delimited) control ; Infinitary 位-calculus ; Separation property ; Shift/reset ; Streams
- 刊名：Theoretical Computer Science
- 出版年：2012
- 期刊代码：114_03043975
- 类别：cp
- 出版时间：1 June, 2012
- 卷：435
- 期：Complete
- 页码：106-138
- 文件大小：483 K
摘要
Parigot鈥檚 -calculus (Parigot, 1992聽) is now a standard reference about the computational content of classical logic as well as for the formal study of control operators in functional languages. In addition to the fine-grained Curry-Howard correspondence between minimal classical deductions and simply typed -terms and to the ability to encode many usual control operators such as call/cc in the -calculus (in its historical call-by-name presentation or in call-by-value versions), the success of the-calculus comes from its simplicity, its good meta-theoretical properties both as a typed and an untyped calculus (confluence, strong normalization, etc.) as well as the fact that it naturally extends Church鈥檚 -calculus. Though, in 2001, David and Py proved聽 that B枚hm鈥檚 theorem, which is a fundamental result of the untyped -calculus, cannot be lifted to Parigot鈥檚 calculus.
In the present article, we exhibit a natural extension to Parigot鈥檚 calculus, the-calculus, in which B枚hm鈥檚 property, also known as separation property, can be stated and proved. This is made possible by a careful and detailed analysis of David and Py鈥檚 proof of non-separability and of the characteristics of the -calculus which break the property: we identify that the crucial point lies in the design of Parigot鈥檚 -calculus with a two-level syntax. In addition, we establish a standardization theorem for the extended calculus, deduce a characterization of solvability, describe -B枚hm trees and connect the calculus with stream computing and delimited control.