By defining a combinator, which:
is defined as a lambda term with no free variables, so by definition any combinator is already a lambda term,
you can define, for example, a list structure, by writing:
Y = (list definition in lambda calculus)
Y LIST = (list definition in lambda calculus) LIST
Y LIST = (element insertion definition in lambda calculus)
Intuitively, and using a fixed point combinator, a possible definition is -- consider \ = lambda:
- a list is either empty, followed by a trailing element, say
0
;
- or a list is formed by an element
x
, that may be another list inside the former one.
Since it's been defined with a combinator -- fixed point combinator --, there's no need to perform further applications, the following abstraction is a lambda term itself.
Y = \f.\y.\x.f (x y)
Now, naming it a 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.
The fixed point combinator Y
, or simply combinator, allows you to consider the definition of LIST already a valid member, with no free variables, so, with no need for reductions.
Then, you can append/insert elements, say 1 and 2, by doing:
LIST = (\x.LIST (x 0)) 1 2 =
= (*\x*.LIST (*x* 0)) *1* 2 =
= (LIST (1 0)) 2 =
But here, we know the definition of list, so we expand it:
= (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 =
Now, inserting elemenet 2
:
= ( \x.LIST (x (1 0)) ) 2 =
= ( *\x*.LIST (*x* (1 0)) ) *2* =
= LIST (2 (1 0))
Which can both be expanded, in case of a new insertion, or simply left as is, due to the fact that LIST is a lambda term, defined with a combinator.
Expanding for future insertions:
= 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...)
I'm really glad I've been able to derive this myself, but I'm quite sure there must be some good bunch of extra conditions, when defining a stack, a heap, or some fancier structure.
Trying to derive the abstraction for a stack insertion/removal -- without all the step-by-step:
Y = \f.\y.\x.f (x y)
Y STACK 0 = \x.STACK (x 0)
STACK = \x.STACK (x 0)
To perform the operation upon it, let's name an empty stack -- allocating a variable (:
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)))
And we, once again, name this result, for us to pop the elements:
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))
For what, hopefully, we have the element 3
popped.
I've tried to derive this myself, so, if there's any restriction from lambda calculus I didn't followed, please, point it out.