验证技术：类型λ-演算与高阶匹配的应用

理论计算机科学电子笔记172（2007）589-609www.elsevier.com/locate/entcs类型λ-演算科林·斯特林1英国爱丁堡大学信息学院摘要我们考虑将验证技术转移到具有约束力的结构关键词：游戏，类型lambda演算，高阶匹配，高阶模式。1引言计算机科学的一个显著成就是开发了计算机辅助验证有限和无限状态系统的技术。这些方法包括模型检验和等价性检验。一般的研究目标是将它们转移到具有约束的有限和无限状态系统类在本文中，我们研究了两个问题，涉及类型λ-演算，高阶匹配和高阶程序计划。理解这两个问题的基本思想是将类型化λ-项视为具有绑定的模型，类似于转换图，并通过在不使用替换的情况下对它们进行游戏来理解它们的动力学行为（β在匹配的情况下，我们假设给定一个潜在的解项t。t的模型检验博弈决定它是否是一个解。为了将其转换为匹配的决策过程，需要找到隐含小模型属性的游戏不规则性：如果问题有解，那么它就有一个小解[26]。在这里，我们提出了三阶情况下的证明，因为小模型属性直接来自树模型属性，即每个游戏都下降到解项的分支。在方案的情况下，我们采用Ong我们1电子邮件：cps@inf.ed.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.021590C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589定义一个方案模型检查游戏，其精神类似于Ong [17]定义的游戏语义，但基于定义匹配游戏的思想在第二节中，我们介绍了高阶匹配及其等价问题，对偶插值。匹配博弈在第3节中定义，在第4节中我们展示了三阶情形的可判定性。高阶格式将在第5节介绍，其对策将在第6节介绍。2匹配和对偶插值我们考虑使用binary→操作符从单个基类型0生成的简单类型。类型是0或A→B，其中A和B是类型。 如果A/= 0，则 它的形式为A1→. →An→0，假设→关联到右边，这里写为（A1，.，An，0），遵循Ong [17]。秩序的一个标准定义是：0的阶数是1，并且（A1，.，An，0）是k +1，其中k是An的阶的最大值。简单类型化λ演算的项是从类型化变量x，y，.的可数集合构建的。和类型化常量a，f，. （每个变量和常量都有唯一的类型）。简单类型项的集合是最小集合T，使得(i) 如果x（f）有类型A，则x：A∈T（f：A∈T），(ii) 若t：B∈T且x：A∈T，则λx.t：A→B∈T，(iii) 若t：A→B∈T且u：A∈T则tu：B∈T.类型化术语的顺序是其类型的顺序。如果类型化术语不包含自由变量，则它是封闭的在整个过程中，我们假设α-等价、β和η-约化的定义定义2.1匹配问题是一个方程v=u，其中v，u：0，u是封闭的。问题的顺序是自由变量x1，.的顺序的最大值。，xn在v中。一个解是一个项序列t1，. ...，tn/xn}=βηu.决策问题是：给定一个匹配问题，它有解吗？匹配是高阶统一的一个特殊例子，当u是闭项时：v能与u模式匹配吗？ 虽然高阶统一是不可判定的（甚至如果自由变量只有二阶），高阶匹配被Huet证明是可判定的[12]。如果匹配是可判定的，那么它就具有非初等的复杂性.可判定性已被证明为一般问题，直到4阶使用观测等价的λ-项和各种特殊情况[18，19]。Comon和Jurski定义了树自动机，它描述了一个四阶问题的所有解，从而表明它们形成了一个正则集[6]。Loader通过将λ-可定义性编码为匹配，证明了当β-等式是相同的范式时，匹配对于变量定义是不可判定的[15]，也参见[13]。在[26]中，我们描述了一个程序，该程序表明匹配是可判定的，它使用λ项上的有限模型检查游戏。在本文中，我们描述了模型检查游戏，以及它如何导致三阶情况下的可判定性，作为前奏C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589591检查（无限）模型检查游戏的高阶计划。我们假设所有正规形式的项都是η-长形式，(i) 如果t：0，则它是u：0，其中u是常量或变量，或者u t1. tk在 哪里u：（B1，...，Bk，0）是常数或变量，并且每个ti：Bi是η-长形式，(ii) 如果t：（A1，. ，An，0）则t是λy1. 其中每个yi：Ai和tJ：0都在η-长形式。我们使用λz1... znfor λz1.λzn.如果变量y在λ-抽象中的每次出现都是唯一的，则项是良名的设u：0，每个vi：Ai，1 ≤i≤n，是正规形式的闭项，x：（A1，.，An，0）。插值方程的形式为xv1. vn= u，插值方程为xv1. vn/= u。有限插值族方程式xvi. vi= ui，i：1 ≤i≤m，其中x是同一个自由变量1N插值问题P. 有限族插值方程和不等式，xvi. vi<$iui，i：1 ≤i≤m且每个<$i∈ {=，/=}，具有相同的自由变量1Nx是一个对偶插值问题P。 问题P的类型是x的类型，P的阶是x的阶。A型P的解是一个闭项t：A，标准形式，使得对于每个方程tvi... vi= βui，且对每个方程1N电视我. vi/= βui. 我们写t| = P，如果t是P的解。1NSchubert证明了n阶匹配问题可归结为插值问题问题的顺序最多n+2和Padovani表明，它减少到一个对偶插值问题的顺序n[20，19]。由于正规形，β-等式和β η-等式重合。因此，高阶匹配问题简化为以下决策问题：给定（对偶）插值问题P，是否存在项t |P？例2.2[6]中的问题x λy1y2.y1λy3.f y3y3=faa的阶为3，x：（（0，0，0），（0，0），0），并且每个yi：0。Q例2.3问题x λz.z=f（λx1x2x3.x1（x3））a也有3阶，其中x的类型为（（0，0），0）。这个例子说明了封闭项u：0可以包含绑定变量：这里f：（0，0），0，0，0），0，0）。Q3配对游戏我们使用了一种受模型检查游戏（如[23]）启发的对偶插值的博弈论表征，其中模型，转换图，相对于属性遍历，玩家在适当的位置做出选择。类似地，在下面的博弈中，模型是相对于对偶插值问题P遍历的假定解项t。我们的核心动机是模拟动态的β-还原，而不是通过代入t来改变t。P的一个势解项t具有正确的类型，是正规形式，是命名恰当的（变量与P中的变量不相交）。项t被表示为树，tree（t）。如果t是y：0或a：0，则tree（t）是标记为t的单个节点。在uv 1的情况下。。 当u是一个变量或常数时，我们假设一个哑元592C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589. ..(1) λyJ(2) yJ(3) λJ(4) yJ(5) λ. . ...，c(7) λxz1z2J(8) XJ(9) λJ(10) z2J(6) F、、、、、、，z(11) λJ(12) 一Fig. 1. 解项具有空变量序列的λ被放置在其树表示中的任何子项vi：0之 前 。有了这个理解，如果t是uv1.那么树（t）由标记为u的根节点和标记为树（v i）的k个后继节点组成。我们使用符号u↓itJ来表示树tJ是节点u的第i个后继。 如果t是λy.v，其中y可能是空的，那么树（t）由标记为λy的根节点和单个后继节点树（v）组成，λy↓1树（v）。下面我们使用t来表示λ项t、它的λ树或它的根节点的标签（常量、变量或λy）。例3.1解项t 问题的例如2.3是λy.y（y（f（λxz1z2.x（z2））a））。t的树（在边缘上没有索引）在图1中。例如，在这个树（6）↓2（11）中。 在树中存在具有伪λ的各种节点，例如（5）和（9）。Q我们假设树t的每个节点都是唯一可识别的：例如，在例3.1中，我们用一个不同的自然数标记每个节点，以区分z和λ的不同出现。Ong在[17]中的无辜博弈语义提供了一种可能的博弈论基金会 给定一个潜在的解决方案项t和一个（dis）方程xvi.我爱你1N在图2中有游戏板。玩家对手选择ui的分支。.、、、、C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589593JJJJJ.. .. ......你好。J哦哦，，oo oooo，oooo、、，，，，，，，，，，osozi.. .，ziutv1vni......λyλz......y，z，，得双曲余切值.、、、，，z得双曲余切值.、、，z图二、说明游戏语义然后，有一个有限的游戏，它从t的根开始，可能会反复地在t和vi之间在一个恒定的a：0游戏结束。在其他常量中，玩家Proponent试图匹配对手当游戏结束时，如果遇到的常量序列与对手选择的分支相匹配，则支持者获胜。例如，Play可以在t中到达y，然后在vi中跳到λz，因为它是λz处的子树应用于λy，然后当在zinviplay可以返回到t到y的直接后继者。博弈语义在图2的固定结构上对β约简进行建模，而不使用替换对其进行更改。这就是树检查游戏的基本原理。然而，它从只有t是问题P的公共结构的假设开始。 所以，游戏永远在t中。当play遍历t时，使用状态对vi的跳跃进行此外，游戏通过调用迭代定义的查找表来避免游戏语义的公正指针。树检查博弈G（t，P）由一个参与者参与，参与者是试图证明t不是P的解的反驳者。它诉诸于一组有限的状态，包括左项，vi的子项，和右项，v i的ui有三种状态：参数、值和最终状态。参数状态具有形式q [（l1，.其中每个Lj是左项（并且k可以是0）并且r是右项。这样的状态将发生在标记为λz 1的节点处. zkin t，其中每个lj具有与z j相同的类型：（l1，.，lk）是应用于λz1..zk.值状态具有形式q[l，r]，其中l是左项，r是右项。该状态与标记有t中的变量y的节点相关联，其中y和l共享相同的类型：某些vi在博弈语义学中会跳到什么最终状态是q[]或q[]。、594C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589我Dm+1MJA. tm=λy1. . . yj，tm↓1tJanddqm=q[（l1， . . . . ，lj），r]。因此，tm+1= tJ，θm+1= θm{l1ηm/y1，.，ljηm/yj}和qm+1，ηm+1由t m +1上的情况定义。1. a：0。因此，ηm+1=ηm。如果r=a，则qm+1=q[n]，否则qm+1=q[n]。2. f：（B1，.，Bk，0）。 因此，ηm+1=ηm。 如果r=fs1... sk）thenqm+1=qmelseqm+1= q [m]。3. y：B. 若θm+1（y）=lηi，则ηm+1=ηi且qm+1=q[l，r].B. tm= f：（B1，.，Bk，0），tm↓itJ并且qm=q[（l1，.，lj），fs1. sk]。因此，θm+1=θm，ηm+1=ηm，且θ m选择方向d：1≤d≤k。1. tm+1=tJ. 如果sd：0，则qm+1= q [（），sd]。 如果sd是λx1…xn.s则qm+1= q[（c1，.，cn），s{c1/x1，.，Cn/Xn}]，其中Ci是新的常数，并且每个C i具有与X i相同的类型。C. tm=y和qm=q[l，r]。如果l=λz1. . . zj。wandtm↓itJtenn nm+1=nm{tJθm/z1， . . ，tJθm/zj}elsei1jηm+1=ηm。元素tm+1，qm+1和θm+1是l上的特例.1. a：0或λz.a.所以，tm+1=tm，θm+1=θm。如果r=a，则qm+1=q[n]，否则qm+1=q[n]。2. c：（B1，.，Bk，0）。 所以θm+1=θm。 如果r1=cs1. sk则tm+1=tm，qm+1=q[m]。 否则，n选择一个方向d：1≤d≤k且tJ=tJ其中tJ↓dtJ。 如果sd：0，则qm+1= q[（），sd]。 如果sd是λx1… xn.s然后qm+1= q[（c1，.，cn），s{c1/x1，.，cn/xn}]，其中ci是新常数并且每个ci具有与xi相同的类型。3. fw1... wk或λz fw1. wk.所以，tm+1=tm，θm+1=θm。 如果rf=fs1. sk则qm+1= q[k]。否 则 ，k选择一个方向d：1 ≤ d ≤ k。如果sd：0，则qm+1=q[wd ， sd] 。 如 果 sd=λx1.xn.s 和 wd=λy1.yn.w ， 则qm+1=q[w{c1/y1，.，Cn/yn}，s{c1/x1，.，Cn/Xn}]，其中，Ci是新的常数，并且每个Ci具有与Xi和yi相同的类型。4. xl1. lk或λz.xl1. lk. 如果ηm+1（x）=tJθi，则tm+1=tJ，θm+1=θi，qm+1= q[（l1，.，lk），r]。图三. 游戏动作当游戏在t中进行时，有两种自由变量：在t中的自由变量，如图2中的y，以及在状态的左项中的自由变量，如图2中的z。 t中的自由变量与左项相关联，状态中的自由变量与t的节点相关联。所以这个博弈需要一系列的补充查找表θk和ηk，k≥ 1：θk是从t中的变量到对lηj的部分映射，其中l是左项，j是 i时调用π（i）如果π（i+ 1）是移动B1或C2的结果，则π（i+ 1）是π（i）的子节点事实3.8如果π∈G（t，P），j >1，π（j）不是最终位置且λy或y∈π（j），则存在唯一的π（i），i< j，使得π（j）是π（i）的子。598C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589sss、、(1)λx1x2J(2)X1(3) λsssS，ss、、，z(15) λJ(4) X2J(5) λJ(6) X1J(16) B，o(7) λJ(8) X1、、，z(13) λJ(14) B，o(9) λJ、、、、、、，z(11) λJ(10)a（12）b(1) q [（v1，v2），faa]θ1η1(2)q[v1，faa]θ2=θ1{v1η1/x1，v2η1/x2}η2=η1一个3(3)q[（），faa]θ3=θ2η3=η2{（3）θ2/y1，（15）θ2/y2} C4(4)q[v2，faa]θ4 = θ3η4=η1一个3(4)q[y3，a]θ5=θ4η5=η4{（5）θ4/y3}C3(5)q[（），a]θ6 = θ4η6=η5C4(6)q[v1，a]θ7 = θ6η7=η1一个3(7)q[（），a]θ8=θ7η8=η7{（7）θ7/y1，（13）θ7/y2} C4(8)q[v1，a]θ9 = θ8η9=η1一个3(9)q[（），a]θ10 = θ9η10 = η9 {（9）θ9/y1，（11）θ9/y2}C4(10)q[]θ11=θ 10η 11=η 10的1图五. 例2.2的解项定义3.9如果对所有x∈dom（β），βJ（x）=β（x），则查找表βJ扩展βFact3.10若π（j）是π（i）的一个child，则nθj∈π（j）扩张dsθi∈π（i）且dηj∈π（j）推广了ηi∈ π（i）.S、、、C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）5895994判定三阶匹配我们描述了如何匹配的博弈论表征，命题3.4，三阶匹配的可判定性的 这个想法是为了显示小模型属性：如果t|= P则有一个小项tJ|= P。首先，我们将静态600C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589解树t0的结构与演奏的动态。定义4.1假设B =（B1，.，Bk，0）。(i) λ是类型为0的原子叶。(ii) 若xj：Bj，1≤j≤k，则λx1. xk是B型原子叶。(iii) 如果u：0是一个常量或变量，那么u是一个简单的 瓦片。(iv) 如果u：B是常数或变量，并且tj：Bj，1 ≤j≤k是原子叶，则u（t1，.，t，k）是简单的瓦片。项树t0没有其最顶端λy，由简单的瓦片出现组成。在图5中，节点（2）、（3）和（15）形成具有原子叶λ的简单瓦片x1（λ，λ），并且λ、（8）、（9）和（11）形成x1（λ，λ）。节点（10）和（12）也是没有原子叶的简单瓦片。节点（2）本身或（2）与（3）不是简单的瓦片。在整个过程中，我们在t0中使用的tile意味着 我们写t（λx1，.，λxk），如果t是具有原子叶λx1，..，λxk.定义4.2假设t和tJ是简单的瓦片。(i) tJ是j-低于t（λx1，. ，λxk），如果在 t0中存在从λxj到TJ的分支。(ii) tJ是t 0中tile t的直接j依赖，如果tJ是t之下的j -，并且t j的头变量由t中的λy约束。(iii) tJ是t的j依赖的，如果它是t的直接j依赖的，或者存在tJ J是T的直接j依赖的，并且tJ是t jJ的j依赖的，对于某个jJ。(iv)如果对某个j依赖于t，则它依赖于t。在图1中，以（8）为根的瓦片x（λ）比以（6）为根的f（λxz1z2，λ）低1，因此也是直接1依赖于它的定义4.3假设t = t（λx1，.，λxk）是t 0中的简单瓦片。(i) 如果t的自由变量y受t 0的初始lambda λy约束，则t是t 0中的顶部瓦片。(ii) t是j-endint0，如果在t 0中每个低于λ xj的自由变量都有界于t之上. 这是一endtile int0 if it isj-end for allj：1≤j≤k.(iii) 如果t的头部是常数或者它是常数瓦片的依赖项，则t是t 0中的常数瓦片。以（2）、（6）和（8）为根的图块x1（λ，λ）是图5中的顶部和末端图块。瓷砖图1中的f（λxz1z2，λ）和x（λ）是常数瓦片。瓦片也可以根据它们的动态特性通过调用G（t0，P）的子区定义4.4子游戏π是简单瓦片u（λx1，.，λxk），如果1）A（1）A（|π|），则i和π（|π|）是π（1）的子元素。 如果λxj∈ π（|π|）.C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589601在简单常数瓦片u（λx1，.，λxk）是一对位置π（i，i+1）， 其中u∈π（i）且λxj∈π（i+1），对于某个j（通过图3的移动B1或C2）。如果π是例3.2 中的策略，那么π（6，7）是图1中f（λxz1z2，λ）上的1-策略。事实4.5如果π是一个简单的常数瓷砖上的游戏，那么|π|= 2。在一般的高阶匹配情况下，简单的非恒定瓦片y（λx1，.，λxk）可以是任意长度。 它从y开始，在叶子λxj处结束。在这两者之间，控制流几乎可以是t0中的任何位置（包括y）。然而，由于缺乏约束力，发挥是非常有限的，在第三阶的情况下。在一个对策π∈G（t0，P）中，不可能有多个子对策[26]中证明了，如果π（i，m）和π（i，n），n > m，在简单瓦片y（λx1，.，λxk）且λxj∈π（m）则存在位置π（MJ），MJN<，即π（m）的子节点.因此，以下是直接推论，因为三阶项树中的顶部瓦片没有依赖瓦片。命题4.6如果π∈G（t0，P），P是三阶的，且t是t0中的一个简单瓦片，则在π内t上至多有一个子游戏。假设P是一个三阶问题，t0|= P。如果我们自上而下地检查t0，从初始值λ的下面开始，那么它是一个简单瓦片的树：每个瓦片都是一个常数，或者是一个顶部瓦片，也是一个末端瓦片。图1中的树由两个初始顶部瓦片y（λ）和常数瓦片f（λxz1z2，λ）、x（λ）、z2和a组成，其中两个初始顶部瓦片y（λ）也是末端瓦片。假设Π ={π1，. ，πp}是G（t0，P）的余. 我们定义每个π∈Π在阶段中的划分在每个阶段n，我们检查一个简单的瓷砖在t0和一个位置π（in）其控制在TN的头部。我们形式化了子戏π（in，jn）是tn或jn上的戏，|π|.对于每个π∈Π，我们关联一个唯一的颜色c（π）。对于阶段1，我们识别初始简单图块ti= u（λ χ1，.，λxk），其是常数或顶部瓦片（并且可能k = 0）。我们检验t1上的策略，如果是1，由移动π（i1，j1）组成，其中i1=2。如果没有戏，我们让j1=|π|，所以q∈π（j1）是最终的，并且对于所有i：i1≤i≤j1，它遵循u∈π（i）：所以，控制永远不会超出这个初始瓦片。Tilet1对于π是最终的，我们终止于现阶段否则，t1上的游戏在其原子叶之一λxj处结束，并且t2是在t0中直接在λxj下方的简单瓦片，并且i2= j1+ 1。如果t1上的余度π（i1，j1）是nri，则t1是着色的c（π）。 在阶段n，对于任何随后的简单图块tn，我们假设策略π（in，jn）是t n上的策略，如果存在的话。如果没有戏，那么jn=|π|而对于π来说，n是最终的。 如果π（in，jn）是tn上的一个nri余解，则tn是着色的c（π）。 通过这种方式，π的划分下降了t0的一个分支，直到它到达一个final瓷砖。例4.7对于图1中的树和例3.2中的策略π，有如下π的划分。y λ y λ fλxz1z2 x λ z2π（2， 3）π（4， 5）π（6， 7）π（8， 9）π（10， 10）602C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589图块f（λxz1z2，λ）和x（λ）被着色为c（π），z2对于π是最终的。 对于其他C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589603在这个例子中，有一个类似的分区。yλyλ fλaπJ（2， 3）πJ（4， 5）πJ（6， 7） πJ（8，8）其中只有f（λxz1z2，λ）被着色为c（πJ），并且瓦片a对于πJ是最终的。Q考虑关于所有策略π∈Π的划分我们稍微滥用符号：如果π和πJ是两个游戏，我们让π（in，jn），πJ（in，jn）是子游戏在其划分的阶段n，而不是一系列的简单瓦片存在简单瓦片的树，因为它们都共享初始瓦片。我们在树中选择三种简单的瓦片。如果方块t至少有一种颜色，则它是有色的;如果方块t对于至少一个游戏是最终的，则它是最终的。在阶段1结束于t1的同一个原子叶的每一个游戏在阶段2共享t2，依此类推。因此，分支发生在阶段m的tm处，如果存在在tk，k m的相同原子叶处结束的播放，并且在阶段m处播放在tm的不同原子叶处结束：tiletm则是（播放）分隔符。在例4.7中，f（λxz1z2，λ）分离了这些区带。如果t0中的一个简单的瓷砖是彩色的，最终的或分隔符，那么它是特殊的。在t0中具有原子叶的简单图块不是特殊的，它是超级连续的。要么每个播放都避开它，要么每个通过它的子播放都是ri，并在同一个原子叶λxj处结束。如果每个游戏都避免简单的瓦片u（λx1，.，λxk），那么我们可以用简单的常数瓦片b：0来替换t0中以u为根的子树。 如果每个通过u（λx1，.，λxk）为ri且终止于同一个原子叶λxj，tj为t0的λ xj之下的子树，则我们可以用tj替换t0中以u为根的子树。显然，这两种转换都保留了解树。例如，例4.7中y（λ）的两次出现都是冗余的：图1中的树是通过将节点（6）直接移动到节点（1）下面来变换的。唯一具有原子叶的重要瓦片是特殊的。然而，有色人种和最后的瓦片由右项ui的深度和数字u i的深度之和约束。分隔符的个数至多为p-1（其中p是播放次数）。因此，小模型属性如下，其中s（P）是适当的度量。事实4.8如果t0是三阶P的最小解，则|的t0| ≤ s（P）。对于例4.7，其树在图1中的项通过划分被减少为λy，f（λxz1z2.x（z2））a. 类似地，图5中的项被简化为λx1x2.x2（a）。可判定性证明利用了三阶P的潜在解项t0上的博弈的一个关键特征，即树模型性质：每个博弈π∈G（t0，P）向下延伸到t0的一个分支，直到达到最终状态因为只有一个层次简单的非恒定瓷砖，所以，他们都是顶部和结束，游戏玩是严重限制。对于4阶或5阶树，存在两个级别的简单非恒定瓦片：顶部瓦片y（λx1，.，λxk）和端块z（λz1，.，λzl），其中z由λxj约束。级别的数量随着顺序的增加而增加：在第八或第九顺序有四个级别。只要有一个以上的水平，游戏可以跳树周围。为了显示一般情况下匹配的可判定性，论证更加复杂，并呼吁展开，这类似于模态中的展开604C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589=h（z）（zJ逻辑展开导致树模型性质。可判定性的证明使用展开，然后是选择性重折叠（展开的逆），并且从它们的组合性质来看，小模型性质成立，参见[26]。在这里，我们希望在有限λ项上考虑有限博弈5高阶程序格式假设0是有限和无限F-树的域，其中每个节点由基函数（常数）f∈F={f1，.，fk}。每个fi都有一个arity，这是它的分支度：如果fi：0，那么它有arity 0和f：（0，.，0，0）的arity是0减去1个2的个数。根据Damm [8]，一个高阶程序方案是相对于一组基函数定义。定义5.1方案是一个有限族Fixi. Xidef 我≤i≤m，其中1ni =t，1定义，其中每个Fi都是类型化的和不同的，并且每个ti：0都是从类型化变量，xi，.，xi，基函数和Fi的使用应用。有1ni也是起始配置S：0，没有从基函数构建的自由变量而Fi方案的阶是变量的最高阶i出现在定义3的左侧。Ex示例5.2Fxd=effF（g（x））g（x）具有开始配置Fa，是一阶的，x：0：这里，a具有arity 0、garity1和arity 2。Q例5.3以F g h a为起始构型的下式是二阶的Fx1 x2 x3def=f（F（Gx1）（Hx2）x3）x1（x2（x3））Gy1y2d=ef g（y1（y2））Hz1z2def1 2变量x1，x2，y1，z1：（0，0），x3，y2，z2：0，常数a的值为0，g的值为1，第二章.Q一个scheme是一个抽象的函数程序，它的解释是由S生成的F树.例如，例5.2的Fa变成fF（ga）ga，然后f（fF（g（g（a）g（g（a）g（a），依此类推，从而生成无限树，其初始部分如图6所示。在操作上，当应用于S时，以下转换规则生成树。(i) Fis1. Sn−→ti{s1/xi，. ，sn/xn}i1i i(ii) 如果sj−→ sJ对于1 ≤ j ≤ k，则fis1.. sk−→ fisJ. SJj1k(iii) 如果a：0，则a−→a2定义域的顺序是：对 于 每 个 j ， < $t ± t和tj± tJ意味着fit 1. tk± fitJ.. . tJ。j1k3匹配文献假设0是1阶的，遵循一阶逻辑，而方案文献假设0是0阶的，遵循λ-演算文献。然而，一个概型的阶的定义则是任何Fi的最高阶，这与这里当0的阶为1时的定义一致X））C. Stirling/Electronic Notes in Theoretical Computer Science 172（2007）589605CcCcCcf，，CccccJc、、、，，zzf，g，，CcCJC、、vz、、、，，zzf，g，，aCcCJC、、vz、、、，，zzf，g，g，，CccCcCc...、、、、、、，zz...、、、、、、，zz...、、、、、、，zz一见图6。 例子5.2的树从外延上讲，一个方案的意义是关于基函数的自由解释的最小固定点，遵循Damm [8]。对于实施例5.2，F0a=n，Fi+1a=f（Fi（ga））ga.所以F2（a）=f（f（n）g（g（a）g（a）.所得F-树是F ω（a）=.i≥0 Fi（a）是Y（λF）的意义。λx。f（F（gx））g（x））a.显然，操作和指称的观点完全一致。 在下文中我们将注意力限制在不生成具有unfined子树的F-树的方案上对于阶数大于1的情形，概型的定义，定义5.1，比Damm的定义稍微宽松一些。Damm的定义与K n a p ik，N i w i n的k i and d U r z y cz y n [14]：se [1，10]所介绍的安全方案相一致，这是对这个限制的一个详细的讨论，并证明了它确实与Damm的一致。一个悬而未决的问题是，安全是否限制了表达能力。经典的高阶格式问题是：给定两个（可能是安全的）格式，它们是否生成相同的F-树？理解这个问题的一种方法是将模式与形式语言联系起来。每一个基函数f∈F的元数n> 1可以被分解成终端符号f1，.，fn表示可以被满员你一个F树的分支语言是确定性的一组单词，这些单词是从根到终端节点a：0的路径：