patternMinor
Encoding (binary) trees using lambda calculus
Viewed 0 times
calculustreesbinaryusingencodinglambda
Problem
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?
https://en.wikipedia.org/wiki/Church_encoding
Is there a way to encode (binary) trees?
Solution
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.
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.
Context
StackExchange Computer Science Q#96922, answer score: 5
Revisions (0)
No revisions yet.