怎麼理解從lambda運算元到實際的函數式程序設計語言？

01-05

之前有學習過函數式程序語言，主要是scheme，學習的時候使用了Dracket這個平台來編寫代碼（選擇R5RS規範）。在完成一定的代碼後總體感覺主要是加深了可計算性的理解，但是對scheme本身的理解不多。
現在理解到內容主要有一下幾條：
（1）lambda運算元的三條公理，在這個基礎上定義了程序設計語言達到的可計算性；
（2）lisp的七個基本操作符定義了lisp在語言實現上的計算能力，但是對於文件操作等並沒有定義；
（3）scheme通過在lisp的七個基本操作符基礎上定義一些：基本類型（true，false等），基本模式（form）和過程（process）來最小化定義該語言本身，並完成語言本身的形式化語言描述；

（4）scheme標準化種將這些模式和過程按照實際編程需要確定，然後提出R5RS等規範，然後對實際編程中涉及到的擴展編寫可移植庫（R7RS的努力）；
感覺有些不是很清晰的地方在於：
（1）lambda運算元的三條公理描述的可計算性是否和lisp的七個基本操作符定義的可計算性等價，這七個基本操作符是否是三條公理的語法糖？
（2）使用lisp的七個基本操作符（quote,atom,eq,car,cdr,cons,cond）能不能定義如lambda等不涉及副作用（define）或者文件操作的其他scheme中基本組件？
（3）scheme內部支持的數學運算，如基本的數字定義（0,1,1.1,1E4等）是否就是邱奇數，如+,-,*./等是否也是同樣定義的？
//補充說明：
因為想從圖靈完備的lambda演算來，然後加入一些有副作用的最小操作符，這樣構成最簡化的可以實際使用的程序設計語言。
明白邱奇數定義數字在實現的時候很複雜，而且沒有類型信息，但是至少說明了用這種方式實現定義的可行性，認為實際編程語言的實現則是圖靈模型下馮諾依曼機的優化。

覺得從這種角度能夠加深對理論到實現的認識

你去看 idris 那篇文章《Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation》吧，手把手教你從 idris 編譯成 TT（超級簡單的帶類型 λ 項）

（quote,atom,eq,car,cdr,cons,cond）和 λ 的轉換可以靠 Church encoding 做

然後（quote,atom,eq,car,cdr,cons,cond）怎麼自舉好像有篇文章裡面寫過……忘了哪裡看到了

最後，你可以用 Church number 去實現數學運算，不過 scheme 肯定不會這麼乾的，太慢了

不管是圖靈機還是 lambda 演算都是為了解決可計算問題，也就是說圖靈完備僅僅是

「可以計算出一個值」而不涉及其他的。

函數式中將超過計算的東西叫做副作用，因為文件讀寫，列印，隨機數，這些東西都不是純的計算過程，而是涉及到外部世界的交互，依賴於機器，不在理論的範疇。

你想寫文件，那麼是你的程序調用操作系統的 API，操作系統再執行 CPU 的指令，控制磁碟的晶元，磁頭開始在盤面上寫入原本位於內存或寄存器的信息。但是在圖靈完備中，是不需要什麼磁碟，磁頭，內存的，這些都是理論之外的。

也就是說一門圖靈完備的語言，只要有無限的時間和空間，你絕對能用來解微分方程組，三體問題，甚至模擬整個宇宙，但這些語言可能不能在屏幕上打 Hello, world.

=====

語法糖沒有一個嚴謹的定義，如果意味著能相互實現的話，任何不帶副作用的操作都是任何圖靈完備的操作的語法糖。

不過看題主提問，應該不是這個意思。實際上 Lambda 演算作為一個偏邏輯抽象的東西，對編程語言有指導的作用，但基本沒有直接的相同之處。簡而言之，Lambda 演算和 Lisp 的關係類似於馬克思主義和中華人民共和國的關係。

所以邱奇數也不是 Scheme 的數的實現。不說效率問題，最本質的是，你所說的 Lambda 演算是只有函數類型的，而 Scheme 不可能這樣做，它有好多類型呢。如果是邱奇數的話，你可以試試調用一下數字。

當然你可以在 Scheme 裡面用純 Lambda 來實現一整套 Lambda 演算系統，基本上就是簡單翻譯一下語法。

Lisp 七條公理什麼的其實挺無聊的，要說可以構造那當然可以構造，lambda 實際也是就是根據參數表和函數體進行規約操作，明顯可以定義出來。但是毫無意義，給我構造出一個 vector 出來試試？要 O(1) 索引的…

去看看 R5RS 的文檔吧。裡面給出了一些基本過程和擴展過程，並明說擴展過程是能被基本過程定義的，比網上的X條公理明晰嚴謹不知道多少，而且你還真能做出來。

謝邀……

（1）不是

brainfuck也是圖靈完全的，那brainfuck定義的幾種操作符是不是lambda演算三條公理的語法糖？

可計算性等價和語法糖沒有必然聯繫

（2）不能

硬要說能的話，用無副作用的操作定義出副作用，也就是Haskell里的那套monad的東西了

（3）不是

(+ 1 1)和(+ 100000 100000)用的時間是不是相差無幾？

邱奇編碼，真正用來做計算，複雜度可是很高的，數字越大越高

《The Implementation of Functional Programming Languages》

取決於語法糖的定義。 @徐釀泉答案正確。
能定義出，但性能差。
scheme是一套標準。你可以開發一款scheme解釋器，用邱奇數實現schema的算術運算。但是一般的scheme實現不這麼干，因為性能差。一般的scheme實現最終都是調用CPU指令來實現算術運算，而CPU設計中的晶體管連接結構和邱奇數無關。

我覺得關鍵是理解lambda演算中函數定義和函數調用的含義。

參考，

http://mp.weixin.qq.com/s?__biz=MzIwMDgyNzUzNw==mid=2247483658idx=1sn=2dde89033d2fef0cba307db9b8b5489escene=0#wechat_redirect