计算机科学中的“原因”一词是什么意思？答案

【问题标题】：What does the term "reason about" mean in computer science?计算机科学中的“原因”一词是什么意思？
【发布时间】：2013-09-11 02:06:35
【问题描述】：

在学习函数式编程时，我不断遇到“原因”一词，尤其是在纯函数和/或引用透明性的上下文中。谁能解释一下这到底是什么意思？

【问题讨论】：

“关于程序的原因”表达是指可能存在于函数式编程语言的工具，允许在数学上证明它们相对于正式表达的规范的行为。这些工具类似于 Java 的 KeyY 或 C 语言的 Frama-C。 en.wikipedia.org/wiki/KeY frama-c.com
CS 中的“原因”与任何其他领域或上下文中的“原因”完全相同。
您可能还想了解停机问题以及它是如何被证明是不可判定的。这严重限制了我们推理图灵完备语言程序的能力。
reason about in Reat：传递了哪些 props，使您的应用易于推理。 facebook.github.io/react/docs/context.html
“推理”是“关于”“程序”做它应该做的事情。（这是 60 年代出现的计算机科学和软件工程术语。）（硬推理是条件和不变量（递归、循环和并发）。

标签： scala haskell functional-programming

【解决方案1】：

通常，在编写程序时，您的工作不会仅仅以编写代码而告终，您还想知道代码表现出的一些属性。您可以通过两种方式得出这些属性：逻辑分析或经验观察。

此类属性的示例包括：

正确性（程序做它应该做的）
性能（需要多长时间）
可扩展性（输入对性能有何影响）
安全性（算法会被恶意滥用）

当您凭经验测量这些属性时，您会得到精度有限的结果。因此，从数学上证明这些性质要优越得多，但并不总是那么容易做到。函数式语言通常将使其属性的数学证明作为其设计目标之一。这就是程序推理的典型含义。

就功能或较小的单位而言，上述适用，但有时作者也只是意味着考虑算法或设计算法。这取决于特定的用法。

顺便说一下，一些例子说明了人们如何对其中一些事情进行推理以及如何进行经验观察：

正确性：我们可以证明代码是正确的，如果我们可以用方程式证明它做了它应该做的事情。所以对于一个排序函数，如果我们可以证明我们给它的任何列表都具有被排序的属性，我们就知道我们的代码是正确的。根据经验，我们可以创建一个单元测试套件，在其中我们提供输入代码示例并检查代码是否具有所需的输出。

性能和可扩展性：我们可以分析我们的代码并证明算法的性能界限，以便我们知道它所花费的时间如何取决于输入的大小。根据经验，我们可以对我们的代码进行基准测试，看看它在特定机器上的实际运行速度。我们可以执行负载测试，看看我们的机器/算法在折叠/变得不切实际之前可以接受多少实际输入。

【讨论】：

对于这四个类别，经验主义的意思是：1.让QA找到bug。 2.让你友好的用户抱怨。 3. 让您的 IT 人员在服务器崩溃后凌晨 3 点给您打电话。 4. 将您的数据和服务器捐赠给不友好的用户。这些方法中的任何一种都意味着您的工作以编写代码结束。在这种情况下，你的老板会说，“让我告诉你我解雇你的原因。”他说的时候可能会无意吐口水。

【解决方案2】：

推理代码，在 这个词最宽松的意义上，意味着考虑你的代码以及它真正做了什么（而不是你认为它应该做什么。）这意味着

了解代码的行为方式，当您向其抛出数据时，
知道可以在不破坏的情况下重构哪些内容，以及
密切关注可以执行哪些优化，

除其他外。对我来说，在调试或重构时，推理部分起着最大的作用。

举一个你提到的例子：当我试图找出一个函数有什么问题时，引用透明度对我有很大帮助。引用透明性保证了当我使用函数时，给它不同的参数，我知道函数会在我的程序中以相同的方式做出反应。它不依赖于它的论点以外的任何东西。这使得函数更容易推理——而不是命令式语言，其中函数可能依赖于一些外部变量，而这些外部变量会在我眼皮子底下发生变化。

另一种看待它的方式（这在重构时更有帮助）是，您越了解您的代码满足某些属性，它就越容易推理。例如，我知道

map f (map g xs) === map (f . g) xs

这是一个有用的属性，我可以在重构时直接应用。我可以陈述 Haskell 代码的这些属性这一事实使推理更容易。我可以尝试在 Python 程序中声明这个属性，但我对它的信心会大大降低，因为如果我在选择 f 和 g 时不走运，结果可能会有很大差异。

【讨论】：

【解决方案3】：

通俗地说，它的意思是“能够通过查看代码来判断程序将要做什么。”由于副作用、强制转换、隐式转换、重载函数和运算符等，这在大多数语言中可能会非常困难。也就是说，当您无法仅使用大脑来推理代码时，您必须运行它以查看它适用于给定的输入。

【讨论】：

【解决方案4】：

通常当人们说“推理”时，他们的意思是“等式推理”，这意味着在不运行代码的情况下证明代码的属性。

这些属性可以非常简单。例如，给定(.)和id的以下定义：

id :: a -> a
id x = x

(.) :: (b -> c) -> (a -> b) -> (a -> c)
(f . g) = \x -> f (g x)

...然后我们可能想证明：

f . id = f

这很容易证明，因为：

(f . id) = \x -> f (id x) = \x -> f x = f

请注意我是如何为 all f 证明这一点的。这意味着我知道这个属性无论如何都是正确的，因此我不再需要在某种单元测试套件中测试这个属性，因为我知道它永远不会失败。

【讨论】：

“证明代码的属性”的硬推理是重新暗示——不变量（递归、循环和并发）和条件。

【解决方案5】：

“推理程序”只是“分析程序以查看它的作用”。

这个想法是纯度简化了理解，无论是通过人类更改程序，还是通过机器编译程序或分析程序以找出破碎的极端情况。

【讨论】：

【解决方案6】：

已经给出了这个问题的许多正确答案，指的是正确性的数学证明。但我希望能为不一定是数学专业的程序员提供一个实用的答案。

正如 Douglas Crockford 所观察到的那样，正确性的形式证明在当代编程实践中并不重要。[1]

在调试阶段，“关于您的代码的原因”这句话首先对我来说很实用。问题是：当出现问题时，您是否容易确定错误的原因？

如果每个函数的行为仅取决于其输入，那么预测函数体内会发生什么应该是相当简单的。意外错误意味着未处理某些输入案例。（例如，一个常见的问题是没有预料到 null 参数。）

另一方面，如果函数的结果取决于函数不拥有或控制的外部变量的状态，那么很难追踪导致系统所处状态的原因，当错误发生。（解决这些问题是系统进行大量日志记录的动机。）

这就是说函数式样式允许您“推理”您的代码的原因。

它将可能出错的地方限制在函数参数与其返回值之间可能发生的情况。
它将可能出错的地方限制在函数拥有和控制的少数元素上。

如果您知道在哪个函数中遇到了错误，那么您应该能够很容易地找出肯定出了什么问题，以及它是如何出现的。（并且，如有必要，将调用堆栈展开到必须有意外值的地方。）

“推理”也体现在行为驱动开发范式中：

鉴于：可能的初始条件数量有限。（例如，参数。）

何时：执行您定义的流程。

那么：可能的结果范围有限且已知。

简而言之，这就是“推理”代码。

（当然，这也取决于你的函数体不修改外部变量，这就是函数式程序员喜欢称之为“副作用”的地方。）

Edsger Dijkstra 著名地反对goto 声明。他推断，如果允许程序任意跳转到其定义中的任何行，那么您就无法期望预测其运行时行为。

函数式编程范式更进一步：它希望将程序逻辑外部的任何状态的影响限制为实现其目的所必需的。

这样 - 当您调试错误时 - 只需阅读代码就足以了解其原因。

[1]：克罗克福德，道格拉斯。 “测试如何工作”。 Javascript 的工作原理。 Virgule-Solidus LLC，2018 年。EPUB。

【讨论】：

【解决方案7】：

正如@John Wiegley 所说，推理意味着

仅通过查看代码就能知道程序会做什么

更重要的是了解阻碍我们推理代码的原因。这些是副作用。

【讨论】：