括号抽象的递归算法与设计特性

A=p如果p∈V ar或p∈ZJA=

AA<λx.p >A= [x]A

A（Z是ZJ加上表示组合子的符号在这项工作中研究的括号抽象和不同的translations组合子的属性如下：WD：若p，q∈λ-项（V ar，λZ′），则p<$αq<$

A=ASC：若q，t∈λ-term（V ar，<$λZ′）且x∈V ar则

A =

A[A|x]SBA：（[x] Ap）t→ p [t|x]I：如果p，q∈λ−term（V ar，<$λZ′），则

A=A<$p<$αq。WD属性由所有括号抽象填充，并声明Λ平移将被定义如下：<>Λ：Λ→CL（V ar，VZ）

Λ=其中pJ是pSC属性声明S替换C相对于<>A交换。SBA性质是比BA更强的S性质。性质I指出，具有在Λ中的域的平移<>Λ是内射的。1.1贡献如前一节所述，有几种括号提取算法，但没有统一的理论来推广所有这些算法，事实上，前一节中描述的性质是从零开始为每个算法和组合子系统证明的。通过这种方式，这些类型的演示在整个参考书目中一遍又一遍地重复在这项工作中，定义了一个递归算法方案，它通常定义了一个无限的括号抽象族，这里引用的参考书目的所有括号抽象都可以找到。在此基础上发展了统一的理论F. Flaviani、E.Tahhan Bitar/理论计算机科学电子笔记349（2020）2529证明前一节中描述的属性，并为每个属性指明在该方案中必须假设的假设，以使该属性为真。在设计新的抽象算法时，定义的方案可以用作基础，因为根据所需的属性，保证属性符合性的方案和定理假设将是在设计新算法时要考虑的另一方面，这里有一些标准，递归方案必须有，为了使I被填充，一个属性显然与函数语言的编译无关，因此没有被其他作者研究过。然而，它与SBA性质是相关的，因为它们几乎建立了Λ与<>Λ的像之间的重写系统的同构。对于Broda和Damas的括号抽象（将表示为[x]BD），在[7]中表明，SBA几乎是满的（参见备注4.17），但本文表明，消除这个括号抽象的η规则（将被去记为BD−η的算法），然后SBA是满的。利用I和WD属性，在Broda和Damas性质I和WD给出了判定两项p，q∈λ-term（Var）是否α-等价的算法.这个算法包括通过函数<>计算两项的图像，如果它们相等，那么它们是α等价的，否则它们不是。该算法是[8]中使用的算法，以避免在术语数据库中存储同一术语的两个α等价版本此外，对于那些符合I的括号抽象，阐述了一个<>-1算法来计算的逆。该算法用于 Web应用程序[9]，这是计算逻辑的证明助手，其中每个定理t都被编码为λ项，因此，由于I，唯一索引t，而不管绑定变量的名称。以这种方式，被存储在数据库，但对用户来说，<>-1。这种类型的技术感谢我，是相关的，因为使用组合子进行交互式和自动定理证明是最近的一个研究课题1.2相关作品在项[ x ] A t的大小方面，相对于t的大小，ΔH、fab、abf、SH不是特别有效的。例如，fab和H是指数整数，abf是O（n3），因此它们对于实现函数式语言没有用处。在[10，11]中，分析了不同算法的[x]At的大小对Schéonfinkel算法的第一次改进是由于Turner [ 12 ]，他定义了后来用于实现应用程序语言的最坏情况下的Turner算法的复杂度是O（n2）[11]平均时间复杂度为O（n3/ 2）[14]。特纳算法有几种形式，因为它的公式包含二义性。文[15]研究了Turner算法的不同解释，其中基于带边条件的递归方程的解释是本文所采用的算法30F. Flaviani、E.Tahhan Bitar/理论计算机科学电子笔记349（2020）25函数式语言实现技术的进步意味着括号抽象理论的进步。Bunder [16]讨论了Turner算法的不同扩展。文[17]中用组合子B_j：=λfxyz.f（x（yz））代替B_J：=λkxyz.kx（yz），在其优化规则中改进了Turner算法。然而，实现应用程序语言的其他方法成为标准，因为它们产生了更快的实现，其中包括超级组合子[18]。变量抽象方式的根本变化是由于导演字符串[19，20]，虽然这是一个正式的系统以外的组合逻辑，它是一个先驱的图标表示。Stevens[21]在组合逻辑中变量抽象的算法设计方面做出了重大贡献，他开始使用图标表示来表示组合子，其中组合子后来Broda和Damas[7]定义了一个具有图标表示的组合子基和一个抽象算法，在最坏情况下复杂度为O（n2）。最后，Antoni Diller [22]定义了具有图标表示的组合子和在最坏情况下复杂度为O（a2n）的抽象算法，其中a是抽象变量的数量。在硕士论文[23]中研究了WD、BA、SBA、SC和I的性质，分别对算法H、abf、HS、SH和BD进行了比较。 在目前的工作中，同样的研究是在所有抽象算法的统一理论的框架内进行的。WD，I和SBA属性的应用，在修改的Broda和Damas括号抽象中，可以在等级论文[24]中找到，它解释了使用这些属性评估lambda演算的算法的细节以及[8]中的实现细节。近年来，人们研究了组合子和括号抽象在交互式或自动定理证明中的应用。例如，Jacques Carette和Russell他的建议是使用组合子来表示数学陈述和理论的应用结构，以便在不同的数学理论中识别和保持共同的结构从实验的角度来看，在[27]中，比较了这里研究的几种括号抽象算法的性能，但是在一阶数学理论中抽象变量的背景下，为了加速形式证明的构建，在交互式定理证明中。2一般递归方案在引言中给出的括号抽象算法中，可以看到[x]p依赖于p的某些子项。而要使用的子项的位置取决于它如何是p。由于这个原因，在子项位置中形式化位置和替换的概念是方便的定义2.1项p的位置Pos（p）被定义为字符串的集合F. Flaviani、E.Tahhan Bitar/理论计算机科学电子笔记349（2020）2531i=1J在正整数字母表上，递归地定义为：• 如果p∈V ar或p∈Z，则Pos（p）={}，其中表示空串。• 如果p的形式为qr，则Pos（p）={}{1 σ|σ ∈ Pos（q）}<${2 σ|σ ∈ Pos（r）}位置p和q被称为平行（p||q）i.它们相对于prefix阶是不可比较的。定义2.2如果σ∈Pos（p），则在位置σ上定义p的子项，记为p|σ，递归地：• p|n= p• 如果p = qr，则p|1 σ= q|σ• 如果p = qr，则p|2 σ= r|σ定义2.3如果σ∈Pos（p），则p[t]σ定义为p的位置σ处的子项被t替换。递归：• p[t]n=t，• 如果p=qr，则p[t]1σ=q[t]σr• 如果p=qr，则p[t]2σ=q（r[t]σ）如果σ1，...，σk是位置列表，则p [t1，...，tk] σ1，.，σk是（（p [t1] σ1）[t2] σ2）.的缩写。 [tk] σk。定义2.4|p|q是术语的缩写，递归地定义为：• |（qt）：=| PQ |t，|p|q：= pq y|p|p：= p。|ϵ := p.前面的定义是简短的，|p|w与左边相关联，将w 的 所有应用与右边相关联作为自变量。例如|（w 1（w 2（w 3 w 4）是pw 1 w 2 w 3 w 4的缩写。|(w1 (w2 (w3w4))) is anabbreviation of pw1w2w3w4.为了说明一个一般的递归算法方案，为了定义一个括号抽象，将使用一个位置列表σj，以指示当p具有某种形式或属于某个集合Ai时，哪些是p的子项。设CL（V ar，VZ）是一个组合逻辑，m和k满足1≤k≤m设{Ai}m是V ar×CL（V ar，Z）的子集族，使得：•iAi=V ar×CL（V ar，• 对所有的x存在i，其中1≤i≤k，使得当p为变量或常数时，（x，p）∈Ai• 设y，z∈Var. Ifi是（x，p）∈Ai且x∈/{y，z}的最小指数suc h然后i是最小的索引使得（x，p [z|y]）∈Ai• 设z∈Var. 如果i是（x，p）∈Ai和z∈/p的最小指标su c h，则i是使得（z，p[z]）的最小指标|x]）∈Ai对于1≤i≤m，设σi是长度为ni的位置列表。 σi将表示为32F. Flaviani、E.Tahhan Bitar/理论计算机科学电子笔记349（2020）25Jii=1Znink1nm1nm位置σ i的第i个列表的第j个元素。 如果i> k，则没有位置σi是。尼日对于1≤i≤m，设t：<$CL（V ar，<$）→CL（V ar，<$Z），其中ni=ni当k+1≤i≤m时，nJi= 2ni.函数ti使得：• 是关于替换算子[ z]的同态|y]（z∈V ar）即ti（p1，...，pn′i）[z|y] = ti（p1 [z|y]，.，pn′i [z|y]）。• 若（x，p）∈Ai，则theNx∈/ti（p|σi， . ，p|σi）when1≤i≤k• 若（x，p）∈Ai，则theNx∈/ti（p|σi， . ，p|σi，r1，.，rni）当k+ 1≤i≤m且1nix∈/rj∈CL（Var，<$Z）.定义2.5为了定义括号抽象，一般递归算法方案定义如下：[x] p = t1（p|σ1，...，p|σ1 ）如果（x，p）∈A11N1. .[x] p = tk（p|σk，...，p|σk） 如果（x，p）∈Ak[x] p = tk+1（p|σk+1，.，p|σk+1，[x]（p|σk+1），..，[x]（p|σk+1））如果（x，p）∈Ak+11nk+11. .nk+1[x] p = tm（p|σm，.，p|σm，[x]（p|σm），.， [x]（p|σm））如果（x，p）∈Am注2.6如果对（x，p）属于几个Ai还考虑了m= ∞的可能性（如定义3.11）。3经典递归抽象与一般递归格式本节展示了参考书目的括号抽象如何适应一般的递归模式。定义3.1[fab[5]]fab算法可以通过建立k= 2，t1（p）=I，t2（p）=Kp，t3（p，q，r，w）=Srw的来定义A1：={（x，p）∈A|x = p}，A2：={（x，p）∈A|（p∈V ar <$px）<$p∈Z}，A3：={（x，p）∈A|（q，r）（p = qr）}，其中A：=V ar×CL（V ar，<$Z′<${I，S，K}）定义3.2[Hilbert（H）]Hilbertt1（p）=SKK和A：=Var×CL（Var，<$Z′<${S，K}）.定义3.3[abf[3]]abf算法定义相同，除了A2：={（x，p）∈A|x∈/p}。定义3.4[Hindley，Lercher y Seldin（HS）[6]]HS算法可以通过实例化一般方案来定义，其中k：= 3，t1（p）=I，t2（p）=Kp，11F. Flaviani、E.Tahhan Bitar/理论计算机科学电子笔记349（2020）2533⎧t（p，q，r，r）=0| Φ cα|（qw）如果r1 = |Φ α|Wt（p，q，r，r）=0| Φ bα|（pw）如果r2= |Φ α|Wt（p，q，r，r）=0 ||Φ（α1，α2）|w1|w2，如果r1 = |Φ α1 |w1和r2= |Φ α2 |w2t3（p，q）=p，t4（p，q，r，w）=Srw，具有与abf相同的fab+σ4：=1，2和with集合A1，A2的列表A3：={（x，p）∈A|（<$q）（p=q x<$x∈/q）}和A4：={（x，p）∈A|（nq，r）（p=qr）}，其中hA为fab.定义3.5[Shonfinnkel（SH）[4]]SH算法定义为SHS，除了t4（p，q，r，w）=Crq，t5（p，q，r，w）=Bpw，t6（p，q，r，w）=Srw，σ5：=1，2，σ6：=1，2，且集合A4：={（x，p）∈A|（<$q，r）（p=qr<$x∈q <$x∈/r）}，A5：={（x，p）∈A|（<$q，r）（p=qr<$x∈/q<$x∈r）}A6：={（x，p）∈A|（<$q，r）（p = qr<$x∈q <$x∈ r）}其中A：=V ar×CL（V ar，<$Z′<${I，S，K，B，C}）。定义3.6[Shonfinn kelmodified（SH−η）]altax mSH−η的定义与SH相同，但消除了η规则。 这对应于使k：= 2，从SH中去除t3，σ3，A3，并从函数ti，集合Ai和列表σi的索引中减去1，其中i> 3。定义3.7[Turner（T）[12]]T算法被定义为SH，除了k：= 4，t4（p，q）=Cpq，t5（p，q，r，w）=Spw，t6（p，q，t，r，w，s）=BJpqs，t7（p，q，t，r，w，s）=CJpwt，t8（p，q，t，r，w，s）=SJpws，σ4：= 11， 2，σ5：= 11， 2，σ6：= 11， 12， 2，σ7：= 11， 12， 2，σ8：= 11， 12， 2，和t9，t10，t11，σ9，σ10，σ11，A9，A10，A11作为t4，t5，t6，σ4，σ5，σ6，A4，A5，A6的集合，A4：={（x，p）∈A|（<$q，r）（p=qxr<$x∈/qr）}A5：={（x，p）∈A|（<$q，r）（p=qxr<$x∈/q<$x∈r）}A6：={（x，p）∈A|（<$q，s，r）（p=qsr<$x∈/qs<$x∈r）}A7：={（x，p）∈A|（<$q，s，r）（p=qsr<$x∈/qr<$x∈s）}A8：={（x，p）∈A|（<$q，s，r）（p=qsr<$x∈/q<$x∈s <$x∈r）}其中A：=V ar×CL（V ar，<$Z′<${I，S，K，B，C，S′，B′，C′}）。定义3.8[Broda and Damas（BD）[7]Broda和Damas索引A是字母b和c的字符串，具有以下形成规则：∈A（是空字符串），如果α1，α2∈A，则cα1，bα1，（α1，α2）∈A。Broda和Damas的组合子是形式为ΦK或Φα的常数，其中α∈A。这些组合子的集合记为K。BD算法的定义与SH相同 但以A ：= V ar×CL（Var，<$Z′<$K），其中函数t1（p）= Φk，t2（p）= ΦKp，t3（p，q）=p，4 12最后一个问题5 12最后一个问题6 1234F. Flaviani、E.Tahhan Bitar/理论计算机科学电子笔记349（2020）25否则，F. Flaviani、E.Tahhan Bitar/理论计算机科学电子笔记349（2020）25351122∈≤∗ninini这是一个快速的定义Bunder[28]。注3.9在上述函数的条件下，考虑到w、w1、w2、α、α1和α2可以是任意的。定义3.10[Broda和Damas修改（BD−η）]BD−η算法的定义与BD相同，但删除了η规则。这对应于使k：= 2，从BD中移除t3，σ3，A3，并将函数ti，集合Ai和列表σi的索引减去1，其中i>3。定义3.11[Diller（D）[22]] Diller的组合子，称为yn-strings，是字母y和n的字符串。算法D通过实例化一般方案来定义，其中k：=2，σ1，σ2：=0，0，t1（p）=yI，t2（p） =np，并且dA1，A2为fab。定义J：=3j−3 还有q q... Q作为（i-J）以3为底，当J≤i J，j212jJj−1乘以j −2乘以j j+1假设m：=∞ni：=j，σi：= 2001年。X.”他说。1个月，1美元。X.”他说。 1分2秒 .. . ，12，2对于所有i>2（pl=x），φ1=y，Ql=rl，Fl：=（x∈pl<$plx），φ2=n，Ql=pl，Fl：=（x∈/pl）.而集合Ai：={（x，p）∈A|J（第1页，...， pj）（p = p1. pj<$p1∈ V ar <$Z<$F 1<$.. 其中A：=V ar×CL（Var×Z′q1j每个函数ti都是关于[ z]的同态|x]。例如在SH中，满足t5（p，q，r，w）[z|y] =（Bpw）[z|y] = Bp [z|y] w [z|y] = t5（p [z|y]、q [z|y]，r [z|y]，w [z|y]）。对于ti的其余部分，可以进行类似的证明4抽象的性质4.1>= [z|x]证据 通过对r的结构归纳：如果r∈V ar且r=x：>= = z = x [z|x] = r [z|x] = [z|x]。如果r∈ZJ或，r∈V ar且r x：>= = r = r [z|x] = [z|x]。如果r=pq，其中p，q∈λ-term（V ar，<$λZ′）：< r >= >=

q >=

>[z|x] [z|x] =（

< q >）[z|x] = [z|x] = [z|x]。如果r=λy.p，其中y∈V ar且p∈λ-term（V ar，<$λZ′）：它在两种情况下分离案例1y =x：< r>=<（λ y. p）>= <λy。p>=[y]

Lemm=a4. 1（[y]

）[z|y]=（[y]

）[z|x] = <λy.p >[z|x] = [z|x]。案例2y x：< r >=<（λy.p）>= <λy。（p ）>=[y] [z|x]）（z∈/Var（r）<$x/=y<$z/=y<$x=/y）n引理4. 3（[y]

）[z|x]=<λy。p>[z|x] = [z|x]。Q定理4.6（WD）若p，q∈λ-项（V ar，λZ′），则pαq

=证据 通过对P的结构归纳，如果p∈Var<$ZJ：pαqdefp=qdefp<>=p=q=。如果p=rt，其中r，t∈λ-term（V ar，<$λZ′）：F. Flaviani、E.Tahhan Bitar/理论计算机科学电子笔记349（2020）2541pαdefqq=rJtJ，42F. Flaviani、E.Tahhan Bitar/理论计算机科学电子笔记349（2020）25||∈\||

== t>= t>==且=jJ t >= t>jJ JJ如果p=λx.r，其中x∈V ar且r∈λ-项（V ar，<$λZ′）：pαdefqq=λy，RJ，其中RJ∈λ-项（Var，λλZ′ ），y∈V ar且有有限个一个变量是这样的，r< z|x >αrJ>= >对于所有z∈V ar\A，定义AJ：= A{x∈V ar |x∈V ar（< rJ> rrJ）}则< r>[z|x] Lemm=a4. 5>=< rJ>Lemm=a4. 5[zy]forallzVarAJ[z]是一个函数jJ[z]（[z|x]）=[z]（[z|y]）对于所有z ∈ V ar\Az∈/z∈/引理4. 2拉吉[x]= [y]⇐⇒

=<λx.r >=<λy.r>=Q引理4.7如果变量x在t∈λ-项（V ar，<$λZ′）中不自由出现，则x∈/t>证据通过对t和引理4.1的结构归纳。Q4.2SC属性SC属性一般不为真，例如，使用希尔伯特括号抽象进行转换，我们必须< （λy.x）[λy. xx]>H= <λy. （x[λy.x x]）>H=<λy.λy.x >H=备注4. 4