函數式編程被認爲是更「數學」的嗎？如果是這樣，爲什麼？

Question

我偶爾會聽到有人說「函數式編程語言更加數學化」。是這樣嗎？如果是這樣，爲什麼和如何？例如，Scheme是比Java還是C更數學的？還是Haskell？

我無法準確定義什麼是「數學」，但我相信你可以感受到。

謝謝！

Answer 1

有兩個常見的（*）models of computation：Lambda Calculus（LC）模型和Turing Machine（TM）模型。

Lambda Calculus通過使用數學形式表示方法來計算，其中結果是通過類型域上的函數構成產生的。 LC也與Combinatory Logic有關，這被認爲是對同一主題的更普遍的方法。

圖靈機模型通過使用一系列基本操作（如添加，變異等）將其表示爲對存儲在理想化存儲中的符號的操縱來處理計算。

這些不同的計算模型是不同系列編程語言的基礎。Lambda微積分引起了諸如ML,Scheme和Haskell之類的語言。圖靈模型產生了C,C++,Pascal等。作爲一種推廣，大多數functional programming語言在lambda演算中都有理論基礎。

由於Lambda微積分的性質，關於建立在其原理上的系統行爲的某些證明是可能的。事實上，可檢驗性（即correctness）是液相色譜中的一個重要概念，並且使得關於液相色譜系統的某些推理和結論成爲可能。 LC還涉及（並依賴於）類型理論和類別理論。相比之下，圖靈模型更少依賴於類型理論，更多地將計算結構化爲底層模型中的一系列狀態轉換。計算機的圖靈機模型更難以作出斷言，並且不適用於基於LC的程序所做的相同類型的數學證明和操作。然而，這並不意味着這種分析是不可能的 - 在研究虛擬化和程序的靜態分析時，會使用TM模型的一些重要方面。由於函數式編程依賴於仔細選擇類型和類型之間的轉換，所以FP可以被認爲是更「數學」的。 （*）也存在其他計算模型，但它們與本討論的相關性較低。

Answer 2

我認爲一個主要原因是純函數式語言沒有副作用，即沒有可變狀態，它們只將輸入參數映射到結果值，這正是數學函數所做的。

Answer 3

函數式編程的邏輯結構很重based on lambda calculus。雖然它可能不是完全基於代數形式的數學的數學，但它被寫爲very easily from discrete mathematics。

與命令式編程相比，它沒有規定如何做某件事，但必須做什麼。這反映了拓撲。

Answer 4

函數式編程語言的數學感受來自一些不同的特性。最明顯的是名字; 「功能」，即使用功能，這是數學的基礎。另一個重要的原因是函數式編程涉及定義總是真實的事物集合，通過它們的交互實現所需的計算 - 這與數學證明如何完成相似。

Answer 5

純粹的函數式編程語言是functional calculus的例子，所以在理論上，用功能語言編寫的程序可以從數學意義上推論。理想情況下，您希望能夠'證明'該計劃是正確的。

在實踐中，除了微不足道的情況外，這種推理是非常困難的，但它在某種程度上仍然是可能的。您可能能夠證明程序的某些屬性，例如您可能能夠證明給定程序的所有數字輸入時，輸出始終受限於一定範圍內。

在具有可變狀態和副作用的非功能語言中，嘗試推理程序和'證明'正確性幾乎是不可能的，至少在這一刻。使用非功能程序時，您可以通過程序來思考並說服自己，其中的部分內容是正確的，並且可以運行測試某些輸入的單元測試，但通常無法構建關於程序行爲的嚴格數學證明。