\documentclass[finalversion]{FPSAC2023}
\articlenumber{5} % option ``revision'' for revision

%% note that the class file already loads {amsmath, amsthm, amssymb}
\usepackage{graphicx}
\usepackage{color}
\usepackage[backend=bibtex]{biblatex} % cannot set alphabetic style...
\addbibresource{lambda-bipartite.bib}

% Theorem and the like
\newtheorem{thm}{Theorem}[section]
\newtheorem{prop}[thm]{Proposition}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{coro}[thm]{Corollary}
\newtheorem{conj}[thm]{Conjecture}
\theoremstyle{remark}
\newtheorem{rmk}{Remark}
\newtheorem{example}[thm]{Example}
\theoremstyle{definition}
\newtheorem{defn}[thm]{Definition}
\newtheorem{constr}[thm]{Construction}

\newcommand{\unary}{\operatorname{unary}}
\newcommand{\leaf}{\operatorname{leaf}}
\newcommand{\conn}{\mathcal{C}}
\newcommand{\redskl}{\mathcal{RS}}
\newcommand{\skl}{\mathcal{S}}
\newcommand{\sklf}{\operatorname{Sk}}
\newcommand{\syndiag}{\operatorname{Diag}}
\newcommand{\vtree}{\mathcal{V}}
\newcommand{\bipartite}{\mathcal{B}}
\newcommand{\planar}{\mathcal{M}}
\newcommand{\onecorner}{\mathcal{U}}

\newcommand{\excess}{\operatorname{ex}}
\newcommand{\uchain}{\operatorname{uc}}
\newcommand{\applv}{\operatorname{Appl}_{v}}
\newcommand{\appla}{\operatorname{Appl}_{a}}

\newcommand{\lnode}{\operatorname{lnode}}
\newcommand{\znode}{\operatorname{znode}}
\newcommand{\rlabel}{\operatorname{rlabel}}
\newcommand{\edge}{\operatorname{edge}}

\newcommand{\white}{\operatorname{white}}
\newcommand{\black}{\operatorname{black}}
\newcommand{\face}{\operatorname{face}}
\newcommand{\outdeg}{\operatorname{outdeg}}

\newcommand{\outvertex}{\operatorname{outv}}

% Useful commands
\newcommand{\tdef}[1]{\textcolor{blue}{\emph{#1}}} % Definition of terms
\newcommand{\defs}{\stackrel{\mathsf{def}}{=}} % Definition in equations
\newcommand{\horiz}{\begin{center}\rule{0.3\textwidth}{0.5pt}\end{center}}
\newcommand{\insertfig}[2]{\includegraphics[page=#1, width=#2\textwidth]{fig-ipe.pdf}}

\title[Bijections between planar maps and planar linear normal $\lambda$-terms with connectivity condition]{Bijections between planar maps and planar linear normal $\lambda$-terms with connectivity condition}

\author{Wenjie Fang\thanks{\href{mailto:wenjie.fang@univ-eiffel.fr}{wenjie.fang@univ-eiffel.fr}. Wenjie Fang is partially supported by ANR LambdaComb (ANR-21-CE48-0017). }\addressmark{1}}

\address{\addressmark{1}Univ Gustave Eiffel, CNRS, LIGM, F-77454 Marne-la-Vallée, France}

\received{\today}
%\revised{} % reserved for revised version

\abstract{The enumeration of linear $\lambda$-terms has attracted quite some attention recently, partly due to their link to combinatorial maps. In 2019, Zeilberger and Reed conjectured that 3-connected planar linear normal $\lambda$-terms have the same counting formula as bipartite planar maps. In this article, we settle this conjecture by giving a direct bijection. We also explore its enumerative consequences. With a similar approach, we give a new and direct bijection between planar linear normal $\lambda$-terms and planar maps, whose restriction to 2-connected $\lambda$-terms leads to loopless planar maps.}

\resume{L'énumération des $\lambda$-termes linéaires a récemment attiré un intérêt grâce à leur lien avec les cartes combinatoires. En 2019, Zeilberger et Reed ont conjecturé que les $\lambda$-termes linéaires planaires normaux 3-connexes sont comptés par la même formule que les cartes planaires bipartites. Dans cet article, nous provons cette conjecture grâce à une bijection directe. Nous explorons aussi ses conséquences énumératives. Avec la même approche, nous présentons une nouvelle bijection entre les $\lambda$-termes linéaires planaires normaux et les cartes planaires, qui est directe et dont la restriction aux $\lambda$-termes 2-connexes donne les cartes planaires sans boucle.}

\keywords{Bijection, $\lambda$-term, combinatorial map, edge-connectivity, enumeration.}

\begin{document}

\maketitle

As a well-known model of computation, $\lambda$-calculus has been well studied in logic and related fields. However, its enumerative aspect only attracted attention relatively recently. One of the most well-studied family is that of \textit{linear $\lambda$-terms}, partly due to its connections with combinatorial maps. Such connections were pioneered by Bodini, Gardy and Jacquot in~\cite{lambda-cubic}, where a simple bijection from linear $\lambda$-terms to cubic maps was given. This bijection has led to the study of asymptotic properties and statistics distribution of related $\lambda$-terms (see, \textit{e.g.}, \cite{generalized-BCI, lambda-cubic, linear-stat}), and connections to other objects \cite{chord-diagram-bridgeless}.

Independently, Zeilberger and Giorgetti found in \cite{planar-lambda} a bijection between \emph{planar linear normal $\lambda$-terms} and planar maps, which is not a simple restriction of the one in \cite{lambda-cubic}. Moreover, when restricted to $\lambda$-terms that are also \emph{unitless}, \textit{i.e.}, without closed sub-term, this bijection leads to bridgeless planar maps. The unitless condition here is equivalent to the 2-connectedness of the syntactic diagram of the $\lambda$-term. Such connections lead naturally to the consideration of higher connectivity conditions on $\lambda$-terms. In a talk at CLA 2019 \cite{3-conn-conj}, Zeilberger and Reed considered a possible interpretation of connectivity in logic. Based on experiments, they proposed the following conjecture.

\begin{conj}[\cite{3-conn-conj}] \label{conj:3-conn}
  Planar 3-connected linear normal $\lambda$-terms with $n+2$ variables are counted by the same formula as bipartite planar maps with $n$ edges given in \cite{Tutte-census}:
  \[
    \frac{2^n}{(n+1)(n+2)} \binom{2n+1}{n}.
  \]
\end{conj}

In a talk at CLA 2020 \cite{grygiel-yu}, Grygiel and Yu tried to relate these 3-connected $\lambda$-terms to~$\beta(0,1)$-trees, which are in bijection with bicubic planar maps \cite{desc-tree} and thus with bipartite planar maps \cite{Tutte-census}, and succeeded in a few special cases. The key of their work is a characterization of skeletons of such $\lambda$-terms (\cref{prop:chara-lambda}).

In this article, based on the characterization given by Grygiel and Yu in \cite{grygiel-yu}, we prove \cref{conj:3-conn} by giving a bijection between 3-connected planar linear normal $\lambda$-terms and bipartite planar maps via the so-called \emph{degree trees} defined in \cite{fang-bipartite}.

\begin{thm} \label{thm:main-3-conn}
  For $n \geq 2$, there is a bijection between 3-connected planar linear normal $\lambda$-terms with $n$ variables and bipartite planar maps with $n-2$ edges.
\end{thm}

Using this new bijection, we study the refined enumeration of such $\lambda$-terms under several statistics, and also their asymptotic distribution, which are all done by translating known results on bipartite planar maps.

With a similar approach, we also give a new and direct bijection between planar linear normal $\lambda$-terms and planar maps, whose restriction to 2-connected $\lambda$-terms leads to loopless planar maps.

\begin{thm} \label{thm:main-conn}
  There is a direct bijection between planar linear normal $\lambda$-terms with $n$ variables and planar maps with $n-1$ edges. Furthermore, it sends those $\lambda$-terms that are also 2-connected to loopless planar maps.
\end{thm}

For the second bijection, we define a family of node-labeled trees called \emph{v-trees}, which can be seen as description trees (see \cite{desc-tree}) of planar maps under a seemingly new recursive decomposition. We then give direct bijections from v-trees to both planar maps and planar linear normal $\lambda$-terms, thus linking the two families.

The rest of the article is organized as follows. In \cref{sec:prelim}, we define the objects that we study. Then we characterize in \cref{sec:chara} the skeletons of planar linear normal $\lambda$-terms with different connectivity conditions, which is then used in \cref{sec:bij-3} to give a bijection from 3-connected planar linear normal $\lambda$-terms to degree trees, which are in bijection with bipartite maps. In \cref{sec:bij-2}, we define v-trees and relate them bijectively to planar linear normal $\lambda$-terms, and a direct bijection to planar maps is given in \cref{sec:map-decomp}.

Due to space limit, some results and proofs are omitted in this extended abstract. Readers are referred to the full version~\cite{full-version} for all details.

\section{Preliminaries} \label{sec:prelim}

In mathematical logic, \tdef{$\lambda$-terms} can be defined recursively using three constructions:
\begin{itemize}
\item Atoms, which are variables $x, y, \ldots$;
\item Application $t \; u$ with two $\lambda$-terms $t$ and $u$;
\item Abstraction $\lambda x.t$ with $t$ a $\lambda$-term and $x$ a variable. We say that every atom with the variable $x$ in $t$ is \tdef{bound} by the abstraction, if not yet bound.
\end{itemize}

In the following, we consider $\lambda$-terms up to \tdef{$\alpha$-renaming}, \textit{i.e.}, changing the name of a variable in an abstraction and all atoms it binds. A $\lambda$-term $t$ is \tdef{closed} if all atoms are bound, and it is \tdef{linear} if it is closed and each abstraction binds exactly one atom. Computation on $\lambda$-terms is done using \tdef{$\beta$-reduction}: we replace a sub-term of the form $(\lambda x. u) v$ in a $\lambda$-term by $u[x \leftarrow v]$, where the sub-term $u$ has all its atoms of $x$ replaced by a copy of $v$. A $\lambda$-term is \tdef{$\beta$-normal} (or simply \tdef{normal}) if no $\beta$-reduction is possible. Given a $\lambda$-term $t$, its \tdef{skeleton} $\sklf(t)$ is a plane unary-binary tree defined recursively as follows.
\begin{itemize}
\item If $t$ is an atom, then $\sklf(t)$ is a leaf;
\item If $t = u \; v$, then $\sklf(t)$ is rooted at a binary node, with $\sklf(u)$ its left sub-tree, and $\sklf(v)$ its right sub-tree;
\item If $t = \lambda x.u$, then $\sklf(t)$ is rooted at a unary node, with $\sklf(u)$ its only sub-tree.
\end{itemize}
We identify atoms and abstractions in $t$ with their corresponding leaves and unary nodes in $\sklf(t)$. Many properties of $t$ can be read off from $\sklf(t)$. For instance, $t$ is normal if no binary node of $\sklf(t)$ has a unary node as its left child. The \tdef{size} of a skeleton is its number of leaves, which is also the number of atoms in the original $\lambda$-term.

The skeleton $\sklf(t)$ of a $\lambda$-term $t$ still misses the binding relations between atoms and abstractions. The \tdef{syntactic diagram} (or simply \tdef{diagram}) of a $\lambda$-term $t$, denoted by $\syndiag(t)$, is obtained from its skeleton $\sklf(t)$ by replacing each leaf by an edge from its parent to the unary node of abstraction that binds its atom. It is clear that two different $\lambda$-terms never share the same diagram. Given a leaf of $\sklf(t)$, we draw the corresponding edge starting from the parent of the leaf, traveling counter-clockwise and entering the unary node from its right. If such a drawing can be done without intersection, then the $\lambda$-term $t$ is \tdef{planar}. \cref{fig:lambda-example} gives an example of a planar $\lambda$-term, with its skeleton and syntactic diagram. We note that this $\lambda$-term is also normal.

\begin{figure}
  \centering
  \insertfig{6}{0.6}
  \caption{Example of a normal planar $\lambda$-term, its skeleton and syntactic diagram.}
  \label{fig:lambda-example}
\end{figure}

As diagrams are graphs, we may transfer notions in graph theory to $\lambda$-terms. If the diagram of a $\lambda$-term $t$ is \tdef{2-edge-connected} (or simply \tdef{2-connected}), \textit{i.e.}, the removal of any edge does not disconnect the diagram, then we say that $t$ is \tdef{2-connected}. Similarly, a $\lambda$-term $t$ is \tdef{3-edge-connected} (or simply \tdef{3-connected}) if the removal of any two edges in $\syndiag(t)$ does not disconnect $\syndiag(t)$, except possibly the two edges adjacent to the root of $\sklf(t)$ when $t$ starts with an abstraction binding one atom.

In this article, we consider planar linear $\lambda$-terms. For planarity, given the skeleton of such a $\lambda$-terms, we take a clockwise contour walk starting from the root, in which we read off the unary nodes and leaves on first visit. By planarity, we must obtain a well-parenthesized word with each abstraction paired up with the atom it binds. As the binding of atoms is given by planarity, we may identify planar linear $\lambda$-terms with their skeletons. By abuse of notation, given a skeleton $S$ of some planar linear $\lambda$-term $t$, we denote by $\syndiag(S)$ the diagram $\syndiag(t)$ of $t$.

In the following, we relate previously defined $\lambda$-terms to planar maps. A \tdef{planar map} is an embedding of a graph on the plane defined up to orientation-preserving continuous deformations, such that its edges only intersect at vertices. The connected components of the complement of the embedding are called the \tdef{faces}. The face that extends to infinity is called the \tdef{outer face}. Furthermore, we only consider \tdef{rooted} planar maps here, which means that we mark a special corner on the outer face, called the \tdef{root corner}. The edge next to the root corner in the clockwise order is called the \tdef{root edge}, and the vertex of the corner is called the \tdef{root vertex}. We also consider the \tdef{empty map}, which consists of a single vertex. A planar map is \tdef{bipartite} if we can color its vertices with black and white such that each edge links a black and a white vertex. The root vertex is colored black by convention.

\section{Characterization of planar linear normal $\lambda$-terms with connectivity conditions} \label{sec:chara}

We may classify planar linear $\lambda$-terms by the connectivity of their diagrams. We denote by $\conn^{(1)}_n$ the set of planar linear normal $\lambda$-terms of size $n$. Similarly, we denote by $\conn^{(2)}_n$ (resp. $\conn^{(3)}_n$) the terms that are 2-connected (resp. 3-connected) in $\conn^{(1)}_n$. We take $\conn^{(1)} = \bigcup_{n \geq 1} \conn^{(1)}_n$, and we define $\conn^{(2)}$ and $\conn^{(3)}$ similarly. It is clear that $\conn^{(3)} \subset \conn^{(2)} \subset \conn^{(1)}$.

Due to the correspondence between planar linear $\lambda$-terms and their skeletons, in the following we will focus on skeletons instead of $\lambda$-terms. We denote by $\skl^{(1)}_n$ (resp. $\skl^{(2)}_n$ and $\skl^{(3)}_n$) the set of skeletons of terms in $\conn^{(1)}_n$ (resp. $\conn^{(2)}_n$ and $\conn^{(3)}_n$). We also take $\skl^{(1)} = \bigcup_{n \geq 1} \skl^{(1)}_n$, and we define $\skl^{(2)}$ and $\skl^{(3)}$ similarly. It is clear that $\skl^{(3)} \subset \skl^{(2)} \subset \skl^{(1)}$.

We start by characterizing skeletons of planar linear $\lambda$-terms. Given a unary-binary tree $S$ and a node $u$ in $S$, we denote by $S_u$ the sub-tree induced by $u$, by $\leaf(S)$ the number of leaves in $S$, and by $\unary(S)$ the number of unary nodes in $S$.

\begin{prop} \label{prop:chara-conn-lambda}
  A unary-binary tree $S$ is in $\skl^{(1)}$ if and only if
  \begin{itemize}
  \item (\textbf{Linearity}) $\leaf(S) = \unary(S)$;
  \item (\textbf{Normality}) No binary node in $S$ has a unary node as its left child;
  \item (\textbf{Connectedness}) For every binary node and leaf $u$ in $S$, we have $\leaf(S_u) - \unary(S_u)$ greater than or equal to the number of consecutive unary nodes above $u$.
  \end{itemize}
  Furthermore, a unary-binary tree $S \in \skl^{(1)}$ is also in $\skl^{(2)}$ if and only if
  \begin{itemize}
  \item (\textbf{2-connectedness}) For every binary node and leaf $u$ in $S$, we have $\leaf(S_u) - \unary(S_u)$ strictly larger than the number of consecutive unary nodes above $u$.
  \end{itemize}
\end{prop}

For skeletons of $\lambda$-terms in $\conn^{(3)}$, we start with an observation from \cite{grygiel-yu}.

\begin{prop}[See \cite{grygiel-yu}] \label{prop:lambda-root}
  Let $S \in \skl^{(3)}$ and $u$ its first binary node. The left child of $u$ is a leaf.
\end{prop}
\begin{proof}
  Let $v$ be the left child of $u$. If $v$ is not a leaf, then by planarity, the leaves of $S_v$ are connected to an initial segment of the unary nodes above $u$. Cutting $\{u, v\}$ and the edge below the said initial segment disconnects $\syndiag(S)$, contradicting 3-connectedness.
\end{proof}

We define the \tdef{reduced skeleton} of a skeleton $S$ in $\skl^{(3)}$ to be the unary-binary tree obtained from $S$ by removing the first binary node, its left child (which is a leaf by \cref{prop:lambda-root}), and the nodes above it. By (\textbf{Linearity}) on $S$, we can reconstruct $S$ from the reduced skeleton of $t$. We denote by $\redskl_n$ the set of reduced skeletons of skeletons in $\skl^{(3)}_n$, and $\redskl = \cup_{n \geq 3} \redskl_n$. The following characterization of reduced skeletons was first discovered and stated without proof in \cite{grygiel-yu}. Readers are referred to the full version \cite{full-version} for its proof.

\begin{prop} \label{prop:chara-lambda}
  A unary-binary tree $S$ is in $\redskl$ if and only if
  \begin{itemize}
  \item (\textbf{Normality}) No binary node in $S$ has a unary node as its left child;
  \item (\textbf{3-connectedness}) For every binary node $u$ in $S$, let $v$ be its right child, then $\leaf(S_v) - \unary(S_v)$ is strictly larger than the number of consecutive unary nodes above $u$.
  \end{itemize}
\end{prop}

\section{Bijection from $\lambda$-terms in $\conn^{(3)}$ to degree trees} \label{sec:bij-3}

A \tdef{degree tree}, as defined in \cite{fang-bipartite}, is a pair $(T, \ell)$ where $T$ is a plane tree and $\ell$ a labeling on the nodes of $T$ such that
\begin{itemize}
\item If $u$ is a leaf, then $\ell(u) = 0$;
\item For $u$ with children $v_1, v_2, \ldots, v_k$ from left to right, let $s(u) = k + \sum_{i=1}^{k} \ell(v_i)$, then $s(u) - \ell(v_1) \leq \ell(u) \leq s(u)$.
\end{itemize}
The \tdef{size} of a degree tree $(T, \ell)$ is the number of edges in $T$. We denote by $\mathcal{T}_n$ the set of degree trees of size $n$. Given a degree tree $(T, \ell)$, we define its \tdef{edge labeling} $\ell_\Lambda$ as follows: for each internal node $u$, we put a label $s(u) - \ell(u)$ on its leftmost descending edge, and~$0$ on all other edges. It is clear that we can recover $(T, \ell)$ from $T$ and $\ell_\Lambda$. Later, we will use both $\ell$ and $\ell_\Lambda$. We now define a bijection $\varphi$ from reduced skeletons to degree trees.

\begin{defn} \label{defn:redskl-degree-tree}
Given $S \in \redskl$, we perform the following:
\begin{enumerate}
\item Remove all leaves from $S$, and add a new unary root above the old root. Then smooth out all unary nodes and put the number of smoothed-out nodes at each edge. We obtain a binary tree $S'$ with an edge labeling $\ell_\Lambda'$.
\item Perform the classical bijection (\emph{switching left and right}) from binary tree $S'$ to plane tree $T'$: given a node $u$, its \emph{right child} in $S'$ is turned into its \emph{leftmost child} in $T'$, and its \emph{left child} in $S'$ into its sibling immediately \emph{to its right}. The edge labels of $\ell_\Lambda'$, which are all on rightmost descending edges in $S'$, are transformed into an edge labeling $\ell_\Lambda$ with only non-zero values on the leftmost descending edges of nodes.
\end{enumerate}
We define $\varphi(S)$ to be $(T', \ell)$, where $\ell$ is the node labeling corresponding to $\ell_\Lambda$ constructed above. See \cref{fig:bij-example} for an example of the bijection $\varphi$.
\end{defn}

\begin{figure}
  \centering
  \insertfig{1}{0.8}
  \caption{Example of the bijection $\varphi$ from reduced skeletons in $\redskl$ to degree trees (zeros in $\ell_\Lambda$ are omitted).}
  \label{fig:bij-example}
\end{figure}

\begin{prop} \label{prop:bij-redskl-degree-tree}
  A unary-binary tree $S$ is in $\redskl_n$ if and only if $\varphi(S)$ is in $\mathcal{T}_{n-2}$.
\end{prop}

Given the bijection from $\redskl$ to degree trees, which are also in bijection with bipartite planar maps, we can transfer enumeration results from maps to $\lambda$-terms via degree trees. Some statistics are also transferred alongside.

We first define several statistics on reduced skeletons. Given $S \in \redskl_n$, we define its \tdef{excess} $\excess(S) = \leaf(S) - \unary(S)$, and we denote by $\applv(S)$ the number of binary nodes of $S$ whose right child is a leaf, $\appla(S)$ the number of binary nodes of $S$ whose right child is also a binary node, and $\uchain_k(S)$ the number of maximal chains of unary nodes of length $k$. In the language of $\lambda$-terms, $\excess(S)$ is the number of abstractions at the beginning of the original term minus one (from the leaf in \cref{prop:lambda-root} deleted in the reduced skeleton), $\applv(S)$ the number of applications of terms to a variable, $\appla(S)$ the number of applications of terms to another application, and $\uchain_k(S)$ the number of maximal consecutive abstractions of length $k$, except the one at the root.

Now we introduce some statistics on degree trees. Given $(T, \ell)$ a degree tree, we denote by $\lnode(T, \ell)$ the number of leaves in $T$, by $\znode(T, \ell)$ the number of internal nodes whose leftmost descending edge has label $0$, by $\rlabel(T,\ell)$ the label of the root in $(T, \ell)$, and by $\edge_k(T, \ell)$ the number of edges with label $k \geq 1$. The following transfer of statistics is clear from \cref{defn:redskl-degree-tree}.

\begin{prop} \label{prop:stat-lambda-tree}
  Given $S \in \redskl_n$, let $(T, \ell) = \varphi(S)$. Then we have
  \begin{align*}
    \applv(S) = \lnode(T, \ell), &\quad \appla(S) = \znode(T, \ell), \\
    \excess(S) = \rlabel(T, \ell), &\quad \uchain_k(S) = \edge_k(T, \ell).
  \end{align*}
\end{prop}

The statistics mentioned in \cref{prop:stat-lambda-tree} are also transferred to bipartite planar maps. More precisely, let $\bipartite_n$ be the set of bipartite planar maps with $n$ edges. For $M \in \bipartite_n$, we denote by $\white(M)$ (resp. $\black(M)$) the number of white (resp. black) vertices in $M$, and $\outdeg(M)$ the half-degree of the outer face. For $k \geq 1$, we denote by $\face_k(M)$ the number of inner faces of degree $2k$. We have the following result from \cite{fang-bipartite}.

\begin{prop}[See Proposition~3.3~and~3.6, and Remark~1 in \cite{fang-bipartite}] \label{prop:bij-tree-map}
  There is a bijection $\mu$ from $\mathcal{T}_n$ to $\bipartite_n$. Moreover, for $(T, \ell) \in \mathcal{T}_n$, let $M = \mu(T, \ell)$, and we have
  \begin{align*}
    \lnode(T, \ell) = \white(M), &\quad \znode(T, \ell) = \black(M), \\
    \rlabel(T, \ell) = \outdeg(M), &\quad \edge_k(T, \ell) = \face_k(M).
  \end{align*}
\end{prop}

We obtain \cref{thm:main-3-conn} using the bijections from $\redskl_n$ to $\mathcal{T}_{n-2}$ and from $\mathcal{T}_{n-2}$ to $\bipartite_{n-2}$.

\begin{proof}[Proof of \cref{thm:main-3-conn}]
  Consider $\mu \circ \varphi$ with $\varphi$ from \cref{defn:redskl-degree-tree} and $\mu$ from \cref{prop:bij-tree-map}. It is a bijection from $\redskl_n$ to $\bipartite_{n-2}$ according to \cref{prop:bij-redskl-degree-tree,prop:bij-tree-map}.
\end{proof}

Combining \cref{prop:stat-lambda-tree,prop:bij-tree-map}, we have the following transfer of statistics from reduced skeletons of $\lambda$-terms in $\conn^{(3)}$ to planar bipartite maps.

\begin{thm} \label{thm:stat-lambda-map}
  Let $S \in \redskl_n$ and $M = \mu(\varphi(S)) \in \bipartite_{n-2}$. Then we have
  \begin{align*}
    \applv(S) = \white(M), &\quad \appla(S) = \black(M), \\
    \excess(S) = \outdeg(M), &\quad \uchain_k(S) = \face_k(M).
  \end{align*}
\end{thm}

A consequence of \cref{thm:stat-lambda-map} is that the generating function of $\redskl$ refined by all related statistics can be written using that of bipartite maps refined by corresponding statistics. For instance, the enumeration of $\redskl$ refined by $\excess$ and $\uchain_k$ for all $k$ is given by the generating function of bipartite maps refined by face degrees, which was found implicitly in \cite{BMS}, then written explicitly in \cite{BDFG}.

Furthermore, we can also use \cref{thm:stat-lambda-map} to transfer known results on the distribution of various statistics on bipartite planar maps to $\lambda$-terms in $\skl^{(3)}$. As an example, in \cite{bipartite-root-degree}, Liskovets studied the asymptotic vertex degree distribution of many families of planar maps, including Eulerian planar maps, which are duals of bipartite planar maps. Transferring the results in \cite{bipartite-root-degree} to $\redskl$ using \cref{thm:stat-lambda-map}, we have the following corollary.

\begin{coro} \label{coro:bipartite-root-degree}
  Let $X_n$ be the number of abstractions at the beginning of a $\lambda$-term chosen uniformly randomly from $\conn^{(3)}_n$. Then, for $k \geq 2$, when $n \to \infty$, we have
  \[
    \mathbb{P}[X_n = k] \to \frac{k-1}{3} \binom{2k-2}{k-1} \left( \frac{3}{16} \right)^{k-1}.
  \]
\end{coro}

\section{Bijection from $\lambda$-terms in $\conn^{(1)}$ and $\conn^{(2)}$ to v-trees} \label{sec:bij-2}

In the following, we consider skeletons in $\skl^{(1)}$ and $\skl^{(2)}$. We start by defining a transformation $\psi$ from these skeletons to some trees with labels on their nodes.

\begin{defn} \label{defn:psi}
Given $S \in \skl^{(1)}$, We define $\psi(S)$ to be $(T, \ell)$ obtained as follows:
\begin{enumerate}
\item We label each binary node $u$ by $\leaf(S_v) - \unary(S_v)$, where $v$ is the right child of $u$, and remove all leaves and unary nodes. We now obtain a binary tree $S'$ with node labeling $\ell'$.
\item We perform the classical bijection (\emph{switching left and right}) from binary tree $S'$ to plane tree $T$ as in the second step of the definition of $\varphi$ in \Cref{defn:redskl-degree-tree}. We keep the labels of $\ell'$ on $S'$ in $\ell$ on $T$.
\end{enumerate}
For the reverse direction, we simply reverse all the operations above, then insert unary nodes \emph{from bottom to top} according to labels, but \emph{only to the right branch} of binary nodes, in accordance with (\textbf{Normality}).
\end{defn}

\begin{figure}
  \centering
  \insertfig{5}{0.6}
  \caption{Example of the bijection $\psi$ from skeletons in $\skl^{(1)}$ to v-trees.}
  \label{fig:v-tree-to-skeleton}
\end{figure}

We now characterize the labeled plane trees obtained by $\psi$. A node-labeled tree $(T, \ell)$ is a \tdef{v-tree} if the following conditions hold:
\begin{itemize}
\item Leaves of $T$ are labeled by $0$ or $1$;
\item Every non-root node $u$ with children $v_1, \ldots, v_k$ satisfies $0 \leq \ell(u) \leq 1 + \sum_{i=1}^k \ell(v_i)$;
\item For the root $r$ with children $v_1, \ldots, v_k$, we have $\ell(r) = 1 + \sum_{i=1}^k \ell(v_i)$.
\end{itemize}
The \tdef{size} of a v-tree is the number of its edges. We denote by $\vtree_n$ the set of v-trees of size $n$, and we take $\vtree = \bigcup_{n \geq 1} \vtree_n$. Moreover, we denote by $\vtree^+_n$ the set of v-trees \emph{without label 0} of size $n$, and we take $\vtree^+ = \bigcup_{n \geq 1} \vtree^+_n$. We have the following characterization of $\psi(\skl^{(1)}_n)$.

\begin{prop} \label{prop:psi-chara}
  A unary-binary tree $S$ is in $\skl^{(1)}_n$ if and only if $T = \psi(S)$ is a v-tree of size $n-1$. In other words, $\psi$ is a bijection from $\skl^{(1)}_n$ to $\vtree_{n-1}$.
\end{prop}

The bijection $\psi$ specializes naturally to skeletons in $\skl^{(2)}$.

\begin{prop} \label{prop:psi-chara-2-conn}
  A unary-binary tree $S$ is in $\skl^{(2)}_n$ if and only if $T = \psi(S)$ is a v-tree of size $n-1$ without label $0$. In other words, $\psi$ is a bijection from $\skl^{(2)}_n$ to $\vtree^+_{n-1}$.
\end{prop}
\begin{proof}
  Suppose that $u$ is a non-root non-unary node in $S$, with $k$ consecutive unary nodes above it leading to a binary node $v$. By (\textbf{Normality}), $u$ is in the right sub-tree of $v$ in $S$, meaning that $\ell(v) = \leaf(S_u) - \unary(S_u) - k$. We thus conclude the proof by seeing that $u$ satisfies (\textbf{2-connectedness}) if and only if $\ell(u) > 0$.
\end{proof}

\begin{rmk}
  We note that, unlike degree trees, the definition of v-tree does not distinguish left and right. Therefore, in the definition of $\psi$, there is no need to switch left and right in the second step. However, we keep the current definition for consistency with $\varphi$.
\end{rmk}

\section{Bijection from planar maps to v-trees} \label{sec:map-decomp}

We denote by $\planar_n$ the set of planar maps with $n$ edges, and by $\planar$ the set of all planar maps. For $M$ a planar map, we denote by $\outvertex(M)$ the number of vertices of $M$ adjacent to the outer face. We now define a direct bijection $\rho$ using an exploration procedure of planar maps, in the vein of \cite{fang-bipartite, nonsep}.

Given a planar map $M$, we put the label $\outvertex(M)$ on its root vertex, and then start a contour walk in the clockwise direction from the root corner. Suppose that we are at a corner $c$ and is about to walk along a new edge $e$ starting from $v$ to $w$. We find the corner $c_1$ of $v$ on the other side of $e$ and the next corner $c_2$ in clockwise direction of $v$ that is adjacent to the outer face. We put the label $\outvertex(U)-1$ on $w$, where $U$ is the part of $M$ between $c$ and $c_2$. There are two cases, as illustrated on the left part of \cref{fig:map-to-v-tree-direct}:
\begin{enumerate}
\item If $c_1 = c_2$, then $e$ is a bridge, and we do nothing.
\item If $c_1 \neq c_2$, then $e$ separates the outer face with an inner face. In this case, we detach the part of $M$ between $c_1$ and $c_2$ while duplicating the vertex $v$.
\end{enumerate}
After the whole walk, we obtain a planar map with labels on its vertices, denoted by $\rho(M)$. The right part of \cref{fig:map-to-v-tree-direct} gives an example of the construction of $\rho(M)$. It is in fact always a tree rooted at the original root corner of $M$, as every inner face will be eventually ``opened up'' in the second case above.

\begin{figure}
  \centering
  \insertfig{4}{1}
  \caption{Definition and example of the direct bijection $\rho'$.}
  \label{fig:map-to-v-tree-direct}
\end{figure}

\begin{thm} \label{thm:one-corner-tree}
  For all $n \geq 0$, the transformation $\rho$ is a bijection from the set $\planar_n$ of planar maps with $n$ edges to the set $\vtree_n$ of v-trees with $n$ edges. Furthermore, for $M \in \planar_n$, the label of the root of $\rho(M)$ is $\outvertex(M)$.
\end{thm}

\begin{proof}[Proof of \cref{thm:main-conn}]
  As we may identify $\lambda$-terms in $\conn^{(1)}$ with their skeletons in $\skl^{(1)}$, the bijection is given by $\psi \circ \rho$. The first part is a consequence of \cref{prop:psi-chara,thm:one-corner-tree}. For the second part, we notice that a label $0$ is only produced when opening up a loop in the construction of $\rho(M)$. We thus conclude by \cref{prop:psi-chara-2-conn}.
\end{proof}

\begin{rmk}
  Zeilberger and Giorgetti has given a bijection between planar maps and planar linear normal $\lambda$-terms in \cite{planar-lambda}, using the Tutte decomposition \cite{Tutte-census}. Furthermore, Zeilberger also showed in \cite{lambda-trivalent} that the same bijection sends terms that are also unitless to bridgeless planar maps, which are the duals of loopless planar maps. We have checked that our bijection is different from the one in \cite{planar-lambda}, even after taking the dual.
\end{rmk}

\acknowledgements{We thank Katarzyna Grygiel and Guan-Ru Yu for discovering \cref{prop:chara-lambda} and for their inspiring discussions. We also thank \'Eric Fusy for inspiring the one-corner decomposition. We are grateful to the organizers of the workshop series of Computational Logic and Applications (CLA), in which Grygiel and Yu got to know \cref{conj:3-conn} from Zeilberger and Reed, and in which the author got to know \cref{prop:chara-lambda} from Grygiel and Yu. We are also grateful for the useful comments from Noam Zeilberger.}

% biblatex
\printbibliography
\end{document}
