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

Question

我正在尝试使用固定点组合器在lambda演算中定义一个数据结构stack，并定义两个操作：元素的插入和移除，即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演算中定义数据结构的任何进一步解释或示例将不胜感激。

- Rubens

---

单向链表不就是一个完美的栈吗，push等同于cons，pop等同于head/tail？我提出这个问题是因为单向链表已经被实现了无数次，可能更容易理解。 - user395760

@delnan，这与我在答案中提出的方法接近，因为我使用了list定义的一部分来定义stack。 - Rubens

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 =

现在，插入元素2：

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

在有新插入时，这两者都可以进行扩展，或者仅保持原样。原因是LIST是一个使用组合子定义的λ项。

为将来的插入进行扩展：

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

我尝试自己推导，如果有来自λ演算的限制我没有遵循，请指出。

- Rubens

---

我们如何定义栈和队列呢？ - Anupam Tamrakar

@AnupamTamrakar 我已经添加了stack的插入/删除功能，请查看。敬礼！ - Rubens

Answer 2

在lambda演算中，栈就是一个单向链表。而单向链表有两种形式：

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

这是使用 Church编码，并以其折叠表示列表。重要的是，您根本不需要一个固定点组合器。在这个视图中，堆栈（或列表）是一个函数，它接受一个参数作为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。

- Apocalisp

---

谢谢您的回复，这种方法更接近我在sml中所见到的。考虑到我的方法可能不必要，正如您所指出的那样，但是使用固定点组合器，我已经得到了一些看起来确实可以工作的东西。有什么问题吗？还是只是不符合标准而已？如果没有问题，您介意看一下我在悬赏信息中提到的应用程序吗？谢谢！ - Rubens

我不认为你的 Y 实现有任何错误，只是过于复杂了。Y 组合子比你需要的更加强大，因为它允许你构造无限堆栈。 - Apocalisp

啊，这就是我一直在寻找的确认！非常感谢您的耐心，我完全同意我编写函数的方式甚至更加混乱。我会等到赏金结束之前再等待任何进一步的评论来奖励这篇文章。再次感谢！ - Rubens