混合编码：高阶抽象推理与懒惰λ-演算的案例研究

60理论计算机科学电子笔记70第二次（2002年）URL：http://www.elsevier.nl/locate/entcs/volume 70. html16页s建立双相似同余的Howe方法的混合编码A.莫米利亚诺1S.J. Ambler2 R.L.克罗尔3，4莱斯特大学数学与计算机科学系英国莱斯特，LE1 7RH摘要本文对文[4]中提出的一种新的交互式定理证明工具Hybrid进行了简要的描述。它提供了一种形式的高阶抽象推理（HOAS），与归纳和共归纳相结合。我们提出了一个案例研究，说明使用混合推理的懒惰λ-演算。特别是，我们证明了模拟的标准概念是一个precongruence。虽然这样的证明不是新的[5]，但发展并不是微不足道的，我们试图说明使用混合的优点，以及一些正在进一步研究的问题。1导言和背景本文描述了一个案例研究，我们证明结果的Meta理论的平凡（对象级）的编程语言使用一个新的机械化工具。编程语言是众所周知的-它只是无类型的懒惰λ-演算。然而，这种语言对于我们的案例研究来说是理想的，我们将很快解释。在Isabelle HOL中编码的机械化工具被称为Hybrid;它在[4]中引入Hybrid的主要特点是• Hybrid提供了一种逻辑框架，在这种框架中，对象级逻辑的语法可以用高阶抽象语法（HOAS）来充分表示。• 混合是兼容的战术定理证明一般，特别是归纳和共归纳的原则1电子邮件：A. mcs.le.ac.uk2电子邮件：S. mcs.le.ac.uk3电子邮件：R. mcs.le.ac.uk4这项工作得到了EPSRC资助号GR/M98555的2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。MOMIGLIANO，AMBLER和 CROLE61• 它是定义性的，保证了经典类型理论中的一致性[12]，而HOAS通常与直觉主义逻辑相关联，例如。[23].该系统提供了一种HOAS形式供用户表示对象日志。用户层与基础设施是分离的，其中HOAS是通过de Bruijn风格的编码实现的-参见第2节。由Abramsky [2]引入的懒惰λ-演算是众所周知的，并且形成了懒惰函数式语言的理论基础的一部分。特别是在[5]中，Ambler和Corle描述了一种基于懒惰λ演算的简单函数式编程在那篇论文中，一个标准的操作语义，上下文等价和双相似性，都编码在伊莎贝尔HOL。关键的结果是一个完全机械化的证明，即双相似性确实是一个一致性，而且它符合上下文等价，遵循Howe的证明技术[15]。证明需要发展相当数量的技术伊莎贝尔霍尔引理，因为编码是严格的一阶，即。通过de Bruijn符号。在本文中，我们重播（一些）在[5]中描述的工作，并试图显示混合方法的实用性。这篇论文是一个非常实用的案例研究，并没有提出任何新的理论。此外，证明的发展并不完全，因为它是在[5]中，有一个小数目， 目前的引理是假设而不是证明。然而，我们描述的代码和证明是大量的，这是我们第一次大规模应用Hybrid。因此，我们希望我们的开发将有助于其他有兴趣证明编程语言属性的从业者，以及那些可能想要将Hybrid作为高阶元语言进行实验的人。我们相信，机械化的豪氏风格的证明特别是支持某种形式的HOAS的人，因为它需要：• 支持绑定构造（推理）。• 支持结构归纳的证明，特别是在开放项上（例如Howe候选关系M• 支持共归纳证明。我们的工作与程序等价，如相似性和双相似性。我们提醒读者注意关键的非正式思想;更多细节见示例[24]。假设s和SJ是程序，我们想知道它们什么时候有相同的行为。一个众所周知的这样的关系是莫里斯风格的上下文等价关系-s和sJ是等价的，如果插入任何更大的程序片段（上下文），两个更大的程序评估为相同的值，或者等价地都终止。虽然这种程序等价的概念是有价值的和直观的，但它确实很难推理出它的元理论属性，主要是由于对每一个可能的上下文进行量化。双相似性已经成为一个更容易管理的，然而，在这种情况下，等价的想法。粗略地说，s和sJ是双相似的，如果每当s计算为一个值时，sJ也是，MOMIGLIANO，AMBLER和 CROLE62⊆⇓⊆⇒⇓⇓≈≈◦并且结果值v和VJ的所有子程序也是双相似的，反之亦然。我们将写ssJ来表示s和sJ具有相同的行为，并将（等价）关系称为双相似性。什么是一个正式的定义的？ 设R是程序上的任意二元关系。 定义新的二元关系Φ（R），通过设置sΦ（R）sJ，恰好在当s λ x.p对任意p时，存在q使得sJ λy，q，且对每个r，p[r/x]是R相关的 [001 pdf 1st-31 files]当t为y时， Q.如果RΦ（R）（即，R是一个后固定的点），则无论何时sRsJ，都遵循sΦ（R）sJ。 因此RΦ（R）是s和SJ具有“相同的当然，R捕捉了一种特定行为模式的形式描述。 我们希望这种关系能够描述“所有可能的行为”。 我们可以通过≈◦ 作为最大关系R，它是一个后固定点而这一点，也就是说，“双相似”是由“Φ”定义的余归纳集合。这就产生了一个共归纳原理，它可以由以下规则来表征：S：a∈S S<$Φ（S）CIa∈gfp（Φ）另一方面，通过提供正确的互模拟来建立特定程序的等价性可能会变得很困难，例如，参见[24]中的滤波器p（mapfs）和滤波器f（filter（pf）s）的证明。等式推理会容易得多，这是建立互模拟是一个全等的关键。我们按以下步骤进行在第2节中，我们简要介绍了混合动力，请读者参考[4]以获得更全面的说明和更多的例子。在第3节中，我们展示了惰性λ-演算是如何在Hybrid中编码的，给出了双相似性的定义。在第4节中，我们对我们的主要证明给出了解释性的注释和评论，该证明确定了双相似性是一个同余。 最后，我们对相关工作提出了意见，并作了总结。 请注意，从现在开始，我们讨论的是模拟和预同余，而不是互模拟和同余。关于后者的结果可以通过对称化我们的证明得到。在本文中，我们使用一个漂亮的印刷版本的伊莎贝尔HOL具体语法;一个规则的结论C和前提H1. Hn将被表示为[H1;. ;Hn]]=C.Isabelle HOL类型声明具有以下形式s：：[t1，. tn] t。Isabelle HOL连接词通过通常的逻辑符号表示。自由变量被隐含地普遍量化。符号==（Isabelle meta equality）用于定义的平等。2介绍混合动力混合动力车在安德鲁·戈登的工作中有其基础。Gordon定义（在HOL中）一种de Bruijn符号，其中表达式命名由字符串给出的自由变量。他可以写出5T=dLAMBDAvt（其中v是a5符号dLAMBDA来自[1];小的“d”表示deBruijn符号。MOMIGLIANO，AMBLER和 CROLE63⇒⇒字符串），它对应于一个抽象，其中v在t中绑定。函数dLAMBDA有一个将T转换为相应的de Bruijn项的定义;这有一个外部抽象，以及一个deBruijn形式的子项t，其中v的（自由）出现被转换为绑定de Bruijn指标。戈登演示了这种方法的实用性。它提供一个很好的机制，通过它可以使用命名的绑定变量，但他没有利用内置的HOAS，HOL本身使用它来表示语法。我们的方法的新颖之处在于，我们利用HOAS在Meta（机）级的伊莎贝尔HOL。我们以Hybrid为例。首先，一些基本的东西。 最重要的是de Bruijn表达式的Isabelle HOL数据类型，其中bnd和var是自然数，con为常数提供名称expr：：= CON con |VAR变量|BND |expr $$expr |ABS expr设T0= Λ V1。Λ V2. V1V3是一个真正的，诚实的善良（对象级）语法树.戈登会用TG=dLAMBDAv1（dLAMBDAv2（dAPP（dVARv1）（dVARv3）其等于dABS（dABS（dAPP（dBND1）（dVARv3）。Hybrid提供了与dLAMBDA相似的结合机制。戈登这只是德布鲁因的一个定义term.在我们的方法中的一个关键的区别是，绑定变量的对象逻辑中的绑定变量在伊莎贝尔HOL。因此LAMv. t中的v是一个元变量（而不是Gordon方法中的字符串）。 在Hybrid中，我们也选择用VARi形式的项来表示对象级自由变量;然而，这基本上对技术细节没有影响-重要的是自由变量的可数性。在Hybrid中，上面的T0被渲染为TH= LAM v1。（LAM v2. （v1$$ VAR 3））。LAM是一种Isabelle HOL活页夹，这种表达是通过定义lambda（λ v1. （lambda（λ v2. （v1$$ VAR 3）其中λvi是Meta抽象，可以看到对象级项是以通常的HOAS格式呈现的，其中lambda：：（expr expr）expr是一个定义函数，它将抽象转换为然后混合动力将减少TH的de Bruijn项ABS（ABS（BND1 $$ VAR3）），在戈登总之，Hybrid提供了一种HOAS形式，• 自由变量对应于VARi形式的混合表达式;• 绑定变量对应于（绑定）Meta变量;• 抽象Λ V. E对应于表达式LAMv. e==lambda（λ v. e）;• 应用E1E2对应于表达式E1$$E2。此外，我们希望能够在Hybrid上执行元推理6我们使用大写的Λ和大写的V来避免与Meta变量v和元抽象λ混淆。MOMIGLIANO，AMBLER和 CROLE64⇒†表情 为了做到这一点，我们要查看函数CON，VAR，$$和LAM作为数据类型构造函数，也就是说，它们应该是单射的，具有不相交的图像。事实上，我们确定了expr和expr expr的子集，这些属性适用于这些子集。expr的子集包含了所有的真表达式，即对应于λ -演算表达式的de Bruijn表达式。谓词abstr：：（exprexpr）bool编码exprexpr的一个子集，该子集由合适的e组成，其中LAM v。 V是正确的。假设ABSe是正确的;例如，令e=ABS（BND 0 $$BND 1）。那么e是1级的，特别是可能有一些现在悬挂的约束索引;例如ABS中的BND1（BND0$$BND1）。抽象是通过用元变量替换每次出现的悬挂索引，然后抽象元变量来产生 我们的例子产生了抽象λ v. ABS（BND 0 $$v）。在Hybrid中，上述构造函数的区别是直接的。类似的是内射性，但是对于lambda绑定器LAM，人们可以证明它在抽象上是内射的-我们将使用大写字母的非正式约定来表示元变量，这些元变量旨在表示抽象：[[abstr E; abstr F]]=（LAM v. E v = LAM v。F v）=（E = F）此外，抽象的可拓性是可证明的：[[abstr E; abstr F;]i. E（VAR i）= F（VAR i）]]=E = F抽象中的适当表达式的替代性也是如此[[abstrE;propert]]=proper（E t）3在Hybrid我们首先展示如何在Hybrid中表示懒惰λ演算。我们主要关心的是这种演算中的程序，即闭表达式。这些形式（像往常一样）的一个子集的表达式给出的e：：= v|有趣的v. e |e1@e 2 †为了以HOAS格式渲染，使用简单类型的λ-演算，以常数作为元语言，我们需要用于抽象和应用的常数，例如cAPP和cABS。回想一下，在元语言中，应用用in fix $$表示，抽象用LAM表示。那么，†将对应于语法e：：= v|cABS $$（LAM诉E诉）|cAPP $$e1$$e2在元语言中。这个语法是用Hybrid逐字编码的，前提是（参见第2节）我们声明con恰好由两个常量（的名称）组成。因此，我们可以把IsabelleHOL理论Hybrid看作是一种元语言，它提供了HOAS的一种形式;特别地，捕获避免替换由元级β-归约表示。MOMIGLIANO，AMBLER和 CROLE65†为了能够在Hybrid中直接编码语法，我们定义了uexp==con expr，然后定义如下@：：[uexp，uexp]uexpe1@e2==CONcAPP$$e1$$e2好玩的 * （uexpuexp）uexp有趣的x。 e x == CON cABS $$LAM x. e x哪里好玩。的确是伊莎贝尔·霍尔的活页夹例如，（对象级λ-演算）项ΛV1。Λ V2. V1V2将由Fun v1代表。Fun v2. v1$$v2，尽管“真正的”底层形式是CONcABS $$（LAMv1. CONcABS $$LAMv2. （CONcAPP$$v1$$v2））我们引入一些一般谓词。这些将在我们的机械化过程中使用。• 当混合表达式e等于语法的表达式时，isExpe成立：isExp（VARi）[[isExpe1;isExpe2]]=isExp（e1@e2）[[abstr E; nov. isExp（E（VAR i））]=isExp（Fun v. E v）这是因为uexp只是一个类型缩写，不会排除外来术语[8]。然后，我们需要证明这个关系也是替代的，即：[[abstr E; isExp p; pagi. isExp E（VAR i）]]=isExp（E p）• cloExpp在isExpp成立且Hybrid表达式p没有自由变量时成立。我们称这种表达式为程序，并且经常使用Meta变量p和q来表示程序.• 当cloExp（Fun x. E x），而且abstr E成立。通过元级β-转换获得对象级替换的好处可以在通过：：[uexp，uexp]bool的归纳定义对惰性求值（封闭项）进行编码时得到体现。这一定义由以下条款给出：cloAbstrE =cloFun x. E x Fun x. E x[[p1Fun x. E x; cloAbstr E; cloExp p2;（E p2）v]]=（p1@p 2）v标准的性质，如唯一性的评估和价值的可靠性有直接的证明，只基于结构归纳法和引进和淘汰规则。我们的中心任务是证明应用模拟bool是一个预同余（推论4.2）。模拟具有单共感MOMIGLIANO，AMBLER和 CROLE66介入规则[[cloExpr;cloExps;T. r T x −→（cloAbstr T −→（U. s Fun x. U x cloAbstr U（p. cloExp p →（T p）“（U p）]=r这里的HOAS风格极大地简化了陈述，相应地简化了元理论。事实上，通过对共归纳关系的适当实例化，（封闭）模拟是一个前序（并且互模拟确实是一个等价关系）的证明是直接的。4定理与证明回想一下，预同余是句法上的二元关系，句法是由句法构造函数保持的部分顺序。 [24]这一定义是标准的，也是省略的。我们的案例研究表明，Howe关于模拟是预同余的证明[15]可以在Hybrid中进行。虽然证明的数学本质上类似于[5]中的证明，但证明本身相当长。我们认为，它提供了一些证据表明，我们的混合系统实现了元语言的HOAS，它是可能的，以推动涉及归纳和共归纳的战术推理。豪由于混合是基于传统的（共）归纳设置，豪关系的定义（表1）涉及到开放项的引入。我们注意到，在一个完全支持HOAS [22]，例如Edinburgh LF，这可以通过仅对封闭项进行假设判断来实现，其中变量和函数的子句合并在以下内容中：很好（m. y“m−→y“·m）−→Ny“·NjyFunv. N Jv“q有趣的v. N v“·q唉，这样的引入规则产生非单调算子，因此在Isabelle HOL中是不允许的因此，我们可以在开表达式上定义开相似性，这是相似性的明显扩展，其中两个开项相关，如果它们的λ-闭包相似。然后证明开放相似是一个预同余。虽然这与非正式的数学发展相对应，但乍一看似乎相当间接。对开放项的定义进行编码的一种方法是通过将自由变量的环境（列表）与表达式联系起来的判断。特别地，我们引入了环境的良构性的归纳定义，即没有重复，（Γ t）和表达式的归纳定义，即使得项t的所有自由变量都出现在良构的Γ中。一些引理保证了相互一致性MOMIGLIANO，AMBLER和 CROLE67►这两个概念。然后，打开模拟Γs“ t由规则s[[isExp s; isExp t; n/∈ Γ; n/p. cloExp p −→Γ-substsnp“γ- substtnp]] =r，ns请注意，在定义中，在s中用p替换VARn是在de Bruijn水平上用替换的原始概念实现的。显然，利用HOAS来表达这个子句是非常可取的，利用抽象的概念，但是上面的公式已经显示出更适合于机械化。然后证明以下性质：• 开放模拟保留了表达式和环境的良好格式。• 通过对Γ-ε结构的归纳，将仿真纳入到开放仿真中。• 是开模拟前序，按列表归纳。• 它是可替换的，其证明需要如下推广：[[r1，n， r2s我们使用Hybrid验证的关键定理是定理4.1开相似关系Γ s“t是一个预相合。一个直接的推论是推论4.2相似关系s“t是一个预同余。双相似性是一个全等性，简单地从这一点得出。推论的思想是，一旦证明，人们可以使用代数推理的通常规则来推理程序的相似性。在给出证明大纲之前，我们在表1中归纳性地介绍了类型为“·：：[ var list，uexp，uexp ] numbool”的Howe关系这种关系是一种前一致性，这是直接的，因为它的定义是结构性的，而（开放的）相似性是反射性的。 因此，我们可以证明定理，如果我们可以证明豪关系和开放相似性一致。这是这个证明的结构。(i) 我们证明了Howe关系的一些一般性质。 这些是：(a) 在Howe中包含了具有开放相似性的Howe关系的合成.在这里，我们在表a中展示了一个最简单的证明脚本MOMIGLIANO，AMBLER和 CROLE68rVARx[[didn't. r，y=N（VARy）n.娱乐，娱乐;N Jv“q]]=rFunv. N v“ · q[[Γm1 mJ1; rm2“· mJ2; r（mJ1@mJ2）“ n]]=r（m1@m2）表1Γs由Howe关系归纳定义产生的归纳原理，Howe.inrs表示其引入规则，besttac是Isabelle的自动最佳搜索策略。 命令addDs指示证明器以前向链接的方式使用引理opensim transs。(b) Howe是自反的，即Γs=Γs这是证明了归纳的结构上的先行词，使用开放的相似性和性质的良好形式的表达。(c) 开放相似性包含在豪（Howe）中，它直接从（a）和（b）得出(d) Howe关系是替代的：形式上r，ysrs[t/y]请注意，这个引理是基本的，并且在完整的HOAS帐户中仍然需要7（而模拟的替代性不是）。在这里，这句话又需要概括为：[[r1，y， r2s=r1， r2substsy t证明，我们的脚本中最长的，是通过归纳法推导第一个判断，使用开放相似性的替代性。以来7cf. Church-Rosser定理[25]中关于并行约化的替代性的类似引理，它具有一个显著的第一性原理全自动证明。目标“env|-s< howe> t ==>env|- t< opensim> u--> env|-s< howe> u”; behowe.induct 1;通过（ALLGOALS（best_tac（HOL_cs addIs howe. inrsaddDs [opensim_transm]）;qed_spec_mp“howe_mrans”;表2Howe关系的半传递性的证明脚本。MOMIGLIANO，AMBLER和 CROLE69►►⇓►⇓►后者是通过混合原始概念的替代，即subst定义的，我们的机械化是相当复杂和特设的，使用了几个关于抽象和替代之间相互作用的混合基础结构属性。(ii) 如果[] Funx. E x“· p，然后p有趣y。其中，对于每个闭pJ，我们有[] EpJ“· F P J。这首先通过Howe关系的反演、开放相似性和最终相似性来证明;注意，当使用消除规则时，Fun的注入性（根据LAM的定义）是至关重要的用途。最后，从Howe的半传递性和替换性（的一个例子）(iii) 如果[] p“· q和pV，则[]v“· Q. 证据如下非正式的一个，涉及到一个归纳评价，和反演豪和（开放）模拟，与一个额外的案例分析v。然而，由于大量的前向链接，自动化程度相对较低。一旦所有这些性质都被证明，通过显示豪关系和开放相似性的重合来建立主要定理就很容易了。证据（定理4.1）我们只需要证明豪包含在开相似中，上面的（c）点建立了相反的包含。回想一下，为了证明Γε1E1和E2通过封闭模拟相关然而，在证明了Howe关系是可替换的，如果我们能证明[]p相似性是共归纳定义的，因此我们只需检查[]p假设p≠Funx。T x. （3）我们有[]乐趣x。 T x“·q，由（2）我们得到qFuny。其中，对于所有闭的pJ，我们有[]T pJ“· U P J。我们结束了✷5相关工作在这里，我们只回顾使用某种形式的HOAS来编码关于（双）相似性的证明的论文;例如，我们参考[4]来回顾与HOAS和（共）归纳相关的更一般的问题;我们只是提到[11]作为使用一阶方法的早期案例研究。据我们所知，关于懒惰λ-演算中互模拟的唯一其他可比较的机械化证明是[21]。这遵循弱HOAS [22]方法（即对象级替换被编码为归纳关系），并补充了上下文理论[13];后者由一组公理组成，参数化HOAS签名，包括类似于新鲜度的名称的关键属性的重新定义，更重要的是，高阶归纳和递归模式。作者证明了互模拟协MOMIGLIANO，AMBLER和 CROLE70≤不通过Howe的方法，而是遵循Stoughton对[3]中报道的Milner上下文引理的改编。这种方法在表达能力更强的函数式语言中可能会变得更加笨拙;此外，形式化严重依赖于术语向量，以编码线性实现对分概念，即：M1nM2N→N. 虽然概念上没有问题，但有几个步骤没有（Marino Miculan，个人通信）。弱HOAS方法在π演算的背景下更成功[14]。后一篇论文包含了形式验证，其中，强后期双相似性是一个一致性。这可以说不仅归因于对名称的“反应”的可能性，这对于诸如失配之类的操作的Meta理论至关重要，而且还因为这里通常不需要在这种风格中仅部分支持的假设判断[8]。事实上，进程类型的构造函数不会引起该类型的任何负事件。因此，β转换可以实现对象级替换，在这种情况下，对象级替换只是在[19]中，作者在FOλλIN中提出了CCS的编码。共归纳推理是通过自然数上的归纳用互模拟的表示来模拟的;这利用了上述概念的共连续性，它允许人们通过从泛关系开始的所有幂n ω的交集来捕获最大固定点。一些全等性质已经用Pi编辑器进行了验证[9]。可以在类似于BMPF的系统中采用类似的方法[23]。最后，我们与[5]中的证明进行了简要的比较;正如我们提到的，语法是使用de Bruijn风格的符号表示的，通常会损失人类的可读性。约束变量替换直接在代表微积分的Isabelle HOL理论中编码。为了部分缓解这一问题，通过β展开定义了封闭模拟，在本文的符号中，[[cloExpr;cloExps;t.rt−→u.s cloExp p →（t @ p）“（u @ p））] = r“s开放相似性的编码和Howe关系与本文的编码基本上是类似的，但值得注意的是，Hybrid编码中的替换谓词属于基础结构而不是对象逻辑。6结论和今后的工作本文报告了我们使用Hybrid对懒惰λ演算中一个关于程序等价的非平凡结果进行机器检验的经验。MOMIGLIANO，AMBLER和 CROLE71⇒⇒⇒以下是我们学到的一些教训：(i) Hybrid的当前版本使用谓词abstr来字符化函数E：：expr expr，它可以合法地形成一个可扩展项LAM x的主体。E x.这种抽象的归纳原则引入了“双抽象”的概念：一个函数f：：expr expr expr，它可以形成一个非线性项LAM x的主体。LAMy. fx y。这个过程无限地继续着，函数有三个、四个、五个参数，等等。最好是N元抽象和归纳的一般理论。这将减少基础结构的数量，将描述抽象和双抽象的理论一次性包含在内我们一直在研究这样的扩展，并且已经有了一个合理的原型。(ii) 一个相关的问题，在整个工作中一次又一次地出现，是如何处理表达式中变量的“解绑定”。这首先发生在子句中的isExp[[abstr E; nov. isExp（E（VAR i））]=isExp（Fun v. E v）有趣的X。如果主体E是一个抽象，那么E x是对象语言的一个表达式，而且，主体通过变量的每个实例化E（VARy）都是一个对象表达式。问题是你应该如何量化？我们可能会有每一个都产生了不同的表达式归纳原则。可以使用McKinna和Pollack [20]提出的技术证明它们是等价的，但这样做是大量的工作，显然必须对每个归纳定义的判断重复。上面的量化器基本上是试图捕捉Gabbay和Pitts的新量化器[16]。 这在性质上是普遍和存在的。如何最好地代表混合中新量化器的双重性质是一个悬而未决的问题。一种可能性是提供一个统一的框架来归纳地定义判断，并使用McKinna和Pollack技术证明“for all fresh”和“for somefresh”的等价性(iii) 混合动力提供的基础设施目前过于分层。许多在Hybrid层次上证明的引理在宾语层次上重复。一个更好的方法是放弃正确的谓词，而使用一个通用谓词“isExp”，它是用对象逻辑的绑定签名参数化的这应减少行政引理的负担。(iv) 虽然该工具在处理封闭术语时似乎成功地提供了一种HOAS形式，但我们不得不求助于更传统的编码，即通过明确的环境，相对于涉及开放的判断，如豪关系。这是由于非分层假设判断和（共）归纳的根本不相容性，MOMIGLIANO，AMBLER和 CROLE72它本身就有问题。然而，可以探索其他一些途径。• 我们可以直接在开放条件下工作，这样相似性就不必分两个部分介绍。主要的困难不仅仅是它的古怪w.r.t.在函数式编程环境中的评估，但似乎这种相似性的概念在文献中并不为人所知。实际上，弱头规范形模拟的相关概念[17]与L′evy-Long不等式--不适用的模拟是一致的。• 我们可以选择接受Miller McDow-ell [18] 的两级方法特别地，Festival提出了后者在Coq中的实现[10]，其中FOλIN的定义反射规则被归纳类型的消除规则所模仿，并补充了一组公理，说明给定签名的构造函数的自由性。我们目前正在研究的一个有趣的可能性是使用Hybrid代替Coq等系统作为后者架构的元元逻辑;这有几个优点：构造函数的自由性和更重要的更高类型的扩展性属性不是假设的，而是通过基础设施的相关属性来证明的。只有不可分层的假设判断，如类型，需要在对象层次上编码，而其余的可以作为一个诚实善良的Isabelle HOL归纳定义;这将使更机械化的结构归纳可用，与规范逻辑中推导高度的完整归纳相比[18，10]。共归纳原理是存在的，可能在Meta层次上表达，然后在客体层次上反映.这与FOλIN相反，在目前的公式中，FO λ IN只允许通过最大固定点进行有点笨拙的归纳编码。·具体化逻辑不必是提供由HOL表示，但是可以变化为例如线性逻辑的片段。这将允许利用函数式编程的元理论的最优雅的编码，并在[7，18]中提出参考。事实上，对Benton KennedyIsabelleHOL代码的源文件可以在http://www.mcs.le.ac.uk/mechsem/Hybrid/Howe上找到···MOMIGLIANO，AMBLER和 CROLE73引用[1] A. 戈登一个机械化的名称携带语法直到阿尔法转换。在J.J.乔伊斯和C. J.H.Seger，编辑，高阶逻辑定理证明及其应用，计算机科学讲义第780卷，第414-427页，加拿大温哥华，8月12日一九九三年不列颠哥伦比亚大学，Springer-Verlag，1994年出版。[2] S.艾布拉姆斯基lazy lambda calculus。In D. Turner，编辑，函数式编程研究主题，第65-116页。Addison-Wesley，1990年。[3] S. 阿布拉姆斯基 和L.昂Lazy lambda演算中的完全抽象。信息与计算，105：159[4] S.安布勒河Crole和A.莫米利亚诺将高阶抽象系统与算术运算结合起来，实现了算术运算和（CO）输入。 InInV. A. 第15届高阶逻辑定理证明国际会议论文集，弗吉尼亚州汉普顿，2002年8月1日至3日，第327-343页，第2342卷，计算机科学讲义，施普林格出版社，柏林，2002年。[5] S. J.Ambler 和 R. L. 克 罗 尔 通 过 （ 共 ） 归 纳 的 机 械 化 操 作 语 义 学 。 在Proceedings of the 12 th International Conference on Theorem Proving inHigher Order Logics，卷1690的Lecture Notes in Computer Science，第221-238页。Springer-Verlag，1999.[6] N. Benton 和 A. 肯 尼 迪 单 子 、 外 接 子 和 变 换 。 在 Proceedings of the 3rdInternationalWorkshopinHigherOrderOperationalTechniquesinSemantics ， 第 26 卷 Electronic Notes in Theoretical Computer Science 中 。Elsevier，1998年。[7] I. Cervesato和F.芬宁线性逻辑框架。在大肠Clarke，编辑，计算机科学逻辑第十一届年度研讨会论文集，第264IEEE计算机学会出版社.[8] J. Despeyroux，A. Festival和A.赫绍维茨 Coq中的高阶抽象语法。In M.Dezani-Ciancaglini和G. Plotkin，编辑，类型化Lambda演算和应用国际会议论文集，第124-138页，苏格兰爱丁堡，1995年4月。第902章.[9] L- H.埃里克森Pi：一个交互式的推导编辑器，用于部分归纳定义的演算。以 . Bundy ， 编 辑 ， Proceedings of the 12th International Conference onAutomated Deduction，pages 821第814章大结局[10] A. 很好Coq中的两级元推理发表于2002年第15届高阶逻辑定理证明国际会议论文集[11] J·弗罗斯特。《伊莎贝尔》中共同归纳的案例研究。技术报告359，剑桥大学计算机实验室，1995年2月。CUCL 308修订版，1993年8月。MOMIGLIANO，AMBLER和 CROLE74[12] M. 霍夫曼高阶抽象语法的语义分析。在G. Longo ， 编 辑 ， Proceedings of the 14th Annual Symposium on Logic inComputer Science（LICSIEEE计算机学会出版社.[13] F. Honsell，M.米库兰和我。史卡内托高阶抽象语法系统元推理的公理化方法。在Proc. ICALPSpringer-Verlag，2001.[14] F. Honsell，M.米库兰和我。史卡内托（共）归纳类型理论中的π-演算。Theoretical Computer Science，2（253）：239[15] D. J·豪函数式程序设计语言中互模拟的全等性证明。信息与计算，124（2）：103[16] M. Gabbay和A.皮茨一种新的涉及绑定的抽象语法方法。In G. Longo，编辑，Proceedings of the 14th Annual Symposium on Logic in Computer Science（LICSIEEE计算机学会出版社.[17] S. Lass en.Bisimulationinuntypedlambdacalcuuus：Büohm将互模拟和互模拟转换为上下文。 In M. M. 斯蒂芬·布鲁克斯，Achim荣格和A.Scedrov，编者，《理论计算机科学电子笔记》，第20卷。Elsevier SciencePublishers，2000.[18] R. McDowell和D.米勒 在逻辑框架中使用高阶抽象语法进行推理。ACMTransactions on Computational Logic，3（1）：80[19] R. McDowell，D. Miller和C. Palamidessi。在微积分中编码转换系统。理论计算机科学，197（1[20] 詹姆斯·麦金纳和罗伯特·波拉克。一些lambda演算和类型理论形式化。发表 在 Journal of Automated Reasoning ， Special Issue on FormalizedMathematical Theories，ed. F. 芬宁[21] M. 米 库 兰 在 语 境 理 论 中 发 展 元 演 算 理 论 。 In S. 安 布 勒 河 Crole 和 A.Momigliano ， editors ， MERLIN 2001 ： Proceedings of the Workshop onMEchanized Reasoning about Languages with variable bINding ， 第 58 卷Electronic Notes in Theoretical Computer Science，第1-22页[22] A. Momigliano，S.Ambler和R.克罗尔Isabelle中变量绑定语言的元理论的形式化比较在TPHOLs 2001的补充程序中，爱丁堡大学技术报告，2001年。[23] F. Pf enn inganddC. 好吧。系统描述：演绎系统的两种逻辑框架. In H.Ganzinger，编辑，第16届自动演绎国际会议（CADE-16），第202- 206页，意大利特伦托，1999年7月。第1632章.MOMIGLIANO，AMBLER和 CROLE75[24] A. M.皮茨基于操作的程序等价理论。技术报告，剑桥大学计算机实验室，1995年。注释伴随着在暑期学校的语义和计算逻辑，艾萨克牛顿数学科学研究所，剑桥，英国。[25] C. 好吧。自动化系统的Meta-Y。2000年，卡内基-梅隆大学博士。CMU-CS-00-146。