<p>Consider the following recurrence in two parameters $n$ and $k$:</p>

<p>\begin{aligned}
NF(0,k) &amp;= 0 \\
NF(n,k) &amp;= Neu(n,k) + NF(n-1,k+1) \\
Neu(n,k) &amp;= [n=1 \wedge k=1] + \sum_{l=1}^{n-1}\sum_{i=0}^k Neu(l,i) \cdot NF(n-l,k-i)
\end{aligned}
The expression $NF(n,k)$ counts the number of (untyped) <strong>ordered</strong> <em>lambda terms in normal form</em> of length $n$ with $k$ free variables. Recall that lambda terms are either variables, lambda abstractions or applications
\begin{aligned}
t &amp;::= x \mid \lambda x.t \mid t\ u
\end{aligned}
that a term is <strong>ordered</strong> if every free or bound variable occurs exactly once <strong>and in the order it was introduced</strong>, and that a term is <em>normal</em> if it contains no subterms of the form $(\lambda x.t)\ u$. I take the length of a lambda term to be defined by
\begin{aligned}
|x| &amp;= 1 \\
|\lambda x.t| &amp;= 1 + |t| \\
|t\ u| &amp;= |t| + |u|
\end{aligned}
The recurrence for $NF(n,k)$ is derived from a standard inductive characterization of normal lambda terms (in a mutual induction with "neutral" terms -- for background see <a href="http://www.cs.cmu.edu/~fp/courses/99-atp/handouts/intercal.pdf" rel="nofollow">these notes</a>, or slide 9 of <a href="http://www2.tcs.ifi.lmu.de/~abel/talkMcGill2012Normalization.pdf" rel="nofollow">this talk</a>).</p>

<p>$NF(n,0)$ thus counts the number of <em>closed</em> normal <strong>ordered</strong> lambda terms of length $n$.</p>

<p>I computed $NF(n,0)$ for $n=0..14$, and derived this sequence:
$$
0,0,1,0,2,0,9,0,54,0,378,0,2916,0,24057
$$
Now, dropping all of the 0s and plugging the result into the <a href="http://oeis.org/" rel="nofollow">OEIS</a>, I landed on <a href="https://oeis.org/A000168" rel="nofollow">A000168</a>, whose first few terms are
$$
1, 2, 9, 54, 378, 2916, 24057, 208494
$$
and which user Don Knuth says corresponds to the
$$\text{Number of rooted planar maps with }n\text{ edges.}$$
A nice explanation (with illustrative pictures) of planar maps is given in <a href="http://www.lix.polytechnique.fr/~schaeffe/Biblio/Slides/Tatihou.pdf" rel="nofollow">these slides</a> (and also <a href="http://arxiv.org/pdf/math-ph/0304034v2.pdf" rel="nofollow">this paper</a>); in particular, a <em>planar map</em> is defined as a proper embedding of a connected graph in the plane (considered up to homeomorphisms of the plane), and it is <em>rooted</em> if one root edge is marked on the infinite face and oriented in counterclockwise direction.</p>

<p><strong>Conjecture</strong>: for all $n$, we have
\begin{aligned}
NF(2n,0) &amp;= \#\text{ of rooted planar maps with }n\text{ edges} \\
NF(2n+1,0) &amp;= 0
\end{aligned}</p>

<p>Questions: Is the conjecture true? Can you prove it by exhibiting a simple bijection between <strong>ordered</strong> lambda terms and rooted planar maps?</p>

<hr>

<p><strong>Update</strong> (12 May 2014): I realized that the way I originally explained the conjecture was not strictly speaking correct, since the recurrence for $NF$ actually counts lambda terms which are <strong>ordered</strong> and not merely linear.  (For example, both $\lambda x.\lambda y.x\ y$ and $\lambda x.\lambda y.y\ x$ are linear lambda terms in normal form, but only $\lambda x.\lambda y.x\ y$ is ordered.  Up to normalization, the two ordered linear lambda terms of length 4 are $\lambda x.\lambda y.x\ y$ and $\lambda x.x\ (\lambda y.y)$.) I am still looking for a proof of this conjecture.</p>

CC BY-SA 3.0
2014-05-07T07:18:52.920Z
Thanks, I shouldn't have conflated them. I corrected that, and added a definition for "rooted planar map" (together with a pair of links).
Noam Zeilberger
CC BY-SA 3.0
2014-05-07T08:00:15.320Z
I think the answer is likely to be "yes" to both of your questions. The combinatorics of linear (and affine) lambda-terms was recently studied in depth by Olivier Bodini, Danièle Gardy and Alice Jacquot in _Asymptotics and random sampling for BCI and BCK lambda terms_, Theor. Comput. Sci. 502:227-238, 2013 (I can't find a free online version, sorry).  They study the generating series and also show a bijective correspondence with certain kinds of combinatorial maps similar to the ones you mention. However, their analysis applies to **all** linear $\lambda$-terms, not just the normal forms...
Damiano Mazza
CC BY-SA 3.0
2014-05-07T08:07:31.730Z
@DamianoMazza Thanks! I found a free version of the paper at http://dmg.tuwien.ac.at/dgardy/Papers/LogiqueQuantitative/BCI.pdf, and will have a look.
Noam Zeilberger
CC BY-SA 3.0
2014-05-07T08:07:34.063Z
Good! Anyway, for those who read french (Noam, I'm pretty sure you do), Alice's thesis is freely available [here](http://lipn.univ-paris13.fr/~jacquot/thesejacquot.pdf). The study of linear and affine $\lambda$-terms constitutes Part III of her thesis and may be even more detailed than in the paper.
Damiano Mazza
<graph-theory><co.combinatorics><pl.programming-languages><lambda-calculus><planar-graphs>
A bijection between ordered lambda terms and rooted planar maps?
Noam Zeilberger
# A bijection between ordered lambda terms and rooted planar maps?

(Asked by: username_0 on 2014-05-07)

Consider the following recurrence in two parameters $n$ and $k$:

\begin{aligned}
NF(0,k) &= 0 \\
NF(n,k) &= Neu(n,k) + NF(n-1,k+1) \\
Neu(n,k) &= [n=1 \wedge k=1] + \sum\_{l=1}^{n-1}\sum\_{i=0}^k Neu(l,i) \cdot NF(n-l,k-i)
\end{aligned}
The expression $NF(n,k)$ counts the number of (untyped) **ordered** *lambda terms in normal form* of length $n$ with $k$ free variables. Recall that lambda terms are either variables, lambda abstractions or applications
\begin{aligned}
t &::= x \mid \lambda x.t \mid t\ u
\end{aligned}
that a term is **ordered** if every free or bound variable occurs exactly once **and in the order it was introduced**, and that a term is *normal* if it contains no subterms of the form $(\lambda x.t)\ u$. I take the length of a lambda term to be defined by
\begin{aligned}
|x| &= 1 \\
|\lambda x.t| &= 1 + |t| \\
|t\ u| &= |t| + |u|
\end{aligned}
The recurrence for $NF(n,k)$ is derived from a standard inductive characterization of normal lambda terms (in a mutual induction with "neutral" terms -- for background see [these notes](http://www.cs.cmu.edu/~fp/courses/99-atp/handouts/intercal.pdf), or slide 9 of [this talk](http://www2.tcs.ifi.lmu.de/~abel/talkMcGill2012Normalization.pdf)).

$NF(n,0)$ thus counts the number of *closed* normal **ordered** lambda terms of length $n$.

I computed $NF(n,0)$ for $n=0..14$, and derived this sequence:
$$
0,0,1,0,2,0,9,0,54,0,378,0,2916,0,24057
$$
Now, dropping all of the 0s and plugging the result into the [OEIS](http://oeis.org/), I landed on [A000168](https://oeis.org/A000168), whose first few terms are
$$
1, 2, 9, 54, 378, 2916, 24057, 208494
$$
and which user Don Knuth says corresponds to the
$$\text{Number of rooted planar maps with }n\text{ edges.}$$
A nice explanation (with illustrative pictures) of planar maps is given in [these slides](http://www.lix.polytechnique.fr/~schaeffe/Biblio/Slides/Tatihou.pdf) (and also [this paper](http://arxiv.org/pdf/math-ph/0304034v2.pdf)); in particular, a *planar map* is defined as a proper embedding of a connected graph in the plane (considered up to homeomorphisms of the plane), and it is *rooted* if one root edge is marked on the infinite face and oriented in counterclockwise direction.

**Conjecture**: for all $n$, we have
\begin{aligned}
NF(2n,0) &= \#\text{ of rooted planar maps with }n\text{ edges} \\
NF(2n+1,0) &= 0
\end{aligned}

Questions: Is the conjecture true? Can you prove it by exhibiting a simple bijection between **ordered** lambda terms and rooted planar maps?

---

**Update** (12 May 2014): I realized that the way I originally explained the conjecture was not strictly speaking correct, since the recurrence for $NF$ actually counts lambda terms which are **ordered** and not merely linear. (For example, both $\lambda x.\lambda y.x\ y$ and $\lambda x.\lambda y.y\ x$ are linear lambda terms in normal form, but only $\lambda x.\lambda y.x\ y$ is ordered. Up to normalization, the two ordered linear lambda terms of length 4 are $\lambda x.\lambda y.x\ y$ and $\lambda x.x\ (\lambda y.y)$.) I am still looking for a proof of this conjecture.

**Tags:** graph-theory, co.combinatorics, pl.programming-languages, lambda-calculus, planar-graphs
> **Comments:**
> **username_0**: Thanks, I shouldn't have conflated them. I corrected that, and added a definition for "rooted planar map" (together with a pair of links).  
> **username_1**: I think the answer is likely to be "yes" to both of your questions. The combinatorics of linear (and affine) lambda-terms was recently studied in depth by Olivier Bodini, Danièle Gardy and Alice Jacquot in _Asymptotics and random sampling for BCI and BCK lambda terms_, Theor. Comput. Sci. 502:227-238, 2013 (I can't find a free online version, sorry).  They study the generating series and also show a bijective correspondence with certain kinds of combinatorial maps similar to the ones you mention. However, their analysis applies to **all** linear $\lambda$-terms, not just the normal forms...  
> **username_0**: @DamianoMazza Thanks! I found a free version of the paper at http://dmg.tuwien.ac.at/dgardy/Papers/LogiqueQuantitative/BCI.pdf, and will have a look.  
> **username_1**: Good! Anyway, for those who read french (Noam, I'm pretty sure you do), Alice's thesis is freely available [here](http://lipn.univ-paris13.fr/~jacquot/thesejacquot.pdf). The study of linear and affine $\lambda$-terms constitutes Part III of her thesis and may be even more detailed than in the paper.  

---

## 0 answers

