函数式程序的增强redex跟踪方法的描述和应用

理论计算机科学电子笔记176（2007）39-63www.elsevier.com/locate/entcs函数式程序奥拉夫·奇蒂尔和罗勇肯特大学计算机实验室联合王国摘要跟踪器帽子记录在一个详细的跟踪计算的程序写在懒惰的函数式语言Haskell。然后可以以各种方式查看跟踪，以支持程序理解和调试。这条轨迹被命名为增强的redex轨迹。它的结构受到函数式语言的标准图重写实现的启发。 在这里，我们描述了一个模型的跟踪，捕捉其基本属性，并允许正式推理。 迹是通过图重写构造的图，但超越了简单的项图。 虽然迹是一个图，其结构是独立于任何重写策略，我们定义的痕迹归纳，从而给我们一个强大的方法来证明其性质。保留字：跟踪，调试，增强redex跟踪，Haskell。1介绍通常，计算被视为执行输入和输出操作的黑盒。然而，当我们想知道程序的不同部分如何导致计算执行输入/输出操作时，我们必须查看黑盒。这样做最常见的需求是调试：当程序的实际语义和预期语义之间存在差异时，我们需要定位导致差异的程序部分观察程序如何工作的其他原因断言）、对不可靠的文档化程序进行逆向工程以及学习编程。跟踪是获取关于计算的内部工作的附加信息的过程。1.1跟踪函数式程序传统的跟踪形式是在程序中引入特定的语句，用于记录有关计算进度的信息，以及使用调试工具。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.03240O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）39用于逐步通过计算并检查计算状态的日志。对于惰性函数式语言，有两种不同的跟踪方法。首先，传统的方法是不合适的，因为中间项有大量未求值的子项很难阅读，而且懒惰的归约策略对于人类程序员来说太复杂了。其次，传统的跟踪方法只考虑命令式程序的计算模型：一长串的状态转换。相比之下，函数式程序员希望忽略低级操作细节，特别是计算顺序，但利用显式数据流和不存在副作用等属性。1.2什么是跟踪？跟踪是由关于计算的信息组成的结构。它（部分地）描述了程序的计算如何从其输入获得其输出.如果计算是确定性的（正如我们在这里假设的），那么整个计算已经由程序及其输入确定。所以痕迹是不是超清晰的？不可以。通过重新运行计算，可以从程序和输入中重建计算的任何细节，但这将是昂贵的。跟踪的目的是提供对任何所需信息的快速和方便的访问。大多数查看工具是交互式的，因此它们必须快速提供所需的信息位，特别是独立于计算的长度。操作语义提供了计算的描述。都是一系列项M0→M1→M2→. 一个小步骤操作语义和证明一个大步骤的自然语义树是计算的描述。然而，它们不适合作为跟踪，这不仅是因为它们不能提供对所有所需信息的快速访问，更明显的是因为它们充满了冗余。在这两种描述中，术语的大部分被重复多次。为了描述长时间的计算，跟踪必须尽可能紧凑1.3现有追踪系统有几个用于惰性函数式语言的跟踪系统，都是针对Haskell的[26，19，12，27，22]。所有系统都采用两阶段追踪方法(i) 在计算过程中，关于计算的信息被记录在一个数据结构中，即轨迹。(ii) 在计算终止后，跟踪用于查看计算。通常，交互式工具会根据需要显示计算的片段。程序员利用他们对程序预期行为的了解来定位故障。一个跟踪是一个复杂的图的长期组成部分，大多数跟踪结构也incor-porate链接到源程序。迹线作为具体的数据结构，将观察者从时间和顺序评估策略中解放出来。每种追踪方法都给出了计算的不同视图;在实践中，这些视图是互补的，可以有效地一起使用[7]。因此O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）3941Haskell Tracer Hat集成了几种方法[27]。在计算过程中，生成一个单一的统一轨迹，即增强的redex轨迹（ART）。单独的工具提供ART的不同视图，例如算法调试[23，19，22]，遵循redex跟踪[26]和观察功能[12]。1.4目标：追踪它将一个Haskell程序转换成一个新的Haskell程序。当编译后的这种通过程序转换对ART的间接定义使得即使是简单的手工计算也很难确定ART。因为涉及到两个程序，原始程序和转换后的程序，所以很难区分对每个程序的语义做了哪些假设。ART还包括许多特殊的结构，因为Haskell是一种庞大而复杂的语言。因此，我们的目标是给ART一个直接而简单的定义，抓住它的基本属性，并使我们能够正式地将视图与程序的语义联系起来。因此，所查看的信息具有明确的含义，并且可以正确地用于理解程序和定位程序故障。已认识到有必要使追踪系统正规化：“程序员在他们的编程环境中依赖于工具的正确性。在过去，语义学家研究的是编译器和编译器分析的正确性，这是最重要的工具。在本文中，我们提出了其他工具，如调试器和步进器，也值得使用[9]第一章我们集中讨论艺术，因为它已经从其他几种痕迹中提炼出来，成为一种统一的痕迹。这种对ART的关注并不排除根据新的见解对其定义进行修改。我们意识到我们打算消除的几个缺点（缺乏信息）。虽然ART只用于Haskell，但它适用于严格和非严格的纯函数语言，正如我们的定义所阐明的那样。1.5本文结构我们首先在第2节中激励我们选择编程语言。然后，我们在第3节给出了一个非正式的介绍ART的基础上，它的起源在图重写实现的函数式语言。第4节和第5节定义了ART。在第6节中，我们证明了ART的一些简单性质，以更好地理解并证明我们的定义允许相对简单的证明。 我们在第7节中证明了ART是无环有向图，在第9节中证明了它们的结构与任何特定的求值顺序无关。 第8节建立了一个属性中心使用ART的计算产生的意见。第10节展示了ART如何表达运行时错误。我们在第11节讨论了相关的工作，并在第11节结论中总结。42O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）392程序描述共享的函数式语言的操作语义，特别是广泛使用的Launchbury [15]及其变体的语义，被定义为λ-演算的子集加上基本模式匹配的case构造。 这个核心演算的构造被选择来优化操作语义的简单性。任何函数式程序都可以转换成这个核心演算，因此核心演算适合于编译器。然而，用核心演算编写的程序看起来与程序员编写的程序相当不同，因为核心演算不包含程序中主要使用的编程结构。因为跟踪支持程序员理解程序是如何工作的，所以跟踪必须与最初编写的程序相关。 因此，我们选择一个包含最常用的程序语言功能的演算：命名函数和模式匹配。我们的程序是应用项重写系统[14]。函数符号f，g，h数据构造器C和D原子a，b：=f函数符号| Cdata constructor变量x，y，z程序项M，N：=原子| xvariable| MN applicationpatternP:= xvariable| Qconstructor patternconstructor patternQ：=Cconstructor| QP构造器应用程序我们写M N1... Nn为程序项（. （（M N1）N2）.. . 它是M对n个自变量的应用每一个原子都与一个自然数相关联，它的arity。元数为0的函数符号有时称为常数符号。定义2.1如果f是n元的函数符号，且P1. Pn是模式和R是一个程序项，使变量R是一个子集的变量f P1. Pn，那么f P1... Pn= R是一个重写规则。一个程序是一组有限的重写规则。下面的示例程序实现插入排序。我们以整数或混合整数表示法编写函数符号的应用程序，这是常见的做法。sort []=[]sort（x：xs）=insertx（sort xs）O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）3943插入x[]=[x]insertx（y：ys）=ifx = ythen x：y：ys elsey： insertxysifTrue thenx elsey = xifFalse thenxelsey = y我们承认高阶程序。例如，我们可以使用以下的sort替代定义：sort= foldr insert []程序的定义列出了我们证明性质所需的所有约束。它比编写函数式程序所需的更通用。这个定义并不要求模式中的所有数据构造器都被完全应用，也就是说，它们的参数数量等于它们的arity。该约束将仅需要用于建立操作重写语义相对于指称语义的完整性。我们的程序不是正交重写系统[14]。我们不要求规则是左线性的;变量可以在规则的左侧重复出现。 在项重写中，左线性已经是期望的，以避免任意大的项的相等性检查，但是在项图重写中，无论如何不存在这样昂贵的相等性检查，因为变量与图节点匹配。本文给出了一个正交项重写系统。我们显式地允许两个规则的左边有一个公共实例，从而重叠。因此，我们可以将这些规则之间的选择留给一个单独的求值策略，其定义我们保持开放，或者我们可以对出现在函数逻辑程序中的非确定性函数进行建模。然而，规则的左手侧不能与规则的左手侧的真子项重叠因此，我们的程序不是亚交换的，而是几乎亚交换的（推论9.3）。3增强Redex Trail的起源术语图重写[21]为函数程序提供了一种操作语义，它是抽象的，与标准术语重写语义密切相关。与术语相比，图允许共享公共子术语，因为它发生在函数式语言的实际实现中，例如G机[13]或更有效的STG机[20]。项图重写可以正确地模拟实际实现的渐近时间和空间复杂度[1]。对我们来说，共享是空间高效跟踪结构的关键，并且接近实现也保证了跟踪的容易创建考虑Haskell术语排序44O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）39·····排序··→······[]插入排序：'t'·······[]插入排序't'···排序····[]：'t'函数sort由以下两个重写规则定义：sort []=[]sort（x：xs）=insertx（sort xs）我们用第二个方程执行一个简化步骤：对于这个简化步骤，我们已经添加了新的图节点，它们表示所使用的重写规则的右侧。我们有一个新的根节点表示项的顶部。为了确保新的top节点被正确共享（当redex只是一个更大的term的一部分时），实现实际上用reduce的top节点覆盖了redex的top节点某些图节点从根节点变得不可访问，并被垃圾收集器删除O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）3945·······排序······[]··[]··[]插入排序：：'t'对于图重写的效率至关重要的是，每个约简步骤仅添加少量的新节点;绑定到重写规则的变量的子项与redex图共享，因此不需要添加。为了跟踪计算，我们简单地不使用reduce覆盖redex，而是单独构造reduce（如上所述与redex共享子项），并通过特殊的约简边缘连接redex和reduce的顶部节点同时使用重写规则sort []=[]插入x[]=[x]我们获得完整计算的以下迹线（虚线箭头是缩减边）：这是计算的增强redex trail（ART）。它是计算的一个紧凑但详细的表示;特别是，它直接将每个redex与其reduce联系起来。它在实践和理论模型中的创建都大大简化了，因为每个简化步骤都只是增加了迹线，而从不修改已经存在的部分。如这里所描述的，ART没有关于缩减步骤的顺序的信息它没有说排序[]→[]发生在插入此信息与Hat提供的大多数视图无关该观察结果这与我们认为函数式程序员从时间中抽象出来的观点一致。因为Hat将ART的节点按照它们创建的顺序写入文件，所以时序信息实际上是可用的。如果后来证明有必要，我们可以很容易地将其添加到我们的模型中。4定义项图图的缺点是节点和边元素的选择通常是不相关的，因为我们最感兴趣的是标签。图形态的概念成为中心，因为我们不想区分同构图。图的同构类不便于处理。因此，我们选择了一个标准的表示图，其中一个节点描述了从图的根到节点的路径。一个节点是一个（可能是空的）字母f，a和r的字符串，46O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）39·εRRR······F一RFRA排序····rar··RRFRRA[]··[]afAArRAFrr··阿贾法：[]插入排序：'t'其中，f意味着进入应用程序的函数组件，a意味着进入应用程序的参数组件，而r意味着遵循归约边缘到归约。节点字母i，j：= f|一|Rnoden，m，o∈{f，a，r}由于共享，多条路径可能通向图中的同一节点然而，在我们的术语图中，存在标准路径。每个节点首先作为一个项的非共享表示的一部分引入在第一种情况下，节点的规范路径是初始项内的唯一路径。在第二种情况下，节点的规范路径由redex节点的规范路径加上从redex节点通过右侧到节点本身的唯一路径组成。因此，一个节点包含有用的信息，因为它描述了它在reduce（或初始项）中的位置以及导致其创建的redex节点的序列。这里是我们之前的节点标识示例术语图的每个节点都有一个标签，可以指向其他节点。我们定义一个术语图，使其尽可能简单。然后，我们详细讨论了一些设计决策。定义4.1标签T：=原子| nm application| nindirection术语图是从节点到标签的部分函数，G：n<$→T。术语图G的域dom（G）是定义函数的节点的集合。我们有时将项图G看作元组{（n，G（n））的集合|n∈ dom（G）}.令项图的自由节点是出现在其标签中而不是其域中的节点如果一个项图没有自由节点，则它是封闭的O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）3947我们之前描绘的示例图正式定义为：G（ε）=f aG（f）=sortG（a）=af aaG（af）=aff afaG（aff）=：G（rf）=rff afaG（afa）=G（rff）=插入G（aa）=[]G（ra）=raf aaG（r）=rf raG（raf）=排序G（rar）=[]G（rr）=rrf rraG（rrf）=rrff afa G（rrff）=：G（rra）=[]因此dom（G）={ε，f，a，af，aff，afa，aa，r，rf，rff，ra，raf，rar，rr，rrf，rrff，rra}并且G的标签集是{fa，sort t，afaa，afafafa，：，'t '，[]，. . . }。我们没有在图中显式地包含约简边，因为它们已经通过我们的节点选择隐式地给出了。约简边总是从节点n指向节点nr。当且仅当图中存在结点nr，则存在从结点n到结点nr的约化边。因此，为了记录减少，我们必须添加至少一个新节点。当我们使用投影（如idx= x）进行约简时，这一为了这个目的，我们有间接标签;它只作为投影的归约出现εr使用间接节点的解决方案受到了函数语言的图形机的启发间接节点的存在对于向后遍历术语图也是至关重要的，从（部分）reduce到redex [25]。后面我们经常需要一条边链的最后一个节点，其中每条边要么是一条约简边，要么是一条来自间接节点的边定义4.2设G是项图，n∈dom（G）.然后[n|G=如果nr ∈ dom（G）则[nr|如果你不介意的话。G（n）= m则[m|其他例如，在上面的术语图G中[ε|G= ar和[f|G= f。···F一IDar··错误阿夫阿夫不是真48O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）39P⎪⎨⎪5定义增强Redex Trails标签不嵌套。标签不包括变量，因为在重写中变量将被节点替换。程序术语不包括节点。为了描述重写，我们需要包含节点的术语定义5.1术语M，N：=原子| nnode| xvariable|MN应用术语包含节点和变量。标签术语是不包含变量的术语程序项是不包含节点的项（如之前定义的计算项是既不包含变量也不包含节点的项并不是每个项图都代表一个计算。增强的Redex Trail（ART）是归纳定义的。初始项M的图表示，图（ε，M），如果G是ART，并且G用程序P在一个步骤中减少到GJ，即G →PGJ，则GJ是ART。定义5.2设P为程序，M为计算项。 项图G图（ε，M）→εG是初始项M的程序P.ART是由有限个归约步骤构成的。ART的定义可以扩展到无限的、非终止的计算，但这样它就不再是一个能够进行简单证明的归纳定义了在实践中，我们只能产生有限步数的迹;我们不能产生无限步数的为了正确地描述redex和reduce之间的子项共享，我们必须用节点（而不是项）替换重写规则的变量。因此，随后的几个定义处理标签术语。首先，我们必须定义给定标签项的图是什么定义5.3graph（n，a）={（n，a）}graph（n，m）={（n，m）}⎧n{（n，M N）}，如果M，N是节点n{（n，M na）}图（na，N），当只有M是结点时graph（n，M N）=<${（n，nfN）}图（nf，M），如果只有N是结点{（n，nfna）}⎩⎪图（nf，M）-图（na，N）O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）3949没有优化来共享给定标签项的公共子项;例如，我们不共享项if g fa thenf42else（f42）+1的公共子项f 42。引理5.4设n、m和o为任意节点，i为字母，M为标号项。让G= graph（n，M）.(i) G是一个项图。(ii) dom（G）<$n{f，a}<$n.(iii) mi∈ dom（G）蕴涵m ∈ dom（G）或mi = n.(iv) G的自由节点是M中出现的节点的子集。(v) 如果M不包含以r结尾的节点，则G的标号不包含以r结尾的节点。(vi) o∈ dom（G）<$G（o）= m =<$o = n <$M = m.(vii) nf∈dom（G）= nm. G（n）=nfm，na∈dom（G）= nm. G（n）= m na.证据通过对M.为了证明图（n，M）是一个项图，我们证明了在集合表示中每个节点只有一个元组Q约简步骤的中心部分是将图中的节点与重写规则的左侧进行匹配。谓词匹配G（n，M）检查节点n是否匹配术语图G中的标签术语M。定义5.5匹配是在匹配的标签词的结构上归纳定义的：匹配G（o，a）=（G（o）=a）match G（o，M N）= n，m，n. （G（o）=m n）匹配G（如果M是节点，则m else [m|G，M）match G（如果N是节点则n else [n|G，N）匹配G（o，m）=（o = m）在我们讨论匹配的定义之前，我们还定义了什么是缩减步骤：定义5.6程序P的项图上的归约关系→P定义如下。如果• G是一个有ithn∈dom（G）且dnt∈/dom（G）的特mgra• L=R是程序P的重写规则，• σ是用节点替换变量的替代，• 匹配G（n，Lσ），则G →P，nG是满足重写规则L=R和置换σ的图G（nr，Rσ）.50O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）39匹配已经被小心地定义，以确保标签项中的节点仅在其直接作为图中的应用节点的一部分出现时才与图中的节点匹配。考虑艺术ε以及重写规则idx = x。 我们发现标签项idx[a/x]=ida在节点ε处匹配：matchG（ε，ida）=（G（ε）= f a）匹配G（如果id是节点，则f else [f|G，id）match G（如果a是节点，则a else [a|G，a）=true匹配G（[f|G（a，a），G（a，a）=matchG（f，id）matchG（a，a）=true因此，在一个步骤中，ART可以重写为上一节中所示的ART。然而，标签项idx[ar/x] =idar在节点ε处不匹配：matchG（ε，idar）=（G（ε）= f a）匹配G（如果id是节点，则f else [f|G，id）match G（如果ar是节点，则a else [a|G，ar）=true匹配G（[f|G，id）匹配G（a，ar）=matchG（f，id）matchG（a，ar）=true= false=false所以我们的图不能重写为术语图··F一IDar··错误阿夫阿夫不是真O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）3951εr事实上，这个术语图不是艺术，为什么我们明确地排除它？否则，我们将有几个结构不同的图表示相同的多重表示只会引起混乱，并在以后导致我们对图的等价类给出复杂的定义。相反，我们选择一个规范的表示：在一个约简步骤中，我们只用一个节点来替换一个变量，这个节点是一个可能很长的约简和间接边序列的起始节点因此，匹配程序项的替换基本上是唯一定义的：引理5.7设G是一个项图，其中匹配G（m，Mσ）和匹配G（m，MσJ）用于程序项M，置换σ和σJ通过节点替换变量。则σ（x）= σJ（x），对于所有变量x出现在M中。证据 诱导M。(i) M=x：匹配G（m，xσ）<$m=σ（x）。 匹配G（m，xσJ）<$m=σJ（x）。因此σ（x）=σJ（x）。(ii) M=a：微不足道，因为a中没有变量。(iii) M=N O：matchG（m，（N O）σ）和matchG（m，（N O）σJ）意味着存在n， o， NJ和 OJ使得G（ m）=no且matchG（ NJ，Nσ）， matchG（ OJ，Oσ），matchG（NJ，NσJ）和matchG（OJ，OσJ）.对于N和O中的所有变量，即N O中的所有变量，归纳假设如下：σ（x）=σJ（x）。Q为什么我们要选择一个归约和间接边序列的起始节点，而不是最后一个？如果我们选择一个不同的节点，图将包含一些关于求值顺序的部分（但不完整）信息，项图约简将不再是几乎次交换的。这些性质将在命题9.2和推论9.3中表达出来。在实际的实现中，也证明了开始节点的选择是最容易实现的。引理5.8设G是一个闭项图，其左侧有匹配G（n，Lσ）L和用节点替换变量的替换然后又道：(i) n是应用或常量符号节点。(ii) 出现在Lσ中的节点是出现在G的标号中的节点的子集。(iii) 出现在Lσ中的节点是dom（G）的一个子集.F···阿阿尔id··假阿夫阿夫不是真52O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）39证据(i) L是一个应用程序或常数符号，因此Lσ也是。然后，属性直接从匹配的定义中得出。(ii) 通过归纳对匹配的定义。(iii) 因为G是闭的，所以从ii得出。Q定义5.9设G是ART，n∈dom（G）和nr∈dom（G）。 我们称n为G的redex节点，称nr为G的redut节点.6ART的简单属性在本节中，我们列出了ART的一些属性，这些属性可以让您感觉到ART的结构以及与任意项图相比它所满足的约束。这些简单的属性也可以具有实用价值：Hat包含一个名为hat-check的工具，该工具对由Hat生成的ART执行许多健全性检查这个测试工具对于发现Hat跟踪程序中的错误非常有价值hat-check的检查是相对低级的，并且依赖于实现，但是应该扩展到包括这里列出的大多数属性每个属性的证明都利用了ART的归纳定义，并使用了匹配和图构造的一些相关属性。定义6.1一个节点集S是预闭的，如果nm∈S=<$n∈S。引理6.2节点集S是预闭的当且仅当对于所有节点n和字母i，ni∈S =<$n∈ S.证据 通过归纳得出节点的长度。Q命题6.3ART G的定义域是预闭的。证据我们通过归纳证明了对所有节点n和字母i，ni∈dom（G）=n∈dom（G）。在基本和归纳的情况下，我们都需要引理5.4。三.最后，前缀封闭性遵循引理6.2。 Q第6.4章一个艺术家被关了证据关于ART定义的归纳。或者G= graph（ε，M），对于初始项M;则根据引理5.4.iv，G没有自由节点。否则，我们假设G是闭的，并证明G的图（nr，Rσ）是闭的.我们从匹配G（n，Lσ）和引理5.8中知道。iii.出现在Lσ中的节点是dom（G）的子集.因为R不包含节点，并且R的变量是L的变量的子集，所以出现在Rσ中的节点是dom（G）的子集。引理5.4。iv.图（n，Rσ）的自由结点是dom（G）的一个子集.所以G-图（nr，Rσ）是闭的.Q命题6.5没有一个ART的标签包含以r结尾的节点。O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）3953P证据关于ART定义的归纳。考虑G=图（ε，M）.初始项M不包含节点，因此根据引理5.4。vG不包含以r结尾的节点。否则，设G是ART，使得没有标签包含以r结尾的节点。在匹配G（n，Lσ）的情况下，根据引理5.8得出。ii.Lσ不包含以r结尾的节点。因为R的变量是L的变量的子集且R不包含节点，Rσ不包含以r结尾的节点。引理5.4。v则图（n，Rσ）的标号不含以r结尾的结点。 所以G-图（n，Rσ）的标号不含以r结尾的结点.Q命题6.6在ART中，只有以r结尾的节点可以是间接的。也就是说，如果G（n）=m，则n以r结尾。证据关于ART定义的归纳。情形G= graph（ε，M）：初始项M不是节点，因此根据引理5.4。vi没有n，其中G（n）=M.情形G=Gj-图（OR，Rσ）：设n∈dom（G），使得G（n）=m. 或者n∈dom（GJ），然后根据归纳假设n以r结尾. 或n∈dom（graph（or，Rσ））. 根据引理5.4。vin=or，所以n以r结尾。Q命题6.7如果n是ARTG的一个redex节点，那么它要么是一个应用节点，要么是一个常数符号节点，即G（n）= mo或G（n）= f。证据关于ART定义的归纳。情形G= graph（ε，M）：由于引理5.4。iiG不包含以r结尾的节点，因此没有redex节点。 情形G=Gj-图（mr，Rσ）：设n是G的一个redex节点.因为mr是dom（graph（mr，Rσ））中唯一以r结尾的节点，根据引理5.4。ii，n∈dom（GJ）. 如果 n=m，则根据引理5.8。是应用或常量符号节点。否则，n是GJ的redex节点，并且根据归纳假设，它是应用或常数符号节点。Q命题6.8设G和GJ是ART，且G → <$GJ和n ∈ dom（G）。 然后[n|GJ=[[n|G|GJ。证据[10]关于《易经》的定义|G.• nr∈dom（G）：所以nr∈dom（GJ）.因此[n|GJ=[nr|GJ和[n|G=[nr|G与归纳假设[nr|GJ=[[nr|G|GJ属性如下。• nr∈/dom（G）andG（n） =m：nGJ（n） =mandD是Prposin6.7nr∈/dom（GJ）.So[n]|GJ =[m|GJ 一个d[n|G=[m|我和我的朋友假设|GJ=[[m|G|GJ属性如下。• nr∈/dom（G）andndG（n）m：那么[n]|G= n，并且该性质平凡地成立。Q命题6.9设G是ART，若nf∈dom（G），则G（n）= nfm，对某个结点m.若na∈dom（G），则G（n）= m na.证据 使用引理5.4归纳ART的定义。七.Q54O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）39GG7艺术中没有循环对于重写常量符号，我们的定义偏离了真正的实现和真正的Hat ART。在整个计算过程中，常量符号只被约简一次，并且约简由常量符号的所有使用事件共享。对这种行为进行建模会增加相当大的复杂性;特别是，因为常量符号可以递归，它会导致循环ART和无限（规则）项。因此，我们把这个扩展和与这里定义的更简单的模型的比较留给将来的工作。为了表示ART是非循环的，我们首先必须定义节点的可达性定义7.1项图G的直接可达关系是节点~G上的最小二元关系，G（n）=m=n~GmG（n）=mo=<$n~Gm且n~Gon，nr∈dom（G）=<$n~Gnr命题7.2一个ArtG是非循环的，也就是说，对于所有n∈dom（G），我们有n+n.证据 使用引理7.3归纳ART的定义。Q引理7.3设G是具有节点m的ART，M是不是具有匹配G（m，M）的节点的标签项。对于M中的所有节点o，我们有m~+o。证据 关于匹配定义的归纳。Q因为任何ART只有有限个节点，我们立即得到：推论7.4可达性终止于ART G，即不存在无限序列n0~Gn1~Gn2~G。......你好。因为ART G是终止的，所以链的最后一个节点[m|对于所有的节点m，定义G，匹配G（m，M）也是如此。8重建还原步骤从旧ART产生新ART的归约步骤使用程序的重写规则，类似于用于实现函数语言的任何基于图重写的抽象机器。这一性质还不能表明ART是从初始项到最终结果（或流产）的整个计算历史的表达性表示，适合于故障定位和程序理解。ART的一个核心特性是，在其分解中执行的每个归约步骤都可以很容易地从其重构，而不必简化计算，只需遍历图的一小部分由于约简边的存在，术语图的单个节点通常表示许多计算术语。我们通过始终遵循约化和间接边，得到图G的节点n的最高评价形式mefG（nO. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）3955定义8.1设G是一个具有redex节点n的ART。mef G（n）= mef T G（G（[n|G（a）= amefTG（m n）= mefG（m）mefG（n）在下文中，我们不仅将mefG应用于节点，还将其同态扩展用于标签项。我们用后缀表示法来写这样一个应用，例如MmefG，就像替换的应用一样。我们还可以从节点重建其他计算项。从一个redex节点，我们可以重建一个redex：定义8.2设G是一个具有redex节点n的ART。.mefG（m）mefG（o），如果G（n）=moRedexG（n）=a，如果G（n）=aRedex、matching和most evaluated form是密切相关的。请注意，redexG和mefG的定义遵循图结构，而matchG则根据匹配标签项的结构定义。命题8.3设G是具有节点m的ART，M是不只是节点的标签项。matchG（m，M）=matchredexG（m）=M mefG证据 案例分析。• G（m）=a：matchG（m，M）<$M=G（m）=a<$ redexG（m）=a= MmefG.• G（m）=n o：如果M是原子或节点，则matchG（m，M）= false。 所以设M=N，O。match G（m，N O）= n match G（如果N是节点则n else [n|G，N）n匹配G（如果O是一个节点，则O else [O|G，O）。对于引理8.4，遵循mefG（n）=N mefG mefG（o）=O mefG。因此mefG（m）= mefG（n）mefG（o）=（N 0）mefG.Q引理8.4设G是具有节点m的ART，M是标签项。匹配G（如果M是节点，则m else [m|G，M）= M mefG（m）= M mefG证据 诱导M。• M= a：匹配G（[m|G，a）G（[m|G）= a mef G（m）= a = a mef G.• M=n：matchG（m，n）<$（m=n）<$mefG（m）= mefG（n）=n mefG.• M= N 0：匹配G（[m|G，N O）n，o. （G（[m|G）= n o）匹配G（如果N是节点，则n else [n|G，N）n匹配G（如果O是一个节点，则O else [O|G，O）。与诱导假说如下：（G（[m|G）= n o）（mef G（n）= N mef G）（mef G（o）= O mef G）. 所以mefG（n）=（N 0）mefG.56O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）39Q与命题8.3相反的方向并不成立，其原因已经在第5节中讨论过了。在给定的例子中，有mefG（ε）=（idar）mefG，但matchG（ε，idar）= false。真正的帽子艺术还包括我们尚未提到的所谓的父边。每个节点都有一个父边，指向导致其创建的redex的顶部节点。父边缘是定位程序故障的redex跟踪视图的关键成分[26，25]。在本文中，我们将只使用它们来从ART重建一个约简在我们的ART模型中，父节点被编码在节点中：定义8.5parent（nr）=nparent（nf）= parent（n）parent（na）=parent（n）parent（ε）= unfined例如，节点t的父节点是节点ε。节点rt的父节点是节点r。在项图中很容易识别出所有形成规则右侧的节点：它们都有相同的父节点。因此，使用父边，我们可以很容易地从一个reduce节点重建一个reduce：定义8.6设G是一个具有redex节点n的ART。reductG（n）= reduct PG（n，nr）reductPG（p，n）= if parent（n）=p then reductTG（p，G（n））else mefG（n）reductTG（p，a）=areductTG（p，m）= mefG（m）reductTG（p，n o）= reductPG（p，n）reductPG（p，o）引理8.7设G是一个ART，节点为m，M是一个标签项，节点的父节点都不是m。 则图（mr，M）<$G =<$reductG（m）= MmefG.证据 从下面更一般的引理得出。Q引理8.8设G是一个ART，节点为m和p，M是一个标签项，节点的父节点都不是p。parent（m）=p图（m，M）n G= n约化PG（p，m）=M mefG证据 诱导M。• M=a：graph（m，a）<$G <$G（m）=a<$ reductPG（p，m）= reductTG（p，a）=a=a mefG.O. Chitil，Y.Luo/Electronic Notes in Theoretical Computer Science 176（2007）3957P• M=n：图（m，n）<$G <$G（m）=n<$ reductPG（p，m）=reductTG（p，n）= mefG（n）= nmefG（n）.• M=N 0：W.l.o.g. 设N=n为节点，O不是节点。 图（m，n O）<$G <$G（m）=N ma<$图（ma，O）<$G .在归纳假设下，约化PG（p，ma）=OmefG.因此reductPG（p，m）=reductTG（p，n ma）= reductPG（p，n）reductPG（p，ma）= mefG（n）（OmefG）=（N O）mefG.Q前面的mef、redex和reduce的定义在它们的特定域上都是total，因为ART中的可达性是终止的。命题8.9设GJ →P，nGJJ，重写