在lambda演算中定义堆栈数据结构及其主要操作

Question

我正在尝试stack使用定点组合器在lambda演算中定义数据结构.我试图定义两个操作,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操作？我想我将不得不应用组合器,以允许递归,但我无法弄清楚如何做到这一点.

参考:http://en.wikipedia.org/wiki/Combinatory_logic

关于lambda演算中数据结构定义的任何进一步解释或示例将不胜感激.

Answer 1

通过定义组合器,其中:

被定义为没有自由变量的lambda项,因此根据定义,任何组合子都已经是一个lambda项,

例如,您可以通过编写以下内容来定义列表结构:

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

直觉上,使用定点组合器,可能的定义是 - 考虑\ = lambda:

• 列表是空的,后跟一个尾随元素,比如说0;
• 或者由一个元素形成一个列表,该元素x可以是前一个列表中的另一个列表.

由于它是用组合器 - 定点组合器定义的 - 所以不需要执行进一步的应用程序,以下抽象本身就是一个lambda术语.

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

现在,将其命名为LIST:

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,或简称组合器,允许您认为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项,因此在新插入的情况下可以扩展,或者简单地保留原样.

扩展以供将来插入:

    = 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...)

我很高兴自己能够得到这个,但是我很确定在定义堆栈,堆或更高级的结构时必须有一些好的额外条件.

试图导出堆栈插入/删除的抽象 - 没有一步一步:

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演算的限制我没有遵循,请指出.

Answer 2

lambda演算中的堆栈只是一个单链表.单链表有两种形式:

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

这是教会编码,其列表表示为其变形.重要的是,您根本不需要定点组合器.在此视图中,堆栈(或列表)是一个函数,它为nil案例提供一个参数,为cons案例提供一个参数.例如,列表[a,b,c]如下所示:

cons a (cons b (cons c nil))

空堆栈nil相当于KSKI演算的组合子.该cons构造是你的push操作.给定一个head元素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.