时不时地，我听到有人说“函数式编程语言更数学”之类的话。是这样吗？如果是这样，为什么以及如何？例如，Scheme 是否比 Java 或 C 更具数学性？还是哈斯克尔？
我无法准确地定义什么是“数学”，但我相信你能体会到。
谢谢！
问问题
1055 次
5 回答
9
有两种常见的 (*)计算模型：Lambda Calculus (LC) 模型和Turing Machine (TM) 模型。
Lambda 演算通过使用数学形式表示计算来处理计算，其中结果是通过类型域上的函数组合产生的。LC 还与组合逻辑有关，组合逻辑被认为是针对同一主题的更通用的方法。
图灵机模型通过将计算表示为使用一组基本操作（如加法、变异等）对存储在理想化存储中的符号进行操作来处理计算。
这些不同的计算模型是不同系列编程语言的基础。Lambda 演算产生了ML、Scheme和Haskell等语言。图灵模型催生了C、C++、Pascal等。作为概括，大多数函数式编程语言都有 lambda 演算的理论基础。
由于 Lambda 演算的性质，某些基于其原理的系统行为的证明是可能的。事实上，可证明性（即正确性）是 LC 中的一个重要概念，它使关于 LC 系统的某些推理和结论成为可能。LC 还与（并依赖于）类型论和范畴论有关。
相比之下，图灵模型较少依赖类型论，而更多地依赖于将计算结构化为底层模型中的一系列状态转换。图灵机计算模型更难做出断言，并且不适合基于 LC 的程序所做的相同类型的数学证明和操作。然而，这并不意味着不可能进行这样的分析——在研究虚拟化和程序的静态分析时，会使用 TM 模型的一些重要方面。
因为函数式编程依赖于仔细选择类型和类型之间的转换，所以 FP 可以被认为更“数学化”。
(*) 也存在其他计算模型，但它们与本次讨论的相关性较低。
于 2010-12-22T23:18:02.773 回答
8
纯函数式编程语言是函数式演算的例子，因此理论上用函数式语言编写的程序可以在数学意义上进行推理。理想情况下，您希望能够“证明”程序是正确的。
在实践中，这种推理是非常困难的，除非是在微不足道的情况下，但在某种程度上它仍然是可能的。您可能能够证明程序的某些属性，例如，您可能能够证明给定程序的所有数字输入，输出始终被限制在某个范围内。
在具有可变状态和副作用的非函数式语言中，试图推理程序并“证明”正确性几乎是不可能的，至少目前是这样。对于非功能性程序，您可以仔细考虑程序并说服自己其中的某些部分是正确的，并且您可以运行单元测试来测试某些输入，但通常不可能构建关于程序行为的严格数学证明。
于 2010-12-22T22:58:51.357 回答
4
我认为一个主要原因是纯函数式语言没有副作用，即没有可变状态，它们只是将输入参数映射到结果值，这正是数学函数所做的。
于 2010-12-22T22:54:24.257 回答
0
函数式编程的逻辑结构很大程度上基于 lambda 演算。虽然它可能看起来不是仅基于数学的代数形式的数学，但它很容易从离散数学中编写出来。
与命令式编程相比，它并没有明确规定如何做某事，而是规定必须做什么。这反映了拓扑。
于 2010-12-22T22:56:32.450 回答
0
函数式编程语言的数学感觉来自几个不同的特性。最明显的是名字；“函数式”，即使用函数，这是数学的基础。另一个重要的原因是函数式编程涉及定义一组永远为真的事物，通过它们的交互来实现所需的计算——这类似于数学证明的完成方式。
于 2010-12-22T22:57:33.630 回答