函数式编程-在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操作?我想我必须应用一个组合子，以允许递归，但我不知道怎么做。

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

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

Answer 1

通过定义一个组合子，它:

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

例如，你可以这样定义一个列表结构:

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的定义，所以我们展开它:

    = (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 =

现在，插入元素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相当于SKI演算的K组合子。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))

同样，这对是Church编码的。一对就是一个高阶函数。对(a, b)表示为高阶函数λf. f a b。它只是一个函数，给定另一个函数f，将f应用于a和b。