铁锈中1和1=2的证明

2020-10-13 20:07:39

1+1等于2这一事实非常明显,可能很难解释为什么。幸运的是,数学家们已经设计出了一种将算术形式化并随后证明1+1=2的方法。自然数是基于皮亚诺公理的。它们是一组简单的规则,定义(与正式系统一起)什么是自然数。因此,为了证明Rust中的1+1=2,我们首先需要一个能够处理逻辑的形式系统。我们将使用的正式系统不是某个随机的板条箱,而是铁锈的类型系统本身!我们将不会有任何运行时代码,相反,类型检查器将为我们完成所有工作。

首先,让我们来看看皮亚诺公理。第一个公理是零是一个自然数。基本上它说的是零的存在。为了在类型系统中表达这一点,我们只需编写:

第六和第七公理指出,每个自然数都有唯一的后继者。此后续函数在数学上写为S(N),并且(根据加法的定义)S(N)=n+1。这些公理可以用如下所示的泛型类型编写:

类型一=后续<;零;类型二=后续<;一&>;类型三=后续<;两&>;类型四=后续<;三&>;类型五=后续<;四&>;;

这个定义也满足第八条公理,即不存在小于零的自然数。第二条、第三条、第四条和第五条公理都定义了等式是如何工作的。我们不必将它们转换成Rust,因为Rust已经有了一个类型之间相等的系统。

第九条公理有点棘手。它说你可以用归纳法来证明关于自然数的东西。然而,对于这样简单的证明,没有必要用铁锈来表示它。

结果关联类型只是加法的值。接下来,我们将实现AddHelper的添加特征:

第一个Iml简单地说明a+0=a。对于非零加法,我们写道:

实施<;A,B&>;为AddHelper<;A,继任者<;添加:其中AddHelper<;A,B&>;:添加{type Result=继任者<;<;AddHelper<;A,B&>;As Add&>;::Result&>;}。

它可能有点难读,但是这个特性是在AddHelper<;A、继承者<;B>;>;中实现的。所以它计算a+(b+1)的结果。如果我们随后查看结果,它的类型是后续<;<;AddHelper<;A,B&>;As Add>;::Result&>;。换句话说,它是S(a+b)+1,所以这个Iml实际上是说a+(b+1)=(a+b)+1,或者如果你想用S(X)来表示后继者,a+S(B)=S(a+b)。

这个递归定义起作用的原因是它本质上减少了右侧,直到它减少到微不足道的a+0情况。例如3+2=3+S(S(0))=S(3+S(0))=S(S(3+0))=S(S(3))=5。

现在我们可以证明1+1=2。要证明两种类型相等,我们可以使用如下Const声明:

在这里,我们使用一个选项来包装类型,因为使用选项不需要创建包装类型的实例,但是类型检查器仍然检查类型是否相等。

左边的类型是<;AddHelper<;one,one>;as add>;::result,换句话说就是1+1。右边有两个。换句话说,1+1=2。

如果我们将两个更改为三个,则会得到预期的错误。如果我们尝试2+2=5,我们也会得到一个错误。

为MulHelper<;A、继任者<;B&>;>;实施<;A,B&>;MUL,其中AddHelper<;A,<;MulHelper<;A,<;MulHelper<;AS MUL<;::Result&>;:Add{type Result=<;AddHelper<;A,<;MulHelper<;AS MUL&>;::Result&>;AS Add>;::Result;}

这里实现了MulHelper<;A,继承者<;B&>t;>;的乘法,它只表示a*S(B)。结果的类型可能比较难读,但它等同于a+a*b。换言之,a*(b+1)=a+a*b。

问题是,这实际上并不起作用,相反,它在计算特征界限时会导致某种无限递归。我可以花几个小时来试图理解Rust是如何计算性状界限并解决这个问题的,但是我会选择懒惰的方式,以一种Rust更容易理解的形式重写乘法。

在数学上,这表示acc+a*b。然后,我们递归定义乘法,如下所示:

特性MUL{type Result;}//S(ACC)+A*B=S(ACC+A*B)对于MulImplHelper<;继任者<;继任者<;,A,B&>;实施<;MUL;其中MulImplHelper<;ACC,A,B&>;::MUL{type Result=继任者<;<;MulImplHelper<;ACC,A,B>;AS MUL&>;::Result&>;}//0+A*S(B)=A+A*B实施<;A,B>;MUL对于MulImplHelper<;零,A,后续<;B>;;其中,MulImplHelper<;A,A,B>;:MUL{type result=<;MulImplHelper<;A,A,B>;As Mul>;::Result;}//0+A*0=0 Iml<;A>;Mull for ImplHelper<;零,A,B>;MUL{type Result=<;MulImplHelper<;A,A,B>;As Mul>;::Result;}//0+A*0=0 Iml<;A>;Mull for ImplHelper<;A,A,B>;{type result=Zero;}struct MulHelper<;A,B&>;(A,B);//A*B=0+A*B Impl<;A,B&>;MUL表示MulHelper<;A,B&>;其中MulplImplHelper<;零,A,B&>;:MUL{type Result=<;MulImplHelper<;零,A,B>;AS MUL&>;::Result;}。

我不确定为什么这个定义比前面的定义工作得更好,但我猜这与这里的递归类型简单得多有关。

//单独定义清晰度类型ThreeSquared=<;MulHelper<;Three,Three>;As MUL>;::result;type FourSquared=<;MulHelper<;Four,Four>;As MUL>;::result;键入FiveSquared=<;MulHelper<;FiveSquared=<;FiveSquared<;::Result;Const QED:Option<;<;AddHelper<;ThreeSquared,FourSquared>;As Add>;::Result>;Option:<;FiveSquared>;As MUL>;::Result>;As Add>;::Result>;=Option:<;FiveSquared>;As Add>;::Result>;=Option:<;FiveSquared>;*无;

Rust的类型系统是图灵完成的,所以理论上你可以在其中实现任何正式的系统,然后使用它。使用香草类型的系统,它可以建设性地证明存在论断。也应该有可能用矛盾的证据来证明某些东西是不存在的。矛盾证明之所以是可能的,是因为当使用泛型实现特征时,您实质上是在说假设X(泛型参数满足某些特征),那么Y(类型满足您正在实现的特征)。如果Y是逻辑矛盾,那么X一定也是,因此X不可能存在。