可判定性
语言是非图灵完备或可判定意味着什么？
非图灵完备和可判定是你经常会听到的关于 Clarity 安全优势的两个术语，但它们是什么意思？
虽然相关，但它们并不完全可互换，因为存在一些差异。
非图灵完备
如果一个系统或语言不能模拟图灵机（图灵机是一种抽象的计算模型），则称其为非图灵完备。与图灵完备系统相比，非图灵完备系统具有有限的计算能力。图灵完备的系统或语言可以模拟任意图灵机。非图灵完备系统的例子包括有限状态机和一些领域特定语言（例如 Clarity）。
非图灵完备语言通常不能表达所有可能的算法。具体来说，一些需要无界循环或递归才能求解的问题无法用非图灵完备语言表示。这一特性在 Clarity 的上下文中特别重要，因为它使得像无界循环和重入这样的特性在语言层面上被禁止。
可判定
如果存在一种算法可以在有限时间内始终确定给定输入是否具有某个特性，则该问题是可判定的。换句话说，可判定问题可以被一个保证对所有输入实例停机的图灵机解决。可判定性是问题的属性，而图灵完备性是语言或计算系统的属性。
Clarity 是可判定的这一事实意味着开发者（和工具）可以更容易地推理并确定性地预测 Clarity 合约的行为，而不必担心输入的不同。
智能合约开发者的思维方式
在深入具体内容之前，先设定我们作为希望编写安全代码的智能合约开发者应持有的上下文和观点。
当你进一步探索 Solidity 和 Clarity 的安全特性时，你会看到总有一些缓解措施可以 被 开发者采取以帮助解决其中的一些安全问题。
这种思路的主要问题在于它增加了智能合约安全中人为错误的概率。如果我们能够在尽可能保留功能性的同时尽量降低人为错误的可能性，我们就应该这样做。
智能合约应该是图灵完备的吗？
我们会发现智能合约的新应用。这些应用将超越当前的智能合约、传统合同，甚至可能开启新的经济机会。鉴于这些可能性，我们应该如何构建智能合约？我们的智能合约语言应具备哪些特性？
把数据与程序分离是一种良好实践。智能合约应该是数据、程序，还是介于两者之间的东西？如果智能合约是数据，那么执行它们的程序应该是图灵完备还是较弱的？如果智能合约是程序，那么应该使用哪种语言编写？这种编程语言应具有什么特性？
丘奇—图灵论题是假说，认为所有形式化的计算概念都被图灵机或现代计算机所捕捉。若一种编程语言捕捉了所有形式化的计算概念，则称该语言为图灵完备。许多编程语言是图灵完备的。例如，Python、C++、Rust、Java、Lisp 和 Solidity 都是图灵完备的。
考虑一个程序及其输入。在最坏情况下，确定该程序的输出是不可能的。对特定输入验证一个程序是通过生成正确性证明来完成的。
正确性证明是可以机械验证的逻辑证明。为程序及其输入找到正确性证明是不可判定的。库尔特·哥德尔证明了存在不可判定的逻辑命题。
这表明在最坏情况下，图灵完备语言中的所有程序都无法被验证。因此，图灵完备的智能合约语言必须允许存在无法验证的合约。
阿隆佐·丘奇和艾伦·图灵证明了存在不可计算的问题。不可计算的问题无法被任何图灵机解决。因此，假设丘奇—图灵论题成立，这些不可计算的问题也不能被任何计算机解决。
我们将在本节稍后进一步探讨这个想法。
图灵完备语言的表达能力非常强。事实上，假设丘奇—图灵论题成立，从某种意义上说图灵完备语言的表达能力已达极限。
是否存在权衡？对于不可计算的问题和其有效性可能不可判定的程序，会发生哪些类型的问题？
随着智能合约涵盖合同法的部分内容，考虑税法的大量法律法规。
例如，美国的税法和法规占据了几百万字。国际税法和法规则使这些数字更高。
这些法律法规是程序还是数据？如果税法用图灵完备语言来书写，那么法律可能会将不可计算的问题编入条文。对于会计师来说，他们的建议不可判定将是噩梦般的情形。
Clarity 是非图灵完备的，但表达能力很强。这使得 Clarity 可判定且不能编码不可计算的问题。关于像 Solidity 这样的智能合约语言，有一些讨论和论文提出了 Solidity 的子集，使其成为非图灵完备的。这些子集是可判定的，不能编码不可计算的问题。然而，对于应采用哪些子集尚无共识，且这些子集并未被广泛使用。
可判定性在智能合约中的优势
为什么在智能合约的背景下可判定性很重要？
首先，在一次调用过程中 Clarity 不可能在中途耗尽 gas。由于其可判定性，可以对调用图进行完整的静态分析，从而在执行前获得准确的成本预估。
Solidity 允许无界循环、递归和动态函数调用，这使得在事前准确预测执行成本或 gas 消耗变得困难。因此，如果 gas 限制设置不当或合约遇到意外高计算需求的场景，Solidity 合约可能在执行过程中耗尽 gas。
一个现实的例子是 Solidity 中特定类型的拒绝服务（DoS）攻击问题，其中合约因无界执行约束而变得无法操作。一个例子是 GovernMental 攻击，其中需要删除以进行支付的映射变得非常大，以至于操作它超出了区块 gas 限制。
Clarity 语言设计有一些不同的属性可以防止此类 DoS 攻击。
分析系统能够准确估算执行成本的原因是 Clarity 有意限制了某些功能。
例如，Clarity 中没有递归，因此我们不能无限次地重复调用同一个函数。
Clarity 中的数据类型也受到限制。任何不需要硬性长度上限的数据类型都不可迭代。
例如 map 和 tuple 在定义时不要求你输入最大长度，但你也不能对它们进行迭代。
另一方面，可迭代的 list 则要求开发者在定义时指定上限。这在很大程度上允许对 Clarity 合约进行准确的静态分析。
那么我们如何在 Clarity 中实现一个未定义大小的映射？我们不会这样做，因为这在智能合约设计中是一种反模式。
相反，Clarity 强迫我们思考更好的解决方案。例如，让用户自己处理映射/列表元素操作，而不是在合约层面进行大规模操作。
如果你 分析 GovernMental 攻击，你会看到它利用了多重安全问题，而这些问题在 Clarity 中都已得到缓解。你还会看到已经添加了一个修复，使得再次实施此类攻击在经济上变得不可行。
这提出了在为智能合约和区块链系统建立合适心智模型时的另一个关键点：复杂性意味着更多潜在的漏洞，这又意味着为了应对这些漏洞而引入更多复杂性。
当这种情况一再发生时，我们就把自己困在创建越来越复杂的系统中。在语言层面上解决这些问题可以防止这种不断增长的复杂性。
如需深入了解 Clarity 的设计，请查看 SIP-002.
你可以在以下内容中查看一些更常见的智能合约漏洞以及它们的缓解方式： 这篇文章.
这在安全测试和审计方面也有二阶效应。常见的智能合约测试工具之一是形式化验证，即我们用数学证明智能合约的某些属性在所有情况下是否成立。
这可能导致路径爆炸问题，即可用路径太多以至于形式化验证变得极其困难。由于程序不可能遇到无界循环，这个问题在 Clarity 中得到缓解。
这引导我们形成一个更广泛的心智模型，用于在智能合约在经济中占据更大比重时思考可判定性。记住，区块链系统的目标是创建一个开放、透明、公平的金融系统。
这意味着智能合约将负责为越来越多的人管理大量财富。随着智能合约涵盖更多的金融结构，它们的复杂性和使用量将增长。
复杂性是安全的敌人。系统越复杂，当对执行步骤没有硬性限制时，就越有可能产生不可计算的问题。
在既开放透明又不可更改的金融基础设施中，这种情况是致命的。让我们进一步探讨不可计算性的概念。
对不可计算性的直觉理解
直观上，不可计算性是对不可判定性的算法视角。不可计算性与不可判定性有相同的基础。不可判定的问题以逻辑命题或关于整数的陈述来表述。当然，程序是逻辑陈述，甚至可以视为整数，尽管我们以不同方式看待程序。我们通常以内存模型、实现细节和执行语义的附加细节来观察程序。
停机问题 : 作为一个例子，给定任意程序P 和任意有限输入 I 对 ，停机问题是确定 和任意有限输入是否在输入 和任意有限输入 上停机的挑战。 对.
阿隆佐·丘奇和艾伦·图灵证明了停机问题是不可解的。
克里斯托弗·斯特拉奇（Christopher Strachey）给出了一种基于矛盾的直观证明，表明停机问题是不可计算的。这是通过假设存在一个程序 H 可以为任意程序解决停机问题来建立的， 和任意有限输入. H(P) 如果 和任意有限输入 停机则返回 true，否则返回 false。然后构造一个程序 和任意有限输入 当 H(P) 为真时不停止，从而产生矛盾。同样，当 和任意有限输入 为假时该程序会停机，这也产生矛盾。 H(P) 不可计算的问题是指无论提供多少时间或资源，都无法被算法或计算机解决的问题。这类问题以各种形式存在，其中一个例子是由埃米尔·波斯特提出的波斯特对应问题（Post correspondence problem）。
波斯特对应问题可以用字符串对和一个整数来描述。设想你有 n 对字符串，称为 P。这些字符串由某个字符集中的字符组成，例如 UTF-8 或任何至少有两个符号的字母表。字符串对看起来像这样：
P = { (x1, y1), (x2, y2), … , (xn, yn) }
x(i1) x(i2) … x(im) = y(i1) y(i2) … y(im)
简单来说，波斯特对应问题涉及尝试找到一个索引序列，该序列应用于给定的字符串对后，会从 x 和 y 分量产生相等的连接字符串。该问题被认为是不可计算的，因为不存在能对所有可能的输入字符串对和整数求解的一般算法。
事实证明，关于程序行为的许多问题都是不可计算的。这对用图灵完备语言构建的智能合约有许多影响，其中许多我们目前还未察觉，但在未来遇到时肯定会意识到。
雷蒙德·斯穆利安对不可判定性的直觉理解
这是雷蒙德·斯穆利安在命题逻辑中理解不可判定性的一部分方法。它使用元信息来表明某事必须为真，尽管在命题逻辑中无法证明。这基于一个悖论。
在命题逻辑中，如果我们无法证明某个逻辑命题为真或为假，则称其为不可判定。给定一个命题逻辑命题 S，证明是一系列形式逻辑演绎，起始于基本事实，结束于说明 S 为真或为假的结论。
斯穆利安从一个骑士与骗子的岛屿开始。骑士总是说真话。骗子总是说谎。除此之外我们无法区分岛上的人。
有一位伟大的逻辑学家叫 Ray。Ray 无论证明什么都是真的。这就像一个好的定理证明器。
岛民 Jack 向逻辑学家 Ray 宣称：“你不能证明我是个骑士”。
接下来的推理基于对此情形的元知识。这种元知识表明在命题逻辑中某些问题是不可判定的。
如果 Ray 能证明 Jack 是骑士，那么 Jack 一定是骗子，因为 Jack 一定是在撒谎。那是因为 Ray 证明了 Jack 是骑士。既然 Jack 是骗子，Ray 的证明就与 Ray 只证明真事的假设矛盾。因此，这种情况不可能成立。
如果 Ray 不能证明 Jack 是骑士，那么 Jack 必定是骑士，因为 Jack 说的是实话。但 Ray 无法证明 Jack 是骑士这一事实。
在智能合约和编程语言的上下文中，像 Solidity 这样的图灵完备语言可能会出现不可判定的问题。
这些不可判定的问题类似于骑士与骗子故事中的悖论，在给定信息下无法确定 Jack 是骑士还是骗子。
在骑士与骗子的故事中，Ray 类似于定理证明器或图灵完备语言中的智能合约。Ray 面临一个在该系统（骑士与骗子）约束下不可判定的陈述，从而导致悖论。
类似地，图灵完备的智能合约语言可能会遇到无法解决的不可判定问题，导致意外行为、漏洞或资源消耗问题（例如以太坊中耗尽 gas）。
另一方面，像 Clarity 这样的非图灵完备语言通过限制其表达能力来避免不可判定问题的出现。
在骑士与骗子的故事背景下，非图灵完备语言将简单地不允许 Jack 做出可能导致悖论的陈述。通过禁止某些特性，如无界循环和递归，非图灵完备语言可以为智能合约的行为和资源使用提供更强的保证。
在许多情况下，这种可预测性是可取的，尤其是在处理高价值交易或关键系统时。
参考文献
The Mathematics of Various Entertaining Subjects: Research in Recreational Math Illustrated Edition, Jennifer Beineke (Editor), Jason Rosenhouse (Editor), Raymond M. Smullyan (Foreword), Princeton University Press, 2016.
各种有趣主题的数学：休闲数学研究（插图版），Jennifer Beineke（编辑），Jason Rosenhouse（编辑），Raymond M. Smullyan（前言），普林斯顿大学出版社，2016 年。
最后更新于
这有帮助吗？