Defining the stack data structure and basic operations in the lambda calculus

Question

I am trying to determine the stack data structure in lambda calculus using fixed point combinators. I am trying to define two operations: insertion and removal elements, so push and pop , but the only one I could determine, insertion is not working properly. Removal I could not figure out how to determine.

This is my approach to push operation, and my definition of stack :

 Stack definition: STACK = \y.\x.(xy) PUSH = \s.\e.(se) 

My stacks are initialized with an element indicating the bottom; I use 0 here:

 stack = STACK 0 = \y.\x.(xy) 0 = \x.(x 0) // Initialization stack = PUSH stack 1 = \s.\e.(se) 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, since my original structure was deconstructed.

How to fix stack definition or push definition and how to define pop operation? I think I will have to use a combinator to allow recursion, but I could not figure out how to do this.

Link: http://en.wikipedia.org/wiki/Combinatory_logic

Any additional explanation or example to determine the data structure in the lambda calculus will be appreciated.

Answer 1

A lambda calculus is just a linked list. And a singly linked list is presented in two forms:

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

This is Church coding , a list of which is presented as catamorphism . It is important to note that you do not need a fixed-point combinator. In this view, the stack (or list) is a function that takes one argument for the case of nil and one argument for the case of cons . For example, the list [a,b,c] is represented as follows:

 cons a (cons b (cons c nil)) 

The empty stack nil equivalent to the combinatorial K calculus SKI. The cons constructor is your push operation. Given the head element h and another stack t for the tail, the result is a new stack with the element h in front.

The pop operation simply translates the list to the head and tail. You can do this with a couple of functions:

 head = λs. λe. se (λh. λr. h) tail = λs. λe. se (λh. λr. r nil cons) 

Where e is what handles the empty stack, since popping the empty stack is undefined. They can easily be turned into a single function that returns a pair of head and tail :

 pop = λs. λe. se (λh. λr. λf. fh (r nil cons)) 

Again, the pair is encoded by the Church. A pair is simply a function of a higher order. The pair (a, b) is represented as a function of a higher order λf. fab λf. fab . It is simply a function that, when using another function f applies f to a and b .

Answer 2

Defining a combinator that:

is defined as a lambda member without free variables, therefore, by definition, any combinator is already a lambda member,

you can define, for example, the structure of the list 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 definition is possible - consider \ = lambda:

• the list is either empty, and the next trailing element, for example 0 ;
• or the list is formed by the element x , which may be another list inside the previous one.

Since it was defined with a combinator - a fixed-point combinator - there is no need to run additional applications, the next abstraction is the lambda term itself.

 Y = \f.\y.\xf (xy) 

Now, calling it a LIST:

 Y LIST = (*\f*.\y.\x.*f* (xy)) *LIST* -- applying function name LIST = \y.\x.LIST (xy), and adding the trailing element "0" LIST = (\y.\x.LIST (xy) ) 0 LIST = (*\y*.\x.LIST (x *y*) ) *0* LIST = \x.LIST (x 0), which defines the element insertion abstraction. 

A fixed-point combinator Y or just a combinator allows you to consider the definition of LIST as a valid member without free variables, therefore, without the need for abbreviations.

Then you can add / insert elements, for example 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 a list, so we expand it:

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

Now by inserting element 2 :

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

What can be expanded in case of a new insertion or simply left as is, due to the fact that LIST is a lambda member defined by a combinator.

Extension for future insertions:

  = LIST (2 (1 0)) = = (\y.\x.LIST (xy)) (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 am very glad that I was able to do this myself, but I am sure that there should be something good in defining a stack, heap or some more attractive structure. >

Trying to get an abstraction to insert / remove a stack - without a phased step:

 Y = \f.\y.\xf (xy) Y STACK 0 = \x.STACK (x 0) STACK = \x.STACK (x 0) 

To perform an operation on it, let's call an empty stack - allocation of a variable (:

 stack = \x.STACK (x 0) // Insertion -- PUSH STACK VALUE -> STACK PUSH = \s.\v.(sv) stack = PUSH stack 1 = = ( \s.\v.(sv) ) 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.(sv) ) stack 2 = = ( stack 2 ) = = \x.STACK x (2 (1 0)) stack = PUSH stack 3 = = ( \s.\v.(sv) ) stack 3 = = ( stack 3 ) = = \x.STACK x (3 (2 (1 0))) 

And again we will name this result so that we can put the elements:

 stack = \x.STACK x (3 (2 (1 0))) // Removal -- POP STACK -> STACK POP = \s.(\ys (y (\t.\bb))) stack = POP stack = = ( \s.(\ys y (\t.\bb)) ) stack = = \y.(stack (y (\t.\bb))) = but we know the exact expansion of "stack", so: = \y.((\x.STACK x (3 (2 (1 0))) ) (y (\t.\bb))) = = \y.STACK y (\t.\bb) (3 (2 (1 0))) = no problem if we rename y to x (: = \x.STACK x (\t.\bb) (3 (2 (1 0))) = = \x.STACK x (\t.\bb) (3 (2 (1 0))) = someone guide me here, if i'm wrong = \x.STACK x (\bb) (2 (1 0)) = = \x.STACK x (2) (1 0) = = \x.STACK x (2 (1 0)) 

For what, I hope, we have element 3 .

I tried to get it myself, so if there were no restrictions on the lambda calculus, I did not follow, please indicate this.