Lisp鬆散地是什麼類型的lambda演算？

Question

我試圖更好地掌握類型如何在lambda微積分中發揮作用。無可否認，很多類型理論的東西都在我的頭上。 Lisp是一種動態類型語言，它大致對應於無類型的lambda演算？還是有某種我不知道的「動態類型lambda微積分」？

Answer 1

Lisp是一種動態類型語言，它大致對應於無類型lambda微積分嗎？

是的，但只是粗略的。在「純」的無類型lambda演算中，所有內容都被編碼爲函數。 （你可以在谷歌搜索受歡迎的「教會編碼」和不太受歡迎的「斯科特編碼」）。Lisp具有非功能性數據，如原子和數字等，因此這可以被視爲「無類型的lambda微積分擴展常量」。

另一個重要的區別是評估順序。減少lambda-演算術語的規則是非常不確定的。 （有一個定理，即教會 - 羅塞爾定理，它鬆散地指出，只要事情終止，評估順序就不重要。）實際上，使用最左邊最外層的「正常順序」縮減來減少lambda項，因爲如果任何減少策略終止，那一個。 這與Lisp總是在進行beta縮減之前將參數評估爲正常形式非常不同。此評估訂單被稱爲「按價值調用」。

綜上所述，Lisp對應於的一種無類型的按值調用的lambda演算，其常量爲。

Answer 2

John McCarthy在his April, 1960 paper "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I"中介紹了LISP。以下段落來自第6頁：

e。函數和形式。在數學邏輯之外的數學中通常不精確地使用「功能」一詞並將其應用於形式 ，例如y + x。因爲我們稍後將用函數的表達式進行計算，所以我們需要函數和形式之間的區別以及用於表示這種區別的符號。這種區別和描述它的符號，我們偏離平凡的 由Church [3]給出。
...
3. A. CHURCH，Lambda轉換的結石（普林斯頓大學 出版社，Princeton，N.J。，1941）。

該Wikipedia article on lambda-calculus有教會的出版物的歷史。麥卡錫引用的1941年的論文似乎是關於型的 lambda演算，這與維基百科文章的介紹相矛盾。

Lisp中的lambda關鍵字可以理解爲僅通過類比來指代lambda-演算。 Lisp lambda表達式是一種anonymous function。

Answer 3

Lisp不是'lambda微積分'，我不知道'lambda微積分'是什麼。

如果你想通過那裏鍵入系統來識別lambda結石，那麼當然Lisp是它自己的。 Scheme之前的任何lisp中的'lambda'關鍵字肯定是自命不凡的，在Scheme之後還有空間可以說。只要使用'func'會更加謙虛。 Lisp主要是列表處理器，而不是'lambda微積分'

我也寫了一篇相當廣泛的文章，一次試圖說明爲什麼A：術語'函數式編程'是無意義的，B：爲什麼說'一個演算，而不是‘一類的制度’也是如此：

http://blog.nihilarchitect.net/archives/289/on-functional-programming/

另外，請記住，在Lisp中，所有功能都有效單個參數只能是有名單作爲他們的論據。