kol*_*vra 4 oop math functional-programming imperative-languages
我时不时地听到有人说"函数式编程语言更具数学性".是这样吗？如果是这样,为什么以及如何？例如,Scheme比Java或C更具数学价值吗？还是哈斯克尔？
我无法准确定义什么是"数学",但我相信你可以得到这种感觉.
谢谢!
有两种常见的(*)计算模型:Lambda微积分(LC)模型和图灵机(TM)模型.
Lambda Calculus通过使用数学形式来表示计算,其中结果是通过类型域上的函数组合产生的.LC还与组合逻辑有关,组合逻辑被认为是针对同一主题的更通用的方法.
该图灵机模型,利用基本操作的主体(如此外,突变等)较其上存储的理想存储符号的操作方法计算.
这些不同的计算模型是不同编程语言族的基础.Lambda Calculus引发了ML,Scheme和Haskell等语言.图灵模型已经产生了C,C++,Pascal等.作为概括,大多数函数式编程语言在lambda演算中具有理论基础.
由于Lambda微积分的性质,可以对基于其原理构建的系统的行为进行某些证明.实际上,可证明性(即正确性)是LC中的一个重要概念,并且使得关于LC系统的某些推理和结论成为可能.LC也与类型理论和范畴理论有关(并且依赖于它).
相比之下,图灵模型较少依赖于类型理论,更多地依赖于结构化计算作为底层模型中的一系列状态转换.图灵机的计算模型更难以做出断言,也不适合基于LC的程序所做的相同类型的数学证明和操作.但是,这并不意味着不可能进行这样的分析 - 在研究程序的虚拟化和静态分析时会使用TM模型的一些重要方面.
因为函数式编程依赖于类型的仔细选择和类型之间的转换,所以FP可以被视为更"数学".
(*)其他计算模型也存在,但它们与本讨论的相关性较低.
纯函数式编程语言是函数式微积分的示例,因此在理论上,用函数式语言编写的程序可以在数学意义上进行推理.理想情况下,您希望能够"证明"该程序是正确的.
在实践中,除了微不足道的情况之外,这种推理是非常困难的,但在某种程度上它仍然是可能的.您可能能够证明程序的某些属性,例如,您可能能够证明给定程序的所有数字输入,输出始终受限于某个范围.
在具有可变状态和副作用的非功能性语言中,尝试推理程序和"证明"正确性几乎是不可能的,至少目前是这样.使用非功能性程序,您可以通过程序进行思考并说服自己部分内容是正确的,并且您可以运行单元测试来测试某些输入,但通常无法构建有关程序行为的严格数学证明.