概率λ-演算与定量程序分析（扩展摘要）

理论计算机科学电子笔记112（2005）5-18www.elsevier.com/locate/entcsλ-演算与定量程序分析（扩展摘要）克里斯·汉金英国伦敦帝国理工学院计算机系赫伯特·维克利茨基英国伦敦帝国理工学院计算机系摘要在本文中，我们展示了概率抽象解释的框架可以应用于静态分析概率λ演算。我们首先回顾经典的抽象解释框架。我们选择使用（一阶）严格性分析作为我们的运行示例。我们提出了概率抽象解释的定义，并使用它来构建概率严格性分析。关键词：概率λ-演算，严格性分析，概率抽象解释。1介绍在本文中，我们的目的是展示如何概率抽象解释[8，9]可以用来分析概率λ演算中的术语。我们的运行示例将是一个简单的严格性分析[14，2]。这种分析已被用于非概率设置，以优化懒惰的函数式语言，允许懒惰的评估被取代的渴望评估，而不损害语义。我们建议，在概率设置，严格性分析可能会被用来执行一个更投机的优化，取代1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.0166C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）5⎨只要引入非终止的风险足够低，就可以通过急切的评估来懒惰。为了说明定量因素如何改变经典分析，我们将提出一个借鉴随机过程理论的例子（见[4]的例2.1），这与经济学，特别是风险管理有关。例1.1[随机游走]一家公司从资本上限0开始，在每一个时间步，它的收入是Ini，满足索赔要求的支出是Outi;收入和支出的序列由相互独立且同分布的变量建模。该公司的命运是仿照通过吸收势垒为0的简单随机游走和跳跃步骤n=输入n−输出n：盖n=Capn−1+Stepn，如果Capn−1>0且Capn−1+Stepn>00.00否则定性地说，我们可以分析随机游走，并得出结论，资本上限在区间[0，∞）上变化;定量地说，我们可以问一个更有趣的问题：对于给定的索赔和收入的统计行为，破产的概率是多少？显然，对于以某种方式使用有限计算资源的计算过程，人们也可以提出类似的问题。本文的其余部分组织如下。 我们首先介绍概率λ演算。在下一节中，我们将回顾经典抽象解释的主要特征，并展示如何应用这一框架对应用λ演算的一阶片段进行严格性分析。本文[2]展示了如何将这些思想扩展到高阶情况。然后，我们提出了基于线性算子的语义方法，并描述了概率抽象解释[8，9]。最后主要部分回到概率λ-演算中的严格性分析问题。2概率λ-演算许多作者已经将概率特征引入λ演算，最近的例子见[17]和[16]Danos和Harmer [6]表明，大多数形式的概率行为都可以使用硬币加密来编码。我们遵循这个最简方案，简单地扩展λ-演算，使其能够在项之间进行二元概率选择我们定义概率λ项的类ΛP为最小类，定义如下：C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）5711 p→1pp• 每个变量x都是一个项。• 每一个常数，包括ε，都是一个 项。• 对M，N∈ΛP，（MN）∈ΛP，（λx.M）∈ΛP.• 对于M，N∈ΛP，（M<$pN），对于某个概率p.这是通常的λ项加上形式为M1<$pM2的项（表示概率选择，右手被加数以概率p被选择）。我们假设最左归约策略。我们写e1→pe2是指e1以概率p降为e2。“一”是一个词，“一”是一个词，“一”是一个词。环境;ρ将Var映射到ΛP。术语的语义由以下归约系统给出：（var）（x，ρ）→1ρ（x）（app）（M，ρ）→p（P，ρJ）（（MN），ρ）→p（（PN），ρJ）（β）（（λx.M）N，ρ）→β（M，ρ[x：=N]）（δ）（（M N），ρ）δ（1−p） （M，ρ）（δ2）（（MpN），ρ）→δ（N，ρ）终端配置有一项是λ-项或常数。的app和β规则一起执行最左归约策略。3古典抽象诠释程序分析的目的是在不运行程序的情况下确定程序的某些特性. 一个经典的例子是到达定义分析，它确定，对于一个图表中的每个节点，哪些定义（分配）到达它[15]。这种分析的结果可用于执行程序的常数折叠变换。这样的转换应该是语义保持的，因此重要的是分析给出了关于程序的正确信息。通常我们感兴趣的属性是不可判定的，因此正确性被一些近似概念所取代（见下文）。我们首先概述基于语义的程序分析的经典方法：抽象解释[3，15]。程序的语义f标识了某个值集合V，并指定了程序如何将一个值v1转换为另一个值v2：f→v1−→v2。8C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）5以类似的方式，程序分析识别属性集L，并指定程序f如何将一个属性l1转换为另一个属性l2：f f l1Dl2。正 如 我 们 所 看 到 的 ， 每 一 个 程 序 分 析 都 应 该 是 正 确 的 ，to thesemantics语义.对于一阶程序分析，即那些抽象值的属性的程序分析，这是通过使用正确性关系将属性与值直接联系起来来建立的：R：V×L→{true，false}。目的是vRl形式化了我们的主张，即值v被描述为财产L。为了有用，我们必须证明正确性关系R在计算中是保持不变的：如果关系在初始值和初始性质之间成立，那么它在最终值和最终性质之间也成立这可以表述为v1Rl1fv1−→v2fl1Dl2v2Rl2抽象解释中最常见的情况是V和L都是完备格。然后，我们在R和L之间施加以下关系：（一）（二）v R l1l1±l2v R l2（<$l ∈ LJ<$L：v R l）<$v R. .LJΣ第一个是关于安全性[15]：如果我们有一个正确描述一个值的属性，那么任何更大的属性也是一个安全的描述。 第二个是关于最佳描述的存在性：如果我们有一组正确描述一个值的属性，那么它们的相遇也是一个正确的描述，并且更准确。正确性关系通常通过伽罗瓦连接来实现：（V，α，γ，L）是完备格（V，±）和（L，±）之间的伽罗瓦连接当且仅当α：V→L和γ：L→V是满足以下条件的单调函数：γ<$α±λv.v和α<$γ±λl.l。在定义了一组合适的属性之后，我们接着定义程序操作的合适解释。抽象解释的框架保证了分析是安全的，只要我们对每个语言运算符F使用一个解释Fabs，满足：Fabs±α <$F<$γ。由于有趣的语言涉及迭代或递归，我们还必须构建有效的实现;这个问题的一般解决方案是扩展和扩展理论[3]。C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）59⊥⊥联系我们⎨⎨具体操作诱导操作基本类型常数1如果x那么y否则zx op yxH（yHz）xHy3.1敏捷性分析精确性分析[14，2]的目的是回答一些函数f：是否f =？如果函数具有此属性，则它要么使用其参数，要么是底部函数。在任何一种情况下，一个肯定的答案都意味着参数可以通过值传递，而不是使用（成本更高的）惰性计算。我们将把自己限制在一阶函数语言中，整数是唯一的数据类型。我们可以构造一个伽罗瓦联络（PH（Z_n），α，γ，Two），其中PH是Hoare幂整环构造，Two是0， 1被0 1排序. 在这种情况下，霍尔幂域的元素只是按子集包含排序的下闭集合：即每个集合都包含n。我们定义：如果Z={}，则α（Z）= 001否则如果S= 0，则γ（S）={}如果S= 1，我们可以构造对应于一阶应用λ演算中的操作的导出操作：条件式有三个参数（x，y，z）;谓词必须定义然后结果至少和两个分支中的任何一个一样被定义。因此，（λ x.如果x= 0，则 15，否则 42）是（λ x. （xH1）H（1H1））<$λx.x. 由于（λ x. x）0 = 0这告诉我们，我们的原始函数是严格的。现在我们将这种方法扩展到概率λ演算。我们可以将经典框架应用于这个新的背景[12，13];相反，我们将应用概率抽象解释的技术[8，9]。10C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）5Σ⎨4线性表示集合X上的向量空间V（X）是X中元素的形式线性组合空间，其系数在某个域W中（例如W=R），即V（X）=，cx→x|cx∈W，x∈X，.在我们的扩展演算的术语的语义可以表示为一个概率约简图的边缘标记的概率。我们将每个数量关系RX×W×X关联到一个矩阵，即V（X）上的线性算子MR，定义为：（男）R（xi，wJ，xj）wJ=wR ij0.00否则对于概率关系W=[0，1]，这给出了一个随机矩阵。4.1概率λ-演算的线性语义我们首先定义三个算子，它们分别表示对应于β-约简、δ-约简（对于概率选择）和空闲（对于正规形式的项）的转移每个算子都是V（ΛP）→V（ΛP）型。在定义一步β-归约的运算符之前，我们定义了一个适当的活动上下文的概念-- 给定这种直觉，C[ ]，具有单个孔的活动上下文的类是最小类，使得：• [ ]∈C[]。• 对于任意的C1[]∈C[ ]和N∈ΛP，C1[ ]N∈C算子B（用于β约简）对于每个约束变量x和项N∈ΛP具有以下矩阵表示：B（x，N）t1，t2=1ift1<$C[（λx.M）N]，t2<$C[M[x：=N]]0.00否则用于概率选择运算符的运算符C具有以下内容：C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）511⎪⎨⎨矩阵表示：Ct1，t 2=如果t1<$C[M<$pN]，t2<$C[M]，pift1<$C [M<$pN]，t2<$C[N]我也不知道最后，空操作符N（对于正规形式）具有以下矩阵表示：Nt1， t2 =1如果t1<$t2，t1是βδnf0.00否则算子T描述了从一个项得到的转换，然后定义为：T=C+N+ Nx，NB（x，N）在实践中，我们将限制到从某个给定的项的可达项M：R（M）={N|M→βδN}并使用受限转换操作符：T=πM其中πM是到V（R（M））上的投影。然后，通过迭代地应用T来恢复术语的语义，TevectorrM→表示初始项M：limTiM→.i→∞如果我们只有有限多个可达项，例如，如果给定项M的归约在有限个归约步骤之后终止，则归约算子T（在效果上）仅在有限维子向量空间上操作V（P）。众所周知，有限维向量上的所有拓扑与代数结构相容的空间是等价的[10，7.18节]。这意味着对于有限约简，操作语义的重构将导致相同的限制，与所考虑的拓扑无关。也可以将构造扩展到非终止约简的情况然而，这需要更仔细地考虑用于构造极限的拓扑 为了使我们的介绍简洁，我们将省略对这种情况的详细研究，因为它需要从功能分析和算子理论中获得更详细的概念。12C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）5444⎜⎜⎟⎟13⎜⎝⎟⎠D ›→C⎜⎟†0 0 0 0 0 1 00 0 0 0 0 0 1例4.1考虑这个术语：（（λx. 0）1（λx.x））（342）2 4可达项的枚举是：• （（λx. 0）1（λx.x））（342）2 4• （λx. 0）（中文342）• （λx.x）（λ342）• 0• ⊥ ⊕342• ⊥• 42我们有：⎛0110 0 0 0⎞2 2⎜ ⎟0 0 0 1 0 0 00 0 0 0 1 0 0T=0 0 0 1 0 0 0⎜0 0 0 0 0⎟4 4⎜ ⎟5可能的抽象解释给定两个概率域（即， λ-项上的希尔伯特空间），C和D，概率抽象解释[8，9]是具体域C和抽象域D之间的一对线性映射A：C <$→D和G：D <$→ C，使得G是A的Moore-Penrose伪逆，反之亦然。设C和D是两个Hilbert空间，A：C<$→ D是它们之间的有界线性映射.有界线性映射A=G：是Ai的Moore-Penrose伪逆AG=PA和GA=PG其中PA和PG表示在A和G的范围上的正交投影。或者，如果A是Moore-Penrose可逆的，则其Moore-Penrose伪逆，A<$满足以下条件：(i) AA† A= A，C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）513VV ›→ WWx∈C(ii) A<$ AA<$= A<$，(iii) （AA†）A=AA†，(iv) （A<$A）=A<$A。其中M是M的伴随。将这些方程与经典的设置进行比较是有益的。例如，如果（α，γ）是伽罗瓦插入：α<$γ<$α=α和γ<$α <$γ =γ。构造概率抽象解释的一个简单方法如下：给定表示具体系统概率语义的某个向量空间上的线性算子Φ，以及从具体域到抽象域的线性抽象函数A：，我们来-求A的（唯一的）Moore-Penrose伪逆G=A†。抽象语义可以被定义为抽象域女：= A在经典抽象解释的情况下，以这种方式构造的抽象语义是正确的。在我们的定量设置中，归纳抽象语义是最接近具体语义的语义。这是由于Moore-Penrose伪逆和所谓的最小二乘近似之间的关系，参见例如。[7，5]。更精确地说：设C和D是两个有限维向量空间，A：C→ D是它们之间的线性映射，A<$=G：D →C是Moore- Penrose伪逆。然后向量x0=yG最小化了C中任何向量x和y之间的距离，即infxA − y=x0A − y。换句话说，如果我们考虑方程xA=y，我们可以将一个（精确）解x<$确定为一个向量，其中<$x<$A-y<$=0。特别是在不存在这样的解向量的情况下，我们可以将精确解的概念推广到“伪解”的概念，即我们可以寻找x 0，使得x 0 A是我们可以构造的现在使用Moore-Penrose伪逆来构造与精确解最接近的近似即取x0=yAt。回到我们的程序分析设置，假设我们有一个运算符Φ和一个向量x。我们可以将Φ应用于x并抽象结果，得到xΦA，或者我们可以将抽象运算符应用于抽象向量，得到xAA<$ΦA。理想情况下，我们希望它们是相等的。如果A是可逆的，它的Moore-Penrose伪逆和逆是相同的，我们就完成了。在程序分析中，A从来不是一个方阵（总有一些损失精度），因此AA<$inxAA< $ΦA将导致精度的一些损失14C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）5×K≈||∈∈K⎧⎨⎩如果矩阵不可逆，则Moore-Penrose伪逆尽可能接近逆，因此对于A的特定选择，A<$ΦA是我们可以拥有的Φ的最佳近似6概率分析在许多情况下，特别是在严格性分析中，抽象是一个满射函数。 在这种情况下，抽象的另一种观点是它将具体值映射到等价类。等价关系可以用一种特殊的算子来表示：分类算子。我们称一个n m-矩阵K为分类矩阵，如果它是一个0/ 1-矩阵，其中每行正好有一个非零元素，列至少有一个非零元素。因此，分类矩阵是特殊类型的随机矩阵。我们用K（n，m）表示所有n×m-分类矩阵的集合（m≤n）。 令X ={x1，.，x n}是一个有限集合。 对于每一个等价在X上的关系，其中X/m=m，存在分类矩阵K（n，m），反之亦然。分类矩阵中的每一列表示一个（非空）等价类。分类矩阵K（n，m）的伪逆对应于它的归一化转置或伴随（对于实数K，这些是一致的）。Kt= N（KT）。其中，对于矩阵A，归一化运算N被定义为：N（A）ij=Aija我如果ai=j Aij= 00否则。概率严格性分析的一个合适的抽象将术语分类为未定义、未知或已定义。我们将表达式中的每一项抽象为这些值之一。未知值用于对定义尚未确定的术语进行分类。传统上，0代表明确的非终止，而1代表可能的终止。这里使用三个值可以进行更有信息量的分析这种抽象是通过一个分类算子实现的。C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）515⎜⎟010⎜⎟001⎜⎝100⎟⎠⎜1⎜⎟⎜⎟⎛⎜0 000 010⎞⎟221 10 0 01 0 01例6.1一个适合我们运行的例子的分类矩阵是⎛0 1 0⎞⎜0 1 0⎟K=⎜0 1 0⎟0 0 1它具有Moore-Penrose伪逆Kt=10 0 0⎟⎝4 4 4 4⎠我们原始程序的抽象语义是⎛1 0 0⎞K†TK=11⎝16 2716⎠0 0 1中间的行和列表示未知值。中间行中间列中的值给出了当我们执行时该行中的其他两个值可能会改变多少的界限-在这个意义上，它给出了当前抽象运算符的精度的度量。迭代这个抽象运算符会导致从不知道到不知道的转换概率⎛1 0 0⎞（K†TK）3=7⎝64149864⎠0 0 1实现一个明确的结果变得越来越有可能。这个结果可以用来支持推测性地评估论证的决定将关系解释为线性算子的一个优点是允许我们测量它们。测量线性算子“大小”的标准方法16C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）5T#=1713⎜⎝⎟⎠⎜0⎟⎜0 0 0 1 0 0 0⎟0 0 0 0 0 1 00 0 0 0 0 0 1是通过算子范数，而算子范数又可以在向量范数中具有其起源：• n→xn ≥0• →x• α→x|α|→x• →x+→y例如，我们可以使用1-范数（绝对值之和），欧几里得范数（绝对值平方和的平方根）或上确界范数（绝对值的上确界）。例6.2从约简图计算出的原始程序的精确抽象是：⎛1 0 0⎞⎝8 8⎠0 0 1考虑到这与我们的第一个抽象之间的差异，我们得到：第一名T−K<$TK虽然T#−（K<$TK）3我们已经抽象了T，但我们也可以抽象这个算子。例6.3我们发现：⎛0 0 01013⎞2 8 8⎜ ⎟130 0 0 1 0 0 0⎜ ⎟⎜0 0 0 0 0⎟⎜44⎟⎜0 0 0 0 0⎟ 4 4⎜ ⎟limi→∞T我=T3 =218C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）5175273K T K−（K TK）∞=8不3这一点的抽象是：（K†）3K）=⎛1 0 0⎞⎜⎝32032⎟⎠0 0 1和T−1†ǁ=K T K∞32最后，还应指出：1ǁ† †37结论我们已经回顾了抽象解释的经典方法，并表明，迪皮耶罗和Wiklicky的概率抽象解释的概念是一个自然的模拟的经典框架。我们已经在一个简单的严格性分析的上下文中说明了λ演算的方法。我们工作的一个缺点是，线性语义和严格性分析都没有以组合的方式定义如果我们能够给出一个组合线性语义，我们会期望组合严格性分析是直接的。不幸的是，这必须在未来继续工作，但早期关于λ-演算和算子代数之间关系的工作可能有助于这一努力。引用[1] H. P. Barendregt. Lambda演算：它的语法和语义。1981年北荷兰[2] G.伯恩角Hankin和S.艾布拉姆斯基高阶线性分析的理论与实践。计算机程序设计科学，1986年。[3] P. Cousot和R.库索抽象解释：一种统一的格模型，用于通过构造或近似固定点对程序进行在POPL的会议记录中，第238-252页ACM。[4] D. Cox和H. R.米勒 随机过程理论。 查普曼和霍尔。一九六五年[5] Ben-Israel，A.，Greville，T.：广义逆-理论与应用。第二个EDN。03 The Dog of the Dog（2003）[6] Danos和R.哈默概率游戏语义ACM Transactions on Computational Logic，2001.[7] F.德语Bet Approximation in Inner Product Spaces，CMS Books in Mathematics第7卷。施普林格出版社，纽约-柏林，2001年。#18C. Hankin，H.Wiklicky/Electronic Notes in Theoretical Computer Science 112（2005）5[8] A. Di Pierro和H.维基基并发约束程序设计：面向概率抽象解释。PPDP'00会议记录，2000年ACM。[9] A. Di Pierro和H. 维基基测量抽象解释的精确度。在LOPSTR '00会议记录施普林格出版社[10] W.H. 格鲁布《线性代数》，数学科学基础第97卷。Springer Verlag，纽约，第三版，1967年。[11] P.Malacaria和L.雷尼尔关于算子代数中λ-演算解释的一些结果。在Proceedings of LICS，第63-72页[12] D.蒙尼奥概率程序分析的一种抽象蒙特卡罗方法（扩展摘要）。在POPL的Proceedings，第93-101页，2001年。ACM。[13] D. 蒙尼奥概率程序的向后抽象解释在ESOP '01会议记录Springer Verlag，2001年。[14] A. 迈克罗夫应用程序的抽象解释和优化转换。博士论文，爱丁堡大学，1981年。[15] F. Nielson，H. Riis Nielson和C.汉金程序分析原理。Springer Verlag，1999年。[16] Sungwoo Park 概率语言的演算。ACM SIGPLAN Notices，37（9），pages 206-217，2002.ACM。[17] N. Ramsey和A.Pfe cheer. 随机lambda演算与概率分布单子。在POPL的会议记录中，第154-165页，2002年。ACM。