# Compaction of Church Numerals
## 3 Proposed Method
### Translation from TAE to \(\lambda\)-Term  
Here, we consider how we translate an TAE \(E_{\varphi}[n]\) to a corresponding \(\lambda\)-term. A simple method is to translate each arithmetic operation occurring in \(E_{\varphi}[n]\) by using \(\lambda\)-terms stated in Corollary 2. For example, for \(E_{2}[200]={}^{3}2\cdot({}^{2}2\cdot 2+{}^{2}2)+{}^{2}2\cdot 2\), the translated \(\lambda\)-term is obtained as  
\[\text{Add}(\text{Mul}(\text{Tet}(2,3),\text{Add}(\text{Mul}(\text{Tet}(2,2), 2),\text{Tet}(2,2))),\text{Mul}(\text{Tet}(2,2),2)).\]  
As seen above, the corresponding \(\lambda\)-term seems to become long. However, we can translate the TAE to a compact \(\lambda\)-term. **Definition 9** (Corresponding functional \(\lambda\)-terms (CFLT)). : _Let \(n\) and \(\varphi\) be natural numbers. We say a \(\lambda\)-term \(M\) is a corresponding functional \(\lambda\)-term (CFLT) of TAE \(E[n]\) if both of the following conditions hold for \(M\):_1. \(M\) _has the form of_ \((\lambda p.\lambda f.\lambda x.\hat{M})\)__\(\mathcal{C}(\varphi)\)_, where_ \(\hat{M}\) _is a_ \(\lambda\)_-term that contains no Church numerals._
2. \(M\longrightarrow^{*}_{\beta}\mathcal{C}(n)\)_._  
_For a given TAE \(E\), We denote a CFLT of \(E\) by \(\Lambda(E)\)._  
For example, for \(E_{2}[200]={}^{3}2\cdot({}^{2}2\cdot 2+{}^{2}2)+{}^{2}2\cdot 2\), one of its CFLTs is  
\[\Lambda(E_{2}[200])=(\lambda p.\lambda f.\lambda x.p\ p\ p\ (\lambda y.p\ p\ (\lambda z.p\ f\ z)\ (p\ p\ f\ y))\ (p\ p\ (\lambda w.p\ f\ w)\ x))\ \mathcal{C}(2). \tag{1}\]  
The size of the above (1) is 48, which is much smaller than \(\#\mathcal{C}(200)=403\). For TAE \(E_{\varphi}\), the following lemma holds. Lemma 1: _For any TAE \(E_{\varphi}\), its CFLT exists._  
Proof: We prove the lemma by induction. Considering \(\lambda\)-terms stated in Corollary 2, for \(E_{\varphi}=\varphi\) and \(E_{\varphi}={}^{t}\varphi\), their CFLTs are obtained as  
\[\Lambda(\varphi) = (\lambda p.\lambda f.\lambda x.p\ f\ x)\ \mathcal{C}(\varphi)\ \ \text{ and}\] \[\Lambda({}^{t}\varphi) = (\lambda p.\lambda f.\lambda x.\overbrace{\,p\ p\ \cdots\ p}^{t}\ f\ x)\ \mathcal{C}(\varphi),\]  
respectively. Let \(E_{\varphi}^{(1)}\) and \(E_{\varphi}^{(2)}\) be TAEs. Then, we assume that there are CFLTs of \(E_{\varphi}^{(1)}\) and \(E_{\varphi}^{(2)}\). Moreover, by Definition 9, we assume that \(\Lambda(E_{\varphi}^{(1)})=(\lambda p.\lambda f.\lambda x.\hat{M}^{(1)})\ \mathcal{C}(\varphi)\) and \(\Lambda(E_{\varphi}^{(2)})=(\lambda p.\lambda f.\lambda x.\hat{M}^{(2)})\ \mathcal{C}(\varphi)\). Here, CFLTs of \(E_{\varphi}+E_{\varphi}\) and \(E_{\varphi}\cdot E_{\varphi}\) are obtained as  
\[\Lambda(E_{\varphi}^{(1)}+E_{\varphi}^{(2)}) = (\lambda p.\lambda f.\lambda x.(\lambda y.\hat{M}^{(1)}[x:=y])\ ((\lambda y.\hat{M}^{(2)}[x:=y])\ x))\ \mathcal{C}(\varphi)\ \ \text{ and}\] \[\Lambda(E_{\varphi}^{(1)}\cdot E_{\varphi}^{(2)}) = (\lambda p.\lambda f.\lambda x.(\lambda g.\lambda y.\hat{M}^{(1)}[ f:=g,x:=y])\ (\lambda y.\hat{M}^{(2)}[x:=y])\ x)\ \mathcal{C}(\varphi),\]  
respectively. For compaction, next we introduce _simplification_ of \(\lambda\)-terms. Definition 10 (Simplification of \(\lambda\)-terms): Let \(x\) be a variable, \(M_{1}\) and \(M_{2}\) be \(\lambda\)-terms, and \(\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\  
For example, for \(n=201\) and \(\varphi=2\), \(T_{\varphi}[n]=T_{2}[201]={}^{3}\!2\cdot({}^{2}\!2\cdot 2+{}^{2}\!2)+{}^{2}\!2 \cdot 2+1\). In Definition 11, note that each coefficient \((p_{i}-r_{i})\) of \({}^{i}\varphi\) is a multiple of \(\varphi\), and then, each \(T_{\varphi}[p_{i}-r_{i}]\) generates just \(E_{\varphi}[p_{i}-r_{i}]\) without any remainder. Theorem 1.: _For given natural numbers \(n\) and \(\varphi\geq 2\), \(T_{\varphi}[n]\) is uniquely determined._  
Proof. : We prove the statement by induction. For \(n\leq\varphi\), the statement clearly holds.