A tutorial on computational classical logic and the sequent calculus
A tutorial on computational classical logic and the sequent calculus
复制标题
计算经典逻辑和序贯微积分教程
DOI：
10.1017/s0956796818000023
复制
发表时间：
2018
影响因子：
1.1
通讯作者：
ARIOLA, ZENA M.
中科院分区：
文献类型：
--
作者：
DOWNEN, PAUL;ARIOLA, ZENA M.
我们提出了一个计算模型，该模型非常强调对偶性和对立面之间的相互作用--生产与消费相互作用。这个框架的对称性通过相对熟悉的概念自然地解释了编程语言的更复杂的特征。例如，将一个值绑定到一个变量对操纵程序中的控制流是双重的。通过观察序列演算的计算解释，我们发现了一种语言，它允许我们将程序中的对偶性、控制流和求值顺序作为一级概念来谈论。我们首先回顾Gentzen的LK序列演算，并展示Curry-Howard同构如何仍然适用于为我们提供表示计算的不同基础。然后，我们说明了顺序演算中计算的基本困境如何导致计算策略之间的对偶性：严格语言对懒惰语言是对偶的。最后，我们讨论了在证明搜索环境中发展起来的聚焦概念如何与顺序演算中表示的用于计算的类型安全的思想相关联。在这方面，我们比较和对比了文献中出现的两种不同的聚焦方法，静态聚焦和动态聚焦，并说明了它们是如何达到相同目的的两种手段。
We present a model of computation that heavily emphasizes the concept of duality and the interaction between opposites–production interacts with consumption. The symmetry of this framework naturally explains more complicated features of programming languages through relatively familiar concepts. For example, binding a value to a variable is dual to manipulating the flow of control in a program. By looking at the computational interpretation of the sequent calculus, we find a language that lets us speak about duality, control flow, and evaluation order in programs as first-class concepts.We begin by reviewing Gentzen's LK sequent calculus and show how the Curry–Howard isomorphism still applies to give us a different basis for expressing computation. We then illustrate how the fundamental dilemma of computation in the sequent calculus gives rise to a duality between evaluation strategies: strict languages are dual to lazy languages. Finally, we discuss how the concept of focusing, developed in the setting of proof search, is related to the idea of type safety for computation expressed in the sequent calculus. In this regard, we compare and contrast two different methods of focusing that have appeared in the literature, static and dynamic focusing, and illustrate how they are two means to the same end.
登录
查看更多内容
DOI：
10.1007/978-3-642-81955-1_11
发表时间：
1973
期刊：
--
影响因子：
--
作者：
通讯作者：
--
经典的按需呼叫和二元性
DOI：
--
发表时间：
2011
期刊：
International Conference on Typed Lambda Calculus and Applications
影响因子：
--
作者：
Z. Ariola;Hugo Herbelin;A. Saurin
通讯作者：
A. Saurin
通过证明转换进行寄存器分配
DOI：
--
发表时间：
2004
期刊：
Journal of Science of Computer Programming 50・1-3
影响因子：
--
作者：
渡谷 賢治;田島 敬史;A.Ohori
通讯作者：
A.Ohori
评估顺序和模式匹配的逻辑基础
DOI：
--
发表时间：
2009
期刊：
影响因子：
--
作者：
F. Pfenning;Peter Lee;N. Zeilberger
通讯作者：
N. Zeilberger
顺序微积分作为编译器中间语言
DOI：
--
发表时间：
2016
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
P. Downen;Luke Maurer;Z. Ariola;Simon Peyton Jones
通讯作者：
Simon Peyton Jones