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, or slide 9 of this talk).

$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, I landed on 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 (and also this paper); 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.

  • $\begingroup$ Thanks, I shouldn't have conflated them. I corrected that, and added a definition for "rooted planar map" (together with a pair of links). $\endgroup$ – Noam Zeilberger May 7 '14 at 7:18
  • 3
    $\begingroup$ 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... $\endgroup$ – Damiano Mazza May 7 '14 at 8:00
  • 3
    $\begingroup$ @DamianoMazza Thanks! I found a free version of the paper at dmg.tuwien.ac.at/dgardy/Papers/LogiqueQuantitative/BCI.pdf, and will have a look. $\endgroup$ – Noam Zeilberger May 7 '14 at 8:07
  • 2
    $\begingroup$ Good! Anyway, for those who read french (Noam, I'm pretty sure you do), Alice's thesis is freely available here. The study of linear and affine $\lambda$-terms constitutes Part III of her thesis and may be even more detailed than in the paper. $\endgroup$ – Damiano Mazza May 7 '14 at 8:07

Your Answer

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

Browse other questions tagged or ask your own question.