理论计算机科学电子笔记140（2005）41-54www.elsevier.com/locate/entcs四阶类型λMarek Zaionc2波兰克拉科夫雅盖隆大学计算机科学系摘要[3][4][ 5][6][7 ][8][9][10][11][12][13][14][15][16][17][18][19][ Loader证明是通过在基于7个元素的域的完整类型层次结构中编码单词问题来完成的。本文的目的是证明，限制在正规四阶类型的lambda可定义性问题在任何有限域中都是可判定的。显然，λ可定义性对于1阶、 2阶和3阶类型是可判定的。作为所述结果的附加结果，我们可以观察到，对于某些类型，不存在生成所有闭项的有限上下文无关文法。我们还证明了随机选择的四阶类型（或不大于4阶的类型）允许可判定的lambda可定义性问题的概率为零。关键词：概率分布，lambda演算，高阶类型。1简单类型lambda演算我们将考虑一个具有单一基类型的简单类型化lambda演算O. 类型的集合T定义如下：O是一个类型，如果τ而μ是类型，则τ→μ是类型。 我们将使用以下符号：如果μ，τ1，τ2，...，τn是类型，则由τ1→τ2→.→τn→μ我们指的是类型τ1→（τ2→. →（τn→μ）. ）. 因此，每个类型τ都有形 式 τ1→.→τn→O.a τk→μ 我 们 指 的 是 类 型 τ.→τ→O ， τ 型 出 现 k 次（τ0→μ=μ）。 如果 τ具有以下形式1由波兰国家科学研究委员会（KBN）支持，研究资助7T11C 022 212电子邮件：zaionc@ii.uj.edu.pl1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.02542M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）41τ1→. →τn→O，则τi（i≤n）称为τ型分支，记为τ[i]。 对于任何类型的 τ，我们定义rank（τ）和arg（τ）如下：arg（O）= 0，rank（O）= 1和arg（τ1→. →τn→0）= n和秩（τ1→.. → τn→ 0）= max i=1. nrank（τ [i]）+1 。 我 们 归 纳 地 定 义 typesτ[i1 ， . ， ik]b y （ τ[i1 ， . ， ik−1] ） [ik] 对 于r1≤ik≤arg（τ[i1，. ，ik−1]）。定义1.1型τ称为正则的，如果rank（τ）≤ 4，且τ的每个分支都有arg≤1。这意味着正则类型只允许O，O→O和（Ok→O）→O（对于任何k）。对于任何类型的τ，给出一个可数的变量集V（τ）。任何类型τ变量都是类型τ项。若T是τ→μ型项，S是τ型项，则TS是μ型项。如果T是μ型项，x是τ型变量，则λx.T是τ→μ型项。项之间的相等公理有βη转换和可转换的形式。项将被写为T=βηS。如果T = λx1.，则T项是长正规形式。xn.yT1. Tk，其中y是一个xi，对于某个i ≤ n或y是一个自由变量，Tj，对于j≤k都是长正规形，而yT1. Tk是O型项。长范式存在，并且对于βη转换是唯一的（比较[6]）。封闭式术语是没有自由变量。通过Cl（τ），我们表示所有闭型τ项的集合设Y是一组类型化变量。我们用Cl（τ，Y）表示所有τ型项的集合，使得这些项的任何自由变量都在Y中。让我们为闭项引入一个复杂性测度π如果T是一个闭项，写在一个长的正规形式和T = λx1. xn.xi则π（T）= 1。如果T = λx1. xn.xiT1. 那么，π（T）= max j=1... k（π（λx1. xn.Tj））+1。 复杂度π就是Büohmtreofagivenenterm. 如果y1，. ，yn是项T中的随机变量的所有发生率，nT[y1/t1，. ，yk/tk]是从T中获得的项，其中y表示每个yi分别是项ti。有关类型化lambda的更详细的处理，见[8]。2简单类型lambda演算一个完整的类型层次{Dτ}τ∈T是有限域的集合，每个类型对应一个域。整个层级由DO决定。我们假设集合DO是一个给定的有限集合，Dτ→μ是从Dτ到Dμ的所有函数的集合。故一切诸法，皆是虚妄。由于任何函数f∈Dτ→μ都是有限集，因此我们假定这些函数的某些可感编码是针对其图表。赋值φ是一个函数，它将来自定义域之一的对象与类型lambda演算的每个变量相关联，使得类型τ变量被赋值给来自定义域Dτ的元素。任何赋值φ都可以扩展为全类型层次中所有项的解释Vφ。函数Vφ定义为：M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）4143LL(i) Vφ（x）=φ（x）(ii) Vφ（TS）=Vφ（T）（Vφ（S））(iii) Vφ（λxτ.Tμ）是这样一个从Dτ到Dμ的函数，使得对于每个元素X∈Dτ，该函数的值是Vφ（T），其中φ是一个与φ相同的赋值，除了φ（x）=X可以注意到，任何类型τ项都被解释为来自Dτ的对象。也很容易注意到，对项T的解释Vφ只依赖于对T中自由变量的赋值φ。因此，封闭项在完整的类型层次结构中有一个固定的解释。函数f∈Dτ称为lambda可定义的，如果有一个封闭的τ项T被解释为f。定义问题是一个决定是否或者给定的对象f∈τ∈TDτ不是lambda可定义的。 它被证明是由装载机的问题是不可判定的。对于特定类型的τ，τ-lambda可定义性问题是判定给定对象f∈Dτ是否是lambda可定义的问题。在这种情况下，类型τ不是问题的一部分。定义2.1一个函数α：Dτn→Dτ称为λ保持函数，如果下面的含义成立：如果x1，...， xn是D τ中的lambda可定义对象，则α（x1，...，xn）也是D τ中的lambda可定义对象。定义2.2我们称{a1，...，ap，α1，...，αk}aλ系统在Dτ中，如果a1，...，ap是D τ和α 1中的一些λ可定义对象，...，αk是D τ中的几个保λ函数。定义2.3通过λ系统{a1，.，ap，α1，...，αk}在Dτ中，我们表示域Dτ中包含元素a1，.，ap且对所有函数α1，...，αk。显然闭包中的所有对象都是λ可定义函数。λ系统{a1，...，ap，α1，...，D τ中的αk}称为λ完备的，如果系统的闭包由所有λ可定义的组成Dτ中的对象。引理2.4对于λ系统L ={a1，.， ap，α1，...， αk}闭包是等价可构造的。证据 我们将通过λ保持函数的迭代来构造闭包。让我们递归地定义集合D0，D1，. 通过L L(i) D0={a1，.， ap}L(ii)Di+1=Di{αj（x1，.， xp）：x1，.， xp∈ Di}LL1≤ j≤ kj jL我们在Dτ中有一个λ可定义对象集的单调链。0天1小时我... Dτ。 由于Dτ是有限的，那么将有一个指数i0，Di0=Di0+1。 因此，D10是系统L的闭包。 我是说L L LD44M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）41L当系统完备时，Dτ中所有λ可定义对象的闭合Di0c。Q3术语语法在[9]中引入了术语语法。在[8]或[10]中可以找到对术语语法的更详细的处理。术语文法G是三元组（V，P，S），其中V是非终结符的有限集合，每个非终结符都是类型变量，P是产生式的有限集合，每个产生式都是一对（y，t），表示为也可作为y→t，其中y∈V，t∈Cl（τ，V），其中τ是一个常见类型对于y和t。S是V的一个特殊的非终结符。闭项T由闭项t1∈ τ1，.得到， tk∈τkby production y → t如果恰好有k个非终结变量y1，.，yk在t中，具有类型τ1，. ，τk表示，因此T=βηt[y1/t1，. ，yk/tk]。 通过闭项T的一个导数，我们指的是闭项t0，t1，.的有限序列，tn= T，使得对于序列中的每个项ti，在文法G中存在产生式y→ti（这意味着ti是闭项），或者ti从前一个术语是由某些生产所产生的。Letuswriteey→T到表示T是从一些闭项t1，...，tk在G中可由产生式y → t导出。L（G，y），其中y∈V，我们指的是所有闭的由文法G从y生成的项，即如果y是类型τ变量nL（G，y）={t∈Cl（τ）：y→τt}。 假设y→t是生产量而y1，...，yn是t项中所有非终结变量的自由出现。设y∈τ，y1∈τ1，.，yn∈τn。这个产生式决定了函数α：Cl（τ1）×. . ×Cl（τn）→Cl（τ）definedbyy：α（t1，... ，tn） =t[y1/t1，. ，yk/tk]，其中对每一闭项t1∈ Cl（τ1），.， tn∈ Cl（τn）. 如果t项中没有非终结变量，则产生式y→t确定一个属于Cl（τ）的0元函数（常数）t例3.1设τ是如下类型（（O→O→O）→O）→（O→O）。让我们考虑下面的文法（{y}，P，y）。所使用的辅助变量的类型是以下p∈（O，O→O）→O和x，v，z∈O。在集合P中有4个产品。(i) y→λpx.x(ii) y→λpx.p（λvz.ypx）(iii) y→λpx.p（λvz.ypv）(iv) y→λpx.p（λvz.ypz）设α，β，γ，δ分别是由这些产生式所决定的函数。τ型闭项λpx1.p（λx2x3.p（λx4x5.p（λx6x7.x4）具有M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）4145跟随导子序列(i) λpx.x(ii) λpx.p（λvz.x）(iii) λpx.p（λvz.p（λx6x7.v））(iv) λpx1.p（λx2x3.p（λx4x5.p（λx6x7.x4）或者该项可以表示为β（γ（β（α）。很容易证明这个文法生成所有的τ型闭项（比较[9]或定理3.3）。定理3.2对于每一个秩为3的类型τ，存在一个有限文法，它具有一个生成所有闭的类型τ项的类型τ非终结变量。证据令τ = τ [1]，τ [2]，.，τ [n] →O.证明了下列文法（{y}，P，y）产生所有闭型τ项.文法包含正好n个具有以下形式的产品：(i) y→λx1. xn.xiif arg（τ [i]）= 0(ii) y→λx1. xn.xi（yx1... xn）. （yx1. xn），如果arg（τ [i]）= k > 0很容易看出，由文法产生的任何项都具有类型τ。逆蕴涵是通过归纳闭项的复杂度π来实现的。设T是长正规形中的闭型τ项。 如果T是一个投影λx1...xn.xi，那么显然它可以直接由第i个生产 假设T有一个长正规形λx1. xn.xiK1. Kk对于一些τ[i]使得arg（τ[i]）=k，其中Kj是O型项。 让我们定义T1，...， Tk乘Tj= λx1.xn.Kj.每一项Tj都是一个闭型τ项，并且在复杂度π方面比原始项T更简单。因此，通过归纳，封闭项T1，...，Tk是由文法G生成的。项T可以从T1，...，生产（二）。Q定理3.3[见Zaionc [9]]对于每一个正则秩4型，使得有i≤arg（τ）使得τ [i]= O，存在一个有限文法，其中一个非终结变量生成所有闭型τ项。例3.1给出了这种情况的说明证据令τ = τ [1]，τ [2]，.，τ [n] →O.每个τ [i]是以下类型之一：O，O→O或（O，...，O→O）→O.假设τ[r] =O，其中r≤n。我们将证明以下文法（{y}，P，y）产生所有闭型τ项。 文法包含产生式，每个类型O和类型O →O分量有一个产生式，每个二阶分量τ [i]=（O，.， O → O）→ O. 产品具有以下形式：46M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）41piy→ λx1. xn.xiif τ [i]）= Oqiy→ λx1. xn.xi（yx1... xn）如果τ [i]= O → Oliy→ λx1. xn.xi（λz1. zp.yx1. xn）如果τ [i]=（Op→ O）→ Ori，1Ri，arg（τ[i]）y→ λx1. xn.xi（λz1. zp.yx1. xr−1z1xr+1. xn）如果τ [i]=（Op→ O）→ O...y→ λx1. xn.xi（λz1. zp.yx1. xr−1zpxr+1. xn）如果τ [i]=（Op→ O）→ O我们可以看到，对于任何项λx1. xn.T的长正规形式，其中T∈Cl（O，{x1. xn}），它有一个规则的类型τ，在所有x1.在T中自由发生的xn。我们将证明每一个闭型τ项都可以由文法得到。设λx1. xn，T是闭型τ项。(case 1）如果T = xi对于某个O型变量xi，则λx1. xn.T可以通过生产p i来获得。(case（二） 如果T有形式xiS，对于某个项S∈Cl（O，{x1. xn}），其中xi的类型为O→O，则项λx1. xn.S也有τ型，比λx1简单. xn.T相对于复杂度测度π。因此，通过归纳λx1... xn.S可以通过文法得到。因此我们的项λx1. xn.T可以通过从λx1. xn.S.(case（3）如果T具有形式xi（λz1. zp.S）为一些termS∈Cl（O，{x1. xn，z1. zp}）其中xi具有类型（Op→O）→O，则λx1.xnz1. zp.S是封闭的正则型项τ [1]，τ [2]，...，τ [n]，Op→O.根据我们所注意到的，在所有类型中，最多出现一个O型变量。x1... xn，z1. zp在S中自由出现。(case 3a）如果在S中自由出现的唯一O型变量是xs，对于某些s≤n，则λx1..xn.S是一个闭型τ项，在复杂性测度π方面比T简单。因此，通过归纳λx1... xn.S可以通过文法得到。 因此我们的项λx1. xn.T可以通过从λx1. xn.S.LLM. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）4147我，(case 3b）如果S中唯一自由出现的O型变量是zs，对某个1≤s≤p，则thennλx1. xrzsxr+1. xn. S是闭合的，并且相对于复杂性度量π比T简单。因此，通过感应λ x1... xrzsxr+1. xn. 这可以从语法中得到 因此我们的项λx1. xn.T可以通过生产获得。蒂安·勒雷从T ermλ x1. xrzsxr+1. xn. S.Q定理3.4[见Zaionc [9]]对于每一个正则秩4型，使得不存在i≤arg（τ）使得τ [i] = O，存在一个有限文法，其中两个非终结变量生成所有的τ型闭项。证据令τ = τ1，.，τn→O. 让我们定义τJ= τ1，.，τn，O→O. 新的类型τJ满足定理3.3的假设，因此存在一个文法，其中有一个非终结类型τJ变量yJ，生成τJ的所有闭项。让我们在现有的文法中添加以下额外的产生式：y→ λx1. xn.xi（yx1... xn）如果τ [i]= O → Oy→ λx1. xn.xi（λz1. zp.yJx1. xn，z1） 若τ [i]=（Op→ O）→ O...y→ λx1. xn.xi（λz1. zp.yJx1. xn，zp）若τ [i] =（Op→O）→O新语法的起始符号是y。这个构造的正确性证明类似于定理3.3的证明。Q4主要结果定理4.1假设有一个文法恰好有一个非终结的τ型变量y，生成所有闭的τ型项。则对任意的满型族，D τ中必然存在完备λ系。证据设{Dτ}τ∈T是由某个有限集合DO构成的一个全型族.首先我们确定所有的产生式y→t，使得t中没有非终结变量。对于每个这样的产生式p：y→t，项t是闭型τ项。让我们在完整的类型层次中计算t，以找到一个对象ap∈Dτ。然后，让我们确定所有产品p：y → t [y，. y]，使得在t中有k > 0次非终结变量y出现。对于每一个这样的产生式，我们将定义一个函数αp：Dτk→Dτ。令p：y → t [y，. y]是在t [y，. y]。让48M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）41τJt1，. ，tk是来自DT的任意对象。 Letusdefineethettermt[y1，. ..k分别。现在让我们定义αp（t1，. tk）作为对象Vφ（t[y1，. ，yk]），其中reφ是一个将yi与ti进行局部化的自适应算法，对于所有i≤k。因此，我们定义了函数αp：Dτk→Dτ。所有这样的函数和这样的对象形成Dτ中的λ系统。我们需要证明这样的λ系统是完备的。假设一个对象a∈Dτ是λ可定义的。 我们将证明a属于刚刚构造的λ的闭包系统有一个封闭的λ项Ta被解释为a。项Ta在文法G中有一个有限派生。如果导子的长度为1，则意味着Ta是从产生式y→Ta得到的。在这种情况下，Ta的解释是一个a∈Dτ，属于 λ系统。 在这种情况下，当Ta的导数大于1时，Ta由前面的一些项得到在推导序列中，假设从R1，...，Rk，由文法中的某个产生式p：y→t。设αp是与p：y→t有关的函数αp：Dτk→Dτ. Letb1，. ，bk是对闭合条件R1，. ，Rk在Dτ中的分布。 通过归纳，我们假设b1，. ，bk早已成为λ系的闭包从λ系统的构造可以得出a=fp（b1，. ，bk）。 因此a∈Dτ长到闭包。Q定理4.2对于任意秩3型τ或任意正则秩4τ，其中i≤arg（τ）使得τ [i] =O，λ可定义性问题在由任意有限集DO建立的全型层次中是可判定的。证据给定一个对象f∈Dτ。对于τ型，存在一个有限文法，它有一个非终结变量生成所有闭的τ型项。以下程序适用。首先，我们找到文法（定理3.2 ，3.3），其生成所有闭型τ项。然后，有了文法，我们使用定理4.1中描述的过程构造λ系统。 由这样的文法形成的λ系统必须是完备的（定理4.1）。最后，我们找到这个系统的闭包（引理2.4），它由Dτ中所有λ可定义对象组成。然后我们检查给定的函数f∈Dτ属于这个闭包。Q定理4.3设τ是秩为4的正则型，使得不存在i≤arg（τ）使τ [i] = 0。τ的λ可定义性问题在由任何有限集合D O建立的全型层次中是可判定的。证据给定一个对象f∈Dτ。假设τ = τ [1]，.，τ [n] →O.让我们定义一个新的类型τ J为τ [1]，.， τ [n]，O → O. 类型τJ满足定理3.3的假设，因此存在一个有限文法，其中恰好有一个非线性变量yJ生成所有闭类型τJ项。根据定理4.2，我们构造Dτ J中所有λ可定义对象的有限性集合Dλ。 ToM. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）4149τJ生成闭型τ项，我们添加额外的产生式(1)y→ λx1. xn.xi（yx1... xn）如果τ [i]= O → O(2.1) y→ λx1. xn.xi（λz1. zp.yJx1. xn，z1） 若τ [i]=（Op→ O）→ O...(2.p) y→ λx1. xn.xi（λz1. zp.yJx1. xn，zp）如果τ [i]=（0，.，O →O）→ O任何（1）型产生式都以通常的方式定义一元函数α：Dτ→Dτ生成2.1 - 2.p定义一元函数β1：DτJ →Dτ，. ，βp：DτJ→Dτ。以下程序适用。首次发现D λ的像I由所有函数β1，...，βp。I=β（Dλ）1≤i≤p iτJ然后我们求出集合I在Dτ中关于所有函数α的闭包（见引理2.4）。这个闭包是Dτ中所有λ可定义函数的集合。最后，我们检验给定函数f∈Dτ是否属于这个闭包。这个过程的正确性证明与定理的证明是一致的4.2.Q定理4.4 λ可定义性问题对所有秩为1、2、3的类型和正则秩为4的类型都是可判定的。证据 对于秩3和正则秩4类型，见定理4.2和4.3。对于秩为0的类型O，λ可定义性问题是平凡的，因为在DO中没有λ可定义的对象。对于秩为2的类型，问题是可判定的，因为对于这种类型，只有有限个闭项。Q定理4.5 λ可定义性问题对于任何非正则秩4型都是不可判定的。证据 证明是基于观察到的类型L =（（O → O）→O）→（（O→（O→O）→O）是秩为4的最简单的非正则型。因此，通过简单的lambda可定义编码，L可以嵌入到任何非常规类型的秩4. 但λ可定义性问题对于L是不可判定的(see[1]）。Q例4.6让我们考虑从集合DO={0， 1}。问题是要找到集合Dτ中所有λ可定义的元素，对于Church数的类型τ让我们分别用a，b，c和d来命名集合DO→O的4个元素，其中这些元素由以下给出50M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）41真表：01一00B01C10D11集合Dτ由256个泛函组成。生成所有丘奇数词的文法(i) y→λux.x(ii) y→λux.u（yux）与文法相关的λ系统{a0，α}由一个λ可定义对象a0和一个一元函数α组成，前者是项λux.x的解释，后者是产生式y→λux.u（yux）的解释对象a0由真值表给出。a0={a→b，b→b，c→b，d→b}很容易发现，物体a0上的α值是另一个物体a1由下式给出a1={a→a，b→b，c→c，d→d}a1上的α值是一个新对象，假设a2由下式给出：a2={a→a，b→b，c→b，d→d}由于值α（a2）=a1，我们找到了所有lambda可定义泛函{a0，a1，a2}在Dτ的所有256个元素中。事实上，客体a1是所有奇丘奇数的解释对象a0是丘奇的零的解释定理4.7作为定理4.1和4.5中所描述的结果的一个平凡的推论，我们可以观察到对于任何非正则秩4类型，不存在生成所有闭项的有限文法。5概率方法在本节中，我们将考虑随机选择的4阶类型具有可判定的lambda可定义性问题的概率因此，我们研究了给定长度n的类型数的分数的大小，其中λ可定义性问题在全类型层次中可判定，M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）4151KK所有类型的长度n.我们特别感兴趣的是这个分数的渐近行为。我们的兴趣在于找到当n→ ∞时该分数的极限。如果极限存在，它表示0和1之间的实数，我们可以称之为可判定性密度。我们证明了具有可判定λ的秩4型可定义性问题是渐近空的，这意味着该分数的极限是0。首先，我们必须确定类型长度的测量方法定义5.1τ的长度是指类型τ的长度，定义为给定类型中原子类型O出现的总数。括号有时是必要的，箭头符号本身不包括在类型的长度。形式上，ai = 1且φ→=φ+。定义5.2我们将密度μ（A）与类型的子集AT关联为：（一）μ（A）=lim#{τ∈A：ττ=n}如果极限存在。n→∞#{τ∈T：<$τ<$=n}数μ（A）如果存在，则是在所有类型中从类A中找到类型的渐近概率，或者可以解释为集合A在类型集合中的渐近密度可以立即看到密度μ是有限可加的，所以如果A和B是不相交的公式类，使得μ（A）和μ（B）存在，那么μ（A <$B）也存在，并且μ（A <$B）= μ（A）+ μ（B）。很容易观察到，对于任何有限集合A，密度μ（A）存在且为0。对偶地，对于有限余集A，密度μ（A）= 1。然而，密度μ不是可数可加的。5.1类型的基本计数在本节中，我们将介绍一些表征不同秩类型数量的数的性质。我们可以观察到，许多结果和方法可以纯粹地用具有给定性质的二叉树来重新表述显然，任何类型的大小为n的树都可以看作是一棵有n片叶子的二叉树更先进的类型计数可以在Moczurad，Tyszkiewicz，Zaionc [4]中找到。”[11]又见《金刚经》，《金刚经》定义5.3Fn和Gn分别表示类型K K和秩≤k和大小n的类型的总数，所以：（2）Fn=#{φ∈T：<$φ<$=n}，（3）Gn=#{φ∈T：<$φ <$≤n}.引理5.4Fn和Gn由以下相互递归给出：K K52M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）4111KK(4)Fn=如果n= 1则1否则0(5)Gn=如果n= 1则1否则0(6)Fn乌恩=FiGn−i+GiFn−ik+1KKi=0时i=0时kk+1(7)Gn=Gn+Fnk+1k+1证据等式4和5是显而易见的，因为类型O是唯一一个大小为1的类型。递归方程7直接从第1节中的秩的定义得到。 当τ恰好是秩k时，τ→μ型的秩为k+1当τ的秩≤k且μ的秩正好是k+1时，μ的秩≤ k这导致递归方程6。Q5.2母函数我们将利用母函数技术证明适当分数的渐近性。为了满足每个人的需求，k≥1定义生成函数fk（z）的对=∞i=0 Fizi和gk（z）=∞i=0 吉吉吉引理5.5函数fk和gk满足以下递归定义：(8) F（x）=fk（x）gk（x）k+11 −gk（x）（9）gk+1（x） =gk（x） +fk+1（x）证据通过对4、5、6和7进行简单编码，我们得到方程(10)f1（x）=x(11)g1（x）=x(12)fk+1（x） =fk（x）gk（x） +gk（x）fk+1（x）（13）gk+1（x） =gk（x）+fk+1（x）解决它证明了引理Q定理5.6设R ∈ T是秩为4的所有正则型的集合。设Rn是R 中大小为n的元素的个数。序列R n的生成函数fR为X3fR（x）=（1− 2x）（1−x−x2）证据 我们从计算秩不大于3的常规类型开始。让Ln代表大小为n的此类类型的数量。 显然我们得到L0=0，L1 = 1，而且Ln=Ln−1+Ln−2 ，因为任何秩不大于3的正则型对于某些情况必须是O→τ或（O→O）→τ的形式。M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）4153i=1.短正则型τ。正如我们所看到的，Ln构成了斐波那契数列。因此，序列Ln的生成函数fL为1fL（x）= 1 − x − x2.一般正则四阶类型指的是形式为（（Ok→O）→O）→τ的任何类型，对于某个秩不大于3的正则类型τ，且对于某个k≥1。设Gn表示这种类型的大小为n的数量。因为对于每个k≥1，恰好有一种形式（（Ok→O）→O），序列Gn的生成函数fG必须是X3x 3fG（x）= 1 − x·fL（x）=（1 − x）（1 − x − x2）。最后，我们观察到，任何正则四阶型要么是一般的正则四阶型，要么可以由秩为4的其它较短正则型τ通过构造O→τ或（O→O）→τ或（（Ok→O）→τ得到O）→τ。 令Rn表示所有正则四阶类型的个数，尺寸;大小因此，Rn必须满足以下递归方程Rn=Gn+i=n−1Ri. 这可以转化为用于生成函数fR即fR（x）=fG（x） +xfR（x）。Q1−x定理5.7在所有秩4类型中具有可判定λ可定义性问题的秩4类型的密度为0。证据 找到所涉及的生成函数的封闭形式就足够了。即，对于所有秩4类型，从等式8计算的函数为X4f4（x）=1− 5x + 7x2−2x3.. 3+50万美元它可以很容易地变成动力严重的氧气. 闭合函数fR（x）enu的形式项。M. eratinngregular4ordertypesreturnsFibonacci数的比率，即O1+105nQ2添加所有我们知道lambda可定义性问题是可判定的三阶类型并不可判定性再次成为一个主导因素。定理5.8在所有秩≤ 4的类型中具有可判定λ可定义性问题的秩≤ 4的类型的密度仍然为0。证据 找到所涉及的生成函数的封闭形式就足够了。对于所有秩≤4的类型，函数为x−2x2g4（x）=1− 3x +x254M. Zaionc/Electronic Notes in Theoretical Computer Science 140（2005）41各自的权力严重又是O.. 3+50万美元2.函数g3得到从等式y9是x3（1−2x）（1−x）. 函数fR（x）+g3（x）枚举常规4阶类型加上所有第三阶类型返回率的O（2n）。Q引用[1] Thierry Joly，关于λ可定义性I，固定模型的问题和匹配问题的推广，出现在FundamentaeInformaticae。[2] Zo fia Kostrzycka，Marek Zaionc，Statistics of intuitionistic versus classical logics，StudiaLogica 76（3）（2004）307 - 328。[3] Ralph Loader，λ-可定义性的不可判定性，逻辑，意义和计算：纪念Alonzo Church的论文，331-342，C.A. Anderson和Zeleny编辑，Kluwer学术出版社，2001年。[4] Ma-lgorzata Moczurad，Jerzy Tyszkiewicz，Marek Zaionc，Statistical properties of simpletypes，Mathematical Structures in Computer Science 10（2000），575-594.[5] 戈登·D.普洛特金λ可定义性和逻辑关系，备忘录SAI-RM-4，爱丁堡大学人工智能学院，1973年10月[6] 理查 德 · 斯塔 曼关 于类型 λ- 演算 中闭 项的存 在性 。 In ： R. Hindley 和 J. Seldin ， eds.Combinatory Logic ， Lambda Calculus and Formalism （ Academic Press ， NewYork ，1980）.[7] Richard. 斯塔曼在洛杉矶，重新审视了泛函的平等性Harrington等人（编），HarveyFriedman[8] David A.Wolfram 类型的Clausual理论，剑桥理论计算机科学21，剑桥大学出版社1993。[9] 马雷克·扎昂克类型λ演算中的单位元集作为正则表达式，重写技术和应用，计算机科学讲义202，Springer 1985，430-440。[10] 马雷克·扎昂克在类型化λ演算中定义的字运算，Theoretical Computer Science 52，（1987）pp 1- 14。[11] Marek Zaionc，关于蕴涵和否定逻辑中重言式的渐近密度，数理逻辑报告39（2004）。
我的内容管理
展开
