title: How to check for empty list in pure (untyped) lambda calculus in DrRacket?
body: <p>I'm trying to build lists in pure lambda calculus (actually Binary Trees masquerading as lists (in the form of <code>[Root, [Left SubTree], [Right SubTree]]</code>), but for the purpose of this specific question, we can talk about general lists in lambda calculus).</p>
  
  <p>Some basic definitions of lambda calculus (expressed in Racket syntax) I'll be using in this question:</p>
  
  <pre><code>(define true (lambda (x) (lambda (y) x)))
  (define false (lambda (x) (lambda (y) y)))
  (define if (lambda (x) (lambda (y) (lambda (z) ((x y) z)))))
  
  ; I'm using Parigot Encodings to represent numbers
  (define zero (lambda (s) (lambda (z) z)))
  (define one (lambda (s) (lambda (z) ((s zero) z))))
  (define two (lambda (s) (lambda (z) ((s one) ((s zero) z)))))
  
  ; Here are some converter functions for debugging/printing
  (define (p-&gt;int n)
     ((n (lambda(x) add1)) 0))
  
  (define (int-&gt;p i)
     (if (zero? i)
         (lambda (f) (lambda (x) x))
         (let ((m (int-&gt;p (- i 1))))
           (lambda (f) (lambda (x) ((m f) ((f m) x)))) )))
  
  ; Building blocks for Lists. A list consists of a single element Head,
  ; followed by the rest of the list (Tail). Lists are thus recursively
  ; defined. An empty list consists of only the element 'nil'
  (define mkpair (lambda (a) (lambda (b) (lambda (c) ((c a) b)))))   
  (define Head (lambda (p) (p true)))
  (define Tail (lambda (p) (p false)))
  (define nil false)
  </code></pre>
  
  <p>For operating on such lists, I need to detect when a list is empty (for example, to detect a leaf node while doing a binary search on a Binary Search Tree represented as a list). The following <a href="http://safalra.com/lambda-calculus/tuples-and-lists/" rel="nofollow noreferrer">link</a> gives that function as <code>isempty = λl.l(λab.false)true</code>, which I've defined in Racket as follows:</p>
  
  <pre><code>(define Null? (lambda (p) (p (lambda (x) (lambda (y) false)))true))
  </code></pre>
  
  <p>This seemingly works, as you can see in the following:</p>
  
  <pre><code>(p-&gt;int (((if (Null? (Head ((mkpair nil) one)))) two) one))
  </code></pre>
  
  <p>In words, the above application checks if the head of the list <code>[nil, one]</code> is an empty list (containing only <code>nil</code>), and if so, evaluates to <code>two</code>, which when fed to converter function <code>p-&gt;int</code>, produces <code>2</code>. All good, except the <code>Null?</code> function doesn't seem to evaluate to <code>false</code>, as seen by the below snippet:</p>
  
  <pre><code>(p-&gt;int (((if (Null? (Tail ((mkpair nil) one)))) two) one))
  </code></pre>
  
  <p>Which also evaluates to <code>2</code> in Racket.</p>
  
  <p>Can someone point me out in my error, which i hope is something syntactical that I can't detect! </p>
  
  <p>PS: Just in case I'm totally approaching this the wrong way, I'm trying to implement a Binary Search Tree in pure lambda calculus in Racket. Any pointers to my final goal would be greatly appreciated - I've listed one of the approaches that I took.</p>
  
  <p>(For some additional reading about the function I'm trying to simulate, see <a href="https://math.stackexchange.com/q/65847/7959">this</a>).</p>