LogRu

Logic programming in Rust.

概述

本项目的核心是一个用于解决像Prolog中那样的单谓词逻辑表达式的、小型、高效的Rust库。

此外，还有一个REPL示例，用于与实现进行交互式操作。

与Prolog相比，它目前缺少一些功能。最值得注意的是：

• 没有否定或剪枝（cut），
• 没有内置类型（如整数），
• 没有具有副作用（如IO）的谓词。

展示

在REPL中，您可以快速加载提供的测试文件之一，其中包含一些预定义的事实和规则，例如用于佩亚诺算术的

#===================#
# LogRu REPL v0.1.0 #
#===================#

?- :load testfiles/arithmetic.lru
Loaded!

然后可以要求它解决 2 + 3（并找到正确答案 5）

?- add(s(s(z)), s(s(s(z))), $0).
Found solution:
  $0 = s(s(s(s(s(z)))))
No more solutions.

还可以列出所有加起来等于五的项对

?- add($0, $1, s(s(s(s(s(z)))))).
Found solution:
  $0 = s(s(s(s(s(z)))))
  $1 = z
Found solution:
  $0 = s(s(s(s(z))))
  $1 = s(z)
Found solution:
  $0 = s(s(s(z)))
  $1 = s(s(z))
Found solution:
  $0 = s(s(z))
  $1 = s(s(s(z)))
Found solution:
  $0 = s(z)
  $1 = s(s(s(s(z))))
Found solution:
  $0 = z
  $1 = s(s(s(s(s(z)))))
No more solutions.

Rust API

API的核心不使用与REPL相同的文本表示形式的项，而是将所有内容编码为半透明的ID。然后，有更高层次的API为这些ID提供命名。

核心API

求解器的核心是持有所有已知事实和规则的 logru::Universe 类型。可以像这样定义一些简单的规则，如佩亚诺算术

let mut u = logru::Universe::new();

// Obtain IDs for t he symbols we want to use in our terms.
// The order of these calls doesn't matter.
let s = u.alloc_symbol();
let z = u.alloc_symbol();

let is_natural = u.alloc_symbol();
let add = u.alloc_symbol();

// Define the fact `is_natural(z)`, i.e. that zero is a natural number
u.add_rule(Rule::fact(is_natural, vec![z.into()]));

// Define the rule `is_natural(s(P)) :- is_natural(P)`, i.e. that
// the successor of P is a natural number if P is also a natural number.
u.add_rule(forall(|[p]| {
    Rule::fact(is_natural, vec![ast::app(s, vec![p.into()])])
    .when(is_natural, vec![p.into()])
}));

// Now we define a predicate for addition that we'll call add.
// The statement `add(P, Q, R)` is true if P + Q = R.

// Define the rule `add(P, z, P) :- is_natural(P)`, i.e. that
// adding zero to P is P if P is a natural number.
// This is the base case of Peano addition.
u.add_rule(forall(|[p]| {
    Rule::fact(add, vec![p.into(), z.into(), p.into()])
    .when(is_natural, vec![p.into()])
}));

// Finally, define the rule `add(P, s(Q), s(R)) :- add(P, Q, R)`,
// the recursive case of Peano addition.
u.add_rule(forall(|[p, q, r]| {
    Rule::fact(
        add,
        vec![
            p.into(),
            ast::app(s, vec![q.into()]),
            ast::app(s, vec![r.into()]),
        ],
    )
    .when(add, vec![p.into(), q.into(), r.into()])
}));

现在可以要求求解器证明该宇宙中的陈述，例如“存在一个X，使得X + 2 = 3”。对于X = 1，这个陈述确实是正确的，而且求解器确实会提供这个答案

// Obtain an iterator that allows us to exhaustively search the solution space:
let solutions = query_dfs(
    &u,
    &exists(|[x]| {
        Query::new(
            add,
            vec![
                x.into(),
                ast::app(s, vec![ast::app(s, vec![z.into()])]),
                ast::app(s, vec![ast::app(s, vec![ast::app(s, vec![z.into()])])]),
            ],
        )
    }),
);
// Sanity check
assert_eq!(
    solutions.collect::<Vec<_>>(),
    vec![vec![Some(ast::app(s, vec![z.into()]))],]
);

求解器使用从左到右的深度优先搜索来遍历提供的和派生的目标。这很高效，但需要对谓词进行一些注意，以避免无限递归。

文本API

有关文本API的示例，请参阅例如 examples/zebra.rs，解决泽布拉斯谜题的一个变体。

语法与Prolog非常相似，主要区别在于没有通配符（每个变量都必须显式命名）且变量仍以数字命名。

性能

使用一个效率不高的Zebra谜题版本（testfiles/zebra-reverse.lru）对SWI Prolog进行了基本的性能比较，其中规则的子句顺序被颠倒。

对于SWI Prolog和Logru来说，这使解谜的速度大大减慢（毫不奇怪，因为据我所知，SWI Prolog使用相同的搜索顺序）。

虽然Logru需要大约60毫秒来解决谜题并得出没有更多解的结论，但Prolog需要大约25毫秒来找到解决方案，并额外6毫秒来排除任何其他解决方案，总共31秒。

这部分差异显然是由出现检查引起的，这似乎是Prolog的默认设置。在未启用出现检查的Logru版本中，同样的谜题在约35毫秒内解决。

?- :load testfiles/zebra-reverse.lru
Loaded!
?- :time puzzle($0).
Found solution:
  $0 = list(house(yellow, norway, water, diplomat, fox), house(blue, italy, tea, physician, horse), house(red, england, milk, photographer, snails), house(white, spain, juice, violinist, dog), house(green, japan, coffee, painter, zebra))
No more solutions.
Took 0.0603s

?- consult('zebra-inv.pro').
true.

?- time(puzzle(Houses)).
% 86,676 inferences, 0.025 CPU in 0.025 seconds (100% CPU, 3428088 Lips)
Houses = list(house(yellow, norway, water, diplomat, fox), house(blue, italy, tea, physician, horse), house(red, england, milk, photographer, snails), house(white, spain, juice, violinist, dog), house(green, japan, coffee, painter, zebra)) ;
% 22,610 inferences, 0.006 CPU in 0.006 seconds (100% CPU, 3518245 Lips)
false.

未来计划

不承诺任何时间表，值得实验的其他特性包括

• 递归和内存限制。
• 一个分析模式，可以统计关于求解器的一些有趣的事实和数据（例如，所采取的步骤数，实例化规则数，峰值内存使用量）。
• 通过优化出现检查等手段使事物运行得更快。
• 文本API中的命名变量。
• REPL中的自动完成。
• 不纯的谓词（即那些在Rust中有实现并能直接操作求解器状态的谓词）。
• 剪断和否定（这可能会根据前一点实现）。

许可证

根据您的选择，许可协议可以是以下之一

• Apache License，版本2.0（LICENSE-APACHE 或 http://www.apache.org/licenses/LICENSE-2.0）
• MIT许可证（LICENSE-MIT 或 http://opensource.org/licenses/MIT）

。

贡献

除非您明确声明，否则根据Apache-2.0许可证定义的，您提交的任何有意包含在作品中的贡献，都应按照上述方式双许可，不附加任何额外条款或条件。