代数对象与处理程序编程教程

可在www.sciencedirect.com在线获取理论计算机科学电子笔记319（2015）19-35www.elsevier.com/locate/entcs代数学导论特邀辅导论文Matija Pretnar1卢布尔雅那大学数学和物理学院斯洛文尼亚摘要这篇文章是关于代数对象和处理程序的教程。在这本书中，我们解释了什么是代数对象，给出了大量的例子来解释处理程序如何工作，定义了一个操作语义和一个类型对象系统，展示了如何对对象进行推理，并为进一步阅读提供了指针关键词：代数对象，处理程序，对象系统，语义，逻辑，教程代数运算是一种计算结果的方法，其前提是不纯行为来自一组操作，例如可变存储的getset，交互式输入输出的readprint，或异常的raise[16，18]。这自然地产生了处理程序，不仅是异常，但任何其他事件，产生一个新的概念，其中，可以捕获流重定向，回溯，合作多线程，和定界的延续[21，22，5]。我不断听到有人说他们对代数的对象和处理程序感兴趣，但不知道从哪里开始。这就是本教程希望解决的问题。 我们将研究如何使用代数对象和处理程序进行编程，如何对它们建模，以及如何对它们进行推理。本教程不需要特殊的背景知识，除了对编程语言理论的基本熟悉（可以在[8，15]中找到很好的介绍http://dx.doi.org/10.1016/j.entcs.2015.12.0031571-0661/© 2015作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。20M. Pretnar/理论计算机科学电子笔记319（2015）19.......值v：：=x变量true false布尔常量funx›→c函数h处理程序handlerh：：=handler{returnx›→cr，（可选）return子句op1（x;k）›→c1， . ，opn（x;k）<$→cn}操作子句计算c：：=returnvreturnop（v; y. c）操作调用dox←c1 inc2sequencingifv thenc1 elsec2条件.v1v2应用. 用v处理c处理Fig. 1. 一系列条款。1语言在我们深入研究处理程序的例子之前，我们需要确定一种工作语言。由于评估的顺序在处理效果时很重要，我们将语言术语（图1）分为惰性值和潜在有效的计算，遵循称为细粒度按值调用的方法[13]。有几件事值得一提：在dox←c1inc2中，我们首先计算c1，一旦返回一个值，我们将其绑定到x并继续c2。如果x不出现在c2中，我们将排序改为c1;c2。操作调用调用op（v; y. c）将参数值v（例如，要读取的存储器位置）传递给操作op，并且在op执行了e_ect之后，其结果值（例如，存储器位置的内容）被绑定到y，并且重新开始对c的评估，称为延续。但是，请注意，包含处理程序可能会覆盖此行为。在调用中有一个显式的延续对于语义来说是方便的，但对于程序员来说就不那么方便了，因为他们只想得到操作的结果。因此，我们定义了一个函数，而不是一个完整的操作调用，称为泛型对象[18]，也标记为op，它接受一个参数并将其传递给一个具有平凡延续的操作调用OPd=EF funx ›→ op（x; y. return y）虽然使用起来更简单，但泛型对象同样具有表达性，因为我们可以恢复操作调用op（v; y）。c）通过在c中计算doy←opv。语言扩展为了专注于新的构造，我们将保持我们的语言小型化，但对于示例，我们将使用整数、原始值1该材料基于美国空军空军装备司令部空军科学研究办公室的支持工作，FA9550-14-1-0096。M. Pretnar/理论计算机科学电子笔记319（2015）1921−2−112算术函数，字符串，递归函数rec funfx→c，unit（）和pairs（v1，v2）。此外，我们允许绑定构造中的模式（函数、处理程序子句、操作调用和排序）。特别地，我们使用模式来表示被忽略的参数，并且使用对模式（x1，x2）来从对中提取分量。例如，我们在应用程序中将7绑定到x并忽略8（fun（x，）›→6+x）（7， 8）。&在编写最后一个示例时，我们对值和计算的分离有点松懈。由于加法6+x实际上是一个双重应用（（+）6）x，第一个应用（+）6已经是一个计算。因此，它不能应用于x，因为应用程序的两个子项都必须是值。相反，我们需要使用序列并在我们的限制语法中编写示例：（fun（x，）›→dof←（+）6infx）（7， 8）然而，这种较长的形式几乎没有增加任何价值，并且使示例难以阅读，因此在记住它的同时，我们将从现在开始使用较短的形式相反，每当我们在需要计算的地方使用一个值时，我们将隐式地插入return例如，我们应该写funx<$→funy <$<$→ （x，y）而不是funx<$→return（funy <$→return（x，y））。语义观察每个操作调用在evaluation中创建一个分支点，有尽可能多的分支，因为可能有结果可以产生延续。例如，decide将有两个分支，print只有一个，read将有无限多个分支：每个可能的输入一个。因此，我们可以将计算想象成树，其叶子是返回值，分支点称为操作。例如，请参见图2。printdon←get（）inifn0thenprintreturn−n2其他返回n+ 1···打印−4打印−1打印get（）01 23···图二. 计算和相应的树。在存在递归的情况下，树的一些叶子也可以被标记为“n”，以指示不调用任何操作的发散计算。重复调用操作的发散计算由非良基树表示。指称语义将在6.3节中进一步讨论。22M. Pretnar/理论计算机科学电子笔记319（2015）192示例我们现在通过示例非正式地描述处理程序的行为。你也可能更喜欢先看看第3节中给出的操作语义。2.1输入输出让我们从输入输出开始，因为它是一个非常简单的代数对象，但它几乎暴露了处理程序的所有重要方面。它可以通过两个操作来描述：print，它接受一个要打印的消息并产生单位值（），以及read，它接受一个单位值并产生一个被读取的字符串。例如，一个计算要求用户输入他的名字和姓氏，并打印出他的全名，可以写成：printFullNamed=efprint做名字←读（）在打印dosurname←read（）inprint（joinname）其中join是一个函数，它接受两个字符串并在中间用空格连接它们。2.1.1恒定输入处理程序的一个简单示例是：handler{read（;k）›→k“Bob”}其在每次调用read时提供恒定的输入字符串当然，我们可以将其推广为一个函数，该函数接受字符串s并返回一个处理程序，该处理程序将其提供给读取：alwaysReadd=effuns›→handler{read（;k）›→k s}这个处理器的工作方式如下：每当read被调用时，我们忽略它的unit参数，并在函数k中捕获它的延续，该函数k期望得到结果字符串，并在应用时恢复求值。接下来，我们不调用read，而是在handling子句中评估计算：我们恢复continuationk，但不是从交互式输入中读取字符串，而是产生常量字符串s。处理程序隐式地继续处理continuation，因此在处理的计算中的任何读取都将再次产生s。如果被处理的计算调用了除读之外的任何操作，则该调用将转义处理程序，但处理程序再次将自己包装在延续部分周围，以便它可以处理任何进一步的读调用。例如，评估with（alwaysReadM. Pretnar/理论计算机科学电子笔记319（2015）1923首先打印出“What is your name？”因为打印未处理。然后，读取被处理，因此类似地，第二个打印是未处理的，并且在第二次读取中，处理程序是否应该继续处理continuation中的操作，或者只处理第一个调用，这并不明显。异常处理程序的经验在这里不给我们任何指导，因为引发的异常没有延续，所以这两种选择是等效的。事实证明，我们在本文中确定的第一个选择具有更好的指称语义，这是人们在实践中通常希望的，并且可能也更直观，因为使用h处理c表明整个c应该由h处理。第二种选择导致了浅处理程序[10]，这对于某些用途来说更方便，并且可以被认为是一种更基本的方法，因为它们可以通过递归来表达通常的处理程序2.1.2反向输出我们不仅可以使用处理程序来改变延续的内容，还可以改变延续的使用方式。例如，为了颠倒principal的顺序，我们使用：用途：反向d=ef handler{print（s;k）›→k（）;prints}在这里，我们通过首先调用continuation来处理print，只有在完成之后，才打印出s。由于处理程序将自身包装在k周围，因此相同的规则适用于continuation，因此所有的principal都被反转。如果我们定义abcd=ef 打印然后用反向句柄abc打印出第一个“C”，然后“B”，最2.1.3收集输出一个更有用的处理程序是将所有的principal都收集到一个大字符串中，并将其与final值一起收集d=efhandler{returnx›→return（x，““）print（s;k）›→do（x，acc）←k（）in return（x，joins acc）}如果处理的计算没有打印任何东西，只是返回某个值x，我们需要通过返回一个空字符串来处理它。但是如果一个计算打印了一些字符串s，我们就继续延续。由于这是以相同的方式处理的，它除了返回最终值x之外还返回累积的字符串acc。现在，我们只需要将s与acc连接起来，并将它与x一起返回。如果我们用collect处理abc，我们会得到一对（（），24M. Pretnar/理论计算机科学电子笔记319（2015）19我们还可以嵌套处理程序，带收集手柄（带反向手柄abc）计算为（（），我们嵌套处理程序的顺序很重要，因为最里面的处理程序决定了如何首先处理调用。如果我们在上面的例子中切换处理程序，我们得到（（），或者，我们可以使用一种称为参数传递的技术来实现相同的处理程序[22]，其中我们将处理的计算转换为传递参数的函数，在我们的例子中是累积字符串：收集Jd=efhandler{returnx›→funacc›→return（x，acc）print（s;k）›→funacc›→（k（））（joinacc s）}当一个计算返回一个值x时，将不会有进一步的principal，所以我们可以返回给定的累加器acc除了x。但是如果print被调用，我们通过产生预期的单元结果来恢复continuation。由于延续被进一步处理到一个函数中，我们需要传递k（）新的累加器，它是用s扩展的acc。为了获得计算c的收集输出，我们将结果函数应用于空累加器：（带有收集J句柄c）在第5节中，我们证明了collect和collectJ确实表现出等效的行为。使用参数传递，我们还可以实现一个逆向处理程序，将给定字符串中的单词输入到输入。2.2例外当然，异常处理程序是处理程序的一个特殊实例。我们用一个操作raise来表示异常，该操作接受一个异常参数（例如错误消息），并且不产生任何结果（有关如何强制执行的更多细节，请参见例4.1）。在实践中，异常处理程序很少被重用，但更通用的异常处理程序的示例是：默认d=effunx›→handler{raise（;）›→returnx}在处理的计算引发异常的情况下返回默认值x2.3非决定论处理程序不仅可以用来覆盖现有的有效行为，还可以定义新的行为。为了实现非确定性，我们采取一个单一的操作decide，M. Pretnar/理论计算机科学电子笔记319（2015）1925它接受一个单位参数，并且非确定性地产生一个布尔值。然后，可以将二元选择实现为函数选择d=effun（x，y）›→dob←decide（）inifbthen（returnx）else（returny）然而，与print不同的是，我们假设decide没有内在行为，我们必须使用处理程序来确定是否返回固定结果，随机结果，最佳结果或所有结果。如果没有包含处理程序，应用程序choose（3，4）在遇到decide调用时会卡住。最简单的decide处理程序是pickTrued=efhandler{decide（;k）›→ktrue}这使得每一个决定都服从于连续性，所以choose总是选择左边的参数。如果我们定义chooosedid=efdox1←choose（15， 30）in dox2←choose（5，10）in return（x1−x2）然后使用pickTrue句柄pickDiDi将为x1选择15，为x2选择5，因此将返回10。2.3.1最大结果使用handler，我们还可以遍历所有可能的分支来选择最大结果：pickMaxd=efhandler{decide（;k）›→doxt<$ktrue indoxf<$kfalse inreturnmax（xt，xf）}在这种情况下，使用pickTrue句柄pickeDi进行计算将做出获得最大可能差异25所需的选择，即使这意味着选择较小的参数choose（特别是，我们为x1选择30，为x2选择5）。如果我们在我们的语言中包含列表，我们可以将pickMax适配为选择所有可能结果的处理程序pickAll[5]。为此，return子句将返回一个包含返回值的singleton列表，而decide子句将连接列表xt和xf，这两个列表是从产生两个可能的结果到处理的延续中产生的。2.3.2回溯为了实现回溯，我们对给定的解决方案采用非确定性搜索，我们添加了一个操作失败来表示不存在解决方案。那么对于26M. Pretnar/理论计算机科学电子笔记319（2015）19←举例说明：recfun seInt（m，n）›→如果m>n则fail（）elsedob←decide（）inifbthen（returnm）elsebaseInt（m+1，n）是一个非确定性地选择区间[m，n]中的整数的函数，或者如果该区间为空则失败，而：pythagoreand=effun（m，n）›→做一个←函数Int（m，n−1），（a+1，n）在ifisSquuare（a2+b2）then（return（a，b，a2+b2））elsefail（）是一个函数，用于搜索整数勾股三元组（a，b，c），使得m≤a b≤n。我们通过处理每个决策来执行回溯，首先尝试产生true，如果失败，则产生false：回溯d=efhandler{decide（;k）›→与handler{fail（;）›→kfalse}handlektrue}然后，使用回溯句柄pythagorean（m，n）找到（5， 12， 13）（m，n）=（4，15），但失败（m，n）=（7， 10）。找到的确切三元组取决于处理程序的实现。相反，如果我们首先尝试产生false，则（m，n）=（4，15）的结果三元组将是（9，12，15）。为了得到所有可能的三元组的列表，我们可以使用2.3.1节中的处理程序pickAll，但是扩展了一个子句，处理空列表的失败2.4状态我们用操作set来表示状态，set用于设置状态内容，get用于读取状态内容。为了简单起见，我们假设一个单一的内存位置保存一个整数。因此，set接受一个整数，存储它，并返回一个单位结果，而get接受一个单位参数，读取存储的整数，并返回它。我们可以使用处理程序临时更改存储的值或记录所有更新。但是我们也可以使用它们来实现有状态行为，即使我们不假设一个内置的。与2.1.3节一样，我们使用参M. Pretnar/理论计算机科学电子笔记319（2015）1927数传递处理程序来传递28M. Pretnar/理论计算机科学电子笔记319（2015）19围绕当前状态：状态d=efhandler{get（;k）›→funs›→（ks）sset（s;k）›→fun›→（k（））sreturnx›→fun returnx}我们使用一个函数来处理get，该函数接受当前状态s并首先传递它由于get到continuation，然后再次作为未改变的状态。相反，我们处理set首先产生单位结果，然后将处理后的延续应用于get参数中给定的新状态s。state的return子句忽略了final state，但是如果我们想检查它，我们可以通过将return子句改为：returnx›→funs›→return（s，x）2.4.1交易以类似的方式，我们可以实现transactional memory，只有在处理的计算成功终止一个值后，我们才提交更改的状态，所以如果引发异常，内存内容保持不变：交易d=efhandler{get（;k）›→funs›→（ks）sset（s;k）›→fun›→（k（））sreturnx›→funs›→sets;returnx}3操作语义为了使关于计算行为的直观具体化，我们现在给出一个操作语义。它背后的思想是操作调用不执行实际的操作（例如，打印到输出设备），而是表现为向外传播的信号，直到它们到达具有匹配子句的处理程序。为了简单起见，任何逃逸所有处理程序的操作调用都将被视为终止计算，即不会进一步减少的计算。我们可以假设实际的有效行为是由最外层的处理程序模拟的，或者考虑6.5节中列出的方法之一。小步操作语义使用关系c~cJ给出，定义见图3。注意，对于价值来说，没有这样的关系，因为它们是惰性的。条件和函数应用的规则是标准的。对于在 c2中排序dox←c1，我们从计算c1开始。如果它返回值v，我们将它绑定到x并evalu-吃了C2。但是如果c1调用了一个操作，我们将把调用向外传播，并将进一步的求值推迟到调用的继续，如图4所示。对于使用h句柄c进行处理，行为类似。我们从计算c开始，如果它返回一个值，我们继续计算h的return子句。如果c调用一个操作op，有两个选择：如果h有一个匹配op的子句，我们开始计算它，传入参数和处理的延续;如果没有，我们M. Pretnar/理论计算机科学电子笔记319（2015）1929..c1~c′1dox<$c1inc2~dox<$c′1 inc2dox<$returnv inc~c[v/x]dox←op（v; y. c1）在c2~op（v; y. dox←c1inc2）if true thenc1elsec2~c1iffalsethenc1 elsec2~c2（funx<$→c）v~c[v/x]在以下规则中，我们设置h=handler{returnx>→cr，op1（x;k）>→c1， . . . ，opn（x;k）<$→cn}：c~c′withhhandlec~withhhandlec′withhhandle（returnv）~cr[v/x]用h处理opi（v;y. c）~ci[v/x，（funy<$→withhhandlec）/k]（1≤i≤n）使用h句柄op（v; y. c）~ op（v; y. 带h手柄c）（op ∈ {op1，.，（操作n}）图三. 阶跃关系。dox1<$（dox2<$op（x; y. c2）inc1）inc~dox1←op（x; y. dox2←c2inc1）inc~op（x; y. do x1←（do x2← c2in c1）in c）图四、在最里面的序列中，op的调用向外传播，直到到达顶部。向外传播调用，并将进一步的处理推迟到continuation，就像在排序中一样。4类型系统为了确保评估顺利进行，我们按照[4，10]中提出的思路引入了一个类型和结果系统。正如我们将术语分为值和计算一样，我们将类型分为值类型和计算类型，如图5所示。值类型A，B：：=bool布尔类型A→C函数类型C语言处理程序类型计算类型C，D：：=一个！{op1，.， 操作n}图五. 的类型。值类型A→C被赋予接受类型A的值并执行类型C的计算的函数，而处理程序类型CD被赋予将类型C的计算转换为类型D的处理程序。 每个计算类型都有A的形式！Δ，其中A是计算返回的值的类型，Δ是它可能调用的操作的集合，即集合Δ是下式的过度近似30M. Pretnar/理论计算机科学电子笔记319（2015）19实际调用的操作。还要注意，Δ不包含有关出现次数、传递参数或操作顺序的有关操作的键入信息在以下形式的签名文件中给出：{op1：A1→B1，.，操作n：An→Bn}其将参数值类型Ai和结果值类型Bi分配给每个操作opi。例4.1假设值类型被扩展为整数的int类型、字符串的str类型、单元类型（它被赋予单元值（））和空类型void，我们在第2节中看到的操作可以被赋予以下类型：print ： str→unitread：unit→strraise ：str→voiddecide：unit→boolfail：unit →voidget：unit→intset：int →unit因为没有void类型的值，所以对raise或fail的调用会有效地中止继续，因为没有处理程序可以通过产生合适的值来恢复它。在图6中，我们定义了两个类型判断：对于值，为Γv：A;对于值，为Γc：Cfor computations计算.在这两种情况下，上下文Γ都是将值类型赋值给变量。（x：A）∈Γrx：Artrue：boolrfalse：boolr，x：AΔ′Σr，x：Ac：CΓfunx›→c：A→C（opi：Ai→Bi）∈πΓ， x：Ai， k：Bi→B！ Δ′ci：B！ Δ′1≤i≤nΔ\{ op i } 1 ≤i ≤ n Δ\{ op i } 1≤i≤nΔ′r}处理程序{returnx<$→cr，op1（x;k）<$→c1， . ，opn（x;k）<$→cn}：A！ 啊！Δ′中文（简体）返回v：A！Δ（op：Aop→Bop）∈rv：Aopr，y：Bop c：A！ Δop∈ΔΓ op（v; y. c）：A！Δ第一个！Δ r，x：Ac2：B！Δ在c2：B中的rdox←c1！Δrv：boolrc1：Crc2：Crifvthenc1elsec2：CΓv1：A→CΓv2：AΓv1v2：Crv：C Drc：Crwithvhandlec：D见图6。 打字判决。打字规则没有什么奇怪的，除了：M. Pretnar/理论计算机科学电子笔记319（2015）1931→返回你可能会期望结论是Γreturnv：A！这是人们可以分配的最精确的类型。然而，我们以允许较粗糙类型的形式给出所有规则，因为这不会失去一般性（例如，在这个特定规则中，我们可以设置Δ=Δ），对于我们的目的是可满足的，并且导致更简单的类型系统。参见[23]，了解一个产生更精确类型的算法类似地，我们可以假设虽然Δ包含op，但即使c不调用op，它也可以被分配给连续c。处理根据上面的解释，CD被赋予处理程序，将C类型的计算转换为D类型的计算，处理行为像函数的应用程序给处理程序一个类型A！啊！ΔJ，我们需要检查它是否正确地处理返回值和操作，无论是否有匹配的操作子句。对于返回值，很简单：给定一个A类型的值，return子句必须是B类型的计算！ΔJ。接下来，对于每个已处理的操作opi：Ai Bi，处理子句再次需要是类型B的计算！ΔJ。在这里，参数应该具有类型Ai，由λ确定。类似地，捕获的延续是一个函数，它接受Bi类型的结果并执行B类型的计算！ΔJ。请注意，即使处理的计算具有类型A！Δ，延续有一个不同的类型，因为它是进一步处理。最后，我们要处理的计算调用操作没有匹配的操作子句在处理程序。对于这种情况，我们允许Δ包含不在{opi}1≤i≤n中的操作，但是任何这样的操作也必须出现在ΔJ中，因为它也可以在处理的计算中被调用（因此也可以在处理的操作的延续给定的类型化系统可以确保良好类型化的计算不会卡住[4]。定理4.2（安全性）如果：Δ成立，则：• c=返回v，对于某个bv：A，或者• c = op（v; y. cJ）对于某个op∈ Δ，或• c~cJfor some cJ：A！Δ。5推理回想一下，如果我们可以将第一项的任何出现与第二项交换，而不考虑周围程序的可观测性质，那么两项在观测上是等价的由于语法上的分离，我们定义了计算（ccJ）和值（vvJ）的观测等价性。我们可以证明[4]，它是一个同余，并且满足图7中给出的基本等价集合。我们可以用来推理代数结果的主要新工具是归纳原理[20，4]，它指出，对于一个给定的谓词φ，φ（c）32M. Pretnar/理论计算机科学电子笔记319（2015）19dox← returnv inc c[v/x]（一）dox←op（v; y. c1）在c2中 op（v; y. dox←c1inc2）（二）dox←c in returnx C（三）dox2←（dox1←c1inc2）inc3 dox1←c1in（dox2←c2inc3）（四）if true thenc1 elsec2 C1（五）if false thenc1 elsec2 C2（六）ifvthenc[true/x]elsec[false/x] c[v/x]（七）（funx›→c） c[v/x]（八）funx›→v x v（九）在以下规则中，w e h=handler{returnx>→cr，op1（x;k）>→c1， . ，opn（x;k）<$→cn}：带h句柄（returnv） [v/x]（10）使用h句柄（opi（v;y. c））ci[v/x，（funy<$→withhhandlec）/k]（1≤i≤n）（十一）使用h句柄（op（v;y. （c））dupop（v;y. 带h手柄c）（op∈{opi}1≤i≤n）（12）with（handler{returnx→c2}）handlec1在c2中执行x←c1（13）见图7。基本等同。对于所有计算c成立，如果：(i) φ（returnv）对所有值v都成立，(ii) φ（op（v; y. cJ））对于所有操作op和参数v都成立，如果我们假设φ（cJ）对所有可能的结果y成立。我们可以使用归纳原理来推导等价式（3）、（4）和（13），但为了更有趣的例子，让我们展示处理程序收集和收集2.1.3节中的J表现出等价的行为，特别是withcollecthandlec在g中执行g←（withcollectJhandlec）为了成功地进行归纳，我们需要证明一个更强的声明，即对于任何字符串，s0，我们有do（x1，s1）←（带有收集句柄c）返回（x1，joins0s1）dog←（withcollectJhandlec）ing s0我们通过设置s0=““来恢复期望的目标。 关于c的归纳如下：M. Pretnar/理论计算机科学电子笔记319（2015）1933(i) 基本情况是平凡的：如果c=returnv，两边都等于return（v，s0）。(ii) 对于当c = op（v; y. cJ），我们有两种可能性：34M. Pretnar/理论计算机科学电子笔记319（2015）19op/=print，这也是很简单的，或者op=print，我们在这里显示：do（x1，s1）←（with collect handle print（s2;. cJ））in return（x1，joins0s1）第11章（8）10）intn =1（do（x，acc）←（带有collect句柄cJ）in return（x，joins2acc））in return（x1，joinss1）中国（4）do（x，acc）←（带有收集句柄cJ）indo（x1，s1）←（return（x，joins2acc））in return（x1，joins0s1）中国（1）do（x，acc）←（带有收集句柄cJ）in return（x，joins0（joins2acc））关联性（associativity ofjoin）do（x，acc）←（带有收集句柄cJ）in return（x，join（joins0s2）acc）归纳假说dof←（withcollectJhandlecJ）inf（joins0s2）（1）（8）dog←return（funacc›→dof←（withcollectJhandlecJ）inf（joinacc s2））单位为g s0第11章（8）dog ←（with collectJhandle print（s2;. cJ）），单位为g s06进一步阅读6.1按推值调用按推值调用[12]是细粒度按值调用方法的演变版本虽然在本教程中使用了后者，因为它更接近于更熟悉的call-by-value，但最近关于代数效应的工作的重要部分使用了前者。要比较给定的操作语义和输出系统与按推值调用设置中完成的操作语义和输出系统，请参见[10]，而指称语义和推理，请参见[22]。6.2使用处理程序第2节列举的例子并非详尽无遗。对于更多涉及的例子，包括多线程，分隔延续，选择泛函，文本处理，资源管理，效率回溯，或逻辑编程，见[5，10，6，25]。处理程序的许多实现也如雨后春笋般涌现，无论是作为独立的语言[3，14]，还是作为现有语言中的库[10，6，25]。最近，OCaml [1]的多核[2]分支已经开始采用处理程序作为实现并发原语的一种方式。M. Pretnar/理论计算机科学电子笔记319（2015）1935（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ））（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（2）6.3指称语义在朴素的设置中，操作只返回一阶值，没有递归，我们可以用集合A解释每个值类型A，而计算类型A！Δ被解释为树的集合（类似于第1节中描述的树），叶子在A中，节点对应于Δ中的操作处理程序被解释为树之间的函数，并通过处理计算的树上的结构递归来定义，而处理则通过应用这些函数来解释。更抽象地说，我们将Δ的模型定义为一个集合M和一个映射对于每个运算op：A→B∈ Δ，op M：A × MB → M，而模型M和N之间的同态被定义为映射h：M→N，使得（hopM）（x，k）= opN（x，hk）. 事实证明一个！Δ 正是免费模式A上Δ的同态h，即具有以下普适性质的模型：给定Δ的任意模型M和任意映射f：A→M，存在唯一的同态h：A！Δ→M，在叶上与f一致。我们可以使用这个通用属性来解释处理程序：操作子句定义操作模型，return子句提供了可以扩展为同态的函数f。更多详情，请参见[22]。在递归和高阶结果的一般设置中，我们需要从集合切换到域，但一般思想是相同的[4]。6.4代数理论传统上，代数效应不仅由一组运算来描述，而且还由捕捉它们的性质的方程理论来描述。例如，非决定性可以用二元运算决定和陈述其幂等性、交换性和结合性的方程来表示[18，9，17]。方程的好处是它们验证了某些程序优化[11]，并更好地捕捉了有效的操作行为。通过对这些理论的各种扩展，人们也可以描述复杂的效应，例如即使在没有处理程序的情况下的控制流跳跃[7]或量子计算[24]。然而，许多计算上感兴趣的处理程序（例如第2.3.2节的回溯）不遵守这些方程，因此无法接收上述的同态解释[22]。由于这个原因，目前对处理程序的研究没有假设这样的方程，但连接存在于两个方向：一方面，我们仍然可以通过假设一个平凡的方程理论来应用以前的结果，另一方面，我们可以使用推理技术从处理程序的行为中恢复方程[4]。6.5模拟实际效果人们可以用一个共模型来模拟因此，当操作调用op（v; y. c）转义所有处理程序，我们将当前状态w∈W和参数v传递给opW，并返回新状态和结果，我们将其分配给y并继续计算c。更多的细节，见[5，4.1节]，这是基于一个更抽象的处理36M. Pretnar/理论计算机科学电子笔记319（2015）19在[19]中，更详细地解释了模型和共模型之间的对偶性确认我要感谢Andrej Bauer和Alex Simpson提供的真正有用的反馈。引用[1] 奥卡姆网址http://ocaml.org[2] Ocaml多核分支。URLhttps://github.com/ocamllabs/ocaml-multicore[3] 鲍尔A.和M.普雷特纳尔网址http://www.eff-lang.org[4] 鲍尔A.和M. Pretnar，An Escherect System for Algebraic Escherects and Handlers，Logical Methods inComputer Science10（2014）。URLhttp://dx.doi.org/10.2168/LMCS-10(4:9)2014[5] 鲍尔A.和M. Pretnar，Programming with algebraic ections and handlers，J. Log.代数Meth.程序. 84（2015），pp. 108-123URLhttp://dx.doi.org/10.1016/j.jlamp.2014.02.001[6] Brady，E.，用代数效应和依赖类型进行程序设计和推理，在：G。Morrisett和T. Uustalu，editors，ACM SIGPLAN International Conference on Functional Programming，ICFP133-144。URLhttp://doi.acm.org/10.1145/2500365.2500581[7] Fiore，M.和S. Staton，Substitution，jumps，and algebraic effects，in：T. A. Henzinger和D.第二十三届EACSL计算机科学逻辑年会（CSL）和第二十九届ACM/IEEE计算机科学逻辑研讨会（LICS）联席会议，CSL-LICS第四十一章。URLhttp://doi.acm.org/10.1145/2603088.2603163[8] 哈珀河，[9]Hyland，M.，G. D. Plotkin和J.功率，组合效应：总和和张量，理论。Comput. Sci. 357（2006），pp. 70比99URLhttp://dx.doi.org/10.1016/j.tcs.2006.03.013[10] Kammar，O.，S. Lindley和N.Oury，Handlers in action，in：G.Morrisett和T.Uustalu，编辑，ACM SIGPLAN函数式编程国际会议，ICFP-2013年日（2013年），pp. 145-158.URLhttp://doi.acm.org/10.1145/2500365.2500590[11] 卡马尔岛和G. D. Plotkin，电子束相关优化的代数基础，在：J.Field和M。Hicks，editors，Proceedingsof the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ， POPL2012，Philadelphia，Pennsylvania，USA，January 22-28，2012（2012）. 349-360URLhttp://doi.acm.org/10.1145/2103656.2103698[12] Levy，P. B.，“Call-By-Push-Value: A Functional/Imperative Synthesis,” Semantics Structures in[13] Levy，P.B、J. Power和H.Thielecke，在按值调用编程语言中建模环境，Inf.Comput. 185（2003），pp.182-210网址http：//dx.doi.org/10.1016/S0890-5401（03）00088-9[14] McBride，C.，Frank.URLhttps://hackage.haskell.org/package/Frank/[15] 皮尔斯湾C.的方法，“Types and programming languages,” MIT Press,[16] Plotkin，G. D. 和J. Power，代数效应的计算性，在：F. Hon