title: Defining a stack data structure and its main operations in lambda calculus
body: <p>I'm trying to define a <code>stack</code> data structure in lambda calculus, using fixed point combinators. I am trying to define two operations, <code>insertion</code> and <code>removal</code> of elements, so, <code>push</code> and <code>pop</code>, 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.</p>
  
  <p>This is my approach on the <code>push</code> operation, and my definition of a <code>stack</code>:</p>
  
  <pre><code>Stack definition:
  STACK = \y.\x.(x y)
  PUSH = \s.\e.(s e)
  </code></pre>
  
  <p>My stacks are initialize with an element to indicate the bottom; I'm using a <code>0</code> here:</p>
  
  <pre><code>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)
  </code></pre>
  
  <p>But now, when I try to insert another element, it does not work, as my initial structure has be deconstructed.</p>
  
  <p>How do I fix the <code>STACK</code> definition or the <code>PUSH</code> definition, and how do I define the <code>POP</code> operation? I guess I'll have to apply a combinator, to allow recursion, but I couldn't figure out how to do it.</p>
  
  <p>Reference: <a href="http://en.wikipedia.org/wiki/Combinatory_logic">http://en.wikipedia.org/wiki/Combinatory_logic</a></p>
  
  <p>Any further explanation or example on the definition of a data structure in lambda calculus will be greatly appreciated.</p>