赋值正规化与代数运算的计算效应与类型相互作用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记298（2013）51-69www.elsevier.com/locate/entcs赋值正规化与代数运算丹尼尔·阿曼爱丁堡大学计算机科学基础实验室山姆·斯塔顿2剑桥大学计算机实验室摘要我们研究计算效应和更高类型之间的相互作用。我们这样做，提出了一个规范化的评估算法的语言函数类型以及计算的ececections。我们用代数理论来处理归一化算法中的计算效应，路上了我们的算法是在一个类别的预层配备部分等价关系的解释。规范化算法及其正确性证明是形式化的依赖类型理论（Agda）。关键词：代数学，类型论，赋值正规化，预层，单子1引言在学习计算机程序时，通常将它们看作是一些方程。本文考虑不纯函数规划的一个方程理论。通过找到这个方程理论的一类标准形式，我们能够直接理解和操纵所研究的概念。此外，有人提出，规范化算法在部分求值中是有用的：如果一个带有自由变量的程序片段在编译时被规范化，那么它通常会运行得更快。1电子邮件：d. ed.ac.uk2电子邮件：sam. cl.cam.ac.uk1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.09.00752D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）51. fng：（（unit-unit）-unit）inp[return fnxout0[h x]，（†）更准确地说，我们介绍了一个小程序在ML类语言。(fn（g：（unit-> unit）-> unit）=>g（ifrecv（）=0 then fn x=>send 0;h x else fn y=>send 1））（ fn （ f ： unit->unit ）=>f （ ） ;f （ ） ）（n）这里recv：unit->bit 和send：bit->unit是网 络通 信原 语， 如Concurrent ML[41]，h：unit->unit是函数类型的自由标识符。请注意，我们不能简单地编译和运行这个程序来找出它做了什么，因为它有一个自由的标识符h，因为它的执行将取决于从网络接收到在我们规范化程序之前，我们将其翻译为一种中间语言，使评估顺序清晰。我们还从程序中删除了位类型，因为它使规范化过程复杂化，并且与我们正在研究的内容正交。(We返回到§ 6中的sum类型问题）。我们通过使用代数运算消除了对位类型的需要，如下[36]：我们用inp[M，N]替换（如果recv（）=0则MelseN），用out 0 [ M ]替换（send 0;M），用out 1 [ M ]替换（send 1; M）。因此，程序（）变为. fnf：（单位-单位）f到y。f返回fn y返回1[返回fn]]到f。 gf中间语言（§2）有一个简单的等式理论，包括β-和η-等式。对于这些方程，程序（†）不是正规形式例如，它具有β-redex。 我们的归一化算法产生以下程序：输入[输出0 [h]到x。输出0 [h]到y。return返回]]，out1 [out1 [return返回]]因此，我们发现程序（xm）的作用：它从网络输入一个位。如果该位为0，则它输出0，调用h，输出0，然后再次调用h。如果来自网络的位是1，则它输出1两次。注意我们是如何用代数签名描述计算结果的：inp是一个二元运算，out0，out1是一元运算。一个重要的观察是，如果我们从计算结果的不同代数签名开始，相同的归一化算法也会起作用许多其他的效应已经用代数的方式描述，包括非确定性，概率，内存访问[36，35，26]和逻辑编程[43]。我们的框架是所有这些例子的通用框架。1.1评价规范化的实质我们在§3中使用评估归一化（NBE）范式定义了我们的归一化算法。这种想法最早由马丁-勒夫[24]讨论，后来由语法中间语言语法正常形式Model：functors，单子和单子群≥指称语义重新分配D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）5153伯杰和施维希滕贝格[8]发展54D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）51有两个关键要素：（1）可执行程序中编程语言的类型理论（Agda3），其中术语被自动规范化;（2）一个1.2指称语义的组成部分我们的NBE指称语义有三个重要组成部分：1.函子范畴中的语义：我们遵循构造指称语义的一般范式，通过找到一个范畴并将类型解释为对象，将程序解释为对象之间的态射。在[14，3，9]之后，我们将指称语义建立在函子的范畴SetRen上，从上下文的范畴Ren这个范畴的行为非常类似于集合范畴，但有额外的特征，允许我们用自由标识符来解释术语。集合Ren的关键特征是，对于中间语言的每一个类型τ，都有一个可区分的对象Ren（τ，−），这个对象的行为就像一个特殊的类型τ的标识符集合。2. 一个剩余的单子：我们的中间语言是莫吉的单子元语言的变体遵循Plotkin和Power [35]，我们从描述计算效应的代数签名中的操作构建单子。然而，对于NBE，我们必须在单子中添加更多：在Filinski的开创性工作[ 13 ]和随后的发展[21，5]之后，我们还将函数类型的标识符应用于参数的例如，在上面的范式（normalform）中，虽然对h的调用结果被忽略，但函数调用可能会产生副作用，这取决于h代表什么。因此，我们保留了3. 使用PER来解释效应项上的方程：除了代数签名中的运算之外，许多计算效应还使用指定其计算行为的附加方程来在[9，33]之后，我们在我们的nbe算法中通过考虑其余域配备有部分等价关系（PERs）的预层来容纳这些效应。这是一个特别优雅的方法，因为从NBE算法的角度来看，我们可以天真地处理集合，然后在证明算法正确性时参考PER1.3贡献我们的主要贡献是建立一个规范化算法，我们有效的功能语言的语义分析。我们的指称语义学（§1.2）的三个组成部分以前没有被组合过通过结合（1）和（2），我们3Agda实施我们的NBE：https://github.com/danelahman/Normalization-By-EvaluationD. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）5155def实现一个干净的和模块化的数学帐户Filinski通过结合（2）和（3），我们能够在表达式（§5）的级别上分析方程和规范化，而不是语言的函数方面我们还提出了一个证明的归一化算法的正确性。我们的证明使用逻辑关系，并进一步利用剩余单子和规范形式的语法致谢我们特别感谢James Chapman对Agda组织化提出的建议。我们还要感谢安德烈·鲍尔、萨姆·林德利、安迪·皮茨和菲尔·斯科特进行了有益的讨论。我们还要感谢Pierre Clairambault，他为我们指出了Okada和Scott这项工作的核心出现在第一位作者的哲学硕士论文中第一作者参加会议得到了爱沙尼亚国家奖学金计划Kristjan Jaak的支持，该计划由阿基米德基金会与教育和研究部合作资助和管理。2一种带有代数运算的我们介绍了一种高阶编程语言的语法和方程理论，该语言使用代数理论结合了计算结果，如下[35]。我们的语言是基于按值调用的范例。求值顺序是完全显式的，因此它更像是一种中间语言而不是前端语言。这种语言基于莫吉2.1代数学概论我们使用代数签名描述了计算中涉及的简单事件[36]。例如，我们可以用二进制操作inp和一元操作out0，out1来描述固定通信信道上的比特输入/输出所涉及的效应。代数表达式inp[M，N]描述了一种计算，该计算首先从通道读取比特，然后如果它是0则作为计算M进行，或者如果它是N则作为计算N进行。为1.表达式out0[M]描述了一种计算，该计算将位0输出到通道，然后作为M继续进行。再举一个例子，我们可以用一个二进制运算来描述非确定性的影响，理解为MN描述了一个行为为M或N的计算。形式上，代数签名由一组运算Op和一个arity赋值ar组成：Op→N。对于输入/输出，设Op={inp，out0，out1}56D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）51defdefdefdefdef并且ar（inp）= 2，ar（out0）= 1，ar（out1）= 1。对于非确定性，设Op={0}且ar（n）= 2。人们通常会强加等式，例如幂等性，交换性和结合性。我们把这个问题的讨论推迟到第5节。在§6中，我们讨论了更一般的代数理论，包括值参数和变量约束。2.2将代数对象扩展到具有更高类型的按值调用语言效应的代数分析涉及一类未指定类型的计算我们现在描述一种类型化语言，暂时使用产品和函数类型：σ，τ∈Ty：：=单位|σ∗τ| σ-τ我们用一个鱼叉符号来表示函数类型σ-τ，以强调函数可能有边项。（Moggi[29]的符号是σ→T（τ）。相反，在我们的语言中，形格转换结构（unit-（−））是单子。我们没有包括其他类型，如和或递归类型，因为我们在这篇文章中的主要目的是提出一个明确的基本框架，为NBE的有效语言与代数有效。我们将在第6节中回到这一点。一个类型上下文是用变量名x，y，z标注的类型列表。我们不需要考虑非类型化术语，因此我们立即在上下文中提供了类型化术语在[20]之后，有两个类型判断：一个是值ΓvV：τ的类型判断，一个是生成器ΓpM：τ的类型判断。这个想法是，价值是没有效果的东西，而生产者可能有副作用。r， x：τ， rJvx：τ简体中文V：τ返回V：τΓvV1：τ1ΓvV2：τ2ΓvV1，V2：τ1τ2V：τ1τ2V：τirpM：σr，x：σpN：τrpM到x。N：τΓ，x：σpN：τΓvfnx：σN：σ-τΓvV：σ-τΓvW：σΓpVW：ττ_pM_1：τ. . . rpMn：rpopτ[M1， . ，Mn]：τ每个n元运算op∈Op都有一个右下规则的实例每一种类型的τ。例如，对于输入/输出签名，我们有这样的语法：rpM：τrpM：τrpinp[M，N]：τrpM：τr=0[M]：τrpM：τr/p输出1[M]：τ2.3等式理论这种语言的方程理论是从λ -calculus的βη-方程、Kleisli合成定律（例如[20，29]）和代数性[40，§3.3]建立的。我们D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）5157defdefdef（）（）（）def已经省略了通常的自反性、对称性、传递性和全等定律。ΓvV1：τ1ΓvV2：τ2Γv#iV1，V2Vi：τiV：τ1τ2ΓvV#1V，#2V：τ1τ2V：unitΓvV：单位r，x：σpM：τrvV：σΓp（fnx：σM）VM[V/x]：τV：V：V，V：V，V：V，V：V，V：Vrp将V返回到x。NN[V/x]：τV：σ-τΓvVfnx：σ（Vx）：σ-τrpM：τrpMM到x。返回x：τrpM：σr，x：σpN：τr，y：τpP：ρrp（M到x. N）到y。 P=x。 （N到Y。P）：ρΓπpM1：σ 。 . . rpMn：σr，x：σpN：τΓpopσ[M1， . . . ，Mn]到X。 N= pτ[M1tox. 不. . . ，Mn到x。N]：τ2.4指称语义我们现在回想一下§2.2 - 2.3中在一个具有充分结构的范畴中语言的指称语义学的一般纲领给定代数签名Op，单子模型由具有以下数据的范畴C给出• 一个选定的carbohydrate封闭结构，即。 选择有限乘积（包括一个终端对象1 ） ， 对 于 所 有 的 对 象 A 和 B ， 一 个 对 象 [A<$B] 连 同 一 个 求 值 态 射 ε ：[A<$B]×A→B ， 使 得 对 于 每 个 f ： C×A→B ， 有 一 个 唯 一 的 态 射 λf ： C→[A<$B]，使得f= ε<$（λf× idA）。• C上的一个强单子T，即对于每个对象A，一个对象T A，一个态射η：A→T A，对于所有对象A和B，一个态射str：A×TB→T（A×B），对于每个态射f：A→TB，一个态射f：TA→TB（也称为f的Kleisli扩张），满足适当的条件（例如[29]）。• 对于每个运算op∈Op，其中ar（op）=n，自然变换T-op：T（−）n→T（−）在函子C →C之间。我们通过将类型解释为对象，将术语解释为态射来解释monad模型中的中间语言。将类型解释为对象公式为：<$unit）=1，<$τ1<$τ2）=<$τ1）×<$τ2），<$σ-τ）=[<$σ）<$T<$τ）]。我们解释上下文（x1：τ1，.，x n：τ n）也作为一个对象，作为其构成类型的解释： （x1：τ1，.，x n：τ n） = τ1 × ··· × τn.也就是说，上下文被解释为该上下文的环境的对象58D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）51（）（）（）把V型判断ΓvV：τ解释为态射Vv：Γ→τ，并给出了V型判断Γp M：τ作为态射<$M）p：<$Γ）−→T <$τ）。D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）5159=π=λ<$N）defdefdefdef（）（）vvvvVV：τvV：τp这些态射是由导子结构的归纳法定义的：（x）vdefXdef<$fnx：σ<$N）vdefpdef（1）v（2V）v=π1π <$V）v=π2π<$V）vdef<$V W）p=ε<$V）v，<$W）vε<$returnV）p=η<$V）vdef∗（V，W）v（1）v=<$V）v，<$W）v=M到X。 N）p=<$N）p，<$M）p<$opτ[M1，.，M n]）p=T-opαM1）p，.，<$Mn）p命题2.1（合理性）在任何单子模型中：如果r∈vV∈W：τ，则Vv=Wv。 IfrpM<$N：τ则Mp=Np。对于单子模型的一个简单例子，让C是集合和它们之间的函数的范畴Set我们可以将包含A且在Op中的运算下闭的最小集合T（A）与任何集合A相关联。这就产生了一个强单子。这个单子的Eilenberg-Moore代数可以理解为集合A，对于每个n元运算op∈Op，集合A都配备有函数An→A。不幸的是，这个集合论模型对于NBE来说不够好，非正式地说，因为它不支持更高类型的rei化我们在§3.2中建立了一个适用于NBE的模型。3通过评估实现NBE的一般程序按照1.1节分为三个步骤进行：识别范式（§3.1），构建支持指称语义的模型（§ 3.2），以及定义从模型到范式的rei fication（§3.3）。3.1正规形我们语言的规范形是基于简单的t型lambda演算的η -长β -规范形。我们最终定义了正常值的判断，正常生成器（PRODUCERS，PRODUCERS）、原子流（ATOMIC，ATOMIC）和原子生成器（ATOMIC，ATOMIC，ATOMIC）。p vΓ►n1 1n2 2pΓ， x：σnN：τnr， x：τ，rJax：τrV1，V2：τ1τ2Γnfnx：σ<$N：σ-τa12an伊春v V：τ一ΓvV：σ-τΓvW：σ一v 单位：unitV：τiVW：τn ann1nnrvV：τrpM：σr，x：σpN：τpM：τ。 . . rpM：τnnΓn1n返回V：τr∈pM到x。N：τp opτ[M，.，M]：τ原子判断是我们用来定义正常判断的一个辅助概念。非正式地，原子判断是从析构函数（投影，函数应用）构建的唯一能用原子生产者做的就是强迫60D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）51任仁它的执行和替代的结果，使用。原子值可以代替变量，而不需要对项进行反规范化3.2一个带标识符我们的NBE算法适用于具有自由变量的程序，即开放程序。为了适应这一点，我们建立了一个集合论模型，其中每种类型都有一个“标识符集”。我们使用预层构造来分类地构建模型，如下[3，9，14]。（名词性集合[32]从语义的角度也是相关的上下文和重命名让Ren成为其对象是我们语言的上下文的类别：类型列表，非正式地一个态射（σ1，...，σ m）−→（τ1，.，τ n）由函数f：m→n给出，使得σ i= τ f（i），其中1 ≤i≤m。态射的复合就是函数的复合。一类预层我们将考虑（协变）预层的范畴集合Ren对象是函子Ren→Set，态射是自然变换。我们将函子F：Ren→Set理解为给每个上下文分配一个集合，该集合可能依赖于该上下文中的自由变量。对态射的函子作用解释了变量的重命名。一个有用的观点是将这个范畴视为直觉主义集合论的模型（例如[23]）。对于任何类型τ，都有一个可表示的预层Ren（τ，−），它可以被认为是一个这些标识符是纯粹的：它们不能被操纵或比较。范畴SetRen有乘积、和和函数空间（例如[23，§III.6]）。• 产品名称： 对于F1，...，设（F1×···×Fn）（Γ）= F1（Γ）×···×Fn（Γ）.• 余积：设（F1+···+Fn）（Γ）=F1（Γ）··········Fn（Γ）.• Carnival闭包：对F，G ∈ Set，设[F<$G]（Γ）= Set （Ren（Γ，−）×F，G）.句法预层对于任 何类型的 τ，我们 都有六个 由§2.2 和§3.1 中的语 法构造构 建的预层Ren→Set：值的预层（VTermsτ），生产者（PTermτ），正常值（NVTermsτ），原子值（AVTermsτ），正常生产者（NPTermτ）def并计算了微处理器的功耗（AP Termsτ）。 例如，VT =τ（r）={VT|V：τ}。预层动作由变量重命名给出：我们令VTermsτ（f）（V）=V[f]。剩余单子我们语义分析的关键是在前层范畴SetRen上剩余单子T。我们从对它的抽象描述开始，接着是具体的归纳定义。D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）5161p（2）（2）ΓΓΓ，x：σΓΓ，x：σΓΓ我们简单地定义了一个剩余化代数为一个预层F：Ren→Set，对于签名Op中的每一个n元运算都有一个自然变换 Fn→F，对于每一个类型τ也有一个自然变换APTermsτ×（[Ren（τ，−）<$F]）→F.来自签名的代数结构解释签名中的效应，并且附加结构描述具有原子产生器的效应的排序。回想一下，原子生产者是涉及自由标识符的函数调用有了适当定义的代数同态，我们得到一个在集合Ren上是一元的范畴。也就是说，剩余化代数的范畴是范畴集合Ren上的强单子T的Eilenberg-Moore代数的范畴。（这是由“粗糙单子性定理”得出的单子T有以下具体的归纳描述。设F：Ren→Set是一个预层。我们定义一个新的预层TF：Ren→Set，使得集合TF（Γ）最不满足以下规则：d∈F（Γ）（T-返回d）∈TF（Γ）r∈TF（r，x：σ）（MT-tox. d）∈TF（Γ）d1∈TF（Γ）. d n∈TF（Γ）T-op（d1，.，d n）∈TF（Γ）functorial操作使用F的操作和原子产品的重命名， 呃。注意剩余单子和正规单子之间的紧密对应（§3.1）：存在自然同构NPTermsτ=T（NVTermsτ）（也参见[21]）。另一种理解单子的方法是把它看作是自由的副产品由代数签名Op生成的单子和由T-to和T-return，asdescri bedyGhani，Uustalu，Ad'amekandothers[1，15].命题3.1范畴SetRen与剩余化单子T一起形成§ 2.4意义下的单子模型。3.3修正和修正回想一下，NBE算法有两个组成部分：模型的指称语义，以及重新定义为范式。我 们 定 义 rei fication作 为两家 庭的自 然转 换 ：v↓τ∈Ty ：τ→NPTermsτ和p↓τ∈Ty：T τ→NPTermsτ。为了说明函数类型的自洽性，必须用反射函数相互定义修正函数，v↑τ∈Ty：AVTermsτ→τ和p↑τ∈Ty：APTermsτ→T τ。•v↓τ：<$τ）→NVTermsτ通过类型τ的结构归纳来定义：v↓单位dd=ef⟨ ⟩v↓τ1<$τ2dd=ef Δv↓τ1（πd），v↓τ2（π（d）v↓σ~τdd=effnx：σ（p↓τ（εd，（v↑σ（x）1262D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）51ΓΓΓΓ，x：σΓΓr，x：τ- （Ⅲ）Ren（τ，−）−→AVTerms−→<$）。τΓ（）（）（）1nτΓ1ΓnΓΓ，x：σΓ，x：σΓ1ΓΓvΓΓΓpΓΓ其中变量被解释为标识符：letid-envΓd=efv↑τ1x， . ，v↑τnxn-是的•p↓τ：T<$τ）→NPTermsτ通过对T<$τ）结构的归纳来定义：p↓τ（T-返回d）d=ef return（v↓τd）p↓τ（MT-至x. d）d=ef M到X。（p↓τ d）p↓τ（T-op（d， . ， d））d=ef op[p↓τd， . . . ，p↓τd]（注意，（p↓τ）是从自然同构NP T sτ = T（NV T sτ）导出的。）• v↑τ：AVTermsτ→<$τ）是通过对类型τ的归纳来定义的：v↑unitVd=ef⟨ ⟩v↑τ1<$τ2Vd=ef πv↑τ1（πV），v↑τ2（πV）Γv↑σ~τVd=efΓ1λd. p↑τΓ（V（v↓σ2（d））def• p↑τ ∈Ty：APTermsτ→ T <$τ）定义为p↑τ M = MT-to x。 （T-返回（v↑τx））。由于变量是原子值，反射态射允许我们从标识符Ren（τ， ）的对象映射 τ，通过复合材料v↑τ3.4归一化算法总结我们现在将指称语义与rei fication结合起来构建一个规范化算法。任何上下文r =（x1：τ1. xn：τ n）有一个环境id-envΓ（在集合Γ中）通过具体化积分，得到了一个值判断函数τ ∈V：τ的标准形。解释Vv： 在环境id-envΓ中，Γ→τ。同样，通过具体化这一解释，找到了降阶判定函数ΓpM：τ的标准形<$M）p：<$r）→T<$τ）在环境id-env<$r：nf（V）d=efv↓τ（<$V）（id-env））nf（M）d=efp↓τ（<$M）（id-env））我们在定理4.1中证明了这种归一化算法的正确性。我们的规范化算法是基于一个纯粹的语义分析。规范化的另一种常用方法是基于穷尽重写语法程序项来计算它们的规范形式。为了进行重写，考虑方程Γv VW：τ和ΓpMN：τ作为重写规则。Lindley和Stark [22]研究了在这种情况下Moggi的一元语言的规范化。他们开发了一种基于TT提升的证明方法，该方法基于简化候选项的简单类型lambda演算的强规范化结果（参见[11]）。D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）5163D⇐⇒vΓ⇐⇒DD⇐⇒DvΓpΓ⇐⇒⇐⇒pΓvpΓpττ第一名τ1τ2MvΓ3.5关于执行情况本节中的算法将编程语言的规范化简化为集合论中的求值。为了使这是一个有效的过程，我们需要以建设性的方式理解“集合的范畴”。我们使用Agda [ 30 ]来实现这一点，Agda是Martin-Léo f的类型理论[ 25 ]的一个实现。我们实现的结构及其正确性证明密切遵循本文的介绍4算法的正确性我们现在证明我们在§3中定义的归一化算法是正确的。我们的证明已经在阿格达正式化了。与[14]类似，正确性的证明分为三个主要定理。定理4.1(i) 规范化尊重等价性。若Γ∈vV∈W：τ则n f（V）=n f（W）。 IfΓpM<$N：τ则nf（M）=nf（N）.(ii) 标准化保持了标准形式。如果r∈nV：τ，则n f（V）=V。 IfΓ<$nM：τ则n f（M）=M。(iii) 项等价于它们的标准形式。如果rvV：τ，则rvVn f（V）：τ。 IfΓpM：τthenΓpMn f（M）：τ.第（i）项直接从语义的可靠性（Prop.2.1和3.1）得出。第（ii）项是通过归纳法证明的正常值/生产商的推导。在本节的其余部分，我们将概述使用逻辑关系对第（iii）项的证明。4.1将价值和生产者与其外延我们首先定义价值/生产者之间的克里普克逻辑关系及其定义，记法：v r（T<$τ）（T）× V项τ（T）和p r（T <$τ）（T）× P项τ（T）。我们通过归纳来定义它们： 关于τ的结构，τ对T.单元vΓdefV P真dτ1τ2Vdef（π1vΓV）<$（π2vΓσ~τvΓdeff ∈ Ren（Γ，Γ J）. j.j.，V.DJ σpΓ⇐⇒pVJ=ε（<$σ-τ）fd，dJ）τ′ （V[f]）VJ（T-返回d）τMdefV. Γ（NT-到X。d）τMdefP.ΓP：τ dτP（T-op（d1... DnpΓτdefpΓM1p... Mn∈PTermsτ （r）。pΓ，x：σrpMopτ[M1， . ，Mn]：ττd1τM1π. . nτMn））V第二名（五）V64D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）51vΓvΓpΓpΓvΓpΓpΓdefdefvΓ↓ΓpΓΓvΓvΓpΓpΓvΓvΓ′vΓ′vΓM[ρ]。¢ ）vvΓvΓppΓvτ命题4.4逻辑关系与具体化和反映很好地相互作用。def命题4.2逻辑关系在等价下不变：如果dτV且ΓvVW：τ则dτW. 如果dτ M和ΓpM<$N：τ则dτN。命题4.3逻辑关系在集合Ren中是次优的。 对于f∈Ren（Γ， ΓJ）：如果dτV，则τ（d）τV [f]。 如果dτM，则（T τ）f（d）τM [f]。（f）f′（f）(i) 若dτV，则Γv（v↓τd）<$V：τ。 IfdτM则Γp（p↓τd）<$M：τ。(ii) 若V为V：τ，则（v↑τV）τV。 IfΓaM：τthen（p↑τM）τM.我们将逻辑关系扩展到环境和同时替换。 对于任何上下文r =（x1：τ1，.，xn：τn），设SubΓ = VTermsτ1× · ··×VTermsτn. SubΓ中的一个元素决定了对Γ中每个变量的一项替换 给定一个判断， V：τ，letV[−] ：SubΓ→V Termsτbe通过y替换定义。类似地，给出了一个乘积r_pM：τ，我们定义M[−]：Subr→PT_sτbysubsti。学费。我们现在定义Γρ（τ）×Sub为eΓρ（τ）∈ Γ。（ex）τ（ρ x）.命题4.5（逻辑关系的基本引理如果ΓvV：τ且eΓ′ ρthen（Ve）τ′ V[ρ]。Iffrp M：τ和eΓ′ ρthen（<$M）e）τ′4.2定理4.1（iii）我们用逻辑关系来证明项与其正规形是等价附加势V：τ。 我们将证明，在f（V）：τ中，（回想一下，nf（V）=（I）（I）（使用Prop。4.4（ii），我们推断身份环境和替换由Γ相关。通过Prop。4.5，（Vid-env）τV.从vΓ′（1）vΓvΓ号提案 4.4（i）weconclu de rvVn f（V）：τ，asrequired. 对于公关人员来说，相似5方程和结果前面章节中描述的归一化过程与§2.3中的方程有关。我们现在讨论如何在两项之间调整方程。5.1效应方程举第一个例子，非确定性的签名通常与半格方程x<$x=x，x<$y=y<$x，x<$（y<$z）=（x<$y）<$z一起考虑。为了在我们的语言中捕捉到这一点，我们通过在eachypeτ处包括这三个等式来扩展生产者等式（ΓpMN：τ，§2.3）：rpM：τrpMMM：τrpM：τrpN：τrpM<$N<$N<$M：τrpM：τrpN：τrpP：τrpM（NP）（MN）P：τvΓD. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）5165pppvpvp我们还使用以下三个规则以及自反性、对称性、传递性和同余性定义了正规形式上的等价关系nn rnn n nrpM：τΓnMMM：τrpM：τrpN：τrnM<$N<$N<$M：τpM：τrpN：τrpP：τrnM（NP）（MN）P：τ我们的NBE算法（§3）遵循这些方程：定理5.1(i) 如果ΓvV<$W：τ，则Γ<$nn f（V）<$n f（W）：τ。若Γ<$pV<$W：τ则Γ<$nn f（M）<$n f（N）：τ.(ii) 如果r∈nV：τ，则n f（V）=V。 IfΓ<$nM：τ则n f（M）=M。(iii) 如果rvV：τ，则rvVn f（V）：τ。 IfΓpM：τthenΓpMn f（M）：τ.虽然我们不必改变NBE算法来尊重等价关系，但我们必须改进剩余化模型以建立正确性（定理5.1）。从语义的角度来看，我们改变了剩余化代数的概念（§ 3.2），要求剩余化代数满足半格方程。这给了我们一个不同的剩余单子，它是在§ 3.2中，我们有一个同构（NPTermsτ/n）n= T（NPTermsτ）.但从实现的角度看，Agda的类型是紧张的，不允许通过等价关系来实现。为了弥补这一点，我们重新审视语义框架。我们将“集合”理解为配备有部分等价关系的Agda类型，遵循Cubric，Dybjer，Scott [ 9 ]和Pitts [ 33，§C.1]。例如，函数类型[X<$Y]配备有以下PER：f<$X→Yg i <$x，xJ：X. x<$XxJ=<$f（x）<$Yg（xJ）。 在这种情况下，我们被引导到重做范畴理论，因此，有关更多细节，请参阅[9]或我们的Agda实现。在我们的分析中，没有关于半格的具体内容。一般来说，我们使用剩余单子上的PER来同样重要的是，PER在归一化算法的构造中不可见。它们只在正确性论证的形式化中起作用（定理5.1）。我们顺便提到一种替代方法，以达到一个合适的模型，以适应方程的有效条件：setoid结构[7]。setoid是一种配备了等价关系的类型（也是反射性的：x）。xx）。该setoid模型具有不同的carriage封闭结构：给定setoid X和Y之间的函数setoid为{f：X→Y|xxJ = f（x）<$Yf（xJ）}。 （这 与PER的域大致相同。）在像Agda这样的证明相关的系统中，规范化算法的基于setoid的实现将用函数类型的所有居民的证明证人来填充。尽管setoid模型在很多方面都表现良好，但PER构造更适合我们的目的，因为它产生的算法不会因证明义务而复杂化66D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）51ppp1均p0defdef5.2结果归一化在前一节中，我们只确定了正则形式，直到方程的有效项。在特定情况下，我们可以做得更好。例如，考虑信号-def def一位存储器单元的性质：Op={lookup，update0，update1}，ar（lookup）= 2，ar（update0）= 1，ar（update1）= 1，具有以下等式[26，35]：x=10okup[update0[x]，updat1[x]]update1[updatejj[x]]=updatejj[x]更新0[lookup[x，y]]=更新0[x]更新1[lookup[x，y]] =更新1[y]（一）其思想是，lookup[M，N]是读取内存的程序，根据结果继续作为M或N，而updatei[M]在继续作为M之前将i写入内存。我们可以按照Mell i ` es [ 26 ]的方法，直接用正规形式表示效应项，而不是给正规生产者配备由这些方程生成的per。 我们使用辅助判断法。Γ►n'n'恩恩恩恩pM：ττpN：τ[M，N]：τrpM：τrpN：τ[更新日期[M]， N]：τrpM：τrpN：τInlookup[M，up date[N]]：τΓ►n'n'n a npM：ττpN：τ伊春V：τn'rpM：σr，x：σpN：τn'p查找[更新1[M]，更新0[N]]：τ返回V：τr∈pM到x。N：τ回想一下，剩余化单子是两个单子的余积在本例中，我们可以将其理解为无效应的剩余化单子（§3.2）和一位状态单子[{0， 1}< $（{0， 1}×（−））]的余积。具体地说，单子的这个余积是下面的最小不动点（遵循[16]中的定义TF= μG。 {0，1}{0，1} ×。F+在这个单子中，等式（1）的商是在类型中进行的，并且不需要PER严格地说，这个单子同构于具有非平凡PER的单子。然而，具体地说，这个定制的monad提供了一个NBE算法，它不仅规范化了更高的类型，而且尽可能地部分评估了命令式命令。为了说明，考虑介绍中的程序（†），但用查找/更新代替了inp/out。我们的算法也对结果进行了归一化，而不是范式（normal form），从而最大限度地减少了写入次数lookup [h]到x. lookup [h]到y. lookup [return jumper，return jumper]，更新0 [h]到y。lookup [return footer，returnfooter]]，return[返回]。D. Ahman，S.Staton/Electronic Notes in Theoretical Computer Science 298（2013）51676关于语言在本文中，我们考虑了一种限制语言，只有足够的功能来证明我们的贡献。虽然递归和和类型等语言特性非常重要，但可以使用文献中的标准技术来处理它们。我们简要概括了主要观点。递归我们的NBE算法是保证终止的，因为它是用Agda编写的。尽管如此，现实的编程语言具有不可终止的潜力这就把我们引向了部分求值和NBE之间长期建立的联系[10，12]。粗略地说，在递归语言中，每个子表达式都应该用它的“绑定时间”来注释Dybjer和Filinski [12，13]概述了如何在一元语言中容纳这一点和类型大多数实用的编程语言都有sum类型。例如，我们可能有一个类型bitof bits，它有两个常量（0， 1），并遵循公式的类型规则：rvV：bitrpM：τrpN：τrpifVthenMelseN：τifithenM0elseM1<$Mi（i= 0，1）MifxthenM[0/x]elseM[1/x]（二）基于预层范畴的语义分析已经被扩展到解释纯语言中没有计算效应的带和类型的NBE[2，6]。Filin-ski [13]和Lindley [21]从更实用的角度讨论了带和的有效语言的nbe 这些语言将类型case表达式视为计算而不是值，这允许它们使用剩余化monad来处理原子值的模式匹配。基类型和局部效应我们的剩余单子是一个前层范畴上的单子。不同的作者使用monad在预层范畴上描述局部事件和名称生成，包括局部存储[27，35，37]，π-演算[42]和逻辑编程[43]。第二位作者最近为这些分析