【问题标题】:Quine's algorithm with Single Sided Unification in PrologProlog中具有单面统一的Quine算法
【发布时间】:2021-05-16 22:45:03
【问题描述】:

SWI-Prolog 的新版本 8.3.19 引入了单面统一 在新的 Picat 样式规则中。这可能是一个受欢迎的补充 序言系统。我想知道我们是否可以重写Quine算法

Quine算法的Prolog实现
https://\stackoverflow.com/q/63505466/502187

Picat 样式规则以及这是否可行?如果是并且如果 Quine算法的编写变得更简单,那么SWI-Prolog可能 此次添加对社区有很大帮助。

有没有人接受这个挑战? SWI-Prolog 8.3.19 已经可以从开发中获得。

【问题讨论】:

    标签: prolog unification propositional-calculus picat


    【解决方案1】:

    虽然正常的统一又名双边统一与内置 (=)/2 密切相关,但模式匹配又名单边统一和内置 (==)/2 之间存在类似的关系。这些引导将起作用:

    =(X,X) :- true.
    ==(X,X) => true.
    

    如果我们查看 Quine 算法的代码,取自 here,我们会发现很多 (==)/2 用法。模式匹配可以直接做的工作:

    simp(A, A) :- var(A), !.
    simp(A+B, B) :- A == 0, !.
    simp(A+B, A) :- B == 0, !.
    Etc..
    

    所以我们尝试了一下,将所有规则都转换为模式匹配。然后不再需要初始的 var/1 保护, (==)/2 也不再需要。但是我们观察到我们需要更多 (=)/2 来返回函数值:

    simp(0+B, X) => X = B.
    simp(A+0, X) => X = A.
    Etc..
    

    我们做了一个小基准测试并验证了来自 Principia 的 193 个命题逻辑测试用例。我们测试了正常的统一和模式匹配。我们还比较了一个尚未编译的模式匹配变体,即使用 subsumes/2 的扩展:

    首先通过 subsumes/2 扩展,不编译模式匹配:

    /* Jekejeke Prolog 1.5.0 */
    /* normal unification */
    ?- time((between(1,380,_), test, fail; true)).
    % Up 996 ms, GC 6 ms, Threads 984 ms (Current 02/14/21 11:30:28)
    Yes
    
    /* pattern matching */
    ?- time((between(1,380,_), test, fail; true)).
    % Up 3,525 ms, GC 24 ms, Threads 3,500 ms (Current 02/14/21 11:42:50)
    Yes
    

    现在 SWI-Prolog 的新编译模式匹配:

    /* SWI-Prolog 8.3.19 */
    /* normal unification */
    ?- time((between(1,380,_), test, fail; true)).
    % 4,940,000 inferences, 0.547 CPU in 0.534 seconds (102% CPU, 9033143 Lips)
    true.
    
    /* pattern matching */
    ?- time((between(1,380,_), test, fail; true)).
    % 4,940,000 inferences, 0.531 CPU in 0.531 seconds (100% CPU, 9298824 Lips)
    true.
    

    我是期待编译的方式显示一个tick比较bang而不是只保存正常统一的表现?不过,这是一个好的开始。

    开源:

    1847 年的布尔方法,Prolog 风格
    https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole-pl

    1847 年的布尔方法,皮卡特风格
    https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole2-pl

    Picat 扩展
    https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-picat-pl

    来自 Principia 的 193 个命题逻辑测试用例
    https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-principia-pl

    【讨论】:

      【解决方案2】:

      除了使用基于 subsumes/2 的翻译进行单面统一之外,另一种方法是使用较低级别的单面统一。 SWI-Prolog 8.3.19 已经实现了,但我的系统的另一个答案没有显示。

      我们是否找到其他也提供较低级别实现的 Prolog 系统 单面统一?事实证明是的,例如 ECLiPSe Prolog:

      4.6 匹配
      在 ECLiPSe 中,您可以编写使用匹配(或单向统一)而不是头部统一的子句。此类条款是 用 ?- 函子而不是 :- 编写。匹配有属性 调用者中的任何变量都不会被绑定。

      ECLiPSe - 教程介绍
      第 47 页(逻辑第 37 页)
      http://eclipseclp.org/doc/tutorial.pdf

      我们也在我们的系统中添加了这样的运算符。规则现在写成如下:

      simp(0+B, X) ?- !, X = B.
      simp(A+0, X) ?- !, X = A.
      Etc..
      

      现在我们又回到了平时的表现:

      /* Jekejeke Prolog 1.5.0 */
      ?- time((between(1,380,_), test, fail; true)).
      % Up 1,067 ms, GC 11 ms, Threads 1,032 ms (Current 02/14/21 21:43:56)
      Yes
      

      注意!

      开源:

      1847 年的布尔方法,ECLiPSe 风格
      https://gist.github.com/jburse/713b6ad2b7e28de89fe51b98be3d0943#file-boole3-pl

      【讨论】:

        猜你喜欢
        • 1970-01-01
        • 2014-09-20
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        • 1970-01-01
        相关资源
        最近更新 更多