I'm trying to define a stack data structure in lambda calculus, using fixed point combinators. I am trying to define two operations, insertion and removal of elements, so, push and pop, but the only one I've been able to define, the insertion, is not working properly. The removal I could not figure out how to define.
This is my approach on the push operation, and my definition of a stack:
Stack definition:
STACK = \y.\x.(x y)
PUSH = \s.\e.(s e)
My stacks are initialize with an element to indicate the bottom; I'm using a 0 here:
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)
But now, when I try to insert another element, it does not work, as my initial structure has be deconstructed.
How do I fix the STACK definition or the PUSH definition, and how do I define the POP operation? I guess I'll have to apply a combinator, to allow recursion, but I couldn't figure out how to do it.
Reference: http://en.wikipedia.org/wiki/Combinatory_logic
Any further explanation or example on the definition of a data structure in lambda calculus will be greatly appreciated.
A stack in the lambda calculus is just a singly linked list. And a singly linked list comes in two forms:
nil = λz. λf. z
cons = λh. λt. λz. λf. f h (t z f)
This is Church encoding, with a list represented as its catamorphism. Importantly, you do not need a fixed point combinator at all. In this view, a stack (or a list) is a function taking one argument for the nil case and one argument for the cons case. For example, the list [a,b,c] is represented like this:
cons a (cons b (cons c nil))
The empty stack nil is equivalent to the K combinator of the SKI calculus. The cons constructor is your push operation. Given a head element h and another stack t for the tail, the result is a new stack with the element h at the front.
The pop operation simply takes the list apart into its head and tail. You can do this with a pair of functions:
head = λs. λe. s e (λh. λr. h)
tail = λs. λe. s e (λh. λr. r nil cons)
Where e is something that handles the empty stack, since popping the empty stack is undefined. These can be easily turned into one function that returns the pair of head and tail:
pop = λs. λe. s e (λh. λr. λf. f h (r nil cons))
Again, the pair is Church encoded. A pair is just a higher-order function. The pair (a, b) is represented as the higher order function λf. f a b. It's just a function that, given another function f, applies f to both a and b.