没有合适的资源?快使用搜索试试~ 我知道了~
基于依赖类型的基于栈的遗传程序设计拉里·迪尔http://github.com/larrytheliquid/dtgp/tree/aaip11抽象。遗传程序设计(GP)可以作为一个强大的搜索工具,对许多类型的归纳规划问题。已经做了大量的研究来探索各种术语表示、遗传算子和通过考虑类型信息来智能地导航搜索空间的技术的有效性。本文探讨了不太熟悉的概念,正式捕获的不变量典型假设GP实现。依赖类型编程(DTP)扩展了通常可用的类型级表达能力函数式编程语言中的任意命题。我们使用DTP来表达和执行与GP相关的语义不变量在类型级别,特别关注强类型的基于堆栈的GP的类型安全交叉。鉴于GP实现的复杂性以及引入逻辑和运行时错误的可能性,我们希望通过使用经过验证的实现来帮助研究人员避免错误地将进化解释归因于GP运行现象。1介绍这项工作的目标是不拿出一个新的GP算法的进化性能,而是给一个例子,一个非平凡的,但验证和简单的理解GP的实现。随着GP算法和技术的复杂性和复杂性的增加,验证算法的部分和整体正在执行预期的操作变得更加为此,我们提出了基本验证GP的基础,特别强调交叉操作的正确性。虽然遗传编程最早的工作使用树结构作为问题的候选解决方案,但此后已经开发了许多替代表示(例如,线性的、图形的、基于语法的)。扁平线性结构在概念上比嵌套树更简单,并且对函数程序员非常熟悉因此,我们将专注于开发基于堆栈的遗传规划算法。关注形式化方法的研究人员已经产生了许多不同的定理证明器,可以用来证明GP的正确性。然而,在这方面,s被接受在第四届归纳编程方法和应用国际研讨会上发表。典型的GP研究人员比证明助手更熟悉编程语言依赖类型语言(如Agda [6])是一个很好的选择,因为它们在类型级别上具有足够的表达能力,可以强制执行GP中存在的不变量,同时保留编程语言的外观和感觉,而不是证明助手。在对堆栈语言和依赖类型进行概述之后,本文的结构将遵循GP的通用分类方案:– 参数:我们将从一个非依赖类型化的表示开始,并研究如何使用标准的事务依赖类型化来确保遵守种群大小参数。– 表示:然后我们将修改我们的术语表示,以使用精确的依赖类型,在候选程序的类型中编码arity信息。– evaluation函数:然后我们将引入一个演化术语的评估函数,通过利用宿主语言的整体要求,该函数可以确保终止并且不会以其他方式发散– 遗传算子:然后我们将传递性的属性编码到与交叉相关的函数类型中,确保病态类型的程序永远不会进入种群。– 初始化过程:最后,我们将说明初始化我们的种群的基本过程,注意只随机选择与目标程序的类型签名1.1堆栈语言在基于堆栈的语言中,例如Forth [3],“常量”和“过程”之间没有区别。相反,每个句法元素被称为“词”。每个单词都可以被建模为一个函数,该函数将前一个堆栈状态作为值,并返回随后的(可能已更改的)状态。例如,考虑布尔域中的一种小型语言,由true、not和and组成。像true这样的单词(通常被认为是一个常量)对输入堆栈没有任何要求,只是返回输入堆栈加上一个推到顶部的布尔值“true”。另一方面,并要求输入堆栈至少有两个元素,在将它们的逻辑合取推 回堆栈以替换它们之前,它会弹出并计算这两个元素。对于像我们的例子这样的单类型语言,出现了简单的类型规则,为每个单词分配两个自然数。第一个表示所需的输入堆栈长度(前置条件),而第二个表示输出堆栈长度(后置条件)。这样的词的序列形成堆栈程序,对于该堆栈程序存在聚合输入/输出对。在遗传操作,如交叉,堆栈程序必须以某种方式进行操作,以产生后代的下一代。Tchnernev [8]展示了如何使用与消耗/产生的堆栈大小相关的arity信息,仅在将产生良好类型的术语的点处执行交叉。Tchnernev [9]已经记录了许多不同的方法来做到这一点,但为了简单起见,我们将使用1点交叉。1.2依赖类型依赖类型语言允许类型签名中的参数被标记为(sim-类似于值级别的变量绑定),并在类型签名中的其他地方使用,clare类型和值之间的依赖关系。本文将使用依赖类型化语言Agda [6]作为其所有示例。1Agda是一种像Haskell [2]一样的纯函数式语言,但它是完全的(而不是部分的),并且具有更具表达力的类型系统(允许类型检查器强制执行更多属性)。在编译时,Agda程序必须通过两个检查来证明它们的完整性。终止检查是通过检查结构递减递归调用来完成的覆盖检查是通过要求在函数定义中考虑函数参数的每个类型正确的值来完成的因此,Agda程序不会由于意外输入而无法终止2由于语言的整体性,任何2参数出于教学的目的,我们将首先考虑如何以典型的非依赖函数式编程风格表示术语/程序的群体。之后,我们将扩展该示例以使用依赖类型。32.1人口列表首先,让dataWord: Setwheretrue not and:Word这个简单的示例语言旨在使用众所周知的常量和函数对布尔域进行操作。当然,堆栈程序不仅仅是一个单词,而是我们想要按顺序执行的一系列单词。熟悉的基于cons的列表可以作为多个单词的容器,所以让我们将其键入。1应该可以将例子翻译成类似的语言,如Epigram [4]或Idris [1]。2Agda程序可以通过共归纳定义和corecursion成功地不终止,如果受控的不终止是我们想要的。3有关Agda中依赖类型编程的完整和适当的教程,请参见[6]data List(A: Set):Set其中 []: ListA_::_:A→列表 A→列表 A术语:套件术语=列表单词特别注意列表类型的A:Set部分。Set是Agda中的类型,A是一个标签,它的作用类似于变量,但在类型签名级别。换句话说,我们已经创建了一个多态列表类型,它由它可以包含的数据类型参数化术语是列表的一个具体实例,可以保存我们示例语言的单词下面是我们现在可以展示的一些notNot:术语notNot = not:: not::[]anotherTrue:术语anotherTrue= not:: not:: true::[]:术语= not:: and::[]GP要求我们研究的不是一个术语,而是几个术语的集合,称为总体。通常,这可以表示为术语列表的列表总体:设置总体=列表项虽然上面的类型当然是功能性的,但它留下了错误的空间。这将我们带到了第一个在依赖类型的帮助下保持GP不变量的例子。也就是说,GP作用的人群预计将一定的大小,并且随着GP从一代到下一代的发展,它应该保持这个大小。2.2人口矢量在依赖类型的世界中,一种简单有效的方法来确保保持某个不变量是创建一个类型,该类型只能构造满足该不变量的值(在我们的例子中,我们希望种群大小参数是我们在配置运行时指定的某个自然数。这给我们带来了一个典型的例子,一个依赖类型,向量。我们已经看到了列表类型是如何实现多态性的参数。向量有一个额外的参数来表示它们的长度。→→→ →→data Vec(A:Set):N Setwhere[]:VecAzero_::_:{n:N}→ A→ Vec A n→ Vec A(n)人群:N设置人群n = Vec术语n空向量的长度为零。由“cons”产生的向量的长度是尾长度的后继。给定一个类型的这样一个归纳定义,任何给定向量的自然数索引只能是它的长度。就像我们对Term的定义一样,Population只是一个更一般的类型(Vec)的具体实例化。作为一个例子,这里是前面提到的三个术语的一小部分流行:人口3pop = notNot:: anotherTrue:[]再次注意,该类型需要正好三个项的填充。如果我们要提供更多或更少的值,则在编译时会发生类型错误时间我们已经有效地将对程序的某些语义属性的检查移到了编译时,这意味着当程序正在运行4现在我们已经看到了如何构造依赖类型,让我们看看在Vec上操作的函数如何利用它的属性。在选择期间,GP将需要从群体中检索候选程序。一个非常常见的错误(甚至在入门级编程课程中也会教授)是在容器结构的边界之外进行索引。我们有什么办法来防止这种情况发生?理想情况下,用于查找成员的参数的类型应该与我们的vector的长度一样多这样,在查找索引类型和向量位置之间将存在双射。data Fin:N→ Set wherezero: {n:N}→ Fin(n)n: {n:N}→ Fin n→ Fin(n)lookup:{A:Set} {n:N} Fin nVec AnAlookup zero(x::xs)= xlookup(x:: xs)= lookupi xs有限集Fin的类型对于任何Fin n都有n个可能的值在查找函数中,自然数索引在有限集合和向量参数之间共享。这种共享的效果是,每个有限集参数具有与向量参数的长度一样多的可能构造4事实上,唯一的其他原因是由于程序员错误的编码而导致的逻辑错误。编译器不允许由于非终止或缺少覆盖而导致的典型运行时错误→静态地防止任何由于我们的Population仅仅是一种特定类型的向量,因此我们可以在为选择过程定义函数时使用安全查找。3表示在上一节中,我们将人口中的术语表示为未经修饰的单词列表。为了以[8]描述的方式执行类型安全的交叉,我们的术语的类型需要更有说服力。3.1类型推导当我们实现一个类型安全的crossover版本时,我们需要密切注意我们在操纵。就像Vec有一个额外的自然数参数来表示它的长度一样,我们希望一个Term类型有一个额外的参数来表示消费/输入堆栈的大小,另一个参数来表示生产/输出堆栈的大小在为任意语言展示一个广义的列表类型的Term类型之前,我们先来看看一个更传统的类型关系到Agda的嵌入。dataTerm(inp:N):NSetwhere[]:Terminp inp真:{out: N}→Terminp out→ Term m(1 +out)不是:{out: N}→ Terminp(1 +out) → Term m(1 +out)和:{out:N}→ Terminp(2 +out)→ Term m(1 +out)回想一下,第一个参数是消耗的堆栈大小,第二个是产生的堆栈大小。空项[]消耗一些值inp并产生相同大小的堆栈,充当标识程序。也请注意,它没有前提,所以它可以被认为是一个类型理论公理。其他三个构造函数由前一个Term值参数化,表示每个类型化规则的前提。这一任期代表应当将术语2 1单独视为一种类型时,2和3分别表示输入和输出堆栈大小。在一个带有Term前提的构造函数的上下文中,前提的“输出”位置表示该词的前提条件,而结论的“输出”位置表示w或d的前提条件。真规则指出,如果我们有某项消耗了某个值inp,并产生另一个任意值out,那么结论允许我们推断另一项的存在,该项具有相同的输入和一个额外的输出。换句话说,true有一个始终有效的前提条件和一个声明前提条件中的值将递增1的后置条件。在not规则中,前提相反,以前的输出堆栈大小必须至少为1,但可以更大。因为out参数是在大括号中给出的,Agda将其视为一个隐式参数,可以根据上下文中的其他类型进行统一/推断。这样,1 + out可以表示多个值,例如1 + 0或1 + 7。not的结论允许我们推断输出堆栈大小1 + out的另一项的存在。这符合我们非正式的心理模型,即不需要至少一个参数弹出堆栈,并将逻辑否定推回。最后,并遵循相同的模式,不同之处在于它需要至少两个值,而只生成一个值,从而使输出堆栈大小比以前的大小正好小一个。作为类型化派生,我们前面的基于列表的术语看起来像下面这样(注意,我们重载了Word和Term类型的构造函数)。notNot:第1项1notNot= not(not[])anotherTrue:Term 0 1anotherTrue= not(not(true[])):第2项1andAnd:第3项1andAnd = and(and[])我们的术语现在在它们的类型中有了额外的消费/生产价值。andAnd项显示表示如何正确组合多个项的类型 第一个和需要两个值,并产生一个,它满足第二个和的要求之一,导致最终类型的术语3 1。我们可以强调输入堆栈在整个子项中保持不变,并在andAnd中分解每个子项。a :术语33 a =[]b :术语32 b =和ac :第3项1c =和b3.2句法非唯一性为了避免混淆,我们将指出,在我们的表示中,多个语法相同的术语可以有不同的类型。具体来说,可以改变的是堆栈上最底层的空构造函数提供的参数的原始数量。→→→→→empty: Term 42 42empty =[]'andAnd能够用语法相同的子项表示多个不同的类型是一个属性,我们稍后在定义函数时将利用这个属性来安全地拆分和重组交叉项。3.3派生抽象当在term类型上编写函数时,为语言中的每个单词提供大小写将是乏味的。相应地,我们将把我们语言的构造函数中的公共部分提取到一个通用的术语中,这可以被认为是抽象出上面给出的每一个类型规则。诀窍是使用模块参数的类型的字,以及功能的前提/先决条件和结论/后置条件的每个规则。其结果是一个通用的类似列表的术语结构,并使库不依赖于任何特定的语言来发展。模块DTGP(字:集合)(前后:字→N→N),其中dataTerm(inp:N):NSetwhere[]:Terminp inp_::_:{n:N}(w:Word)→Term inp(prew n)→Terminp(postwn)pre:WordN Npretrue n=n prenot n=1+n preandn=2+npost:novemberpost truen=1+n postnotn=1+n postandn=1+ n开放importDTGP Word pre post就像List或Vec一样,我们的新Term现在只有一个空的case和一个cons(::)case。现在我们可以重写我们的示例,使其看起来像List对应的示例,除了在它们的类型中添加额外有用的消费/生产¬∧→ →→notNot:术语1 1notNot = not:: not::[]anotherTrue:术语0 1anotherTrue= not:: not:: true::[]第二学期1= not:: and::[]和和:第三学期1andAnd = and:: and::[]4评价职能当比较进化术语之间的相对性能时,通常需要评估它们以确定适应性。我们将继续为到目前为止使用的示例语言编写一个eval- uation函数。请放心,Agda将执行终止和覆盖检查,以证明功能的完整性。请注意,下面的示例对每个可能的项和输入向量都有一个case,并在递归调用中使用输入项的结构上较小的尾部。eval:{inp out:N}Terminp outVecBool inpVecBool outeval[] is=iseval(true:: xs)is=true:: evalxsis eval(false:: xs)is=false:: eval xsis eval(not::xs)iswith eval xsis... | o :: os =o :: oseval(and:: xs)is与eval xsis... | o 2:: o 1:: os =(o 1o2) ::ns eval (or:: xs) is with eval xs is... | o 2:: o 1:: os = (o 1∨ o 2) :: os除了要计算的项之外,eval还接受一个布尔向量5,其长度inp等于项所期望的输入数。函数的返回类型是另一个bools out的向量,与计算项当然,这两个属性都是静态地强制执行的,从而更保证我们的算法正在做我们期望的事情。4.1适应度函数再次,我们使用一个模块来接受一个通用的评分/适应度函数作为参数。下面是一个函数的例子,它分配一个程序(5不要被Bool类型和Term类型的true/false构造函数所迷惑。Agda可以根据它们在上下文中的类型来区分重载的构造函数名称。→→→ →→接受两个输入并产生一个输出),其得分等于其满足偶奇偶性的所提供示例的数量。模块Evolution {inp out:N}(score: Term inp out→N)其中评分:第2学期1Nscore xs=count(λishead(eval xsis)==evenParityis)((true::true::[])::(true::false::[])::(false:: true:: [])::(false:: false::[])::[])开放式Evolution评分5遗传算子当编写遗传算子时,例如 Tchnernev的[8]1点交叉,我们需要采取不同术语的子部分,并以安全的方式重新组合它们。Tchernev指出,我们需要在相等输出堆栈的一个点上拆分父项,以实现安全的重组。这就引出了一个问题:在两个任意项以这种方式分开后,安全附加它们的标准是什么?5.1可传递追加术语可能有不同的初始输入堆栈,并根据其包含的单词产生不同的输出。两个项的安全附加说明了传递性。_++_:{inp midout:N}Term midoutTerminpmid Terminp out[]++ys = ys(x:: xs)++ys= x::(xs++ ys)bc:术语2 1bc =和::[]ab:术语3 2ab =和::[]ac:术语3 1ac = bc ++ ab如果试图附加两个输入和输出要求不满足彼此的术语,则会发生编译错误。使用这样一个信息类型的函数,当在另一个函数(如crossover)中使用时,我们可以高度自信地认为我们正在做正确的事情我们很快就会看到,这个函数的类型实际上给我们的不仅仅是简单的信心。5.2传递拆分现在我们有了一个以传递方式安全地重组术语的函数,我们需要想出一种兼容的方法来拆分交叉父代。在DTP中,视图[5]是一种通用的技术,用于使用特定类型来揭示另一种类型的结构信息。在我们的例子中,我们希望将一个术语看作一个- other类型,表示它被分成的两个子部分。下面是[7]中TakeView类型的衍生物。data Split {inp out:N}(mid:N):Terminp out→ Setwhere_+上面的类型准确地捕获了我们希望如何表示拆分项,以便它们可以传递地重新组合。中自然数索引揭示了一个项被拆分的满足的前/后条件点,而项索引是我们正在拆分的值。构造函数携带两个共享mid的子项,结果类型可以通过xs ++ ys重新组合这两个子项。给定两个父项以这种方式拆分,交叉需要产生两个子代,它们在拆分时交换子项这两种交换的函数都可以直接定义。swap1: {inp mid out:N}{xs ys: Term inp out}→拆分中间xs→拆分中间ys→期限输入输出交换1(xs++swap2: {inp mid out:N}{xs ys: Term inp out}→拆分中间xs→拆分中间ys→期限输入输出交换2(xs++依赖对给定某个项和一个自然数,我们希望在由该数字表示的索引位置处拆分该项。此函数将是决定杂交母本分裂的关键。Split足够具体,可以告诉我们两个子项之间的共享mid。然而,对于这个函数,我们不关心mid是什么(我们实际上希望函数为我们确定分割点数据集(A:Set)(B:A→Set): Set where_,_:(x:A)→Bx→ A B一个非依赖对或元组携带2个任意类型的值。在pairs的依赖版本中,第一个组件中的值用于确定第二个组件中的类型。一种常见的DTP技术是使用依赖对来隐藏返回值的索引类型,当您不知道或不关心它将是什么时。例如,有时我们只想写下一个向量值,并让编译器确定唯一的可能长度。→→→→→→→→specifiedLength:N(λn Vec Booln)specifiedLength= 3,true::false::true::[]discoveredLength:N(λn Vec Booln)discoveredLength=_,true::false::true::[]注意在类型中使用了匿名函数。请记住,在DTP中,我们可以在类型级别做任何我们可以在值级别做的事情,包括使用众所周知的λ。有了这个依赖对我们的袖子把戏,我们准备定义分裂。拆分:{inp out:N}(n:N)(xs:Term inpout)N(λmidSplit midxs)splitzero xs = _,[]++split(n)(x::xs)withsplit nxssplit(n)(x::._)| _ , xs++’ ys =_,(x::xs)++因为我们返回的是一个Split值,所以split将始终包含两个子项,这两个子项可以通过传递组合来生成原始项。通过这种方式,拆分andAnd会得到两个类型为Term 2 1和Term 3 2的and::[]值。5.3类型保持交叉有了前面定义的类型和函数,定义一个crossover函数并不遥远,它接受两个相同类型的父项并返回两个相同类型的子项拆分女性对于1点交叉的第一步,我们需要在某个随机的6点拆分第一个父节点(这里称为因此,我们需要知道女性的长度,然后选择一个随机数,以该长度为界。长度:{inp out:N}输入输出N项长度[]= 0length(x:: xs)=x(length xs)splitFemale:{inp out:N}(xs:Terminp out)Nλmid(λ mid)拆分中间xs)splitFemale xs rand with randmod((length xs))... | i = split (to N i) xs6为了使示例尽可能简单,这里我们将随机数作为参数传递给函数。最后的实现使用了一个标准的状态monad,其中包含一个随机数种子,以增加模块性,并避免错误地重用随机数。→→≡注意,我们使用了一个mod函数,它返回一个表示其两个参数的模的有限集合。这个函数的定义可以在补充源代码中找到,因为它与手头的解释没有直接关系。基于雌性被分裂的中间指数,雄性分裂可以通过选择所有可能的相容分裂的随机成员来确定。拆分:{inpout:N}(nmid:N)(xs:Terminpout)N(λn Vec(Splitmidxs)n)用split zero xs拆分zero mid xs... | mid’ , ys with mid =? mid '... | yes p rewrite p = _ , ys :: []... | no _ = _ , []splits(n)midxs with split(n)xs... | mid’ , ys with mid =? mid'|splitsn mid xs... |_,rewrite p = _,ys::|_ , yss rewrite p = _ , ys :: yss... |没有|_,=_,在分裂的定义中,我们同时在男性术语内的所有可能位置进行分裂,并过滤掉那些不允许成功传递重组的可能性。直观地,算法必须将原始分割的目标中间与当前分割中的“中间”进行通常,两个项的比较是通过将它们传递给一个产生布尔值的函数来执行的,并以不同的方式处理true和false情况然而,我们需要一个更丰富的布尔类型(命题相等类型),其值与额外的类型级别信息相关联,这些信息可用于进行Split值类型检查。考虑是p的情况(类似于典型的真情况)在分裂零的情况下。我们想返回新拆分的ys值,但是类型检查器不允许这样做。为什么会这样?如果我们看一下splits的类型签名,它需要一个Splitmid xs,但ys是一个Splitmid幸运的是=?comparison函数返回的不仅仅是一个布尔值:它产生了一个构造性的证明,证明两个被比较的值实际上是相同的。我们将proof p(模式匹配为yes p)传递给Agda检查器:分割中间的' xs是可以接受的,因为中间的'。我们能从中得到什么?主要的兴趣点是类型检查器需要正式的构造性证据,以强制执行程序员规定的不变量在实践中,这个证据很容易处理,因为它是由普通的依赖类型组成的(就像其他东西一样回报是信心;验证程序是否按预期运行的负担从程序员的肩上卸下,落到了类型检查器的肩上当我们拆分父本时,我们从类型正确的拆分中随机选择一个成员。然而,这个函数返回一个Maybe类型的值,所以如果根本没有兼容的拆分,它可能什么也不返回→→×splitMale:{inp out:N}(xs:Terminpout)(mid rand:N)Maybe(Splitmidxs)splitMale xs mid rand带分割(长度xs)中间xs... | zero , [] = nothing... | suc n , xss=just(lookup(rand modn)xss)请注意,分裂实现中的证明复杂性是孤立的。一旦我们有了一个类型为python的函数定义,我们就可以自由地使用它,而不必重复任何工作。最后,我们可以编写crossover来组合女性和男性的拆分,并使用前面定义的交换返回两个孩子。crossover: {inp out:N}(女性男性:输入输出)(randFrandM:N)长期输入输出长期输入输出交叉女性男性randF randMwith splitFemale female randF... | mid , xs with splitMale male mid randM... | nothing = female , male... | just ys = swap 1xs ys , swap 2xs ys如果不存在有效的男性交换,我们返回原来的两个父对象。6初始化过程在我们的GP运行开始时,我们希望我们的算法能够对类型良好的候选程序进行操作。因此,初始化函数必须确保只生成相对于我们要进化的目标程序的随机类型正确的程序。到目前为止,我们可以(并且将会)静态地强制执行此要求下面采用了一个简单的类型安全枚举和过滤策略6.1类型安全枚举筛选器首先,我们要枚举所有符合给定输入堆栈大小的最大长度的项,即max-inp。然后,filter-out也会过滤这个结果,只包含那些与所需输出堆栈大小匹配的项。最后的列表可以作为一个池,从中随机选择我们的人口。- 输入:(n inp:N)→列出单词→列出(列表(Nλ输出→术语输入输出)→列表(术语输入输出)→→→ →≡¬¬ → ≡ → ⊥¬再次使用依赖对,允许我们返回一个对于inp是同质的,但是对于out是异质的列表。为了实现这一点,我们向用户询问一个函数,该函数确定我们想要扩展术语的单词的先决条件是否可以通过所述术语的当前输出来满足。模块初始化(match:(w:Word)(out:N)Dec(Nλn outprewn))其中同样,footswitch是另一个模块,因此用户可以自由地通过其他方式初始化种群。Decidable RelationsDec是一个多态类型构造函数,其值表示类型/命题的某些证明是否存在,或者任何此类证明是否会导致bottom(dataDec(P: Set):Setwhere yes:( p:P)→Dec Pno:(<$p: P→)→ Dec Pmatch在Dec中使用存在命题(依赖对),并且像所有Agda函数一样是全的它实际上需要一个证明词这意味着实现者不必担心过早地搜索合适的n结尾,就像Maybe(在这种情况下常用的类型)可能发生的那样。match not zero = no p其中p:<$N(λn 0 <$n)p(_,())不匹配(n)=yes(n,refl)上面的例子证明了当一个项的输出为0时,不满足的先决条件是不可满足的7,并展示了如何为任何大于零的输出找到合适的n。Escher-inp的定义很明显地从带有单词列表参数的递归调用中扩展了类型安全术语滤出的实现更加直接,再次使用=?以证明期望的输出等于返回的输出7一对空括号是Agda语法,用于向类型检查器指示此类型的值不可居住。×7结论我们已经给出了一个参数化GP库的轮廓,其操作使用依赖类型进行验证。同样的库也可以用于演化除布尔值以外的领域上的语言,例如自然数等。依赖类型可以通过使用非正式数据类型和函数类型签名来强制执行所需的不变量我们已经说明了使用类型安全的1点交叉创建经过验证的基于堆栈的GP实现的一些基础知识。通过建立在已验证的基础上,可以创建更复杂的GP算法,并且可以以更大的信心分析进化数据,即由实现引起的错误不会影响GP运行行为。希望本文提供的示例可以作为一个有用的模板,以帮助作者在依赖类型编程的上下文中为他们特定风格的GP编码不变量最后,这些技术通过在域类型(例如,N N)上参数化主模块并为所述类型提供决策过程来平凡地扩展到具有多个类型堆栈的语言。目前正在研究如何进一步利用这种技术来发展任意类型的关系,而不是这些类似Forth的堆栈。引用1. E. C. 布雷迪Idris-:系统编程满足完全依赖类型。在第五届ACM编程语言与程序验证研讨会上,PLPV '11,第43-54页,美国纽约州纽约市,2011年。ACM。2. S. P. 琼 斯 。 Haskell 98 语 言 和 库 : 修 订 报 告 。 Journal of FunctionalProgramming,2003。3. M. G. Kelly和N.间谍第四:文本和参考。普伦蒂斯-霍尔公司,上鞍河,新泽西州,美国,1986。4. C.麦克布莱德Epigram:Practical Programming with Dependent Types.第130- 170页。2005年5. C.麦克布莱德和J·麦金纳。从左边看。J.功能程序. ,14(1):696. 联合诺瑞尔agda中的依赖类型编程。高级函数式编程,2008年。7. N. Oury和W. 斯维尔斯特拉π的力量在Proceeding of the13th ACM SIGPLANinternational conference on Functional programming , ICFP '08 , pages 39-50,New York,NY,USA,2008。ACM。8. E.切尔涅夫第四次交叉不是宏突变吗?在J. R。科扎,W. 班扎夫,K. 切拉皮拉湾Deb,M.Dorigo,D.B. Fogel,M.H. Garzon,D.E. 戈德堡,H. Iba 和 R.Riolo , 编 辑 , Genetic Programming 1998 : Proceedings of theThird Annual Conference,第381-386页摩根·考夫曼9. E. B. 切尔涅夫遗传规划中的堆栈校正交叉方法。在E. C antu′-Paz,编辑,GECCOLateB reakingPapers,第443-449页。 A AAI,2002年。
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- zigbee-cluster-library-specification
- JSBSim Reference Manual
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功