Lib.rs

LSTS 是一个证明辅助工具，可能也是一个编程语言。

LSTS 中的证明是通过连接项、类型定义和量化语句构建的。项可以被评估以获得值。类型描述项的性质。语句描述项和类型之间的关系。

项

项是带有一些扩展的 Lambda 演算表达式。

1;
"abc";
2 + 3;
"[" + (for x in range(1,25) yield x^3).join(",") + "]";

类型

类型定义定义了随后附加到项上的逻辑语句。所有有效的项至少有一个类型。某些项可能具有多个类型。类型可以定义不变性质。这些不变性质对该类型可能包含的值的先决条件和后置条件施加限制。进入类型的值必须满足该类型的先决条件。来自项的输出值随后将被认为是满足每个类型的不变性质的。

复数类型通过使用逻辑合取类型实现，类似于求和或积。类型可以被放入合取或投影出来。子类型关系随后用于确定一个合取是否意味着另一个合取。没有逻辑 OR，只有 AND（除非你计算箭头），并且预期类型被归一化到合取范式。

type Even: Integer
     where self % 2 | 0;
type Odd: Integer
     where self % 2 | 1;

语句

语句通过形成结论来连接逻辑。每个语句都有一个项部分和一个类型部分。一个语句可以可选地有一个标签，以便以后可以直接引用。当应用语句时，它为项的类型提供新信息。当应用一个语句时，它必须匹配其应用上下文的模式。一个应用上下文由一个项和一个类型组成，然后将其与语句的项和类型进行比较。这些项 x 类型关系是 LSTS 严格推理的基础。

forall @inc_odd x: Odd. Even = x + 1;
forall @dec_odd x: Odd. Even = x - 1;
forall @inc_even x: Even. Odd = x + 1;
forall @dec_even x: Even. Odd = x - 1;

((8: Even) + 1) @inc_even : Odd

λ☶ 与 LSTS 有何不同

λ☶ 是临时单态的。LSTS 是临时多态的。

#λ☶ programs try to apply the first function candidate,
#    followed by the next, in descending order
f := λ(A a). a
f := λ(B b). b
(: (f x) A)
(: (f y) B)

//LSTS programs try to apply all function candidates,
//     at the same time, immediately
let f(a: A): A = a;
let f(b: B): B = b;
f(x) : A + B

教程

有关更多信息，请参阅教程和参考文档。

• 西班牙语