The logical basis of evaluation order and pattern-matching
The logical basis of evaluation order and pattern-matching
复制标题
评估顺序和模式匹配的逻辑基础
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
N. Zeilberger
中科院分区：
文献类型：
--
作者：
F. Pfenning;Peter Lee;N. Zeilberger
一个古老而著名的类比说，编写程序就像证明定理。这种类比在两个方面都很有效，特别是在推动编程语言的进步方面表现出了显着的效用，例如可以更好地理解抽象数据类型和多态性等概念。这个类比最著名的例子之一实际上上升到了同构的水平：根岑的自然演绎和丘奇的 lambda 演算之间。然而，正如人们长期以来所认识到的那样，lambda 演算未能捕获现代编程语言的一些重要特征。值得注意的是，它没有固有的求值顺序概念，而需要理解具有副作用的程序。相反，lambda 演算的历史后代（Lisp、ML、Haskell 等语言）以临时方式强加求值顺序。
本论文旨在通过从不同的逻辑基础出发，对证明作为程序的类比给出新的看法，更好地解释现代编程语言的特征。受到 Andreoli 对线性逻辑的集中证明的启发，我们解释了如何通过模式概念将逻辑推理的某些规范形式公理化。命题具有内在的极性，这取决于它们是由证明模式还是反驳模式定义的。应用类比，我们获得了一种内置支持模式匹配的编程语言，其中评估顺序明确反映在类型级别，因此可以在本地进行控制，而不是临时的全局策略决策。正如我们所展示的，不同形式的连续传递风格（分析评估顺序的历史工具之一）可以用不同的极化来描述。这种语言提供了对无类型和内在类型计算的优雅、统一的解释（结合了无限证明理论的思想），此外，还可以提供一个外部类型系统来表达和静态强制程序的更精细的属性。最后，我们使用这个框架来探索存在效果的情况下交集和并集类型的类型和子类型理论，并对现有系统的一些不寻常的工件给出简化的解释。
An old and celebrated analogy says that writing programs is like proving theorems. This analogy has been productive in both directions, but in particular has demonstrated remarkable utility in driving progress in programming languages, for example leading towards a better understanding of concepts such as abstract data types and polymorphism. One of the best known instances of the analogy actually rises to the level of an isomorphism: between Gentzen's natural deduction and Church's lambda calculus. However, as has been recognized for a while, lambda calculus fails to capture some of the important features of modern programming languages. Notably, it does not have an inherent notion of evaluation order, needed to make sense of programs with side effects. Instead, the historical descendents of lambda calculus (languages like Lisp, ML, Haskell, etc.) impose evaluation order in an ad hoc way.
This thesis aims to give a fresh take on the proofs-as-programs analogy—one which better accounts for features of modern programming languages—by starting from a different logical foundation. Inspired by Andreoli's focusing proofs for linear logic, we explain how to axiomatize certain canonical forms of logical reasoning through a notion of pattern. Propositions come with an intrinsic polarity, based on whether they are defined by patterns of proof, or by patterns of refutation. Applying the analogy, we then obtain a programming language with built-in support for pattern-matching, in which evaluation order is explicitly reflected at the level of types—and hence can be controlled locally, rather than being an ad hoc, global policy decision. As we show, different forms of continuation-passing style (one of the historical tools for analyzing evaluation order) can be described in terms of different polarizations. This language provides an elegant, uniform account of both untyped and intrinsically-typed computation (incorporating ideas from infinitary proof theory), and additionally, can be provided an extrinsic type system to express and statically enforce more refined properties of programs. We conclude by using this framework to explore the theory of typing and subtyping for intersection and union types in the presence of effects, giving a simplified explanation of some of the unusual artifacts of existing systems.