lambda - 在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演算中的堆栈只是一个单链表。单链表有两种形式:

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

这是 Church encoding，列表表示为其 catamorphism。重要的是，您根本不需要定点组合器。在此 View 中，堆栈(或列表)是一个函数，它为 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))

再次，这对是教会编码的。一对只是高阶函数。对 (a, b)表示为高阶函数 λf. f a b。这只是一个函数，给了另一个函数 f，将 f应用于 a和 b。