元编程中的权衡
摘要：元程序设计语言的设计需要在安全性特性、表达能力和简洁性等重要语言特性之间取得平衡。然而，这些权衡往往不太被理解，我们试图通过使用计算理论的工具对元程序设计语言的权衡进行研究来纠正这种情况。元程序的安全性特性通常是不可判定的；例如，一个元程序总是终止并产生一个类型正确的实例的特性是 $Pi^0\_2$-完备的。尽管这些安全性特性是不可判定的，但它们有时可以被一个受限语言所捕捉，这是我们从复杂性理论中适应过来的一个概念。我们给出了有关捕捉这些特性的语言是否存在的一些充分条件和负面结果：对于元程序而言，不存在能够捕捉总正确性的语言，也不能捕捉高于 $Sigma^0\_3$ 的“功能”安全性特性。我们证明，将一个元程序从通用型元程序设计语言翻译成能够捕捉某一特性的受限元程序设计语言，等价于证明该特性适用于该元程序。令人惊讶的是，当从编程转向元程序设计的视角时，相应的安全性问题并没有显著复杂化——对于典型的安全性特性来说，并没有图灵程度的“跳跃”。
作者：Todd L. Veldhuizen
论文ID：cs/0512065
分类：Programming Languages
分类简称：cs.PL
提交时间：2009-09-29