path_semantics_std

使用约束函数实现的 Rust 类型检查标准路径语义字典

注意！此库处于早期开发阶段，可能包含错误和缺失功能！

示例：证明偶数加法

// Prove `add[even] <=> eq`, which is equal to
// `even(add(a, b)) = eq(even(a), even(b))`.
let add: Add<u32> = Add::default();
let even: Even<u32> = Even::default();
let path: Eq<bool> = add.path(even);

Rust 类型检查器在调用 .path 时证明存在路径的等价性。
它基于一个称为 "约束函数" 的路径语义理论。
您只需要直接在 Rust 代码中表达定理！

上述示例可以缩短为单行

let path: Eq<bool> = Add::<u32>::default().path(Even::default());

要更改约束，请使用 .i 方法（使用变量名称以提高可读性）

let path: Eq<bool, (Id<bool>, Not)> = add.i((even, odd)).path(even);

这会将 add 函数转换为部分函数，并传播约束，以便您可以在预测函数上看到约束。

.ex_path 方法返回一个输出函数

let res: Not = add.i((even, odd)).path(even).ex_path();

在这种情况下，我们证明了如果你将一个偶数和一个奇数相加，你不会得到一个偶数！

什么是路径语义？

这里提供了一个简要介绍，因为大多数人不知道这是什么。
有关路径语义的更多信息，请点击这里。

路径语义是尝试使数学中的深层次思想更加易于理解，并使定理证明对程序员来说更容易理解。它是 依赖类型 和 受保护的命令语言 的扩展和统一，这些语言今天用于推理和验证软件。与现有工作的主要区别在于，路径语义非常高级（更具有表现力），允许由函数定义的任意约束和属性。这使得路径语义在一般情况下是不可判定的，但它有一些规则，允许对特定问题进行一致性检查，以及在将理论扩展到新领域时使用的严格函数身份概念。

路径语义的语法和符号设计得简洁且易于适应源代码。

• f{g} 表示 "用 g : A -> bool 约束 f : A -> B"。
• ∀f 表示 "获取 f 的输入约束"。
• 存在性路径：∃f : B -> bool表示“f : A -> B输出什么？这取决于约束条件。”
• 路径：f[g] <=> h表示“g : A -> B是f : A -> A的属性，由h : B -> B预测。”
• 组合：g . f输出∃g{∃f}。
• 子类型：x : [g] a，其中g : X -> A，如果a : [∃g] true，则是一致的。
• 函数命名：false_1, not, id, true_1: bool -> bool（id是泛型A -> A）。
• 全射或非全射：所有“正常”函数都有∃∃f => {id, true_1}。
• 证明的化简：a : [f] b ∧ [g] c等于a : [f{[g] c}] b或a : [g{[f] b}] c。
• 转换为等式：f[g] <=> h给出g(f(a, b)) = h(g(a), g(b))（例子是二进制函数）。
• 将约束传播到路径：用于在类型检查出错时发出抱怨。
• 概率存在性路径：类似于存在性路径，但用于概率理论。
• 概率路径：从输入属性以概率预测输出属性的一种方法。

路径语义理论揭示，函数在被称为“路径语义空间”的自然发生空间中相互关联，该空间精确地定义了所有函数的同一性。由于空间的组织方式与预测概念密切相关，因此这项研究与人工智能和机器学习有着大量的交叉。路径语义是一个研究领域，它研究如何组织这个空间以及用于提取和应用与完美和概率预测相关的知识的更高阶算法。这不仅仅是为了找到解决单个问题的方案，而是为了研究和理解高阶推理以解决大量问题。

功能

本库中的所有对象都是约束函数的高阶表示。这意味着它们不是“计算”，而仅仅是构建彼此的类型，以Rust可以类型检查的方式。

• Constrain 特性（类型 .i(<constrain>)，.i_force 跳过存在性路径检查）
• ExPath 特性（类型 .ex_path()）
• Path 特性（类型 .path()，.path_force 跳过存在性路径检查）
• 完整的布尔代数（所有路径都检查了所有约束）
• 一些关于自然数的工作

一个问题是由于函数空间复杂性的原因而产生的组合爆炸。为了解决这个问题，应用了一些技巧来减少构建块的数量，例如使用 If 和 IfK 来处理许多非平凡函数。

• If 有一个条件，该条件依赖于分支中依赖的参数
• IfK 有一个条件，它在更高阶时决定，因此不依赖于分支

使用 () 类型而不是 True1 是因为这在Rust中看起来更美观。

未来目标

短期内，这个库仅用于研究，但如果它被证明对定理证明很有用，目标是开发足够的功能，使其能够作为一个核心，并形成一个特定领域理论的生态系统。

• Rust的无符号整数类型（u8，u16，u32，u64）用于一元和二元运算符
• Rust的有符号整数类型（i8，i16，i32，i64）用于一元和二元运算符
• Rust的浮点类型
• 向量
• 复数
• 矩阵