Lambda Interpreter
A λ-calculus interpreter
interpreter used Java by Pkun
我們利用自頂向下的思考方式呢簸，首先搀突，輸入是一個lambda表達(dá)式，為了方便起見柳骄，我們將lambda寫作\团赏，所以輸入的式子應(yīng)該是這樣。
(\x.\y (x y)) (\p.p)(\q.q)
那么改如何去解釋它呢耐薯？我們先用常規(guī)的方法計(jì)算一下舔清。很容易看出我們只需要把后面兩個抽象帶入到前面的抽象就可以了。如果是計(jì)算機(jī)做的話曲初，上面這句話可以分解成
- 識別出三個抽象
- 將后面的抽象按照順序帶入到前面的抽象中
我們先復(fù)習(xí)一下之前學(xué)過的lambda演算的知識
t1 t2 # Application
\x. t1 # Abstraction
x # Identifier
如果要一般化体谒，第一步可以理解成
-
計(jì)算機(jī)必須能夠翻譯lambda表達(dá)式中的所有項(xiàng)，分別是App臼婆，Abs和Ide抒痒。
那么該如何翻譯出所有的項(xiàng)呢冰抢？我們注意到他們?nèi)齻€各有特點(diǎn)考榨，Abs中有l(wèi)ambda熏版，Application有兩支旷坦，Identifier只有一個值似谁，另一方面奖磁，注意到我們讀入的是一個字符串拾并，所以我們可以采用從頭到尾遍歷整個字符串的方法蹦渣，將字符串中的所有項(xiàng)都讀出來誓酒。
到這里惨缆，我們要注意到的一件事情就是Application，Abstraction是可以相互嵌套的丰捷，Identifier也可以是Application的左右兩支坯墨，最后出來的應(yīng)該是一個樹狀的結(jié)構(gòu)，到這里病往，我們不難想到讓三個類都繼承一個節(jié)點(diǎn)類捣染，通過節(jié)點(diǎn)訪問節(jié)點(diǎn)的節(jié)點(diǎn)，來遍歷整棵樹停巷，避免嵌套帶來的類型轉(zhuǎn)換的麻煩耍攘。
我們規(guī)定一個抽象語法樹，它的節(jié)點(diǎn)有三個畔勤，抽象蕾各，應(yīng)用和原子。
既然要遍歷整個字符串庆揪，我們采用枚舉的方式式曲，一旦符合某種模式，就將他歸類為某種語法，所以我們需要規(guī)定一個lambda表達(dá)式中會出現(xiàn)的所有字符吝羞，其實(shí)也很簡單兰伤，是下面六種
LPAREN: '('
RPAREN: ')'
LAMBDA: '\' // 為了方便使用 “\”
DOT: '.'
LCID: /[a-z][a-zA-Z]*/
EOF: null
我們將這些字符命名為Token，并且通過識別不同的Token钧排，把一個Lambda表達(dá)式解析成一個抽象語法樹敦腔。到這里，我們已經(jīng)構(gòu)建出一個計(jì)算機(jī)可以閱讀的Lambda表達(dá)式了恨溜。接下來我們要讓計(jì)算機(jī)在遍歷的過程中符衔，把整個抽象語法樹構(gòu)建出來。為了方便起見糟袁，我們制定三條語法規(guī)則：
Term ::= Application| LAMBDA LCID DOT Term
Application ::= Application Atom| Atom
Atom ::= LPAREN Term RPAREN| LCID
整體的思路就是不斷讀入下一個字符判族，判斷它是Token中的哪一種，然后在Term Application Atom三個方法之中跳轉(zhuǎn)系吭，構(gòu)建出整個樹五嫂。
接下來讓我們考慮第二步颗品，也就是做beta規(guī)約的事情肯尺。其實(shí)想想還是挺容易的一件事情，因?yàn)樵谖覀兊某橄笳Z法樹里面躯枢，如果某個節(jié)點(diǎn)的左支是Abstraction则吟，你可以直接把右支帶入到左支里面去，替換左支body中的所有和param一樣的東西锄蹂。寫成偽碼的話應(yīng)該是這樣子
while(hasnext(Abs.Body)){
if(charInBody==Abs.Param) charInBody = Ide;
}
筆者認(rèn)為也這是一種比較好的處理方式氓仲，但是很多細(xì)節(jié)問題沒有考慮，也不知道這種處理方式最后效果怎么樣得糜。按道理來說是不會出現(xiàn)因?yàn)閮蓚€Abs的param相同而導(dǎo)致代入出現(xiàn)問題的敬扛。接下來我要介紹老師欽定的方法來構(gòu)造求值的函數(shù)。
De Bruijn index
關(guān)于De Bruijn,你可以在下面網(wǎng)站中找到你想要的 De Bruijn Sequence（無法查看的話可以百度百科）
用De Bruijin Index朝抖，我們可以給Abs或者Ide中的項(xiàng)打上自己的標(biāo)簽啥箭，比如說\x.\y x y 可以看成 \x.\y 1 0，但是對于\x.a 這樣的變量沒有綁定的時候治宣，可能是默認(rèn)換成\x. 1吧（如果博客沒寫錯的話）急侥。印入De Bruijn Index最主要的原因是alpha替換，lambda表達(dá)式中的符號是可以隨意替換的侮邀，它并沒有具體的含義坏怪，是一種假變量，就算重復(fù)也沒有關(guān)系绊茧，當(dāng)然铝宵，在同一個abs或者其他的一些式子之中，我們?yōu)榱藚^(qū)分和計(jì)算還是應(yīng)該將變量取上不同的名字华畏。
當(dāng)然捉超，運(yùn)用了De Bruijn Index之后胧卤，我們的前一個階段又出現(xiàn)了一個問題，我們考慮這樣的一個抽象
\x.\y.x (\x. x)
如果你要給上述的抽象進(jìn)行De Bruijn轉(zhuǎn)換的話拼岳，內(nèi)層的x的序號應(yīng)該是多少呢枝誊？我們說，它轉(zhuǎn)換后應(yīng)該是這個樣子
\.\.1 (\. 0)
因?yàn)閮?nèi)層的abs綁定的變量就算名字和外層的一樣惜纸，但是我們認(rèn)為名字是無關(guān)的叶撒，所以應(yīng)該重新計(jì)算內(nèi)層abs的De Bruijn值。
這里我們要引入一個上下文存儲的結(jié)構(gòu)耐版，叫做ctx祠够，運(yùn)用它我們就可以很好的解決這個內(nèi)外層param相同，De Bruijn不同的問題粪牲。
使用De Bruijn Index之后古瓤，當(dāng)你替換了之后，你可能還存在于方法棧的頂端腺阳，意思就是被替換的Abs還沒有被完全改變落君，這時候，有可能產(chǎn)生一種誤解亭引，比如下面這樣：
Abs = \x.\y.x = ..1
ide = \t.a = \t.1
替換后Abs 將會在這個方法還沒跳出棧之前被設(shè)置為 \x.\y.\t.1 這個時候就會產(chǎn)生誤解绎速，這個1到底是指的x還是指的a呢？所以我們要引入一些新的方法焙蚓，來解決這個問題纹冤。我們將\t.1升序，升到\t.2购公，然后帶入到Abs中萌京，然后我們考慮代入的深度，因?yàn)橹贿M(jìn)行一次帶入的話我們只需要考慮最外層會不會產(chǎn)生沖突宏浩，如果被你替換的那個值正好是最外層的值知残，這表明你需要再對你的\t.2進(jìn)行一次升序，升到不會產(chǎn)生沖突绘闷，升多少呢橡庞？保險起見，我們應(yīng)該升到超過它的深度印蔗，這樣就不會產(chǎn)生任何誤解扒最。最后，我們再將一開始升序的那一次降下來华嘹，這樣整個替換的過程就完成了吧趣，也不會出現(xiàn)任何問題。
這樣，整個lambda解釋器的基本原理就已經(jīng)講解完了强挫，其他就是代碼怎么寫了岔霸，不過代碼難度其實(shí)也挺小的，你甚至都不需要知道代碼背后是怎么運(yùn)行的俯渤，而是按部就班的按照上面所寫的慢慢敲出來呆细，最后也可以通過OJ，同時在寫代碼的時候八匠，我發(fā)現(xiàn)也并沒有涉及到是否產(chǎn)生誤解這件事情（如果采用我上面的思路的話）絮爷，因此我在想是否對于計(jì)算機(jī)來說，本來這個誤解就不會產(chǎn)生呢梨树？等有空的時候我會用自己的思路重寫一遍代碼坑夯。
