定义栈数据结构及其在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

通过定义组合器，其中：

被定义为没有自由变量的 lambda 项，因此根据定义，任何组合器都已经是 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

  组成，该元素可能是前一个列表中的另一个列表。

由于它是用组合器（定点组合器）定义的，因此无需执行进一步的应用程序，以下抽象本身就是一个 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

，或简称组合器，允许您将 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 =

现在，插入元素

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

。