I'm new to lambda calculus, and I read all kinds of interesting stuff about encoding data types as functions. Church booleans, numbers and lists. https://en.wikipedia.org/wiki/Church_encoding

Is there a way to encode (binary) trees?


I'll choose to encode binary trees with data in the internal nodes. Intuitively, a tree is either empty leaf, or a triple (data,left subtree,right subtree).

The corresponding Church encoding is:

$$ \begin{array}{l} {\sf Empty} = \lambda e b. e \\ {\sf Branch}\ x\ l\ r = \lambda e b. b x (l e b) (r e b) \end{array} $$

For instance, ${\sf Branch}\ 1\ {\sf Empty}\ ({\sf Branch}\ 2\ {\sf Empty}\ {\sf Empty})$ is an encoded tree. You can easily reduce it to a normal form, if wanted, resulting in $\lambda e b. b \ 1\ e\ (b\ 2\ e\ e)$.

Indeed, the normal form of a tree obtained from the above "constructors" will always start with $\lambda e b.$ and then proceed with the tree where the variable $b$ denotes a "branch" and variable $e$ denotes the empty tree.

To use an encoded tree, you can simply apply it as in $t\ E\ B$, providing two suitable terms $E,B$. This will compute a so-called "fold" of the tree, using constant $E$ and ternary function $B$ over the tree $t$.

For instance, $t\ 0\ (\lambda x l r. x+l+r)$ will result in the sum of all the numbers in the tree $t$, assuming $t$ only contains numbers as data.

It takes a while to convince oneself that this encoding indeed lets us do "whatever we want" with the tree, i.e. run any algorithm over a tree. For primitive recursive algorithms, we can use the encoding itself, directly. For more general algorithms, we can use a fixed point combinator on top of that.

This encoding can be generalized to all the algebraic data types defined through (positive) recursion. Moreover, the encoding can be typed in System F. It is really general.

If you are familiar with some typed functional languages (such as Ocaml or Haskell), I'd recommend you try to implement a "fold" function on trees (with data in the nodes, or in the leaves), or on other algebraic data types. It's a nice exercise which I believe can help a lot in understanding the encoding in its generality.

  • $\begingroup$ How would a "cons" function look for this encoding? $\endgroup$ – jack malkovick Sep 4 '18 at 13:51
  • $\begingroup$ @jackmalkovick What's a "cons" for a tree? There is "Branch" which takes two subtrees and some data and constructs a new tree node on top. $\endgroup$ – chi Sep 4 '18 at 14:46
  • $\begingroup$ sorry... I'm sure you are right. it's just that I'm new to this, and I see "Branch x l r" and I say to myself Branch should apply in order those three arguments. But then I don't see a λa.λb.λc function. Sorry if I'm missing some obvious stuff... $\endgroup$ – jack malkovick Sep 4 '18 at 16:41
  • $\begingroup$ You can define branch = λx.λl.λr.(λe.λb.bx(leb)(reb)) which takes three arguments, and returns the encoded three (which takes other two arguments) $\endgroup$ – chi Sep 4 '18 at 16:45
  • $\begingroup$ all clear now! thanks. you were right "it takes a while to convince oneself ..." :) $\endgroup$ – jack malkovick Sep 5 '18 at 8:04

Sure: take the same idea as a list. Once you can encode a pair a node of a binary tree is either a leaf, represented as (false, value), or a branch, represented as (true, (left-child, right-child)).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.