代数和余代数在函数规划中的新方法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记279（3）（2011）41-62www.elsevier.com/locate/entcs用代数和余代数研究函数规划的一些新方法ViliamSlodiBuccak1，2PavolMacko3香港科技大学计算机与信息学系Kosice，斯洛伐克共和国摘要本文讨论了函数式程序设计中递归和协递归的表示。我们分别讨论了表示递归和上递归的态射。这里我们特别考虑变质作用、变质作用和它们的组成，称为质形作用。本文的主要工作是描述一种利用半同态编程计算阶乘函数的新方法我们表明，使用hylomorphism是一种替代方法的阶乘计算递归方法编程经典。我们的新方法，我们描述的动作语义，这是一个新的形式化方法的程序描述。关键词：递归，对偶，超纯，代数，递归余代数，动作语义。1引言递归在现代编程语言中是一个非常有用的工具，特别是当我们处理归纳数据结构时，如列表，树等。递归函数理论是由KurtGüodel和StephenKleene在20世纪30年代提出的。递归在数学和计算机科学中有着重要的地位。递归方法为许多计算算法提供了非常有趣的解决方案它是函数式编程固有的一部分。另一方面，对偶方法协递归的出现给程序设计带来了新的机遇.在第二节中，我们从范畴理论中阐述了基本概念，范畴理论是近十年来理论信息学发展的重要数学工具。第3节描述递归和协递归之间的关系这种关系由对偶数学结构--代数和1这项工作得到了VEGA基金No.1/0015/10的支持：用于自动软件开发的基于知识的语言的语义丰富和适应的原则和方法。2电子邮件：viliam. tuke.sk3电子邮件：pavol. tuke.sk1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.11.03742V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）余代数[32].代数用于对程序结构进行建模，余代数对于定义行为语义有很大的补充[21]。余代数能够描述简单结构的行为，如自动机[1]，入侵检测系统[20]，计算机模拟[13]到数据库系统[19]。通过使用coalge- bras，我们通常可以对不能用代数建模的结构进行建模;例如，无限数据结构（codata）作为协递归的基础[16，26，29]。需要注意的是，数据类型和余数据类型分别被建模为初始代数和终端余代数。另一方面，递归和上递归分别由称为变形和变形的态射建模。在下一节中，我们基于唯一的余代数到代数的同态（称为质同态）构造一个递归余代数。在最后一节中，我们展示了如何在函数式编程中使用引入的态射，并使用递归和协递归创建一种新的非传统编程计算和评估的结果，我们提出了行动语义，这是一个新的方法来定义程序的语义。动作语义学是一种形式化描述程序设计语言的框架。与其他框架相比，它的主要优势是实用性：动作语义描述能够平滑地扩展到现实的编程语言。在我们的论文中，我们展示了我们的替代方法的阶乘计算的评价。2类别信息学中的代数和余代数概念是以范畴理论为基础的[4，14]。范畴C是由对象组成的数学结构，例如A，B，C，. 范畴论不是仅仅关注表示给定结构的单个对象，而是强调态射-对象之间的结构保持映射f：A → B [5]。 每个对象都有单位态射idA：A→A，并且态射是可合成的-对于态射f：A→B，g：B→C它必须存在f∈g：A→C。态射的复合具有结合性。 因为范畴的对象可以是任意的结构，范畴在计算机科学中很有用，我们经常使用更复杂的结构，而不是用集合来表达。因为范畴本身是一个数学结构，我们能够构造范畴之间的态射，称为函子，例如。从范畴C到范畴D的函子F：C→D。3递归与协递归递归函数是这样的函数，其某个参数的结果依赖于其他参数（在某种意义上更小）的结果。递归在数学和理论计算机科学中是一种定义函数的方法，其中定义的函数在其自身的定义中应用。它在从计算的理论基础到实际编程技术的应用中是非常重要的概念自去年以来，越来越清楚的是，对偶但不太知名的上递归概念就像V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）43有用的. Moss和Danner在他们的工作[22]中使用了上递归程序的概念，该概念适用于范围是递归定义为最大解的函数一个以最大不动点表示的方程。 我们使用双重 术语递归程序，用于定义域递归地定义为某个方程的最小解（最小不动点）的函数[12]。为了以不同的方式说明这一点，协递归产生（可能）无限的数据结构，递归消耗这些数据结构。3.1初始代数与蜕变设F是从C到C的闭函子。F-代数是一个对（A，α），其中称为载体的A是一个对象，代数结构α：FA→A是一个态射inC.对于任意两个F-代数（A，α）和（C，γ），态射f：A→C是F-代数之间的同态-从（A，α）到（C，γ），如果图1中的图交换。FAα）AFffV VFC） CγFig. 1.代数图图1中的图的交换性意味着下面的等式成立αf = Ffγ。因为代数是齐次结构，并且代数同态被定义，我们也能够为每个代数定义一个恒等态射，并且适当的态射是可合成的。这意味着我们可以构造F-代数Alg（F）的范畴，其中代数是范畴对象，代数同态是范畴态射。一个F-代数称为初始F-代数，如果它是F-代数范畴Alg（F）内函子的初始代数的存在性受到以下事实的限制：初始代数，如果它们存在，必须满足以下值得注意的性质：• 它们直到同构都是唯一的，因此我们将初始F-代数记为u：FU=U;• 初始代数有一个逆u−1：U→FU。换句话说，从第一个性质可以得出至多存在一个初始F-代数。由于从初始F-代数到每个F-代数都存在唯一的同态，因此初始F-代数是范畴中的初始对象44V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）∼Alg（F）.文[17]证明了初始F-代数是闭函子F的最小不动点。初始代数是单调函数的最小不动点的推广，因为它们具有到任意F-代数的唯一映射。设F是初始代数的代数结构。 函子的最小不动点我们把F记为μF。 给定任意范畴C上的任意内函子F：C→C，如果（μF，inF）是初始F-代数，则在F：F中μF→μF是同构，FμF = μF [3]。初始性为归纳和递归提供了一个一般框架。给定一个函子F，初始F-代数（μF，inF）的存在性意味着对任何F-代数（A，α），存在唯一的从（μF，inF）到（A，α）的代数同态.在[10]之后，我们用（cata α）F（或仅用cata α）表示这个同态如果函子F是明确的），那么（cata α）F：μF→A被刻画为泛性质在F中，f = Ff <$α惠f =（cata α）F。类型信息在图2的交换图中示出。在[31]是变质作用的证明性质FμFinF）μFFf cata αV VFA） Aα图二.初始代数和catamorfism形式为（cata α）F的态射称为退化态射;结构为（cata（））F的态射是一个迭代器。3.2终端余代数与变形余代数是代数的对偶结构。设F是从C到C的闭函子。一个F-余代数是一个对（U，F），其中U称为状态空间，F：U→FU称为余代数结构（或余代数动力学）。对于任意两个F-余代数（U，n）和（V，n），态射g：U→V称为F-余代数之间从（U，n）到（V，n）的同态，因此图1中的图3次通勤所以它保持了Fg = gF-余代数和它们之间的同态构成一个范畴.范畴Coalg（F）是以F-余代数为对象，同态为它们之间的同态的范畴.构成和恒等式是从范畴的定义中一个F-余代数被称为是一个终结子V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）45U）FUg FgV VV） FVψ图三.余代数图F-余代数，如果它是范畴Coalg（F）的终结对象.终结F-余代数（νF，outF）的存在性意味着对任何F-余代数（U，n），存在唯一的从（U，n）到（νF，outF）的余代数同态.这个同态记为（ana）F. 以此类推，态射（ana）F：U→νF 其特点是g=（ana）F.类型信息在图1的交换图中示出四、U）FU安娜·菲格V VνF） F νF出F图四、终结余代数与变形图形式为（ana）F的态射（或者如果函子F是明确的，则仅为ana α）称为变形，并且（ana（））F的结构是一个复迭子。3.3递归余代数递归余代数的概念，即一个余代数有一个唯一的余代数到代数的态射到每个代数是重要的余代数和代数之间的关系的公式在同一范畴。特别是递归余代数将泛性质扩展到被认为是余代数的初始代数之外[2，6]。设F：C→C是闭函子。余代数（U，α）称为递归余代数，对于每个代数（A，α），在图中存在唯一的余代数到代数态射r：U→A五、46V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）FU（FU）Fr rV VFA）Aα图五.递归余代数对于递归余代数，r = ΔFrΔ α。从（U，α）到（A，α）的唯一余代数到代数态射也可以记为固定F，α（α）[6]。3.4水形现象在[11]中首次定义了hylomorphism递归模式。给定一个函子F，它表示以下由不动点定义的U→A型递归函数[8]hylo（g，h）F= μ（λf.h<$Ff<$g）.对于函数g：FA→A和函数h：U→FU。给定一个F-余代数F：U→FU和一个F-代数α：FA→A，用hylo（α，F）F表示的自同构是使图6中的图交换的最小箭头U→A[15]。FU（FU）Ffhylo（α，α）FV VFA） Aα见图6。质形图此外，质形作用是变质作用与异化作用的组合[15]：hylo（α，α）F=（cata α）F<$（ana α）F.通过产生复杂的数据结构及其处理，hylomorphism捕获了一般的递归。V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）474函数式程序设计中的类形性在本节中，我们将应用前几节中描述的理论，并在一个示例中展示它们。我们把质同态看作是变形和变形的组合，这与递归余代数完全相同，递归余代数是基于余代数态射的，称为余代数到代数态射。余代数表示为变形，代数表示为变形。所有函数式编程语言的共同特征是程序都由函数组成（如数学概念函数，它是λ演算和部分递归函数理论的基础;不要与命令式语言中使用的函数概念大多数现代函数式编程语言都是强类型的，并且具有内置的内存管理;例如语言ML，Haskell和OCaml[9]。 我们展示了一个例子中的花式编程方法的功能，用于计算阶乘使用hylomorphism。程序中的Hylomorphism调用由两个函数组成的复合因此，它必须创建第一个使用变形的函数，然后创建第二个使用变形的函数。因此，结合这两个函数，我们得到一个函数，表达程序中的我们在这项工作中展示了所有用OCaml语言编写的代码示例[18]。OCaml语言（ObjectiveCaml）是一种基于Caml语言的面向对象函数式语言。4.1例子中的变形Anamorphism是一个基于操作的构造函数，因为它在Anamorphism的描述中被定义。通过在信息学中应用变形，我们得到了一个从单个输入（例如整数）开始并将其带入更复杂的输出（例如宽列表）的共递归函数。换句话说，我们接受一个输入，然后将其向上扩展为一个广泛的列表。 我们定义这个过程 在函数式编程中被称为展开函数。它采用类型签名<类型B>到列表类型A>。 在OCaml语言中，变形的类型签名是a→b列表。变形的应用是生成自然数的函数为了说明，我们在实现中将此函数命名为ana，因为此函数的基础是变形。此函数的参数是int类型的元素。该函数返回从n到1的元素列表作为输出。这样一个生成的列表，我们需要计算n的阶乘。这个函数的具体类型签名是：int → intList。所以它是一个接受一个整数并产生一个整数列表的函数。函数ana在OCaml语言中的实现是：let r e c ana n =match n with48V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）| 0 −> []|1 −>[1]|x −>x* *Ana （x −1）;;如果函数ana的参数为0，那么它返回一个空列表。如果参数为1，ana生成一个列表，其中只有1作为元素。否则，ana生成一个附加了新元素的列表4.2例子中的变质作用异化是基于操作的解构，因为它在异化的描述中被定义。通过应用信息学中的变形，我们得到了一个递归函数，它以一个列表开始，并在一个输出中返回它（例如整数）。通过对int类型的元素列表应用变形，我们得到了int类型的单个元素。OCaml中列表上的max（）或length（）方法是一种变形。这些函数在函数式编程中称为fold。它们将ListTypeA>的类型签名带入。 在OCaml语言中，变形的类型签名是列表→b。 我们提出变质作用的乘法函数。此函数接受一个int类型的因子列表作为其参数，并返回乘法运算的结果。 的结果 该函数是int类型的元素，即列表中这个函数的具体类型签名是intList → int。所以它接受一个整数列表并将其折叠成一个整数。为了更好地说明，我们在实现中将乘法函数命名为cata，因为该函数的基础是变形：let r e c cata l i s t =match list with|[] −> 1|头：：t a i l −> head 卡他a i l）;;在本例中，cata函数接受一个列表，如果列表为空，则返回1否则，它递归调用列表上的cata4.3实例中的质构在举例说明变质作用和变质作用之后，我们定义了质形作用。质形被描述为“ana”之后的因此，把一个变形（a→c list）和一个变质（c list→b）放在一起，它们会导致a→b的类型签名。使用fold组合unfold给出了一个函数，该函数接受单个值并返回单个值;构建然后减少列表的递归函数对用户来说是隐藏V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）49我们使用以前的实现来定义hylomorphism。函数ana生成从n到1的自然数列表，函数cata通过使用乘法运算消除这个函数的结果是一个数n的阶乘。两个函数的组合fg用编程语言OCaml写成f（gx）。这个函数的定义如下：让f a c tX =cata（ana x）; ; factorial函数的执行：#f a c t 4;- 啊：I n t = 24使用hylomorphism执行前面的示例：事实4=Cata（安娜四、=4 Cata（安娜第三章=12 Cata（安娜（二）=24 Cata（安娜第一章=24 ID=24因此，我们能够比较我们的新方法与经典的方法没有hypolomorphism。不带hylomorphism的阶乘函数的实现：设r e c f a c t o r i a l x = if x= 1 then 1其他 X （f a c t o r i a l（x− 1））;;这个例子的插图没有hylomorphism：阶乘4 =4 *（阶乘3）=4 * 3 *（阶乘2）=4 * 3 * 2 * （阶乘1）=4 * 3 * 2 * 1 =4 * 3 * 2 =4 * 6 =2450V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）我们可以看到，我们的新方法的阶乘计算使用的hypolomorphism给出了预期的结果。5动作语义行动语义学的框架最初是由奥胡斯大学的彼得·D·Mosses，与来自Univer.com的David Watt合作V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）51Glasgow市动作语义学是一种用于形式化描述编程语言的框架。与其他框架相比，它的主要优势是实用性：动作语义描述（ASD）可以轻松扩展到真正的编程语言[7，23，27，30]。这是由于ASD固有的可扩展性和可修改性，确保对所描述语言的扩展和更改仅需要对其描述进行相应的更改。另一方面，在语言中添加一个不可预见的结构可能需要在[24，25]中表达的指称或操作语义动作语义学与其他语义学方法完全等价，如指称语义学、操作语义学或公理语义学。动作语义的基础是动作，它们本质上是动态计算实体。它们结合了计算行为的性能，使用传递给它们的值来生成反映计算状态变化的新值。因此，动作的执行直接代表了处理该行为的信息，并反映了渐进的、逐步的计算性质：动作执行的每一步都可能访问和/或改变当前信息。动作语义学中使用的其他语义实体是yielders和data。以行为实体为主，以产出者和数据实体为辅。用于指定动作和辅助语义实体的符号被称为动作符号[23]。在动作语义中，编程语言的语义是通过将程序短语映射到动作来定义的。这些动作的执行与程序段的执行密切相关。原始动作可以将数据存储在存储单元中，将标识符绑定到数据，计算值，测试真值等[28]。数据实体由数学值组成，例如整数、布尔值和表示存储器位置的抽象单元，它们体现了信息的粒子。动作语义所使用的数据种类由代数规范定义。Yielders包含未评估的数据片段，其值取决于包含计算状态的当前信息。屈服者是发生在行动和可能的访问，但他们不允许改变当前的信息。一个动作的执行，它可以是一个封闭动作的一部分：• 完成，对应于正常终止;• 转义，对应于异常终止;• 失败，相当于放弃一个替代方案;• 分歧，对应于死锁。不同种类的信息产生了所谓的行为方面，这些方面已经根据[23]进行了分类。他们专注于一次最多处理一种信息• 基本方面，独立于信息的处理（控制流程）;• 功能方面，处理瞬态信息（动作给定并给出数据）;• 声明性方面，处理作用域信息（操作接收和产生52V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）bindings）;• 命令方面，处理稳定信息（动作保留和处理存储单元，并改变存储在单元中的数据• 通信方面，处理永久信息（动作发送消息，在缓冲器中接收消息，以及与代理的缓冲器合同）[23]。指定动作的标准表示法由基本动作和动作组合子组成Action combinators将现有的action组合在一起，通常使用fix表示法，以控制子操作的执行顺序以及子操作之间的数据流动作组合子用于定义顺序、选择、迭代和块结构控制流程，以及管理动作之间的信息流。动作记谱法中使用的标准符号是普通的英语单词。事实上，动作符号非常接近自然语言：• 表示动作的词语构成祈使动词短语，包括连词和副词，如检查它，然后逃跑;• 代表数据和产出者的术语形成名词短语，例如给定列表的项目。这些选择符号的简单原则提供了一个令人惊讶的英语语法片段，使动作的规范变得易于阅读。动作表示法的非正式外观和暗示性的单词应该鼓励年龄的程序员阅读它。与其他形式主义相比，如λ表示法，动作表示法可能显得缺乏简洁性：每个符号通常由几个字母组成，而不是一个单一的符号。但是，这种比较也应该考虑到，每个动作组合子通常对应于λ表示法中的应用和抽象的复杂模式。无论如何，每一个符号的长度的增加似乎远远超过了它的清晰度的增加6函数范型动作语义也可以成功地用于功能程序的描述在动作语义学中，我们通常使用三个主要动作来描述编程语言：• execute- 用于执行语句;• 详细说明- 与声明一起使用• evaluate-用于计算表达式。在函数式范式中，我们只使用两个主要动作：评估和阐述。动作执行在函数式范例中并不重要函数式程序的典型特点是它们不处理存储。因此，在函数式程序的动作语义描述中，我们不会使用命令式方面的动作来分配内存位置，存储值和从内存功能范式的一个重要方面是对表达和阐述功能的评价为了允许在程序代码中引用它们，它们被关联到V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）53（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ））¢名称（标识符）。这些关联称为绑定。绑定可以是全局的，当在源代码的顶层声明时，也可以是局部的，当在包含它的let或letrec表达式let和letrec表达式之间的区别我们提供简单表达式的求值描述：详细说明letI：Var = E：表达式=评价E然后将I绑定到给定值声明后，我们可以在程序中随时使用它。值与它的标识符绑定，所以我们可以简单地通过使用evaluateaction来获得这个表达式的值：评估I：Var=给出I的值带有一个参数的函数的描述应该是这样的：详细说明letIf：VarIp1：Var = E：表达式=评价E然后将If绑定到给定值在表达式中，E是函数的参数，我们可以简单地通过动作求值来获得该值：计算Ip1：Var=给出Ip1具有不同数量参数的函数的一般定义精心制作的信评价E，然后：Var+= E：表达式=将f绑定到给定值6.1动作语义描述设E1是函数ana的替换：E1=matchnwith| 0 ->[]| 1 ->[1]| x -> x :: ana (x-1)我们将Action语义中的函数声明详细说明为54V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）详细说明让recana n=E1=递归地将ana绑定到抽象计算E1=递归地将ana绑定到抽象计算匹配n|0 −>[] |1 −>[1] |x−> x：： ana（x−1）和动作evaluateE1的求值是：评价 与...相配|0 −>[] |1−>[1] |x−> x：： a（x−1）=评价，评价然后（检查给定值是否等于数字0然后给出空列表，检查给定值是否等于数字1然后将数字1添加到列表中）或检查给定值是否大于数字1然后将给定的数字添加到列表中，将evaluateana（n-1）添加到列表中在Action语义中对函数cata的描述是类似的。首先，我们定义一个替代E2的cata函数如下：设E2=match myList with| [] -> 1| head::tail-> head *(cata tail)我们还定义了用于处理数据结构列表原始操作头和尾：V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）55evaluate<$E）=2（Ⅲ）（Ⅲ）头列表=给出列表的第一个元素它给出给定列表的第一个元素，尾列表=从列表中删除第一个元素，然后给出列表它给出了列表的尾部即除第一个元素外的所有元素都将返回。现在我们能够详细说明函数cata的声明，并在Action语义中获得它的完整描述：elaboratelet reccata myList=E2=递归地将cata绑定到抽象评估<$E2）对动作E2）的评价定义如下：给出绑定到myList然后”（《易经》卷五）“言之以实，行之以虚。检查给定的TruthV值然后给出数字1或不检查给定的TruthV值然后给出的乘法（在给定的列表中，evaluatecata（tailthe givenlist））最后，我们定义了用于计算阶乘的函数fact。函数事实声明的详细说明是：56V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（2）（Ⅲ）（Ⅲ）（Ⅲ）elaborate letfact x=cata（ana x）=评价 卡塔（ana x）然后将事实x绑定到给定值=评价 阿纳X之前计算cata（给定列表），然后将事实x绑定到给定值其中，操作evaluateana x和evaluatecata myList按以下方式进行评估：评估分析给出闭包的值抽象评价E1evaluatecata myList给出闭包的值抽象评价E2在定义了描述阶乘计算所需的所有操作之后，我们给出了一个给定输入值的阶乘的例子6.2动作语义在本节中，我们将介绍输入值n= 4时阶乘的计算。我们的阶乘的另一种计算方法已经在第4章中定义。evaluatefact x=cata（ana x）s[x<$→4]=将值绑定到evaluate<$cata（ana x））=V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）57（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）将值绑定到（评价 xs[x›→4]之前评价 cata（给定列表））其中evaluatee s[variable›→value]表示在给定变量被设置为给定值的输入状态下对表达式e的求值。对于输入值x= 4，函数ana x的求值为：求值ana x s[x<$→4]=给出闭包的值抽象评价 匹配x与|0->[] |1->[1] |x-> x：：ana（x−1） s [x <$→ 4]=给出闭包的值抽象给出x s[x›→4]的值然后检查给定的数字是否大于数字1然后将给定的数字添加到列表中，添加评估ana（x−1）s[x<$→4，list<$→ [4]]到list=给出闭包的值抽象给出x s[x<$→3]的值然后检查给定的数字是否大于数字1然后将给定的数字添加到列表中，将evaluate<$ana（x−1））s[x<$→3，list<$→ [4， 3]]添加到列表中=58V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）（Ⅲ）（Ⅲ）（Ⅲ）给出闭包的值抽象给出x s[x<$→2]的值然后检查给定的数字是否大于数字1然后将给定的数字添加到列表中，添加评估ana（x−1）s[x<$→2，list<$→ [4， 3， 2]]到列表=给出闭包的值抽象给出x s[x›→1]的值然后检查给定的数字是否等于数字1然后将给定的数字添加到列表中=给出闭包的值抽象给出列表[4，3，2，1]最后的状态是s[x<$→1，list<$→ [4， 3， 2， 1]]。下一步是动作evaluatecata list [list›→[1， 2， 3， 4]]的评估。在它的评估中，我们应用了在第6.1章中定义的原始动作head和tail。在下一步中，正在评估动作evaluate cata list s [list›→[4，3，2，1]]。使用了第6.1章中定义的头和尾动作。V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）59）（Ⅲ）¢（Ⅲ）evaluatecata lists[list›→[4， 3， 2， 1]]给出闭包的值抽象评价 匹配列表|[]->1 |head：：tail->head *（catatail）=给出闭包的值抽象”（《易经》卷五）“以物定物，以物定物。不检查给定的TruthV值然后给出的乘法（headlists[list›→[4， 3， 2， 1]]和评价cata（tail list）s[list›→[4， 3， 2， 1]]）=给出闭包的值抽象”（《易经》卷五）“以物定物，以物定物。不检查给定的TruthV值然后给出的乘法（数字4）和60V. SlodicBagrák，P. Macko/ElectronicNotesinTheoreticalComputerScience279（3）（2011）（Ⅲ）（Ⅲ）头列表s[list›→[3，2， 1]]和评价cata（tail list）s[list›→[3，2，1]]）=给出闭包的值抽象”（《易经》卷五）“以物定物，以物定物。不检查给定的TruthV值然后给出的乘法（数字4）和数字3和头列表s[list›→[2，1]]和评价cata（tail list）s[list›→[2， 1]]）=给出闭包的值抽象”（《易经》卷五）“以物定物，以物定物。不检查给定的TruthV值然后给出的乘法（数字4）数字3