IDNI Blog

  • Tau和真相危机

    Ohad Asor 发表于2016年9月11日凌晨2:25

    我们生活在一个没有人知道法律的世界里。除了个别案件,你不可能知道什么是合法的,什么是非法的。你所能做的就是试着看看法官或警察在你采取行动后的意见,当然他们彼此之间意见也经常不一致。或者你可以咨询律师,他会告诉你没有绝对的答案,其实这只是一个概率问题,不幸的是没有人知道如何计算这个概率。你可以尽自己最大的努力去过一个有作为的生活,按照你所理解的规则或律师指导去遵守规则,但是没有人能保证你不会被认为是罪犯,或者法律行动不会对你不利。同样,一个人可以过着伤害众人的生活,即使系统意识到这一点,也没有任何法律体系会阻止他。这种悲观的情况并非鲜见,也并非只发生在个别地方。据我所知,Franz Kafka对这种情况进行了最好的描述。

    自人类学会了说话,就开始有意识或无意识地玩弄文字,并将其引导到任何想要的方向,无论有意或无意。最坏的谎言只包含真理,最坏的犯罪行径也往往是有许可证的,并且语言可以为几乎任何事情辩护。这种“真理危机”是后现代哲学的基础,特别是解构主义的方法,它展示了如何用许多矛盾的方式来解释文本。 “没有真理”是后现代主义的基础。但是,我们能否找到一座真理孤岛,其上社会契约是有用的和有意义的?

    不仅法律不能以绝对的方式被理解,而且甚至不能简单地由绝对的过程来实现。法律必须随着时间的推移而改变,因此我们也需要法律来改变法律,即,我们需要的改变法律的法律的法律……,无限循环。但是,我们仍然没有任何逻辑基础来制定规则,而不仅仅是决定什么是合法的,什么是非法的。这一悖论在Peter Suber的在线书《The Paradox of Self Amendment》的附录中得到了描述。他提供了一个两层系统,其中有可变的和不可变的规则,同时包括转换规则的规则(即,使不可变规则变易或反之亦然)。通过这种方式,我们可以避免法律修改方案的无限循环,但我们仍然停留在“真相危机”中。在这个危机中,没有真理,尤其是当你迫切需要它的时候,尽管法律的目的是要有特定的社会秩序,而不是虚假信息和混沌。

    当从法律的世界中走出来,试图在数字和数学对象的世界里回答类似的问题时,这个任务本身并没变得容易,但更容易论证了。逻辑学家对这些问题已经思考了几个世纪了,并提出了可判定性这个概念。如果该语言的每一个可表达的语句都可以被判定是否遵循了该语言中表达的规则,则称这种语言是可判定的。一个惊人的例子是Godel的定理:如果我们的语言能够表达Peano算法,也就是它包含了自然数1 2 3,……,配备了加法和乘法以及它们的规则(这确实决定了它们的独特之处),那么就会有一些关于Peano算法的真实陈述,无法从其定义中得到证明。因此,为了能够判定每个语句的正确性,将需要无限多个公理。可判定性的另一个例子是Presburger算法:如果我们放弃乘法,只用加法定义数字(以某种方式),我们就可以回到可判定性,每一个可表达的语句都可以在有限的过程中判定为真或假。同样的道理也适用于2000年前欧几里得几何学这一可判定的理论。因此,我们有兴趣创造一个社会过程,在这个过程中,我们只用可判定的语言来表达法律,并在不陷入悖论的情况下,共同形成可修改的社会契约。这就是Tau-Chain的初心。

    上述长篇大论强调了在一般的生活中,特别是在Tau中,可判定性的重要性和中心作用。如果我们希望Tau能够为世界做出真正的贡献,它就必须使用一种可判定的语言。旧Tau的设计旨在满足这些要求,但最近我发现我错了,最初选择的语言是非法判定性的。Martin-Lof Type Theory (MLTT) 只在个别方面有可判定性(比如,相等问题),而非对所有方面的表达都是可判定。这种情况使我得出结论,MLTT是一个错误的选择,应该考虑另一个逻辑。事实上,我在博客文章和视频上的一些声明是错误的,而MLTT整体上没有可判定性的类型检查。MLTT是关于所谓的“非独立类型”,我将试着在这一段中稍微解释一下。我们提到了“措辞”和“类型”。措辞可视为陈述而类型视为满足这些陈述条件的规范。这些规范有多普遍?非独立类型在某种意义上给了它们最大的表达能力:类型可以依赖于措辞,而措辞也可以依赖于类型(这就是“非独立类型”的名称的由来)。我们能够表达我们的措辞语言所能够表达的任何规范,或者更准确地说,类型可以由一个计算程序来表示。程序可能包括规范,而规范也可能包括程序。类型检查是确保措辞确实符合它们的类型的过程。但是如果类型可以是通用程序,我们必须要求它们在有限的时间内执行完毕并返回结果。只有当你能够断言你的类型是可以在有限的过程中计算的,那么类型检查的过程才变得可判定。但是这个任务本身是不可判定的,因为停止的问题是不可判定的。因此,如果你想要在非独立类型上达到可判性,你首先必须越过这个不可判定障碍。这在许多情况下是可能的,因为许多程序可以以可证明终止的形式编写(如原始递归,它是整个函数式编程的基础)。但是,这样的方法是不可能适用于所有的程序的,否则,停止的问题就会成为可判定的。非独立型语言在计算机辅助证明和形式验证的领域得到了广泛的应用,但是他们其实是难以处理的。这种困难不仅源于他们的理论比其他语言复杂得多,而且更困难的部分是说服类型检查器(或终止和整体检查器,目的是试图确保类型检查过程是有限的)你的代码符合它的规范。因此,类型检查过程不是自动的,需要大量的人工干预才能说服它接受真实的陈述,这是一种完全来自于语言的不可判定性的困难。随后,我们就失去了始终、完全自动地决定一个句子是否为真的能力,或者同样地,是否 某个动作(措辞)是合法的(输入良好的)或根据给定的规则判定是非法的。

    解决这种情况的办法是选择一种不同的逻辑,一种“完整”的逻辑。一个完整的逻辑意味着一切都是可判定的,而且不仅仅是它的某些方面(比如MLTT中的等式)。Godel研究表明,每一个完整的逻辑,并且能够表达Peano算法,都将不可避免地不一致。所以为了保证一致性和完整性,我们将不得不放弃一部分的算术。不仅已经知的我们可以使用的完整和一致的逻辑,而且最近这些语言的家族被发现比以前所知的更有表现力。具体地说,自20世纪60年代以来,某些类的单值二阶逻辑(MSO或MSOL)被发现是完整和一致的,但是它们没有令人满意的表达能力。直到2006年,Luke Ong才提出了一种“高阶递归方案”的完整证明,即所谓的“高阶递归方案”,它是一种简单类型(相当非独立类型的)高阶函数语言,带有递归,极大地增强了完全可判定语言的表达能力。从那时起,理论和实践都取得了进步,尤其是Naoki Kobayashi。

    这是一个漫长的旅程,直到我发现我的基本前提是错误的,而且当旅程开始的时候,我并不是一个逻辑学家。幸运的是,我们现在可以将Tau的设计修改成比我们之前认为的更好的东西,即使MLTT是可判定的。Tau有三个优点:直接计算模型的存在,推断程序的能力,以及易用性。MSO理论有一个基于自动机的直接的计算模型。 MSO公式可以被翻译成冗余机,该机器读取一个语句并决定它是否满足这个公式。此外,这些自动机可以以一种独特的方式被最小化,因此我们甚至得到了一个可验证的最优代码。另一方面,MLTT不喜欢被直接翻译成自动机,而是使用逻辑自动连接的方式。MLTT认可一个更一般的概念,程序证明,即证明过程被更松散地指定,并且不存在直接转换到自动机的过程。程序证明不可能存在,因为自动机是一个显式的有限决策过程,而非独立类型不是完全可判定的。

    第二个显著的优势是自动编程,在文献中更常见的称为“程序合成”。如果我们给出一个程序(或规则基础)的规范,机器可以自己设计程序(或规则)吗?这个任务在MLTT上是不可判定的,但是在一个完整的逻辑中,这是可能的。我们可以通过简单地陈述我们期望他们做的事情,并命令机器找到一个我们的需求的结构,这样我们就可以得到正确的项目和合约。由于上述原因,MSO逻辑更简单:它是一种更简单的语言,不需要人工干预来说服真实的陈述确实是正确的。MLTT是一种直觉逻辑,这意味着一种被证明为假的陈述并不一定意味着它的反面是正确的。例如,一个人不能总是用矛盾性来证明。直觉逻辑允许用矛盾性来证明不存在:它可以假定某物存在,推导出矛盾,并由此得出结论它不存在。但它不能支持不存在的矛盾性证明:在直觉逻辑下,假设某物不存在,而产生矛盾并不能证明它的存在。更正式的,直觉逻辑明确否定了被排除的中间法则。 这当然是非常不直观的,并且认可人类犯错误的可能性,尤其是面对复杂结构时。另一方面,MSO是一种经典的逻辑,意味着它包括了被排除的中间法则:在同一时间,任何事物都不可能同时是真和假。中间被完全排除在外,而如果我们将这个规则添加到MLTT中,它就失去了一致性。

    作为一个结论,我们的旅程与我们所期望的在实施方面有所不同。但它最终会得到一个更好的产品,它将给我们一个机会来解决真相危机和在全球社会和电子环境中自我修正悖论。我个人意愿(并承诺)保持全职工作,直到我完成了Tau和Agoras,它们将引入比这里描述的更多的特性。最近,我对我承诺要交付的产品做了一个简单的描述。另一篇文章和另一段视频将会解释更多的细节。如果你愿意帮助实现这些目标,如果你会发现自己(或你的朋友)理解Kobayashi的论文,我将非常乐意与你们合作。