通过定义一个组合子,该组合子:
被定义为没有自由变量的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 =
= () *(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)) =
= ) *(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 = \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 = \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
。
我尝试自己推导,如果有来自λ演算的限制我没有遵循,请指出。
push
等同于cons
,pop
等同于head/tail
?我提出这个问题是因为单向链表已经被实现了无数次,可能更容易理解。 - user395760list
定义的一部分来定义stack
。 - Rubens