魔力哈斯克勒：系统演示与合成引擎

MagicHaskeller：系统演示片山进宫崎大学1-1 W。日本宫崎县宫崎市学园祭台889-2192skata@cs.miyazaki-u.ac.jp抽象。 本文介绍了归纳函数式程序设计系统的代表之一--Mag - ic H askeller的使用方法和行为。虽然MAGIC HASKELLER是一种基于系统穷举搜索的生成和测试方法，但在其最近的版本中添加了一个分析合成引擎，这使得一种新的方法能够从给定的输入输出示例的不充分集合中解析地生成许多程序，并使用单独给定的谓词测试这些程序。这两个引擎都提到了。1概述MAGIC HASKELLER [Katayama（2005 b）]是一个基于系统穷举搜索的归纳函数式编程系统。归纳函数式编程（IFP）是编程自动化的一种形式，其中递归函数式程序通过从通常作为一组输入输出对给出的模糊规范的泛化来合成。 目前，IFP有两种方法：分析方法，通过查看输入输出对并进行归纳推理来综合程序;生成和测试方法，生成许多程序并挑选满足规格说明的程序。自2005年第一个二进制版本发布以来，MAGICHASKELLER自其0.8.6版发布以来，增加了分析搜索算法，并且可以称为分析生成和测试方法的新方法已经成为可能，其中分析合成器从给定的不充分的输入输出示例集合中生成许多程序，并挑选那些满足作为规范的一部分单独给出的谓词的程序。在这篇简短的演示论文中，我们介绍了如何使用合成引擎和使用它们的结果2建筑安装MAGIC HASKELLER是在HASKELL中开发的，其最新版本作为库发布。为了构建和安装它的副本，首先需要安装版本6.10。或6.12。GlasgowHaskell Schools（GHC）尽管可以用GHC的版本7构建MAGIC HASKELLER的版本 0.8.6.1，分析生成和测试功能不适用于此版本的GHC。此外，为了简化安装过程，您应该拥有Cabal [Jones（2005）]包，它是分发HASKELL程序的标准框架此外，如果安装了cabal-install包，只需键入阴谋集团更新cabalinstall MagicHaskeller构建并安装MAGIC HASKELLER系统到用户作为一个库实现，MAGICHASKELLER的典型用法是在Glasgow HaskellInteractive（GHCi）中使用它，如QuickCheck[Claessen和Hughes（2000）]。这是通过使用-package MagicHaskeller选项调用GHCi来实现的。使用Template Haskell的语言扩展[Sheard and Peyton Jones（2002）]也是必要的，如果你想用它的牛津括号语法做各种事情。因此，MAGIC HASKELLER通常与ghci -软件包MagicHaskeller-XTemplateHaskell在本文中，当引用使用交互式系统时，我们总是提供-v0选项，表示详细级别为0，以避免混乱。3用于穷举搜索系统穷举搜索模块定义了生成所有程序（直到语义等价）的函数，这些程序可以使用给定的原语集与函数应用程序和lambda抽象来构建，作为无限流[Katayama（2005 a）]。它们还定义了测试生成程序的函数程序流的生成算法是在Curry-Howard同构下，基于Curry-Howard演算，有 效 地 证 明 了 与 给 定 类 型 对 应 的 命 题 的 所 有 证 明 。 03 The Dog（2010）这些模块的最大特点是，它们只需要选择原语集并以谓词的形式编写规范就可以合成程序。规范不需要是一组输入输出对。函数的类型必须通知算法，但用户不需要显式地给出它。它可以从作为谓词给出的规范中推断出来。最后，介绍了系统化搜索引擎的使用方法更多的例子可以在[Katayama（2006）]中找到，尽管它描述了MAGIC HASKELLER的旧版本。3.1一个简单的例子这是一个让MAGIC HASKELLER合成函数的例子，“abc”并返回“aabbcc”：$ ghci -package MagicHaskeller -XTemplateHaskell -v0Prelude>：m +MagicHaskeller.LibTHPrelude MagicHaskeller.LibTH> init075Prelude MagicHaskeller.LibTH> printAll $\f->f“abc”==“aabbcc”\a-> list_para a []（\b_d->b：（b： d））\a -> list_para a（\_ -> []）（\b_ d _->b：（b：d 0））0\a -> list_para a（\_ -> []）（\b_ d _->b：（b：d 0））0\a-> list_para a（\_->[]）（\b_d_-> b：（b： d True））True\a-> list_para a（\_->[]）（\b_d_-> b：（b： d True））False\a-> list_para a（\_->[]）（\b_d_-> b：（b： d False））True\a-> list_para a（\_->[]）（\b_d_-> b：（b： d False））False\a -> list_para a（\_ -> []）（\b_ d _->b：（b：d []））[]\a -> list_para a（\_ -> []）（\b_ d _->b：（b：d []））a\a -> list_para a（\_ -> []）（\b cd _->b：（b：d c））a\a-> list_para a（\_->[]）（\b cd_->b：（b：d c））[]\a-> list_para a（\_->[]）（\b_d_-> b：（b： d Nothing））无\a -> list_para a（\b -> b）（\b_ d e ->b：（b：d e））[]\a-> list_para a（\b-> b）（\b c d_-> b：（b： d c））a\a -> list_para a（\b -> b）（\b cd _->b：（b：d c））[]\a -> list_para a（\b -> b）（\b_ d _->b：（b：d []））a\a -> list_para a（\b -> b）（\b_ d _->b：（b：d []））[]中断。Prelude MagicHaskeller.LibTH> printAllF $\f->f“abc”==“aabbcc”\a-> list_para a []（\b_d->b：（b： d））中断。Prelude和>之间的文本区域是GHCi的提示符。GHCi调用后的第一行用于将模块MagicHaskeller.LibTH引入作用域。第二行描述环境并设置组件库，即用推荐的组合子集构造程序的组合子集。第三行请求打印所有表达式，这些表达式可以使用组件库中满足谓词\f->f“abc”==“aabbcc”的组合子进行合成然后，合成的程序逐行打印，从最小的一个与最少数量的功能应用程序，逐步增加的程序大小。list_para函数是（同构于）列表参数的函数phism（例如，[Augusteijn（1999）]），并在模块MagicHaskeller.LibTH中定义其他符号与HASKELL的- \v -> e表示λv.e相同，[]表示空列表，（：）是二元构造函数，它将一个元素添加到列表的第一个因为算法产生了无限的程序流，它必须在途中被中断。printAllF中的字母F意味着通过使用随机化算法过滤掉与任何已经打印的表达式在语义上等效[Katayama（2008）]这是有用的，尽管它影响了效率。在上面的例子中，似乎所有合成和打印的程序都等同于第一次生成的程序。然而，如果计算没有中断，总有可能其中一些被证明是不同的，并在使用printAllF时打印出来。3.2使用富库在程序生成期间而不是在程序生成之后，可以应用用于去除语义等价表达式的过滤器的变体，以减少程序的数量并加快合成。由于过滤本身需要时间，因此使用此技术生成的程序并不总是比不使用此技术生成的程序快。然而，当使用一组丰富的组合子作为组件库时，它会更快。在MagicHASKELLER的0.8.6.1版本中，可以使用MagicHaskeller.LibTH.exploit进行尝试Prelude MagicHaskeller.LibTH> exploit $\f->f“abc”==“abcba”\a-> list_para（reverse a）a（\_c_-> a++ c）中断。尽管在基准测试时使用富库可能被认为是作弊，但它比使用差库更有用，使结果更具可读性。4分析综合模块从0.8.6版本开始，MAGIC H中增加了一个分析合成引擎，凯勒它使用一个算法的第50集5.6 The Dog（2007）[Hofmann et al.（2010）Hofmann，Kitzelmann，and Schmid]以实现生成将许多节目作为一个列表流，其中具有很少案例分割的节目被高度优先化并提前出现。这是通过在找到最佳节目时不停止搜索而是以广度优先的方式继续搜索来实现的I或 II有时遭受之间的权衡所生成的程序的正确性和计算复杂性：（只有）不需要的程序生成，除非有足够数量的例子，以正确地指定所需的功能，并没有程序生成，如果例子的数量太大，由于时间复杂性进行统一。这种权衡通常迫使用户尝试错误，以找到足够数量的I/O示例对，有时会由于缺少这样的数量而导致搜索失败。这些情况经常发生，特别是当论点在不同的维度上增加时，并且存在一些角落情况。例如，IGOR II无法正确地合成Haskell标准前奏中的concat函数和allodd函数，后者接受一个整数列表，如果所有元素都是奇数，则返回。在这两种情况下，当给出几个例子时，都会产生错误的函数，而当给出十个以上的例子时，至少在五分钟内不会得到任何函数。从不足的输入输出对中分析生成许多程序，然后用单独提供的谓词过滤它们，是对这种权衡的一种回答。事实上，这些功能可以通过我们新的分析合成模块进行合成，而无需用户进行任何试错通过将输入输出示例集划分为用于引导搜索的示例集和用于避免生成非预期解决方案的示例集来解决该权衡对于后者为了达到这个目的，用户通常只需要一个一般的例子（因为它不是在边缘或角落的情况下），很少需要列举许多例子。此外，即使这里需要一些示例，也几乎不影响效率。另一方面，可以最小化用于引导搜索的输入-输出示例的集合。此外，即使没有足够数量的例子，也可以找到解决方案，尽管搜索的效率低于给定最佳数量的例子。分析综合优于系统穷举搜索的优点在于，存在穷举算法不能在实际时间跨度内综合而分析算法可以的函数另一方面，一些其他函数，如斐波那契函数，可以通过搜索合成，但不能通过分析算法合成（不使用专门的加法函数，这可以被视为作弊）。目前，分析合成引擎与系统搜索引擎分开工作，除了它们共享一些共同的模块，例如定义语言的模块和实现组合搜索的模块。他们合作制造一种新的合成发动机将在将来进行试验.还要注意，像in这样[Hofmann and Kitzelmann（2010）]尚未实施。4.1一个简单的例子在下一个例子中，长度函数被合成。分析合成引擎生成许多程序，这些程序使用任何背景知识函数来泛化{f[]= 0;f [a]= 1}，而不 使 用 - out 然 后 ， 它 编 译 生 成 的 程 序 ， 并 使 用 谓 词 \f->f“12345”== 5过滤它们。$ ghci -package MagicHaskeller -XTemplateHaskell -v0Prelude>：m MagicHaskeller.RunAnalyticalPrelude MagicHaskeller.RunAnalytical>：设置提示符>>quickStart [d|f []= 0; f [a]= 1|] noBKQ（\f-> f“12345”== 5）\a ->let fa（b@（[]））= 0fa（b@（c： d））= succ（fa d）在fa a：：for all t2中。[t2]-> Int中断。前两行并不重要。第一行用于将模块MagicHaskeller.RunAnalytical引入作用域。第二行将命令提示符替换为>>。后者不是必不可少的，但在使用窄屏幕时建议使用，因为在每次分析合成时必须输入大量信息第三行很重要，但并不很难。由牛津括号包围的声明集[d|. |]是Template Haskell的声明引号，类型为Q [Dec]。 quickStart函数将目标函数的输入-输出对集作为第一个参数，将背景知识函数的输入-输出对集作为第一个参数，并使用谓词来过滤生成的程序。细心的读者可能会注意到，在第一变元和第三变元之间使用不同的语法。例如，在第一个参数中使用变量模式，而在第三个参数中使用具体值，并且在第一个参数中使用隐式等式，而在第三个参数中使用显式等式。这些都不是作者幻想的结果变量模式可以在第一个参数中使用，因为它具有函数定义的形式它们通常是分析合成所需要的，以便进行递归调用，因为递归调用涉及模式匹配。另一方面，用于过滤生成程序的第三个参数必须使用具体值，因为它们不会被抽象解释，而是被编译和执行。虽然在上面的例子中没有提供目标函数的类型，但它可以作为第一个参数中的类型签名声明提供，如[d| f：：[a]->Int; f []= 0; f[a]= 1|]. 如果省略类型签名，则从输入输出对中出现的构造函数的类型推断类型。整型文字被假定为Int类型。它们被特殊处理并转换为0、succ和negate的组合带有@的模式称为as-patterns，参数在@的两边都与两个模式匹配。在上述情况下，因为两个bs未被使用，所以实际上不需要使用as模式。这种对as模式的冗余使用将从未来的版本中删除。4.2具有背景知识功能的示例当应该使用背景知识函数时，它们在第二个参数中指定。在这种情况下，分析合成器生成以背景知识函数为参数的高阶函数。在指定测试功能时应注意这一点。下一个示例显示了使用加法作为背景知识函数的乘法合成。注意，乘法是I或 II无法合成的无聊函数之一由于（+）：：Int->Int->Int被用作背景知识函数，因此生成的程序需要（+）作为第一个参数。> ：{| quickStartF|[d|intx = 0;return 0;|int 1 = 1;2 = 2;|return 0;mult2 1 = 2;|mut2 2 = 4|]|[d| int x = x;int sum= 1;|return 1= 2;int sum= 3;|int sum= 2;1= 3;|加2 2 = 4|]|（\f-> f（+）5 6== （第30段）| ：}\faa b -> letfb（c@0）d = 0fb（c@succe）d|succe> 0 = fa d（fb ed）其中e = succe-1infb ab：：（Int->Int-> Int）->Int-> Int-> Int\faa b -> letfb（c@0）d = 0fb（c@succe）d|成功> 0 = fa（fb e d）d，其中e =成功-1infb ab：：（Int->Int-> Int）->Int-> Int-> Int中断。：{和：}用于输入多行表达式。GHCi的这种语法被引入到版本7中，并且模块MagicHaskeller.RunAnalytical不适用于GHCi的版本，但是实际的单行输入被手工编辑成这种语法，以便使输入行适合本文的页面宽度此外，更改提示符的命令的效果实际上在：{。：}块，但我们假设它在那里工作。在 这 个 例 子 中 ， 我 们 使 用 了 一 个 带 有 字 母 F 的 动 作 ， 即quickStartF，以避免打印等效函数。当然，我们也可以在这里使用quickStart，尽管这样做会导致打印大量的表达式。如果我们将背景知识函数限制为（+），则打印的两个结果仍然是等价的，但如果我们使用非交换运算符，则它们是不同的因此，这两种功能被认为是不同的。4.3使用MagicHaskeller未知的类型到目前为止介绍的操作只适用于预先已知的类型，其构造函数出现在MagicHaskeller.CoreLang.defaultPrimitives中。 没有出现在那里的类型可以通过以下方式处理>：{| quickStartCF $（c[d| f []=0;f[a]=1;f[a，b]=2|]）noBK|（\f->f“foobar”== 6）|：}\a ->let fa（b@（[]））= 0fa（b@（c： d））= succ（fa d）infa a：：for all t6. [t6]-> Int中断。其中函数c提取出现在Oxford括号中的构造函数的值$（和）之间的代码块描述了应该拼接的内容，并且$和（之间不能有5结论本文举例说明了最新版本的MAGIC- HASKELLER的使用方法和行为.除了旧的系统性详尽搜索引擎的使用外，还解释了新增加的分析综合引擎的使用。新的分析综合引擎是基于I或 II，但可以生成许多假设程序。通过分析生成许多程序并测试它们，我们可以拥有一个比I或 II更强大的新综合系统。引用03 The Dog（1999）奥古斯丁排序态射。在高级功能编程中，LNCS 1608，第1-27页。Springer Verlag，1999年。[Claessen and Hughes（2000）] Koen Claessen and John Hughes.快速检查：一个轻量级工具，用于随机测试Haskell程序。 在ICFP'00中：会议记录第五届ACMSIGPLAN函数式编程国际会议，第268-279页。ACM，2000年。[Hofmann and Kitzelmann（2010）] Martin Hofmann and Emanuel Kitzelmann.I/O列表变形的引导检测：针对IP中程序模板2010年ACM SIGPLAN部分评估和程序操作研讨会论文集，PEPM '10，第93-100页，2010年。[Hofmann et al. （ 2010 ） Hofmann ， Kitzelmann ， and Schmid] Martin Hofmann ，Emanuel Kitzelmann，and Ute Schmid.把伊格II从莫德运到哈斯克尔。在UteSchmid，EmanuelKitzelmann和Rinus Plasmeijer，编辑，归纳编程的方法和应用，第三次国际研讨会，AAIP 2009，LNCS的第5812卷，第140-158页， 2 0 1 0年 。[琼斯]艾萨克·琼斯。haskell cabal：一个用于构建应用程序和库的通用架构。第六届函数式编程趋势研讨会，第340-354页，2005年。[片山]片山进。 系统搜索lambda表达式。在第六届函数式编程趋势研讨会，第195-205页，2005 a。[片山（2005年b）]Susumu片山魔法哈斯克勒：一基于搜索在-归纳的函数式编程系统http://nautilus.cs.miyazaki-u.ac.jp/MagicHaskeller.html，2005 b.05 The Dog （ 2006 ）用 于 系 统 检 索 表 达 式 的 库 及 其 效 率 评 价 。 WSEASTransactions on Computers，12（5）：314603 The Dog（2008）使用蒙特卡洛搜索与迭代深化的函数程序的高效穷举生成。在Tu Bao Ho和Zhi-Hua Zhou中，编辑，PRICAI，计算机科学讲义第5351卷，第199-210页Springer，2008. ISBN 978-3-540-89196-3。第 53集 9.6 The Father of the Woman（ 2010） MagicHaskeller 的 最 新 改 进 。 在 UteSchmid、Emanuel Kitzelmann和Rinus Plasmeijer编辑的《归纳编程的方法和应用》（Approaches and Ap-plications of Inductive Programming），第三届国际研讨会，AAIP 2009，LNCS第5812卷，第174-193页， 2 0 1 0 年 。[2007年]伊曼纽尔·基泽尔曼。数据驱动感应的递归输入/输出示例的函数。在AAIP[2002年]蒂姆·谢尔德和西蒙·L. 佩顿·琼斯。 Haskell的TEM板元编程。 在HaskellWorkshop2002中，2002年10月。网址：http://research.microsoft.com/Users/simonpj/papers/meta-haskell/Meta-haskell.ps。