值得注意的是，在导致类型理论兴起的历史进程中，悖论经常出现。解决罗素的悖论导致了他的类型理论。哥德尔的不完全性定理的证明依赖于说谎者悖论的一个变体。丘奇和图灵用他们独特的形式主义概括了这一结果。直觉主义类型理论就是为了避免这些悖论而设计的。事实就是如此。
作为一名本科生，作为谓词逻辑课程的一部分，我有幸学习了哥德尔的“独一无二的证明”。后来，读了道格拉斯·霍夫斯塔特(Douglas Hofstadter)那本令人愉快的书“哥德尔，埃舍尔，巴赫：永恒的金色辫子”(Gödel，Eschel，Bach：An Eternal Golden Braid)，我的乐趣翻了一番，这本书创造性地反思了与哥德尔的结果相关的主题。所有这一切让我想知道(就像很多人一样)，哥德尔为我们精心铺设的陷阱有没有潜在的模式？更多。
我最初的感觉是，两个条件的存在会让我们面临危险。第一个是递归，即事物直接或间接引用自己的能力。第二种是在递归的情况下的“自我否定”：当遵循递归的路径与早先确立的真理相矛盾时，当两者都被允许时，通往悖论的大门似乎就会打开。
在最近的一次闪电顿悟中，我开始了解到有问题的模式比这更基本、更普遍。它不仅仅是一个理论障碍，它是我们必须经常跨越许多有趣的编程领域的无处不在的挑战。我们不仅经常遇到它，我们也经常克服它，而且不必放弃递归就能做到这一点！最棒的是，我们如何克服这些“悖论”是有模式的。
本文首先使用算术函数演示这些模式，然后说明如何将相同的原则应用于内存管理和死锁。最后一节展示了这些原则如何在帮助我们发展理论工具的能力方面发挥了宝贵的作用。
图灵版本的哥德尔悖论被称为暂停问题：我们能否确定任何给定的程序是否会在某个时刻结束运行，或者它会永远运行吗？图灵证明，没有一种通用算法可以在所有可能的程序中回答这个问题。
一旦我们从终止的角度重新定义了挑战的框架，显然任何没有循环或递归的程序都将终止，因为程序由有限数量的操作组成，这些操作都是按照顺序1精确执行一次的：
使用循环或递归，我们可以创建不会终止(至少对于某些值)的程序：
将0传递给此函数，它会立即停止。然而，任何其他值都会导致它永远运行，在1和2之间翻转。这就像仓鼠爬上一个永不停止的轮子，永远不停地转。
fn阶乘(N U64)：如果n<；1：返回1，否则：返回n*阶乘(n-1)。
这就是我们想要的！递归函数(或循环)，这些函数(或循环)要求在某个点停止，遍历循环有限次。需要向递归周期添加什么额外质量才能保证终止？
正如阶乘所展示的那样，一个有效的策略包括削弱周期，这样它们就可以保证在某个时候“打破”。阶乘是如何做到这一点的？循环的“出口”是基于一个数字(“n”)，这个数字总是从它的起始点开始在算术上变小，直到它不可避免地达到其最小可能的终止值(0)。可视化这种终止递归的一个有用的方法是使用一条螺旋线，它的直线必须在中心终止，不可阻挡。
在展示这种弱化循环模式对其他问题的实用性之前，我想要说明的是，终止分析比在保证终止和保证不终止之间的二元选择要复杂得多(也很有趣)。这个例子说明了这两个极端之间的一些不确定性：
fn f(N Bignum)：While n>；1：if n%2==0：n=n/2否则：n=3*n+1。
到目前为止，对于每个尝试过的数字，这个函数都会终止。然而，没有人证明对每个n值都会终止。这个挑战，Collatz猜想，有它自己迷人的历史，包括与约翰·康威的Fractran和Minsky机器的有趣联系。值得注意的是，尽管Conway从未证明Collatz猜想，但他确实证明了它的广义版本是不可判定的。
与欧几里德的第五个假设一样，寻找完美的自动内存管理策略的圣杯导致了如此多的人走向不光彩的毁灭。Rust的静态单一所有者策略看起来很有吸引力，但它严重限制了我们可以构建的数据结构。在不适当的环境中使用Arena可能会泄露到不可接受的程度。
当程序需要多个引用来指向同一对象，而我们不能静态地确定哪个别名将最后到期时，我们需要一种内存管理策略，该策略可以在运行时确定这一点，以便可以安全地回收分配的内存。因此，为了满足我们对大型、瞬态、复杂、共享的“所有权”数据结构的需求，我们被迫基于引用计数、跟踪或两者兼而有之地实现运行时垃圾回收的某种变体。
那么所有这些与循环弱化有什么关系呢？非常简单：当您允许对同一对象的多次引用时，引用循环成为可能，其中一个对象引用另一个对象，而另一个对象引用另一个对象，最终通过某些引用返回到原始对象。众所周知，在存在这样的引用循环时，引用计数很困难。这样的循环有效地使周期中的每个对象永远处于活动状态。所以内存泄露了。
对泄漏周期的有效解决方案包括从字面上削弱每个周期。当您确保每个引用周期至少包含一个“弱”引用时，完全避免了内存泄漏。与常规引用不同，弱引用没有能力使它所指向的对象保持活动状态，这种弱化足以打破任何循环，并最终被丢弃。
跟踪垃圾收集器使用一种不同的策略来削弱引用周期：颜色标记。收集器从引用的根集合开始，跟踪所有需要保持活动状态的对象的所有引用的路径。当引用是循环的时，这会带来终止挑战，因为愚蠢的收集器将永远追逐这些引用。智能收集器在跟踪时丢弃面包屑，在遍历每个引用时对其着色。引用从白色开始，当我们知道它需要跟踪时变为灰色，然后在跟踪时变为黑色。当收集器遇到有色引用时，不需要再次跟踪它。可变颜色参考的能力削弱了循环，从而保证了终止。
死锁是程序设计的另一个难以解决的问题，当我们有多个独立的线程需要共享、可变的访问相同的资源时，我们需要同步对这些资源的访问以避免数据竞争。通常，这涉及到锁的使用。线程等待，直到它可以获得排他锁，读取或改变资源，然后尽快释放锁。
当只有一个资源在争用时，这很简单。但是，当线程需要同时获取多个资源上的锁时，我们可能会遇到实际问题。如果线程A获取资源X的锁，然后试图获取资源Y的锁，但资源Y已被线程B锁定，而线程B随后想要获取资源X，该怎么办呢？两个线程都将永远等待对方释放它们需要的资源！这是一个简单的死锁示例。
我们创造的是一个资源依赖循环，除非我们以某种方式削弱这个循环，否则这个循环永远不会结束。1965年，埃茨格·迪克斯特拉(Edsger Dijkstra)用“就餐哲学家”(Dining Philosopers)制定了这个挑战的一个版本。每个哲学家都需要吃他们的碗意大利面，但只能把放在碗两边的两个叉子都洗干净。问题是每个叉子都是和桌子周围的相邻哲学家分享的。他们是如何在不挨饿的情况下无言以对地安排这件事的呢？
Dijkstra的解决方案在分叉(争用的资源)上强加了偏序层次结构。每个分叉都是有编号的，每个哲学家只会先获得编号较低的分叉，然后是编号较高的分叉，通过对争用的资源强制执行获取顺序，我们有效地削弱了依赖的循环，从而确保没有哲学家会无休止地等待其他同样等待的哲学家已经获得的所需分叉。
值得指出的是，即使在没有锁的情况下也可能发生死锁。这一点很重要，因为不使用锁的编程语言，例如Pony，仍然会经历死锁。通过使用通过向彼此发送消息来同步的不同角色来仔细地建模每个就餐哲学家和叉子，可以清楚地看到，在某个时刻，哲学家角色只是默默地等待永远不会到达的消息。这种等待和从不前进的状态与对锁定资源的争用一样是死锁。因此，通过使用相互发送消息来同步的不同角色来对每个就餐的哲学家和叉子进行仔细的建模，可以清楚地看到，哲学家角色只是默默地等待着永远不会到来的消息。这种等待和从不前进的状态与对锁定资源的争用一样是死锁。
有了这个背景，我们现在可以在理论家们用来解决遇到的悖论的周期弱化解决方案中看到一个明确的模式2：
罗素阐述了他的悖论(如果R是不是其自身成员的所有集合的集合，则R既不能是它自己的成员，也不能不是它自己的成员)。他的分枝类型理论弱化了集合之间允许的关系。本质上，这种类型理论建立了实体上的偏序。某种类型的实体只能由较低类型的实体建立起来，这很像阶乘和餐饮哲学家问题的解决方案。罗素的可约性公理过于严格，例如。
阿隆佐·丘奇(Alonzo Church)发明了简单类型的λ演算来解决Kleene-Rosser悖论，该悖论表明，某些形式逻辑系统，包括使用丘奇的非类型λ演算的形式化，是不一致的。这也适用于Lambda演算中受罗素启发的类型循环的层次结构。
由Brouwer、Heyting、Kolmogorov和Martin-Löf提出的直觉主义类型理论是为了小心避免悖论结构而设计的。这里有两个例子。通过拒绝排除中间法则，直觉主义逻辑避免了必须表示既不真也不假的悖论，相反，它使用1类型来表示我们可以证明存在的东西，而使用0类型来表示任何不存在的东西，包括任何无法证明的东西(例如，悖论)。
另一个例子是它使用归纳类型，允许将自然数定义为偏序。每个数字都是前一个数字的后继，从0开始。归纳类型可以是自引用的，但通常只能以允许结构递归的方式进行，这会削弱递归(循环)以避免悖论。
成功地处理递归是如此重要，以至于数学和逻辑区分了预言性和非预言性。非预言性的定义是自引用。谓语定义不是，直觉主义理论是设计成谓语的。
在我的最后一个示例中，让我们讨论一下标准ML的模块。模块是嫁接到核心ML语言上的一种单独的语言，能够以一种优雅、隔离的方式丰富模块结构，从而支持提高代码的可重用性。尽管如此，人们仍然在寻找改进SML模块的方法，例如启用对Haskell类型类提供的那种特殊多态性的支持。
Andreas Rossberg提出了一种新的语言，1ML。他的目标是将ML的模块和核心语言集成到一种语言中，并使模块成为一流的，这样它们就可以像值一样传递。这意味着函数、函数器和类型构造器之间没有区别，结构、记录和元组之间也没有区别。本文观察到，核心语言和模块语言之间的句法差异只是增强模块类型预测性的一种粗略方式。1ML取代了循环的这种句法弱化。1ML施加了这样的约束：“在子类型化(也称为签名匹配)过程中，类型类型只能由小的[单态]类型匹配，这些类型本身并不包含类型类型。”
这听起来完全像是削弱循环，以便类型推理变得可判定，同时还确保更强大的模块和类型系统。
就像钻石切割一样，技巧不在于知道它需要被削弱，而在于知道在哪里敲击切割刀以使其价值最大化。
因此，下次你遇到图灵开始另一场没完没了的马拉松比赛时，给他一辆车轮已经巧妙地减弱了的自行车，通过应用有限偏序，以确保他会及时停下来喝茶。
1你不会认为我会写一篇帖子而不引用Cone吧，是吗？
2令我高兴的是，@user自那以后分享了一个关于对角论证的nlab链接。它引用了Lawvere的证明，使用范畴论，这些历史例子(和Cantor的对角定理)是深度等价的。亚诺夫斯基对Lawvere的对应关系提供了更容易理解的解释。如果有人正式证明记忆引用周期和死锁挑战也是这种深度等价的开端，那不是很令人兴奋吗？