\large Compaction of Church Numerals for Higher-Order Compression
% Isamu Furuya$^{\ast
In this study, we address the problem of compacting Church numerals. Church numerals appear as a representation of the repetitive part of data in higher-order compression. We propose a novel decomposition scheme for a natural number using tetration, which leads to a compact representation of \lterms~equivalent to the original Church numerals. For natural number $n$, we prove that the size of the lambda term obtained by the proposed method is $\ord((\slogt{n)^{\log{n/\log{\log{n)$. Moreover, we quantitatively confirmed experimentally that the proposed method outperforms a binary expression of Church numerals when $n$ is less than approximately $10000$.
appli.tex
\section{Application to Higher-Order Compression}
\label{sec:application}

\subsection{Overview of higher-order compression}

%In higher-order compression, first, the source text data is regarded as
In higher-order compression,
an input text is first represented as a $\lambda$-term 
where each terminal symbol is combined recursively by functional application.
For example, the text $ababc\$$ can be represented as $((a~b)~((a~b)~(c~\$)))$.
Here, there is an equivalency between two $\lambda$-terms $M$ and $N$
if they both result in the same calculated $\lambda$-term.
The main part of higher-order compression is to convert the input $\lambda$-term
to a more compact term with the remaining equivalency between them.
%Note that other \lterms~(like $((a~(b~a))~(b~(c~\$)))$, $((((a~b)~(a~b))~c)~\$)$, and more)
%can also regarded as the \lterm~of text $ababc\$$.
%Then, we convert it to another $\lambda$-term whose size is less than the size of the original,
%with the remaining equivalency between them.
%Here, we say that there is an equivalency between $M$ and $N$

% \subsection{Relationship between Church numerals and repetition patterns}


%In the $\lambda$-terms of higher-order compression, repetition patterns can appeare
%with Church numericals.
During higher-order compression processing,
a repetition pattern in the $\lambda$-term appears in the form of a Church numeral.
% as ((a Church numeral corresponding to the repetition number of the pattern)
% (pattern)).
For example, the $\lambda$-term corresponding to the string "$abcabcabcabc\$$"
can be transformed into
  	$(\lambda fx.f(f(f(f~x))))(a~b~c)~\$ =\ch{4}~(a~b~c)~\$$.
%is expressed as follows:
% \begin{align*}
%	((a~b~c)((a~b~c)((a~b~c)((a~b~c)~\$))))
  %	\rightarrow (\lambda fx.f(f(f(f~x))))(a~b~c)~\$
%   	(\lambda fx.f(f(f(f~x))))(a~b~c)~\$	= \ch{4}~(a~b~c)~\$
% \end{align*}
If the repetition number becomes large, i.e., the Church numeral is large,
we can compress it by compaction of Church numerals.


\subsection{Related work}

% We introduce a method that can compress Church numerals using a binary expression,
% which is reported by Kobayashi et al.~\cite{Kobayashi2012}.
% Let $b_0 = (\lambda fpq.f~p~(f~p~q))$ and
% $b_1 = (\lambda fpq.p~(f~p~(f~p~q)))$.
% Then, the term $~(b_1(b_0(b_0(b_1(b_1(b_1(\ch{0}))))))~a~\$)$ 
% generates the $\lambda$-term, which expresses $a^{57}\$$,
% that is, $(\overbrace{a~(a\cdots(a}^{57}~\$)\cdots))$.
% Here, the binary expression of 57 is 111001, and
% the part $b_1(b_0(b_0(b_1(b_1(b_1(\ch{0}))))))$ corresponds to its reverse.

%Kobayashi et al.~\cite{Kobayashi2012} introduce a method that can compress Church numerals using a binary expression.
Kobayashi et al.~\cite{Kobayashi2012} introduce a binary expression of Church numerals.
For $\ch{n}$, the size of the expression is $\Theta(\log{n})$.
% Let $b_0 = (\lambda fpq.f~p~(f~p~q))$ and
% $b_1 = (\lambda fpq.p~(f~p~(f~p~q)))$.
% Then, the term $~(b_1(b_0(b_0(b_1(b_1(b_1(\ch{0}))))))~a~\$)$ 
% generates the $\lambda$-term, which expresses $a^{57}\$$,
% that is, $(\overbrace{a~(a\cdots(a}^{57}~\$)\cdots))$.
% Here, the binary expression of 57 is 111001, and
% the part $b_1(b_0(b_0(b_1(b_1(b_1(\ch{0}))))))$ corresponds to its reverse.
Earlier, Mogensen~\cite{Mogensen2001} proposed a binary expression of Church numerals
and generalized to higher number-bases.
The method introduced by Kobayashi et al. is essentially the same as Mogensen's method.

In addition,
Yaguchi et al. also proposed a compaction method \cite{Yaguchi2014EfficientCompression}.
Their method treats the tetrational feature of \lterms~
and can compress them in super-logarithmic size order, similar to our method.
We refer to their method as the YKS algorithm in this paper.
% We omit the detail because of narrow paper space.


\subsection{Experiment}

To compare the performance of the proposed method to that of the existing methods,
we conducted an experiment to evaluate the compression ratio.
Figures~\ref{fig1} and \ref{fig2} show the experimental results.
We used the artificial data $a^n\$$ as input.

\setlength\textfloatsep{0pt}
\begin{figure}[t]
  %\begin{minipage}{0.5\columnwidth}
  \begin{minipage}{0.5\hsize}
\begin{center}
  \includegraphics[width=76mm]{figure_1.eps}
%  \includegraphics[width=0.48\columnwidth]{figure_1.eps}
\vspace{-14pt}
	\caption{Term size for integer $n$}
\label{fig1}
\end{center}
\end{minipage}
  \begin{minipage}{0.5\hsize}
      %\begin{minipage}{0.5\columnwidth}
\begin{center}
  \includegraphics[width=76mm]{figure_3.eps}
%  \includegraphics[width=0.48\columnwidth]{figure_3.eps}
\vspace{-14pt}
	\caption{Average ratio to binary expression}
\label{fig2}
\end{center}
\end{minipage}
\end{figure}

% \begin{figure}[t]
%   \begin{center}
% 	\includegraphics[trim=50 50 0 0,width=0.8\columnwidth]{figure_1.eps}
%   \end{center}
% 	\caption{Experimental result}
%   \label{figu}
% \end{figure}

In Fig.~\ref{fig1}, the horizontal axis shows the repetition $n$
and the vertical axis shows the size of each $\lambda$-term.
Here, "Binary" denotes the size of the $\lambda$-term compacted 
by the method using the binary expression.
"YKS" denotes the YKS algorithm, and
"Proposed" denotes our proposed method.
The inequality (Proposed $\le$ Binary) holds in 5187 out of 10000 cases.
The average ratio (Proposed / Binary) is approximately 0.9962.
Similarly, the inequality (Proposed $\le$ YKS) holds in 5959 cases, and
the average ratio (Proposed / YKS) is approximately 0.9321.
%From this result, it seems that our method achieves 
%same degree of compression ratio as Binary averagely,
%but for more large repetition numbers, Proposed tends to be larger than Binary.

In Fig.~\ref{fig2}, the horizontal axis shows the repetition $n$
and the vertical axis shows the ratio
((the average size of cumulative sum of $\lambda$-terms from $1$ to $n$) / Binary).
Fig.~\ref{fig2} shows how much the result of YKS and the proposed method will 
increase compared to the result of Binary 
if we assume that $n$ is given in uniform distribution.
As can be seen, the result of Proposed tends to be greater than 
  that of Binary when $n$ is greater than approximately $10000$.
We consider this to be consistent with the theoretical upper bound analysis 
	  result $\ord((\slogt n)^{\log n/\log\log n})$ stated in Theorem~\ref{theo}.

conclusion.tex
\section{Conclusion}
\label{sec:conclusion}

In this paper,
we have addressed the problem of compacting Church numerals,
which is useful for higher-order compression.
We have proposed RTP to decompose large numerals and presented a \lterm\, conversion algorithm using RTP.
We confirmed experimentally that
the \lterms\, produced by the algorithm have sizes
following its theoretical size, $\ord((\slogt n)^{\log n/\log\log n})$
in the worst case.
On the other hand, for $n=\tetr{2}{k}$, $\ch{n}$ is converted to a \lterm\, of $\ord(\slogt n)=\ord(k)$ size.
% We have not proved the lower bound of the size in the worst case;
% it is one of our future works.

About bit encoding of \lterms, 
Tromp~\cite{tromp:DSP:2006:628} proposed a method for untyped \lterms.
In addition, very recently, Takeda et al.~\cite{TakedaCompactLambda-Terms}
proposed an efficient method to encode simply-typed \lterms.
Combining our method with these encodings is one of our future works.
Moreover, efficiently finding repeating regions in an input and counting the number of repetitions are remaining problems in higher-order compression.

intro.tex
\section{Introduction}
\label{sec:intro}

The goal of this study is to obtain a compact lambda term (\lterm) 
that is equivalent to the Church numeral for a given natural number.
Church numerals are unary representations of natural numbers using lambda notation.
Herein, for an integer $n$, the length of the Church numeral increases linearly with $n$.
Let $\ch{n}$ be the Church numeral for a natural number $n$;
% then the lambda expression $\ch{n}$ is as follows:
% \vspace{-10pt}
% \begin{equation*}
% 	\ch{n}=(\lambda fx. \overset{n}{\overbrace{f(f(\cdots f(f}}\, x)\cdots )).
% \end{equation*}
then the lambda expression $\ch{n}$ is
$(\lambda fx. \overset{n}{\overbrace{(f(f(\cdots f(f}}\, x)\cdots ))$.
For a large $n$, decomposing and representing it as an equivalent expression may reduce the length of the \lterm\, for $n$.
For example, $n=500$ can be decomposed as $5 \times 10 \times 10$.
The \lterm\, corresponding to the expression is given as
$((\lambda pqfx.p~(q~(q~f))~x)$ $\ch{5}~\ch{10})$,
which is much shorter than $\ch{500}$.
%Basic arithmetic operations on Church numerals coresponding to those on numbers are defined as functions in lambda calculus.
%チャーチ数の表す数が大きい場合，チャーチ数をそのまま書くよりも，計算結
%果がそのチャーチ数となる演算の形に分解して書いたほうが，ラムダ式のサイズ
%が小さくなる場合がある．例えば，自然数 50 に対応するチャーチ数は
%C(50) = (λfx.
%50
%z }| {
%f (f ···(f x)···)


Reducing the length of Church numerals is applied in data compression.
Kobayashi et al.~\cite{Kobayashi2012} proposed a compression method
called higher-order compression that uses \lterms\, as the data model.
Their method translates an input to a \lterm\, by inducing the input itself
and then encoding the obtained \lterm.
% The input data is first represented as a simple \lterm,
% which consists of nested functional applications of lambda notation.
% The \lterm\, is converted into a shorter term by repeatedly extracting common contexts.
%This conversion corresponds to the reverse processing of $\beta$-reduction in lambda calculus.
% Since repeating patterns in the initial \lterm\, appear as Church numerals,
Since repeating patterns in the \lterm\, appear with Church numerals,
shortening them is important for data compression.
We refer to the task of shortening Church numerals as 
% the \emph{compaction of $\ch{n}$}.
the \emph{compaction of Church numerals}.
%%%圧縮処理の方針は，まずデータを単に直線的なラムダ式として表現し，そのラムダ式に対応する構文木を考える．
%%%そして，構文木内で共通して頻出する部分木をパターンとして抽出し，それらをまとめるようにラムダ式を変形する．
%%%この変形操作は，ラムダ計算におけるβ簡約の逆の処理に相当する．


%In this paper, we propose a method to construct a compact \lterm\, for a highly repeating pattern.
%Since repeating patterns in an input data appear as Church numerals~\cite{} in higher-order compression,
%to quickly shorten the Church numerals is important for this aim.
In this study, 
% we introduce a new scheme,
% named \emph{Recursive tetrational partitioning} (RTP) to decompose a natural number using \emph{tetration}.
we propose the \emph{Recursive tetrational partitioning} (RTP) method
to decompose a natural number using \emph{tetration}.
We also present an algorithm to perform RTP for a given natural number
and demonstrate that the obtained expression is translated into a compact \lterm.
%In the best case, the size of the obtained lambda term can achieves $\ord(\slogt{n})$.
Moreover, we prove that the length of the obtained \lterm\, is $\ord((\slogt n)^{\log n/\log\log n})$ in the worst case.
Although this is slightly worse than $\ord(\log{n})$,
it can be reduced to $\ord(\slog{n})$ in the best case, with $\fact < n$.
%本論文では，連続するパターンに対して，よりコンパクトなラムダ式を構築する手法を提案する．
%提案手法は，連長を非負整数の超冪を用いた式に分解し，
%その式に対応するラムダ式へと置き換えることでデータを圧縮する．


% Kobayashi et al.~\cite{Kobayashi2012} also showed the binary representation of \lterms\, equivalent to Church numerals, whose length is $\ord(\log n)$.
% Although the result of our $\ord((\slogt n)^{\log n/\log\log n})$ is larger than $\ord(\log n)$,
% we confirmed via an experiment that the obtained \lterms\, become much shorter than binary representation in many cases.
%既存のラムダ式による連長の表現手法としては， Kobayashi ら [3] がバイナリ表現に対応するものを示している．
%提案手法は，ほとんどの場合において，このバイナリ表現よりも小さなラムダ式を生成する．
%実験の結果，提案手法は，バイナリ表現より平均して約 21% 圧縮率が向上することを確認した．



%To develop efficient translation and encoding methods is the main problem of higher-order compression.
%Recently, Yaguchi et al.~\cite{Yaguchi2014} propose one solution to the issue.
%As another related work,
Yaguchi et al.~\cite{Yaguchi2014EfficientCompression} recently proposed an efficient algorithm for higher-order compression.
They utilized a simply typed $\lambda$-term for efficient modeling and encoding.
Differing from Kobayashi et al.'s approach wherein each context occurring more than once is extracted,
Yaguchi et al. extracted the most frequent context up to a certain size.
% Their idea was to extract the most frequent context up to a certain size,
% unlike the approach of Kobayashi et al., which extracts every context occurring more than once.
In \cite{Yaguchi2014EfficientCompression},
they state that the performance of their method is often better than the performance of grammar compression,
with regard to compression ratio.
We confirm that the proposed method tends to produce more compact \lterms\, 
for highly repetitive patterns
compared with the method proposed by Yaguchi et al..
Note that the proposed method can be easily incorporated into their algorithm.
%高階プログラムによる圧縮の課題点は，効率よい圧縮処理と符号化である．
%近年，矢口ら [4] は，
%高階プログラムをモデルとするデータ圧縮法を高階圧縮と呼び，その効率よい圧縮処理と符号化を提案している．
%彼らの手法では，効率よい
%符号化と圧縮処理のために単純型付きのラムダ式を用いている．
%%%<----
%%%圧縮処理の方針は，まずデータを単に直線的なラムダ式として表現し，そのラムダ式に対応する構文木を考える．
%%%そして，構文木内で共通して頻出する部分木をパターンとして抽出し，それらをまとめるようにラムダ式を変形する．
%%%この変形操作は，ラムダ計算におけるβ簡約の逆の処理に相当する．
%%%---> ここの部分は小林らのも同じなので，上で先に書く．
%実験の結果より，矢口らの手法は，既
%存の手法と同程度以上の優れた圧縮率を達成することが示されている．
%%%----------
%%%分解アルゴリズムを示すとともに，この表現方法によるラムダ式のサイズが連長 n に対してO(logn) であることを証明する．
%%%----------> O(log n)にはならなかったので，このことはあまり強調しないように，後ろのほうでさらっと述べる．
%提案手法は，矢口らの圧縮手法に容易に組み込むことができる．



\noindent
{\bf Contributions:~}
% Three contributions are made in this paper:
The primary contributions of this study are as follows.
\begin{enumerate}
\item
  For natural numbers,
  we propose a novel decomposition scheme called RTP,
  which leads to compact representation of \lterms\, 
		that is equivalent to the Church numerals of the numbers.
  Note that the proposed RTP differs from $n$-ary notation.
\item
  By incorporating RTP,
  we propose an algorithm to perform the compaction of $\ch{n}$.
  Moreover, we prove that the length of the \lterms~constructed by the algorithm
		is $\ord((\slogt n)^{\log n/\log\log n})$ in the worst case.
%\item
%  We present how to apply the compaction of $\ch{n}$ for higher-order compression.
%  Although the idea is trivial,
%  utilizing the compaction of $\ch{n}$ for this purpose has not yet been discussed explicitly as far as we know.
\item
  % We quantitatively confirmed via experiments that in many cases, our method
  % can produce shorter \lterms\, more than the existing methods;
  % the size reduction is approximately $21\%$ and $23\%$ for $n\le 10,000$ on an average,
  % compared with the binary representation stated in~\cite{Kobayashi2012}
  % and with the method of Yaguchi et al. stated in~\cite{Yaguchi2014EfficientCompression}, respectively.
  We implemented the proposed algorithm and conducted comparative experiments,
  and results show that the proposed method is superior to that of Yaguchi el al.,
  and is also superior to the binary expression of Church numerals when $n$ is less than approximately $10000$.
\end{enumerate}


The remainder of this paper is organized as follows.
In Sec.~\ref{sec:preliminary}, we review lambda notation, Church numerals, and tetration.
In Sec.~\ref{sec:proposed}, we define the proposed RTP method and present the translation algorithm using RTP.
We also prove the upper bound of the length of the \lterm\, produced by our algorithm.
In Sec.~\ref{sec:application}, we describe how our algorithm is applied to higher-order compression,
review related work, and present experimental results.
% Finally, we conclude the paper in Sec.~\ref{sec:conclusion}.
Conclusions are presented in Sec.~\ref{sec:conclusion}.





%Compression methods have two steps: modeling and encoding.
%In LZ77 compression~\cite{LZ77}, for example,
%an input source is parsed and translated into a sequence of pointers,
%and then each pointer is encoded into a series of binary codewords.
%An entropy coding such as Huffman coding and the arithmetic coding is often used at the latter encoding phase~\cite{}.
%データ圧縮は，入力データ系列のモデル化と構築されたモデルの符号化の二つの処理からなる．
%入力データ系列中の記号とそれが連続する長さ（連長）でモデル化し，
%記号と数字の組をそれぞれに適当な符号で符号化を行う．
%Huffman 符号 [1]では，入力データ系列を記憶のない情報源としてモデル化し，各記号の頻度に従っ
%た符号化を行う．


%Better modeling leads better compression.
%It is easy to optimally compress an input data if we know the precise model of it.
%In reality, however, it is rare if we know the model well beforehand;
%we usually assume an appropriate model on the data to express the structure inherent in it.
%Modeling with concise and sufficient expression power is necessary.
%入力データに対するより良いモデル化は，入力データをより良く圧縮する．
%入力データのモデルが既知であるならば，それを最適に圧縮することは容易である．
%しかし現実には，入力データのモデルが既知であるような場合は稀である．
%実際には，適当なモデルを仮定してデータに内在する構造を表現することになる．
%したがって，有限長の入力データを効率よく圧縮するためには，簡潔かつ十分な表
%現力を持つモデル化の方法が求められる．




%Since a \lterm\, has sufficient power to express a complicated structure,
%it highly models the input.
%For example,
%a highly repetitive data in which the number of repetitions is expressed by tetration,
%$a^{\overset{n}{\overbrace{{}_{2^{\cdot^{.\cdot 2}}}}}}\$$,
%is expressed by a \lterm\, whose length is proportional to the depth $n$ of the exponential as follows:
%\[(\lambda f.\overset{n}{\overbrace{f~f~\cdots ~f}}~a~ \$)(\lambda g.\lambda x.g(g(x))).\]
%If we use a grammar compression~\cite{}, which utilizes context-free grammars as a model,
%to compress such a data,
%the length of the produced grammar becomes in proportional to $\overset{n-1}{\overbrace{2^{\cdot^{.\cdot 2}}}}$.
%For another example,
%a \lterm\, can express structures that have different appearances but increase or decrease with the same difference,
%and can also express structures that are almost the same but partly different.
%この問題に対し，小林ら [3] は高階プログラムをモデルとするデータ圧縮を提案している．
%彼らの手法では，入力データに対し，それを生成する高階プログラム
%を構築することでデータ圧縮を行う．
%これにより，複雑な構造を持つデータに対して詳細なモデル化を行うことができる．
%単純な例としては，のように，繰り返しが超冪をなす構造をのように，冪の深さの線形長のラムダ式で表現できる．
%他の手法，例えば文脈自由文法をモデルとする文法圧縮 [2] で同じ文字列を表現すると，に比例した長さが必要となる．
%%%これ以外にも，系列としての見かけは違う
%%%が同じ差分で増減するデータや，ほとんど同じだが一部が異なるパターンなども
%%%柔軟に表現することができる．






%%%%--------------------------------
%%%%ここより後は，やっぱり提案手法の最初にbasic ideaとして書いたほうが収まりがよさそう．

%チャーチ数の表す数が大きい場合，チャーチ数をそのまま書くよりも，計算結
%果がそのチャーチ数となる演算の形に分解して書いたほうが，ラムダ式のサイズ
%が小さくなる場合がある．例えば，自然数 50 に対応するチャーチ数は
%C(50) = (λfx.
%50
%z }| {
%f (f ···(f x)···)
%となり，このサイズは 103 である．一方，計算結果が同じになるような式として，
%例えば 2 × 5 × 5 を考えてみる．この式を表すようなラムダ式は，系 1 より
%(λpqfx.p(qf)x)C(2)((λnfx.n(nf)x)C(5))
%となる．このサイズは 44 であり， C(50) のサイズ 103 より小さい．
%さらに，この式が後述するような条件 γ をみたすとき，式中に出現する各演
%算をまとめた形の，よりコンパクトなラムダ式に変換することができる．例えば，
%上の例での演算の式 2 × 5 × 5 は条件 γ をみたし，
%(λpqfx.p(q(qf))x)C(2)C(5)
%と変換できる．このサイズは 35 である．
%ふつう，ある自然数を上のように演算に分解するとき，その分解の仕方は複数
%通り考えられる．分解の仕方によって，変換後のラムダ式のサイズも変動する．例
%えば自然数 50 には， 2 × 5 × 5 の他にも 7 × 7 + 1 や 5 × (5 + 5) 等といった式が
%考えられ，それぞれのラムダ式とそのサイズは，
%2 × 5 × 5 : (λpqfx.p(q(qf))x)C(2)C(5) ······ サイズ 35
%7 × 7 + 1 : (λpfx.p(pf)(fx))C(7) ······ サイズ 29
%5 × (5 + 5) : (λpfx.p(pf(pf))x)C(5) ······ サイズ 28
%となる．この中では，サイズが一番小さい式 5×(5+5) が最も良い分解というこ
%とになる．一般に，自然数 n に対して変換後のラムダ式のサイズが最小になるよ
%うな分解の式を求めるのは難しいが，提案手法のアルゴリズムは，これがなるべ
%く小さくなるような分解を与える．
%

main.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% One Column
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  \documentclass[smallabstract,smallcaptions]{dccpaper}
\documentclass[a4paper]{article}
% \setlength{\topmargin}{-1.6cm}
% \setlength{\textheight}{25cm}
\setlength{\oddsidemargin}{0cm}
\setlength{\textwidth}{16cm}

\usepackage{epsfig}
\usepackage{citesort}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{color}
\usepackage{url}

\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{amsthm}
\usepackage{fancybox}

\newlength{\figurewidth}
\newlength{\smallfigurewidth}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% One Column
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\setlength{\smallfigurewidth}{2.75in}
\setlength{\figurewidth}{6in}

\newtheorem{theo}{Theorem}
\newtheorem{defi}{Definition}
\newtheorem{ex}{Example}
\newtheorem*{prf}{Proof}
\def\qed{\hfill $\Box$} 
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}

\newcommand{\tetr}[2]{{}^{#2}#1}
\newcommand{\slog}{\text{slog}_{\varphi}}
\newcommand{\slogt}{\text{slog}_{2}}
\renewcommand{\algorithmicrequire}{\textbf{Input:}}
\renewcommand{\algorithmicensure}{\textbf{Output:}}
% \renewcommand{\theprf}{}
% \renewcommand{\thetheon}{}
\newcommand{\CF}{\mathcal{C}}

\def\cond{\gamma}
\def\proc{P}
\def\fact{\varphi}
\def\minf{\varphi^*}
\def\rem{r}
\def\remf{\rem_{\fact}}
\def\minr{\rem^*}
\def\nn{\nonumber}
\newcommand{\ch}[1]{\mathcal{C}(#1)}
\newcommand{\dec}[1]{F[#1]}
\newcommand{\decf}[1]{F_{\fact}[#1]}
\newcommand{\decff}[1]{\mathcal{F}_{\fact}[#1]}
\newcommand{\dect}[2]{T_{#1}[#2]}
\newcommand{\mint}[1]{T^*[#1]}
\newcommand{\dectfn}{T_{\fact}[\nbar]}
\def\nbar{\bar{n}}
\newcommand{\lamb}[2]{\Lambda(#1,#2)}
\newcommand{\minl}[1]{\Lambda^*(#1)}
%\def\tac{\textasciicircum}
\def\tac{\wedge}
\def\ord{\mathcal{O}}
\def\ome{\mathcal{\Omega}}


\newcommand{\lterm}{$\lambda$-term}
\newcommand{\lterms}{$\lambda$-terms}

\begin{document}

\title
{\large
\textbf{Compaction of Church Numerals for Higher-Order Compression}
}


\author{%
	Isamu Furuya$^{\ast}$ and Takuya Kida$^{\ast}$\\[0.5em]
{\small\begin{minipage}{\linewidth}\begin{center}
\begin{tabular}{ccc}
&$^{\ast}$Hokkaido University& \\
&Kita 14-jo, Nishi 9-chome, Kita-ku& \\
&Sapporo, 060-0814, Japan& \\
&\url{{furuya, kida}@ist.hokudai.ac.jp}&\\
\end{tabular}
\end{center}\end{minipage}}
}

\maketitle
\thispagestyle{empty}

\begin{abstract}
  In this study, we address the problem of compacting Church numerals.
  Church numerals appear as a representation of the repetitive part of data in higher-order compression.
  We propose a novel decomposition scheme for a natural number using tetration,
  which leads to a compact representation of \lterms~equivalent to the original Church numerals.
  For natural number $n$,
  we prove that the size of the lambda term obtained by the proposed 
	method is 	$\ord((\slogt{n})^{\log{n}/\log{\log{n}}})$.
  Moreover, we quantitatively confirmed experimentally 
	that the proposed method outperforms a binary expression of Church numerals 
	when $n$ is less than approximately $10000$.
\end{abstract}

\input{intro}
\input{prelimi}
\input{proposed}
\input{appli}
\input{conclusion}

\subparagraph*{Acknowledgments.}
The authors would like to thank Ayumi Shinohara and his colleagues for providing the source code for higher-order compression.
This work was supported by JSPS KAKENHI Grant Number JP15K00002
and JST CREST Grant Number JPMJCR1402, Japan.
In addition, the authors would like to thank Enago (www.enago.jp) for the English language review.

% \Section{References}
% \bibliographystyle{IEEEtran}
% \bibliography{Mendeley}
\input{main.bbl}


\end{document}

prelimi.tex
\section{Preliminary}
\label{sec:preliminary}


\subsection{Lambda terms}

\begin{defi}[Lambda terms and their sizes]\label{defi:lamb}
  Let $S=\{\lambda, ., (, )\}$ be the set of special symbols.
  Let $A$ be the set of characters in the input data,
  where we assume $A\cap S=\emptyset$.
  We call $A$ and $a \in A$ \emph{terminal alphabet} and \emph{terminal symbol}, respectively.
  Let $\Sigma$ be an alphabet such that $\Sigma \cap (A \cup S)=\emptyset$.
  We call $x \in \Sigma$ \emph{variable}.
  For $a\in A$ and $x\in \Sigma$, \emph{lambda terms} (\lterms) are 
	 defined recursively as follows:
  \begin{align*}
	({\rm i})~x \qquad ({\rm ii})~(\lambda x.M) \qquad ({\rm iii})~(M ~ N)
	  \qquad ({\rm iv})~a
  \end{align*}
  where $M$ and $N$ are \lterms.
  We denote the size of the \lterm\, $M$ as $\#M$, 
  and we define each of its lambda terms as follows:
  \begin{align*}
	\#x = \#a = 1,~~~~~
	\#(\lambda x.M) = \#M + 1,~~~~~
	  \#(M\:N) = \#M + \#N + 1.
  \end{align*}
\end{defi}

The definition of the size of a $\lambda$-term can be found in \cite{Kobayashi2012}.
We refer to (ii) and (iii) in Def.~\ref{defi:lamb} as \emph{$\lambda$-abstraction}
and \emph{functional application}, respectively.
Although condition (iv) is added for higher-order compression,
Def.~\ref{defi:lamb} is inherently the same as that of the lambda calculus.
Thus, hereafter, we use well-known lambda calculus omission rules,
such as the omission of parentheses and short notation of nested $\lambda$-abstractions.
%We also follow the usual rules of lambda terms.

%\begin{defi}[De Bruijn index]\label{defi:debruijn}
%	In the de Bruijn index, a $\lambda$-abstraction is represented by only a simple
%	symbol $\lambda$, and a variable is represented by an integer $i$
%	such that $i \ge 0$.
%\end{defi}
We use the \emph{de Bruijn index}~\cite{DEBRUIJN1972381},
which is a simplified notation system for lambda expressions, in our algorithm.
which is one of the simplified notations of lambda expression.
In the de Bruijn index, a $\lambda$-abstraction is written using only $\lambda$,
and each variable is represented by an integer $i\ge 0$.
Variable $i$ is bound by $i$th outer $\lambda$-abstraction
if the abstraction exists; otherwise, the variable is free.
For example, the $\lambda$-terms $\lambda x.\lambda y.(x~(a~(x~y)))$ and
$\lambda w.\lambda z.(w~(a~(w~z)))$ have the same meaning.
Using the de Bruijn index, both are expressed as $\lambda.\lambda.(1~(a~(1~0)))$.
%with variables $x, y, w, z$ and a terminal symbol $a$,


\subsection{Church numerals}

%It is known that natural numbers are represented by \lterms~ as Church numerals,
%and
%some arithmetic operations on numbers
%can also be represented by functions of \lterms\, on Church numerals.

\begin{defi}[Church numerals]\label{defi:Cn}
  Let $n$ be a natural number.
  \emph{Church numerals} for $n$, denoted $\ch{n}$, are defined as follows:
  \vspace{-14pt}
  \begin{align*}
	  \ch{n} := (\lambda fx. \overbrace{(f \:(f \cdots (f}^{n} \: x) \cdots )).
  \end{align*}
  Next, let $n_1$ and $n_2$ be natural numbers.
  Then, each function of addition, multiplication, and exponentiation on $\ch{n_1}$ and $\ch{n_2}$
  are, respectively, defined as follows:
  \begin{eqnarray*}
	  \text{Addition} &{\rm Add}(n_1,n_2)=n_1+n_2
	&:=~(\lambda pqfx.p~f~(q~f~x))~\ch{n_1}~\ch{n_2},\\
	  \text{Multiplication} &{\rm Mul}(n_1,n_2)=n_1\cdot ~n_2
	&:=~(\lambda pqfx.p~(q~f)~x)~\ch{n_1}~\ch{n_2},\\
	  \text{Exponentiation} &{\rm Exp}(n_1,n_2)={n_1}^{n_2}~~~~
	&:=~(\lambda pqfx.q~p~f~x)~\ch{n_1}~\ch{n_2}.
  \end{eqnarray*}
\end{defi}

As can be seen, $\lambda$-abstractions in the above \lterms\ appear first and
are followed by Church numerals.
We refer to the former as \emph{function parts} and the latter as \emph{argument parts}.



\subsection{Tetration and super-logarithm}

\emph{Tetration} is known as the next hyper-operation after exponentiation.
In mathematics, tetration is defined as iterated exponentiation.
For any natural numbers $\fact$ and $i$,
the $i$th tetration of $\fact$ is denoted $\tetr{\fact}{i}$ and defined recursively as follows:
% \begin{align*}
%   \tetr{\fact}{i}:=\left\{
%   \begin{array}{rl}
%     1,& \quad \mbox{for $i=0$,}\\
%     \fact^{\tetr{\fact}{i-1}},& \quad \mbox{for $i>0$.}
%   \end{array}
%   \right.
% \end{align*}
\begin{align*}
  \tetr{\fact}{i}~:=
	~1 ~~ ({\rm for}~ i=0), 
	~~\fact^{\tetr{\fact}{i-1}}~~({\rm for}~ i>0).
\end{align*}
%The exponentiation is a right-associative operation.
For example, $\tetr{2}{1}=2$, $\tetr{2}{2}=4$, $\tetr{2}{3}=16$, and $\tetr{2}{4}=65536$.
Here, from Def.~\ref{defi:Cn}, 
the function of tetration on $\ch{n_1}$ and $\ch{n_2}$ is defined as follows:\\[-20pt]
\begin{eqnarray*}
	\text{Tetration} &{\rm Tet}(n_1,n_2)=\tetr{n_1}{n_2}~~~~
	&:=~(\lambda pfx.\overbrace{p~p\cdots p}^{n_2}~f~x)~\ch{n_1}.
\end{eqnarray*}


%For convenience, it is defined as $\tetr{\fact}{0}=1$.

The following lemma is easily induced from this definition.
\begin{lemm}\label{lemm:tetr}
  For natural numbers $\fact$ and $i$,
  it holds that $\log_{\fact}{\tetr{\fact}{i}} = \tetr{\fact}{i-1}$.
\end{lemm}
%\begin{prf}
%	By the definition of the tetration,
%	$\tetr{\fact}{i} = \fact^{\tetr{\fact}{i-1}}$.
%	Therefore, the proposition has been proven.
%\qed\end{prf}


The \emph{super-logarithm}, denoted as $\mathrm{slog}$, is one of the inverse operations of tetration.
For natural numbers $\fact$ and $i$,
it holds that $\slog \tetr{\fact}{i} = i$.
% On the other hand, the \emph{iterated logarithm} of $n$, denoted by $\log^{\ast} n$,
% is also known as the number of times the logarithm function must be applied to $n$
% before it becomes less than or equal to $1$.
For positive numbers, the super-logarithm is essentially equivalent to the iterated logarithm,
i.e., it holds that $\log^{\ast} n = \lceil \mathrm{slog}_{e} n \rceil$ for any $n>0$.





proposed.tex
\section{Proposed Method}
\label{sec:proposed}


\subsection{Proposed approach}\label{sec:our_approach}
%In this section, we show our algorithm compressing Church numerals.
%This algorithm has 2 steps as follows:
We perform compaction of $\ch{n}$ in the following two steps.
\begin{description}
	\item[Step 1:] Decompose $n$ with natural number $\fact$ ($1<\fact<n$)
		into a numerical expression
	  that includes as much tetration and multiplication of $\fact$ as possible.
  \item[Step 2:] Translate the expression into a corresponding $\lambda$-term such that the translated \lterm\, includes at least a single functional part followed by $\ch{\fact}$.
\end{description}
For Step 1, we introduce the proposed RTP in Sec.~\ref{sec:rtp}, and
for Step 2, we present a translation algorithm in Sec.~\ref{sec:trans_algo}.


As stated in Sec.~\ref{sec:intro},
we may reduce $\#\ch{n}$ for a large number $n$.
For the running example,
it becomes $\#\ch{500}=1003$,
while 
$\#((\lambda pqfx.p~(q~f)~x)~\ch{5}~((\lambda pqfx.p~(q~f)~x)$ $\ch{10}~\ch{10}))=85$,
which corresponds to $5\times 10\times 10$.
Moreover, we can compress the $\lambda$-term by combining two function parts into a single part,
such as $((\lambda pqfx.p~(q~(q~f))~x)$ $\ch{5}~\ch{10})$ with a size of $51$.

For a natural number $n$,
there are many ways to achieve decomposition,
and the size of the \lterm\, changes depending on the employed approach.
% For the running example,
% expressions $7\times 7 +1$ and 
% (ii) $\tetr{3}{2}\times3\times(3+3)+3\times3+3+2$
% are also equal to $500$.
% The corresponding \lterms\, are
% \begin{align*}
% 	{\rm (i)}&: ~(\lambda pfx.p(pf)(fx))~\CF(7),\\
% 	{\rm (ii)}&:
% 	(\lambda pfx.p~p~((\lambda gy.p~(\lambda hzw. p~h~(p~h~w)~z~g~y)~f)~(p~(p~f)~(p~f~(f~(f~x))))))~\ch{3},
% \end{align*}
% and the sizes are $29$ and $28$, respectively.
Note that obtaining optimal decomposition is difficult;
therefore, in RTP, we employ a heuristic approach.


\subsection{RTP}
\label{sec:rtp}

We only consider numerical expressions such as
$F ::=  x~|~F+F~|~F\cdot F~|~F^F$
% \begin{align*}
% 	F ::=  x~|~F+F~|~F\cdot F~|~F^F
% \end{align*}
in BNF, where $x$ is an arbitrary natural number.
If the calculation of $F$ results in $n$, we denote it $\dec{n}$.
Here, the goal is
to obtain $\dec{n}$ such that the size of the corresponding $\lambda$-term becomes smaller.
Reducing the kind of natural numbers used in $\dec{n}$ is effective for compaction.
Therefore, we consider $\dec{n}$ using only $\fact\le n$, denoted $F_{\fact}$, 
such as $F_{\fact} ::= \fact ~|~F_{\fact}+F_{\fact}~|~F_{\fact}\cdot F_{\fact} ~|~{F_{\fact}}^{F_{\fact}}$.
% as follows:
% \begin{align*}
% 	F_{\fact} ::= \fact ~|~F_{\fact}+F_{\fact}~|~F_{\fact}\cdot F_{\fact}
% 	~|~{F_{\fact}}^{F_{\fact}}.
% \end{align*}
Note that $F_{\fact}$ only derives a multiple of $\fact$.
Let $\rem = (n \bmod \fact)$ and $\nbar = n - \rem$.
Then, if $F_{\fact}$ derives $\nbar$, we denote it $\decf{\nbar}$.
Here, $\decf{\nbar}+\rem$ is a numerical expression that derives $n$ 
and includes at most two kinds of natural numbers $\fact$ and $\rem$.

To reduce the size of the $\lambda$-term,
reducing arithmetic operations appearing in $\decf{\nbar}$ is also effective
because the size of the $\lambda$-term increases with the number of arithmetic operations.
Next, we show how the proposed method achieves this reduction.

We partition $\nbar$ into an addition of tetrations with integer coefficients as follows:
% \vspace{-6pt}
\begin{align*}
	\nbar \rightarrow \tetr{\fact}{k}\cdot p_k+ \tetr{\fact}{k-1}\cdot p_{k-1}
	+ \cdots + \tetr{\fact}{1}\cdot p_1
\end{align*}
where $k$ is the maximum natural number such that $\tetr{\fact}{k}\le \nbar$ and
$p_i~(0\le i\le k)$ is the integer such that $0\le p_i < \tetr{\fact}{i+1}$.
The term including $\tetr{\fact}{0}$ does not appear in it
because $\nbar$ is divisible by $\fact$.
Then, we convert each term as follows:
\vspace{-10pt}
\begin{equation*}
	\tetr{\fact}{i}\cdot p_i \rightarrow \tetr{\fact}{i}\cdot (p_i - r_i)
	+ (\overbrace{\tetr{\fact}{i}+\cdots +\tetr{\fact}{i}}^{r_i})
\end{equation*}
where $r_i=(p_i \bmod \fact)$.
Moreover, let $\bar{p_i}=p_i - r_i$ and 
partition $\bar{p_i}$ recursively in the same way. 
As a result, we can convert $\nbar$ to $\decf{\nbar}$.
%The procedure above can be defined as Def.~\ref{defi:tetr}.
The above procedure is defined as follows.

\begin{defi}[RTP]\label{defi:tetr}
	Let $n$ and $\fact$ be natural numbers such that $0 < \fact \le n$, 
    and let $\rem = (n \bmod \fact)$ and $\nbar = n - \rem$.
	Then, we define RTP as follows, where
    the result derived by RTP is denoted $\dectfn$:
    \begin{align*}
		\dectfn = 
		\begin{cases}
			\nbar
			&({\rm if}~ \nbar \le \fact)\\[-10pt]
			\tetr{\fact}{k}\cdot(\dect{\fact}{p_k - (p_k \bmod \fact)})
			+ (\overbrace{\tetr{\fact}{k}
			+\cdots +\tetr{\fact}{k}}^{p_k \bmod \fact})\\[-10pt]
			~~~~~~~~~~~~~
			+ \cdots + \tetr{\fact}{1}\cdot(\dect{\fact}{p_1- (p_1 \bmod \fact)})
			+ (\overbrace{\tetr{\fact}{1}+\cdots +\tetr{\fact}{1}}^{p_{1} \bmod \fact})
			&({\rm otherwise})
		\end{cases}
    \end{align*}
	where $k$ is the maximum natural number such that $\tetr{\fact}{k}\le \nbar$ and
	$p_i~(0\le i\le k)$ is the integer such that $0\le p_i < \tetr{\fact}{i+1}$.
	Here, if $p_i = 0$ or 1, 
	we do not display the term or coefficient, respectively.
\end{defi}

For example, 
% $\dectfn=\dect{2}{65578}=\tetr{2}{4}+\tetr{2}{3}\times 2+\tetr{2}{2}\times 2+2$
% with $n=65579$ and $\fact=2$.
$\dectfn=\dect{2}{200}=\tetr{2}{3}\cdot (\tetr{2}{2}\cdot 2+\tetr{2}{2})+\tetr{2}{2}\cdot 2$
with $n=201$ and $\fact=2$.
In Def.~\ref{defi:tetr}, each coefficient $(p_i-(p_i \bmod \fact))$ is 
a multiple of $\fact$.
Thus, the remainder of each recursion step will always be $0$.
Therefore, no term includes $\tetr{\fact}{0}$ in $\dectfn$.
In addition, $\dect{\fact}{\nbar}$ is determined uniquely
relative to the given $n$ and $\fact$.

\newcommand{\FR}{\textit{FR}}
\subsection{Translation algorithm}
\label{sec:trans_algo}

When numeral expression $F$ is represented by functional representation,
we denote it $\FR(F)$.
In this representation,
${\rm Num}(x)$, ${\rm Add}(x,y)$, ${\rm Mul}(x,y)$, and ${\rm Exp}(x,y)$
correspond to $x$, $x+y$, $x\cdot y$, and $x^y$, respectively.
Then, the following holds:
%\vspace{-8pt}
\begin{align*}
  &\FR(\dectfn) :=
	{\rm Add}(\text{term}(k),
	({\rm Add}(\text{term}(k-1),(\cdots,({\rm Add}(\text{term}(2),\text{term}(1)))\cdots),
\end{align*}
where \\[-32pt]
\begin{align*}
  &\tetr{\fact}{i}:=
  {\rm Exp}(\overbrace{\fact,{\rm Exp}(\fact,\cdots{\rm Exp}(\fact,\fact}^{i})\cdots),
  ~\mathrm{rem}(p_i):=
	{\rm Add}(\overbrace{\tetr{\fact}{i},{\rm Add}(\tetr{\fact}{i},
	\cdots{\rm Add}(\tetr{\fact}{i},\tetr{\fact}{i}}^{p_i\bmod \fact})\cdots),\\
  &\text{and}~\mathrm{term}(i):=
	{\rm Add}({\rm Mul}(\tetr{\fact}{i},(\FR(\dect{\fact}{p_i-(p_i\bmod\fact)}))),
  \mathrm{rem}(p_i))).
\end{align*}

While we can represent any numerical expression
using naive substitution via Def.~\ref{defi:Cn},
the $\lambda$-term generated in this manner tends to be large.
Therefore, we designed an algorithm that enables generation of a compact $\lambda$-term
relative to $\dectfn$.
This algorithm is described in Algorithm \ref{alg:toLambda}, and
we denote the generated $\lambda$-term by $\lamb{\dectfn}{\rem}$
with $\dectfn + \rem$, the numerical expression of $n$.
Note that we denote lambda terms using the de Bruijn index in Algorithm \ref{alg:toLambda}.
%In this algorithm, we denote lambda terms by de Bruijn index defined in
%Def.~\ref{defi:debruijn}.
With Algorithm \ref{alg:toLambda}, for example, 
% $65579=\dect{2}{65578}+1$ 
$200=\dect{2}{200}+1$ 
is translated to 
% $\lamb{\dect{2}{65578}}{1}$, 
$\lamb{\dect{2}{200}}{1}$, 
where
\begin{align*}
	% \lamb{\dect{2}{65578}}{1}=
	% (\lambda pfx.p~p~p~p~f~((p~p~p~(p~f))((p~p~(p~f))((p~f)(f~x))))~\ch{2}.
	\lamb{\dect{2}{200}}{1}=
	((\lambda.\lambda.\lambda.(2~2~2~(\lambda.\lambda.(\lambda.(5~5~(5~2)~(5~5~2~0))~0)~1)~
	(2~2~(2~1)~0)))~\ch{2})
\end{align*}
Thus, $\#\lamb{\dect{2}{200}}{1}=49$, which is much smaller than $\#\ch{201}=405$.

\setlength\textfloatsep{0pt}
\begin{algorithm}[tb]
\caption{Algorithm translating $\dectfn+\rem$ into a $\lambda$-term}
\label{alg:toLambda}
\begin{algorithmic}[1]
\Require $\dectfn, \rem$
\Ensure $\lamb{\dectfn}{\rem}$
	\State {\bf let} ${\rm Translate}(i,j,term)=$
	\State ~~~~{\bf match} $term$ {\bf with}
	\State ~~~~$|~{\rm Num}(term)\rightarrow 2 + i * 2 + j$
	\State ~~~~$|~{\rm Add}(lTerm, rTerm)\rightarrow$
	\State ~~~~~~~~{\bf let} ${\rm LeftSideOfAdd}(lTerm)=$
	\State ~~~~~~~~~~~~{\bf match} $lTerm$ {\bf with}
	\State ~~~~~~~~~~~~$|~({\rm Add}(x,y)$ {\bf or} ${\rm Mul}(x,y))$ {\bf as} 
		       	$term \rightarrow {\rm Translate}(i+1, j, term)$
	\State ~~~~~~~~~~~~$|~{\rm otherwise}$ {\bf as} 
		        	$term \rightarrow ({\rm Translate}(i+1, j, term),2+i)$
	\State ~~~~~~~~{\bf in}
	\State ~~~~~~~~{\bf let} ${\rm RightSideOfAdd}(rTerm)=$
	\State ~~~~~~~~~~~~{\bf match} $rTerm$ {\bf with}
	\State ~~~~~~~~~~~~$|~{\rm Add}(x,y)$ {\bf as} 
		            $term \rightarrow ({\rm Translate}(i+1, j, term),1+i)$
	\State ~~~~~~~~~~~~$|~{\rm Mul}(x,y)$ {\bf as} 
		            $term \rightarrow ({\rm Translate}(i+1, j, term),0)$
	\State ~~~~~~~~~~~~$|~{\rm otherwise}$ {\bf as} 
		        	$term \rightarrow ((({\rm Translate}(i+1, j, term),2+i),0)$
	\State ~~~~~~~~{\bf in}
	\State ~~~~~~~~$\lambda.({\rm LeftSideOfAdd}(lTerm), {\rm RightSideOfAdd}(rTerm))$
	\State ~~~~$|~{\rm Mul}(lTerm, rTerm)\rightarrow$
	\State ~~~~~~~~{\bf let} ${\rm RightSideOfMul}(rTerm)=$
	\State ~~~~~~~~~~~~~{\bf match} $rTerm$ {\bf with}
	\State ~~~~~~~~~~~~~$|~({\rm Add}(x,y)$ {\bf or} ${\rm Mul}(x,y))$ {\bf as} 
		   	       	$term \rightarrow \lambda.\lambda.({\rm Translate}(i, j+1, term),i)$
	\State ~~~~~~~~~~~~~$|~{\rm otherwise}$ {\bf as} 
		   	       $term \rightarrow {\rm Translate}(i, j, term)$
	\State ~~~~~~~~{\bf in}
	\State ~~~~~~~~$({\rm Translate}(i,j,lTerm),({\rm RightSideOfMul}(rTerm),1+i))$
	\State ~~~~$|~{\rm Exp}(lTerm, rTerm)\rightarrow$
		   	$({\rm Translate}(i,j,lTerm),{\rm Translate}(i,j,rTerm))$
	\State {\bf in}
	\State {\bf let} ${\rm TopLevel}(term)=$
	\State ~~~~{\bf let} ${\rm rem} =(\overbrace{1\:(1\cdots(1}^{r}\:0)\cdots )))$ {\bf in}
	\State ~~~~{\bf match} $term$ {\bf with}
	\State ~~~~$|~{\rm Add}(lTerm, rTerm)\rightarrow$
	\State ~~~~~~~~{\bf let} ${\rm LeftSideOfTopAdd}(lTerm)=$
	\State ~~~~~~~~~~~~~{\bf match} $lTerm$ {\bf with}
	\State ~~~~~~~~~~~~~$|~{\rm Add}(x,y)$ {\bf as} 
		   		   	$term \rightarrow {\rm Translate}(0, 0, term)$
	\State ~~~~~~~~~~~~~$|~{\rm Mul}(x,y)$ {\bf as} 
		   		   	$term \rightarrow {\rm Translate}(0, 0, term)$
	\State ~~~~~~~~~~~~~$|~{\rm otherwise}$ {\bf as} 
		      	  $term \rightarrow ({\rm Translate}(0, 0, term),1)$
	\State ~~~~~~~~{\bf in}
	\State ~~~~~~~~$({\rm LeftSideOfTopAdd}(lTerm), {\rm TopLevel}(rTerm))$
	\State ~~~~$|~{\rm Mul}(lTerm, rTerm)$ {\bf as} $term \rightarrow$
		      	$({\rm Translate}(0, 0, term), rem)$
	\State ~~~~$|~{\rm otherwise}(lTerm, rTerm)$ {\bf as} $term \rightarrow$
					$(({\rm Translate}(0, 0, term),1), rem)$
	\State {\bf in}
	\State $(\lambda.\lambda.\lambda.{\rm TopLevel}(\dectfn),\ch{\fact})$
\end{algorithmic}
\end{algorithm}

The $\lambda$-term generated by Algorithm \ref{alg:toLambda} 
% only comprises a $\lambda$-abstraction and $\ch{\fact}$.
is a functional application of a single $\lambda$-abstraction and $\ch{\fact}$.
Here, the $\lambda$-abstraction is considered
a folded function of the arithmetic operations included in $\dectfn$.

\begin{lemm}\label{lemm:size}
	Let $n$ and $\fact$ be natural numbers such that $\fact <n$,
	and let $\rem = (n \bmod \fact)$ and $\nbar = n-r$.
	We denote the number of additions, multiplications, and expressions
	in $\dectfn$ by $N_a$, $N_m$, and $N_e$, respectively.
    %	Then, the following equation holds:
    %	\vspace{-10pt}
    Then, we obtain:
	\begin{equation*}
		\#\lamb{\dectfn}{\rem} < 10N_a + 5N_m + 2N_e + 2\fact + 2\rem + 12.
	\end{equation*}
    %\vspace{-20pt}
\end{lemm}
We omit the proof of Lemma~\ref{lemm:size} due to space constraints.

% \begin{prf}
% 	The form of $\lamb{\dectfn}{\rem}$ is $(\lambda pfx.M)\:\ch{\fact}$.
% 	By Def.~\ref{defi:lsize} and Def.~\ref{defi:Cn},
% 	$\#\ch{\fact}=2\fact +3$.
% 	Then, the size of that $\lambda$-term is as follows:
% 	\begin{align}
% 		\#\lamb{\dectfn}{\rem} = \#(\lambda nfx.M)\:\ch{\fact}
% 		= 3 + \#M + \#\ch{\fact}+1
% 		= \#M +2\fact +7 \label{eq:lemm:size:prf:1}.
% 	\end{align}\\[-16pt]
% 	Initially, the $\lambda$-term $M$ has the form such as $(p~f~X)$
%     with $X = (\overbrace{f~(f\cdots (f}^{\rem}~x)\cdots))$.
% 	Here, $\#M=2\rem + 5$.
% 	If an addition is added in the $\lambda$-term,
% 	the form of $M$ changes into $(p~f~(p~f~X))$, and $\#M$ increases by $4$.
% 	Note that while counting the size of the $\lambda$-term, the parentheses are ignored.
% 	Similarly, in the case of multiplications and exponentiations, 
% 	the form of $M$ changes into $(p~(p~f)~X)$ and $(p~p~f~X)$, respectively.
% 	Both of their sizes increase by $2$.
% 	Therefore, $\#M = 4N_a + 2N_m + 2N_e + 2r + 5$.
% 	Then, by equation (\ref{eq:lemm:size:prf:1}), the following holds:
%     \begin{align*}
% 		\#\lamb{\dectfn}{\rem} &=\#M +2\fact +7
% 		= 4N_a + 2N_m + 2N_e + 2r + 5 + 2\fact + 7\\
% 		&= 2((2N_a + N_m + N_e)+\fact + r + 6).\\[-30pt]
%     \end{align*}
% \qed\end{prf}

% \begin{lemm}\label{lemm:le8}
% 	Let $n$ and $\fact$ be natural numbers such that $\fact <n$,
% 	and let $\rem = n \bmod \fact$ and $\nbar = n-r$.
% 	Then, if $n\le 8$, then $\#\ch{n}\le\#\lamb{\dectfn}{\rem}$.
% \qed
% \end{lemm}
% \begin{prf}
%     By Lemma \ref{lemm:size}, the following inequality holds:
%     \begin{align*}
%     \#\lamb{\dectfn}{\rem}\ge 2 + 2\fact + 2(n \bmod \fact) + 12 = 18.
%     \end{align*}
%     If $n\le 7$, then $\#\ch{n} = 2n + 3 < 18$.
% 	Even if $n=8$, then $\#\lamb{\dectfn}{\rem} > \#\ch{8}=19$
% 	because $\#\lamb{\dect{2}{8}}{0} = 20$,
% 	$\#\lamb{\dect{3}{8}}{2} = 26$, and $\#\lamb{\dect{4}{8}}{0} = 24$.
% \qed
% \end{prf}

% We omit the proof of Lemma~\ref{lemm:size} and Lemma~\ref{lemm:le8}
% because it is easy to see.
% Hereafter, we denote $\fact$ in minimum $\#\lamb{\dectfn}{\rem}$ by $\minf$,
% and denote $\dect{\minf}{\nbar}$ by $\mint{\nbar}$.

\begin{lemm}\label{lemm:ge8}
	Let $n$ and $\fact$ be natural numbers such that $\fact <n$,
	and let $\rem = n \bmod \fact$ and $\nbar = n-r$.
    % Then, the inverse of Lemma \ref{lemm:le8} holds, that is,
    Then,
    $\dectfn +\rem$ such that $\#\ch{n}>\#\lamb{\dectfn}{\rem}$ exists
	when $n > 8$.
	% \qed
\end{lemm}
% \begin{prf}
%   	We show that $\mint{\nbar}$ such that $\#\ch{n}>\#\lamb{\mint{\nbar}}{\rem}$ 
% 	exists for any $n>8$.
%     Let $\fact_u$ be the maximum integer such that $\fact_u \le \sqrt{n}$, and
%     let $\rem_{\fact_u}=n\bmod\fact_u$ and $\nbar_{\fact_u}=n-\rem_{\fact_u}$.
% 	By Lemma \ref{lemm:size} and Lemma \ref{lemm:interval},
%     \begin{align}
% 		\#\lamb{\dectfn}{\rem}
%         \le \#\lamb{\dect{\fact_u}{\nbar_{\fact_u}}}{\rem_{\fact_u}}
%         \le 4\fact_u + 12
%         \le 8\sqrt{n}+12
% 		\label{eq:lemm:ge8:prf:1}
%     \end{align}
%     If $n > 24$,
%   	$\#\lamb{\mint{\nbar}}{\rem} < \#\ch{n}$
%     follows $\#\ch{n} = 2n+3 > 8\sqrt{n} + 14$ and inequality (\ref{eq:lemm:ge8:prf:1}).
%     By Table \ref{table:lemm:ge8:prf},
%     it also holds in the case of $8 < n \le 24$.
%     \begin{table}[tb]
%   	\begin{center}
%   		\begin{tabular}{|c|c|c|c|c|c|c|c|c|}
%   		\hline
%           $n$ & $\#\ch{n}$ &
%           $\#\lamb{\mint{\nbar}}{\rem}$ &
%           $n$ & $\#\ch{n}$ &
%           $\#\lamb{\mint{\nbar}}{\rem}$ &
%           $n$ & $\#\ch{n}$ &
%           $\#\lamb{\mint{\nbar}}{\rem}$ \\
%           \hline \hline
%   		 9 & 21 & 20 & 14 & 31 & 20 & 19 & 41 & 20 \\
%   		10 & 23 & 22 & 15 & 33 & 22 & 20 & 43 & 22 \\
%   		11 & 25 & 24 & 16 & 35 & 24 & 21 & 45 & 24 \\
%   		12 & 27 & 24 & 17 & 37 & 24 & 22 & 47 & 24 \\
%   		13 & 29 & 26 & 18 & 39 & 26 & 23 & 49 & 26 \\
%           &&&&&& 24 & 51 & 10 \\
%   		\hline
%       \end{tabular}
%   		\caption{$\ch{n}=2n+3$ and 
% 		  $\#\lamb{\mint{\nbar}}{\rem}$ in $8 < n\le 24$}
%   	\label{table:lemm:ge8:prf}
%   	\end{center}
%   	\end{table}
% \qed
% \end{prf}
\begin{prf}
  	We show that $\mint{\nbar}$ such that $\#\ch{n}>\#\lamb{\mint{\nbar}}{\rem}$ 
	exists for any $n>8$.
	Let $\fact_{half}$ be the integer such that $\fact_{half} = \lfloor n/2 \rfloor$, and
	let $\rem_{\fact_{half}}=n\bmod\fact_{half}$ and $\nbar = n - \rem_{\fact_{half}}$.
	Here, $\rem_{\fact_{half}}$ is at most $1$.
	If we decompose $n$ into the numerical expression such that
	$\dect{\fact_{half}}{\nbar} + \rem_{\fact_{half}} 
	= \fact_{half} + \fact_{half} + \rem_{\fact_{half}}$,
	then 
	$\#\lamb{\dect{\fact_{half}}{\nbar}}{\rem_{\fact_{half}}}
	= 2\fact_{half} + 16 + \rem_{\fact_{half}} \le n + 18$ holds.
	Therefore, because $\#\ch{n} = 2n+3$, Lemma~\ref{lemm:ge8} holds for $n > 15$.
    As shown in Table \ref{table:lemm:ge8:prf},
    it also holds for $8 < n \le 15$.
\qed
\end{prf}


\setlength\textfloatsep{0pt}
    \begin{table}[tb]
  		\begin{tabular}{|c|c|c|c|c|c|c|c|c|}
  		\hline
          $n$ & $\#\ch{n}$ &
          $\#\lamb{\mint{\nbar}}{\rem}$ &
          $n$ & $\#\ch{n}$ &
          $\#\lamb{\mint{\nbar}}{\rem}$ &
          $n$ & $\#\ch{n}$ &
          $\#\lamb{\mint{\nbar}}{\rem}$ \\
          \hline \hline
  		  9 & 21 & 20 &
          12 & 27 & 24 &
          15 & 33 & 28
          \\
  		  10 & 23 & 22 &
          13 & 29 & 26 &
          & &
          \\
          11 & 25 & 24 &
          14 & 31 & 28 &
          & &
          \\
  		\hline
      \end{tabular}
		% \vspace{-18pt}
  		\caption{$\ch{n}=2n+3$ and 
		  $\#\lamb{\mint{\nbar}}{\rem}$ in $8 < n\le 15$}
  	\label{table:lemm:ge8:prf}
  	\end{table}


\subsection{Further compaction}
\label{sec:further_compaction}

% \begin{lemm}\label{lemm:interval}
%   With any natural number $n$, $\fact^*$ is in $[2, 2\sqrt{n}]$.
% \end{lemm}
% \begin{prf}
%     Let $N_a(\dectfn)$, $N_m(\dectfn)$, 
%     and $N_e(\dectfn)$ be
% 	the numbers of additions, multiplications, and exponentiations in $\dectfn$, respectively.
% 	Note that we can generate $\dectfn$ with some arithmetic operations 
% 	only if $\fact\le n/2$.
%     Let $\fact_t$ be an integer such that $\sqrt{n} < \fact_t \le n/2$, and
%     let $\rem_{\fact_t} = n\bmod \fact_t$ and
%     $\nbar_{\fact_t} =n - \rem_{\fact_t}$.
%     Here, $\dect{\fact_t}{\nbar_{\fact_t}}$ includes
% 	some additions, no multiplication and no exponentiation.
% 	Thus, $N_a(\dect{\fact_t}{\nbar_{\fact_t}}) \ge 1$,
%     $N_m(\dect{\fact_t}{\nbar_{\fact_t}}) 
%     = N_e(\dect{\fact_t}{\nbar_{\fact_t}}) = 0$.
% 	Then, by Lemma \ref{lemm:size}, the following holds:
%     \begin{align}
%   	  \#\lamb{\dect{\fact_t}{\nbar_{\fact_t}}}{\rem_{\fact_t}}
%   	  = 4 N_a(\dect{\fact_t}{\nbar_{\fact_t}}) + 2\fact_t 
%         + 2\rem_{\fact_t} + 12\label{eq:lemm:interval:prf:1}.
%     \end{align}
%     Next, let $\fact_u$ be the maximum integer such that $\fact_u \le \sqrt{n}$,
%     and let $\rem_{\fact_u}=n\bmod \fact_u$ and $\nbar_{\fact_u}=n-\rem_{\fact_u}$.
%     Here, $N_m(\dect{\fact_u}{\nbar}) = 1$, $N_a(\dect{\fact_u}{\nbar_{\fact_u}}) 
%     = N_e(\dect{\fact_u}{\nbar_{\fact_u}}) = 0$.
% 	Similar to the above, by Lemma \ref{lemm:size},
%     \begin{align}
%   	  \#\lamb{\dect{\fact_u}{\nbar_{\fact_u}}}{\rem_{\fact_u}}
%   	  &= 2 N_m(\dect{\fact_u}{\nbar_{\fact_u}}) + 2\fact_u 
%         + 12 + 2\rem_{\fact_u}
%   	  =2\fact_u + 14 + 2\rem_{\fact_u}\nn\\
%   	  &\le 2\fact_u + 14 + 2(\fact_u - 1)
%         = 4\fact_u + 12\label{eq:lemm:interval:prf:2}.
%     \end{align}
% 	Therefore, we obtain the following inequality:
%     \begin{align}
%     (\ref{eq:lemm:interval:prf:1}) - (\ref{eq:lemm:interval:prf:2}) \ge
%     2(\fact_t + \rem_{\fact_t} - 2\fact_u)\label{eq:lemm:interval:prf:3}.
%     \end{align}
%     The right-hand side of inequality (\ref{eq:lemm:interval:prf:3}) is larger than $0$ 
% 	if $\fact_t\ge 2\fact_u$.
%     Since $\fact_t > \sqrt{n}$, 
%     $\#\lamb{\dectfn}{\rem}$ is not minimized when $\fact>2\sqrt{n}$.
% \qed
% \end{prf}

Lemma \ref{lemm:ge8} implies that if $\minf > 8$,
we can convert $\lamb{\mint{\nbar}}{\rem}$ into a more compact $\lambda$-term
by applying RTP to $\minf$ and translating its result into a $\lambda$-term
using Algorithm \ref{alg:toLambda}.
This operation can be applied recursively 
while $\minf$, at each recursion step, is greater than $8$.
We denote the final $\lambda$-term obtained as a result as follows:
\begin{align*}
	(\lambda pfx.M_i)~\ch{\minf_{i+1}}
	&:=\lamb{\mint{\bar{\minf_i}}}{\rem_{\minf_i}}\\
	\minl{n}&:=(\lambda pfx.M_0)((\lambda pfx.M_1)\cdots
	((\lambda pfx.M_N)~\ch{\minf_{N+1}})\cdots),
\end{align*}
where $0\le i\le N,~\minf_0=n,~\rem_{\minf_i}=\minf_i\bmod\minf_{i+1}$, and
$\bar{\minf_i}=\minf_i-\rem_{\minf_i}$.
% We show an algorithm generating $\minl{n}$ for given $\ch{n}$ in Algorithm \ref{alg:main}.
%This is our main contribution in this paper.

% \begin{algorithm}[t]
% 	\caption{Algorithm generating $\minl{n}$ for $\ch{n}$}
% 	\label{alg:main}
% 	\begin{algorithmic}[1]
% 		\Require $\ch{n}$
% 		\Ensure $\minl{n}$
% 		\Function{Compaction}{$\ch{n}$}
% 		\State $n \leftarrow $ the natural number corresponding $\ch{n}$
% 		\For{$\fact = 2$ to $2\sqrt{n}$}
% 		\State $\remf \leftarrow n \bmod \fact$
% 		\State $\nbar \leftarrow n - \remf$
% 		\State $\dectfn \leftarrow $
% 			RTP of $\nbar$ by $\fact$
% 		\State $\lamb{\dectfn}{\remf} \leftarrow $
% 			$\lambda$-term translated from $\dectfn+\remf$
% 			via Algorithm \ref{alg:toLambda}
% 		\EndFor
% 		\State $\mint{\nbar} \leftarrow $
% 			$\dectfn$ in minimum $\#\lamb{\dectfn}{\remf}$
% 		\State $\minr \leftarrow $
% 			$\remf$ in minimum $\#\lamb{\dectfn}{\remf}$
% 		\If{$\minr\le 8$} {\bf return} $\lamb{\mint{\nbar}}{\minr}$ 
% 		\Else ~{\bf return} $(\text{The function part of }(\lamb{\mint{\nbar}}{\minr})
% 			(\Call{Compaction}{\ch{\minr}}))$
% 		\EndIf
% 		\EndFunction
% 		\State {\bf main}
% 		\State ~~~~~{\bf output}
% 		$\Call{Compaction}{\ch{n}}$
% 		\State {\bf end main}
% \end{algorithmic}
% \end{algorithm}

% \subsection{The upper bound of the size}
\begin{lemm}\label{lemm:fsize}
	Let $n$ and $\fact$ be natural numbers such that $\fact <n$,
	and let $\rem = (n \bmod \fact)$ and $\nbar = n-r$.
	Then, the size of the function part of $\lamb{\mint{\nbar}}{\rem}$ 
	is less than or equal to
	that of $\lamb{\dect{2}{\nbar}}{\rem}$.
\end{lemm}
\begin{prf}
	We demonstrate this by reduction to contradiction.
	We assume that the size of the function part of $\lamb{\mint{\nbar}}{\rem}$
	is larger than that of $\lamb{\dect{2}{\nbar}}{\rem}$.
	Relative to the size of the Church numerals appearing in the argument parts, 
	$\#\ch{2} \le \#\ch{\minf}$ holds.
	$\#\lamb{\dectfn}{\rem}$ follows
	the sum of the sizes of the function and argument parts.
	Therefore, 
	$\#\lamb{\mint{\nbar}}{\rem} > \#\lamb{\dect{2}{\nbar}}{\rem}$ follows the assumption.
	However, this contradicts $\lamb{\mint{\nbar}}{\rem}$ 
	being the minimum $\lambda$-term of $\lamb{\dectfn}{\rem}$.
	Thus, the assumption is incorrect and the proposition is proven.
\qed
\end{prf}

\begin{theo}\label{theo}
	$\ord(\#\minl{n})$ is $\ord((\slogt n)^{\log n/\log{\log n}})$
	with natural number $n$.
\end{theo}
\begin{prf}
	Let $\fact$ be a natural number such that $\fact <n$,
	and let $\rem = (n \bmod \fact)$ and $\nbar = n-r$.
	Then, $\ord(\#\lamb{\mint{\nbar}}{\rem})$ is the sum of
	$\ord$(the size of the function part) and
	$\ord$(the size of the argument part).
	First, we consider $\ord$(the size of the function part).
	By Lemma \ref{lemm:fsize}, it is bounded by 
	$\ord$(the size of the function part of $lamb{\dect{2}{\nbar}}{\rem}$).
	Here, $\dect{2}{\nbar}$ is as follows:
	% \vspace{-20pt}
	\begin{align*}
	  \dect{2}{\nbar} = 
	      \tetr{2}{k}\dect{2}{\bar{p}_k}
	    + (\overbrace{\tetr{2}{k}}^{p_k \bmod 2})
	    + \tetr{2}{k-1}\dect{2}{\bar{p}_{k-1}}
	    + (\overbrace{\tetr{2}{k-1}}^{p_{k-1} \bmod 2})
	    + \cdots + \tetr{2}{1}\dect{2}{\bar{p}_{1}}
	    + (\overbrace{\tetr{2}{1}}^{p_1 \bmod 2})
	\end{align*}
	where $\bar{p_i}$ is $p_i - (p_i \bmod 2)$, which is a coefficient of $\tetr{\fact}{i}$
	for $1 \le i \le k$.
	Here, $p_i \bmod 2$ is at most 1.
	Then, $(\slogt{n})-1 < k \le \slogt{n}$
	holds relative to $k$.
	% Then, the following inequality holds with regard to $k$:
	% \begin{align}
	% 	(\slogt{n})-1 < k \le \slogt{n} \label{eq:theo:prf:1}
	% \end{align}
	This indicates that $k$ is the maximum integer such that $k \le \slogt{n}$.
	By Lemma \ref{lemm:size}, in the function part, the size increments
	by addition, multiplication, and exponentiation are at most 10, 5, and 2, respectively.
	Therefore, the maximum size of each term $(\tetr{2}{i}\cdot\bar{p}_i+\tetr{2}{i})$ is
	$2i+5+(\text{the size of $\bar{p_i}$})+10+2i$ where $i\le k$ 
	and these terms appear at most $k$ times.
	Note that RTP partitions each $\bar{p_i}$ recursively.
	We denote the number of recursion times by $\rho$.
	The following holds relative to the upper bound of the size of the function part in
	$\lamb{\dect{2}{\nbar}}{\rem}$:
	\begin{align*}
		\ord((2k+5+(\text{the size of $\bar{p_k}$})+10+2k)\cdot k)
		= \ord(k^2+k+k(\text{the size of $\bar{p_k}$}))
		= \ord(k^{\rho}).
	\end{align*}
	Note that $i$ can be $k$ in each recursion step, therefore,
	by Lemma \ref{lemm:tetr}, the following holds:
	% \vspace{-8pt}
	\begin{align*}
		(\tetr{2}{k})^{\rho} \le n
		\iff \rho \log{\tetr{2}{k}} \le \log{n},~~
		\rho \le \frac{\log{n}}{\log{\tetr{2}{k}}}
		< \frac{\log{n}}{\log{\tetr{2}{(\slogt{n})-1}}}
		% = \frac{\log{n}}{\log{\log{\tetr{2}{(\slogt{n})}}}}
		= \frac{\log{n}}{\log{\log{n}}}.
	\end{align*}
	Thus,
	$\ord(k^{\rho}) = \ord((\slogt{n})^{\log{n}/\log{\log{n}}})$
	holds.

	% \begin{align}
	% 	&(\tetr{2}{k})^{\rho} \le n
	% 	\iff \rho \log{\tetr{2}{k}} \le \log{n}\nn\\
	% 	&\rho \le \frac{\log{n}}{\log{\tetr{2}{k}}}
	% 	< \frac{\log{n}}{\log{\tetr{2}{(\slogt{n})-1}}}
	% 	= \frac{\log{n}}{\log{\log{\tetr{2}{(\slogt{n})}}}}
	% 	= \frac{\log{n}}{\log{\log{n}}}. \label{eq:theo:prf:2}
	% \end{align}
	% Hence, the conclusion below follows inequality (\ref{eq:theo:prf:1}) and (\ref{eq:theo:prf:2}):
	% \begin{align*}
	% 	\ord(k^{\rho}) = \ord((\slogt{n})^{\log{n}/\log{\log{n}}}).
	% \end{align*}
	Second, we consider $\ord$(the size of the argument part).
	If $\minf \le 8$, it is constant because $\ord(\#\ch{\minf}) = \ord(\#\ch{8})$.
	If $\minf > 8$,
	$\ch{\minf}$ is compacted recursively.
	By the above proof,
	the upper bound of the size of the $\lambda$-term result is
	$\ord((\slogt{\minf})^{\log{\minf}/\log{\log{\minf}}}+\#\ch{\minf_1})$
	where $\minf_1$ is $\fact_1$ 
	in minimum $\lamb{\dect{\fact_1}{\minf}}{(\minf - (\minf \bmod \fact_1))}$.
	Here, $\minf$ is clearly less than $n$.
	This is followed by
		$\ord((\slogt{\minf})^{\log{\minf}/\log{\log{\minf}}}) \le
		\ord((\slogt{n})^{\log{n}/\log{\log{n}}})$.
	% \begin{align*}
	% 	\ord((\slogt{\minf})^{\log{\minf}/\log{\log{\minf}}}) \le
	% 	\ord((\slogt{n})^{\log{n}/\log{\log{n}}}).
	% \end{align*}
	If $\ch{\minf_1} > 8$, it is also converted recursively.
	However, a similar inequality holds in each recursion step and
	the final $\minf_{\rho}$ results in a constant such that $\minf_{\rho} \le 8$.
	Therefore, 
	$\ord(\#\minl{n})$ is $\ord((\slogt n)^{\log n/\log{\log n}})$.
\qed
\end{prf}



main.bbl
% Generated by IEEEtran.bst, version: 1.14 (2015/08/26)
\begin{thebibliography}{1}
\providecommand{\url}[1]{#1}
\csname url@samestyle\endcsname
\providecommand{\newblock}{\relax}
\providecommand{\bibinfo}[2]{#2}
\providecommand{\BIBentrySTDinterwordspacing}{\spaceskip=0pt\relax}
\providecommand{\BIBentryALTinterwordstretchfactor}{4}
\providecommand{\BIBentryALTinterwordspacing}{\spaceskip=\fontdimen2\font plus
\BIBentryALTinterwordstretchfactor\fontdimen3\font minus
  \fontdimen4\font\relax}
\providecommand{\BIBforeignlanguage}[2]{{%
\expandafter\ifx\csname l@#1\endcsname\relax
\typeout{** WARNING: IEEEtran.bst: No hyphenation pattern has been}%
\typeout{** loaded for the language `#1'. Using the pattern for}%
\typeout{** the default language instead.}%
\else
\language=\csname l@#1\endcsname
\fi
#2}}
\providecommand{\BIBdecl}{\relax}
\BIBdecl

\bibitem{Kobayashi2012}
N.~Kobayashi, K.~Matsuda, A.~Shinohara, and K.~Yaguchi, ``Functional programs
  as compressed data,'' \emph{Higher-Order and Symbolic Computation}, vol.~25,
  no.~1, pp. 39--84, 2012.

\bibitem{Yaguchi2014EfficientCompression}
K.~Yaguchi, N.~Kobayashi, and A.~Shinohara, ``Efficient algorithm and coding
  for higher-order compression,'' in \emph{In proceedings of 2014 Data
  Compression Conference (DCC2014)}, March 2014, pp. 434--434.

\bibitem{DEBRUIJN1972381}
N.~de~Bruijn, ``Lambda calculus notation with nameless dummies, a tool for
  automatic formula manipulation, with application to the church-rosser
  theorem,'' \emph{Indagationes Mathematicae (Proceedings)}, vol.~75, no.~5,
  pp. 381 -- 392, 1972.

\bibitem{Mogensen2001}
T.~A. Mogensen, ``An investigation of compact and efficient number
  representations in the pure lambda calculus,'' in \emph{Revised Papers from
  the 4th International Andrei Ershov Memorial Conference on Perspectives of
  System Informatics: Akademgorodok, Novosibirsk, Russia}, ser. PSI '02.\hskip
  1em plus 0.5em minus 0.4em\relax London, UK: Springer-Verlag, 2001, pp.
  205--213.

\bibitem{tromp:DSP:2006:628}
J.~Tromp, ``Binary lambda calculus and combinatory logic,'' in \emph{Kolmogorov
  Complexity and Applications}, ser. Dagstuhl Seminar Proceedings, M.~Hutter,
  W.~Merkle, and P.~M. Vitanyi, Eds., no. 06051, 2006.

\bibitem{TakedaCompactLambda-Terms}
K.~Takeda, N.~Kobayashi, K.~Yaguchi, and A.~Shinohara, ``Compact bit encoding
  schemes for simply-typed lambda-terms,'' \emph{SIGPLAN Not.(Proceedings of
  the 21st ACM SIGPLAN International Conference on Functional Programming)},
  vol.~51, no.~9, pp. 146--157, Sep. 2016.

\end{thebibliography}
