Poi

一个实用的无点定理证明助手

标准库

=== Poi 0.24 ===
Type `help` for more information.
> and[not]
and[not]
or
∵ and[not] => or
<=>  (not · and) · (not · fst, not · snd)
     ∵ (not · and) · (not · fst, not · snd) <=> or
<=>  not · nor
     ∵ not · nor <=> or
∴ or

Poi使用数学知识库来自动进行定理证明，同时也向您展示替代方案。

• ∵ 表示 "因为"
• ∴ 表示 "因此"
• <=> 一个替代方案

要从您的终端运行Poi Reduce，请输入

cargo install --example poi poi

然后，要运行

poi

您可以使用 help 来了解Poi中的命令及其背后的理论。

下载并试用！ (将其视为一种通过实践学习的工具)

另外，查看路径语义的常见问题解答

• 总体问题是什么？
• 为什么是正常路径？

示例：连接列表的长度

Poi允许您指定一个目标并自动证明它。

例如，当计算两个连接列表的长度时，有一种更快的方法，就是计算每个列表的长度并将它们相加

> goal len(a)+len(b)
new goal: (len(a) + len(b))
> len(a++b)
len((a ++ b))
depth: 1 <=>  (len · concat)(a)(b)
     ∵ (f · g)(a)(b) <=> f(g(a)(b))
.
(len · concat)(a)(b)
(concat[len] · (len · fst, len · snd))(a)(b)
∵ len · concat => concat[len] · (len · fst, len · snd)
(add · (len · fst, len · snd))(a)(b)
∵ concat[len] => add
depth: 0 <=>  ((len · fst)(a)(b) + (len · snd)(a)(b))
     ∵ (f · (g0, g1))(a)(b) <=> f(g0(a)(b))(g1(a)(b))
((len · fst)(a)(b) + (len · snd)(a)(b))
(len(a) + (len · snd)(a)(b))
∵ (f · fst)(a)(_) => f(a)
(len(a) + len(b))
∵ (f · snd)(_)(a) => f(a)
∴ (len(a) + len(b))
Q.E.D.

concat[len] 的表示法是一个 "正常路径"，它允许您将其转换为更有效的程序。正常路径是可组合的，并且是无点的，与它们的等式表示不同。

示例：Levenshtein证明搜索

对于深度自动定理证明，Poi使用Levenshtein距离启发式。这简单地说就是文本表示中的最小单字符编辑距离。

尝试以下操作

> goal a + b + c + d
> d + c + b + a
> auto lev

命令 auto lev 告诉Poi在所有子证明中自动选择具有最小Levenshtein距离的等价表达式。

Poi和路径语义简介

在 "无点" 或 "沉默" 编程中，函数不标识它们操作的参数（或 "点"）。参见 维基百科文章。

Poi是路径语义的小子集的实现。为了解释Poi是如何工作的，需要简要介绍路径语义。

路径语义是一种用于数学编程的高度表达性语言，它除了常规计算外，还具有“路径空间”。如果常规编程是二维的，那么路径语义就是三维的。路径语义通常与范畴论、逻辑等结合使用。

“路径”（或“常规路径”）是导航函数间的一种方式，例如

and[not] <=> or

用文字翻译这句话意味着

If you flip the input and output bits of an `and` function,
then you can predict the output directly from the input bits
using the function `or`.

在常规编程中，无法直接表达这种想法，但可以将逻辑关系表示为方程

not(and(a, b)) = or(not(a), not(b))

这被称为德摩根定律之一。

以交换图的形式表示时，可以直观地看到维度

         not x not
      o ---------> o           o -------> path-space
      |            |           |  x
  and |            | or        |     x
      V            V           |   x
      o ---------> o           V        x - Sets are points
           not            computation

计算和路径类似于复数，其中“实部”是计算，“虚部”是路径。

这以非对称路径表示法书写

and[not x not -> not] <=> or

在对称路径表示法中

and[not] <=> or

计算和路径空间都是方向性的，这意味着不一定总能找到逆元素。路径空间中的组合仅仅是函数组合

f[g][h] <=> f[h . g]

如果想象computation = 2D，那么computation + path-space = 3D。

路径语义可以被视为方程的“无点风格”子集。这个方程子集在编程中特别有用。

Poi的设计

Poi被设计成用作Rust库。

这意味着任何人都可以在Poi之上创建自己的工具，而不需要很多依赖项。

Poi主要使用重写规则进行定理证明。这意味着其核心设计是“愚蠢”的，当给定错误的规则时，可能会执行无限循环等愚蠢的操作。

然而，这种设计也使Poi非常灵活，因为它可以在任何方向上进行模式匹配，独立于计算方向。在Rust代码中定义此类规则相对容易。

语法

Poi使用Piston-Meta来描述其语法。Piston-Meta是一种用于人类可读文本文档的元解析语言。它使得轻松更改Poi的语法成为可能，并保持向后兼容。

由于Piston-Meta可以描述自己的语法规则，这意味着Piston-Meta的未来版本可以解析旧版本Poi的语法。然后可以使用合成将旧文档转换为Poi的新版本。

核心设计

Poi的核心是Expr结构

/// Function expression.
#[derive(Clone, PartialEq, Debug)]
pub enum Expr {
    /// A symbol that is used together with symbolic knowledge.
    Sym(Symbol),
    /// Some function that returns a value, ignoring the argument.
    ///
    /// This can also be used to store values, since zero arguments is a value.
    Ret(Value),
    /// A binary operation on functions.
    EOp(Op, Box<Expr>, Box<Expr>),
    /// A tuple for more than one argument.
    Tup(Vec<Expr>),
    /// A list.
    List(Vec<Expr>),
}

Expr结构的简洁性很重要，并且高度依赖于高级路径语义知识。

一个符号包含每个领域特定符号和符号的泛化。

Ret变体来自高阶运算符重载中使用的表示法。它不是将值描述为值，而是将其视为某种未知输入类型的函数，该函数返回一个已知值。例如，如果一个函数对所有输入都返回2，则可以写成\2。这意味着函数上的无点变换有时可以计算一些内容，而不需要直接引用具体值。更多信息请参阅论文高阶运算符重载和存在路径方程。

/// Represents knowledge about symbols.
pub enum Knowledge {
    /// A symbol has some definition.
    Def(Symbol, Expr),
    /// A reduction from a more complex expression into another by normalization.
    Red(Expr, Expr),
    /// Two expressions that are equivalent but neither normalizes the other.
    Eqv(Expr, Expr),
    /// Two expressions that are equivalent but evaluates from left to right.
    EqvEval(Expr, Expr),
}