在lambda演算中定義堆棧數據結構及其主要操作

Question

我試圖用lambda演算定義一個stack數據結構，使用了定點組合器。我試圖定義兩個操作，insertion和removal的元素，所以push和pop，但我已經能夠定義的唯一一個插入，無法正常工作。刪除我無法弄清楚如何定義。

這是我在push操作方法，和我一stack的定義：

Stack definition: 
STACK = \y.\x.(x y) 
PUSH = \s.\e.(s e) 

我的書庫與元素指示底部初始化;我使用的是0這裏：

stack = STACK 0 = \y.\x.(x y) 0 = \x.(x 0)  // Initialization 
stack = PUSH stack 1 = \s.\e.(s e) stack 1 =  // Insertion 
    = \e.(stack e) 1 = stack 1 = \x.(x 0) 1 = 
    = (1 0) 

但現在，當我嘗試插入另一元素，這是行不通的，因爲我的初始結構已經被解構。

如何修復STACK定義或PUSH定義，以及如何定義POP操作？我想我將不得不申請一個combinator，以允許遞歸，但我不知道如何去做。

參考：http://en.wikipedia.org/wiki/Combinatory_logic

在演算的數據結構的定義的任何進一步的解釋或者例如將不勝感激。

Answer 1

lambda演算中的堆棧只是一個單獨的鏈表。而單鏈表有兩種形式：

nil = λz. λf. z 
cons = λh. λt. λz. λf. f h (t z f) 

這是Church encoding，以表示其catamorphism列表。重要的是，你根本不需要定點組合器。在此視圖中，堆棧（或列表）是一個函數，其中nil大小寫和一個參數用於cons大小寫。例如，該列表[a,b,c]被表示如下：

cons a (cons b (cons c nil)) 

空棧nil相當於K組合子的SKI演算。 cons構造函數是您的push操作。給定一個頭部元素h和尾部的另一個堆棧t，結果是前面的元素爲h的新堆棧。

pop操作只是簡單地將列表分開放置在它的頭部和尾部。你可以用一對函數做到這一點：

head = λs. λe. s e (λh. λr. h) 
tail = λs. λe. s e (λh. λr. r nil cons) 

哪裏e的東西，處理空棧，因爲彈出的空棧是不確定的。這些可以很容易地轉變成一個函數，返回對head和tail：

pop = λs. λe. s e (λh. λr. λf. f h (r nil cons)) 

同樣，一對是編碼教堂。一對只是一個高階函數。該對(a, b)表示爲高階函數λf. f a b。這只是一個函數，給定f的另一個函數f適用於a和b。

Answer 2

通過定義一個組合子，其中：

被定義爲沒有自由變量拉姆達項，因此被定義的任何組合子已經是一個lambda項，

可以定義爲例如，列表結構中，通過寫：

Y = (list definition in lambda calculus) 
Y LIST = (list definition in lambda calculus) LIST 
Y LIST = (element insertion definition in lambda calculus) 

直觀上，並使用一個固定的點組合子，一個可能的定義是 - 考慮\ =拉姆達：

• 列表要麼是空的，要麼是尾隨元素，比如0;
• 或者列表由元素x組成，可能是前一個列表中的另一個列表。

由於它是用一個combinator - 定點組合器來定義的，所以不需要執行更多的應用程序，下面的抽象本身就是一個lambda項。

Y = \f.\y.\x.f (x y) 

現在，將其命名列表：

Y LIST = (*\f*.\y.\x.*f* (x y)) *LIST* -- applying function name 
LIST = \y.\x.LIST (x y), and adding the trailing element "0" 
LIST = (\y.\x.LIST (x y)) 0 
LIST = (*\y*.\x.LIST (x *y*)) *0* 
LIST = \x.LIST (x 0), which defines the element insertion abstraction. 

的不動點組合子Y，或者乾脆Combinator的，讓你考慮list的定義已經有效成員，沒有自由變量，所以，而不需要削減。

然後，您可以添加/插入元素，比如1和2，通過做：

LIST = (\x.LIST (x 0)) 1 2 = 
    = (*\x*.LIST (*x* 0)) *1* 2 = 
    = (LIST (1 0)) 2 = 

但在這裏，我們知道名單的定義，所以我們展開：

= (LIST (1 0)) 2 = 
    = ((\y.\x.LIST (x y)) (1 0)) 2 = 
    = ((*\y*.\x.LIST (x *y*)) *(1 0)*) 2 = 
    = (\x.LIST (x (1 0))) 2 = 

現在，將elemenet 2：

= (\x.LIST (x (1 0))) 2 = 
    = (*\x*.LIST (*x* (1 0))) *2* = 
    = LIST (2 (1 0)) 

哪個都可以擴大，在新插入的情況下，鄰由於LIST是一個用組合器定義的lambda術語，因此r簡單地保持原樣。

擴大對未來的插入：

= LIST (2 (1 0)) = 
    = (\y.\x.LIST (x y)) (2 (1 0)) = 
    = (*\y*.\x.LIST (x *y*)) *(2 (1 0))* = 
    = \x.LIST (x (2 (1 0))) = 
    = (\x.LIST (x (2 (1 0)))) (new elements...) 

我真的很高興我已經能夠得到這一點我自己，但我敢肯定一定是有好的一堆額外的條件，定義時堆棧，堆，或一些fancier結構。

試圖推導出的堆疊的插入/取出抽象 - 沒有所有的步驟一步：

Y = \f.\y.\x.f (x y) 
Y STACK 0 = \x.STACK (x 0) 
STACK = \x.STACK (x 0) 

要在其上執行的操作，讓我們命名空堆棧 - 分配可變（：

stack = \x.STACK (x 0) 

// Insertion -- PUSH STACK VALUE -> STACK 
PUSH = \s.\v.(s v) 
stack = PUSH stack 1 = 
    = (\s.\v.(s v)) stack 1 = 
    = (\v.(stack v)) 1 = 
    = (stack 1) = we already know the steps from here, which will give us: 
    = \x.STACK (x (1 0)) 

stack = PUSH stack 2 = 
    = (\s.\v.(s v)) stack 2 = 
    = (stack 2) = 
    = \x.STACK x (2 (1 0)) 

stack = PUSH stack 3 = 
    = (\s.\v.(s v)) stack 3 = 
    = (stack 3) = 
    = \x.STACK x (3 (2 (1 0))) 

我們再次名這樣的結果，爲我們流行的元素：

stack = \x.STACK x (3 (2 (1 0))) 

// Removal -- POP STACK -> STACK 
POP = \s.(\y.s (y (\t.\b.b))) 
stack = POP stack = 
    = (\s.(\y.s y (\t.\b.b))) stack = 
    = \y.(stack (y (\t.\b.b))) = but we know the exact expansion of "stack", so: 
    = \y.((\x.STACK x (3 (2 (1 0)))) (y (\t.\b.b))) = 
    = \y.STACK y (\t.\b.b) (3 (2 (1 0))) = no problem if we rename y to x (: 
    = \x.STACK x (\t.\b.b) (3 (2 (1 0))) = 
    = \x.STACK x (\t.\b.b) (3 (2 (1 0))) = someone guide me here, if i'm wrong 
    = \x.STACK x (\b.b) (2 (1 0)) = 
    = \x.STACK x (2) (1 0) = 
    = \x.STACK x (2 (1 0)) 

爲了什麼，希望我們彈出元素3。

我試圖自己推導出這個，所以，如果lambda演算有任何限制，我沒有遵循，請指出。