# how to prove the following is a bijection?

I have a translation function which translates $\lambda$-terms to another representation let me call it $G_\lambda$, as follows.

$\chi(x)$ $=$ $X^2$ if $x \notin \Gamma$

$\chi(x)$ $=$ $X$ if $x:X \in \Gamma$

$\chi(\lambda x.t_1)$ $=$ $abs(X^1,\chi(t_1))$ and do $\Gamma,x:X^1$

$\chi(t_1 \, t_2)$ $=$ $app(\chi(t_1),\chi(t_2))$

where to translate $\chi(\lambda x.t_1)$, it creates a distinct $X^1$ and add a pair $x:X$ to set $\Gamma$.

$\chi(x)$ look $x$ in $\Gamma$, so we can use already added $X^1$ as bound variable or create a distinct $X^2$ for the free variable $x$.

so, a $\lambda$-term $\lambda x.yx$ will be $abs(X^1.app(Y^2,X^1))$.

I think $\chi$ is a bijection. It is obvious that function $\chi$ maps one $\lambda$-term to one $G_\lambda$ representation, so it is injective.

My problem is that since $X^1$ and $X^2$ are created fresh, if you translate a $\lambda$-term $\lambda x.yx$ twice, then you will have two representation such as $abs(X^1.app(Y^2,X^1))$ and $abs(A^1.app(B^2,A^1))$, which are equal terms but not syntactically same.

But how can i prove from $G_\lambda$ to $\lambda$-term is a surjective?

• I believe you need to model the source of fresh variable names more carefully, e.g. adding it as a parameter to $\chi$ (as well as $\Gamma$). – chi Dec 7 '16 at 16:07
• @chi. I am thinking to write a inverse function of $\chi$, and show that function is injection. both way injection, so bijection. do you think that is correct way to do? – alim Dec 8 '16 at 7:10
• You should treat bound variables more carefully. If you declare that terms and expressions are equal up to $\alpha$-conversion, then your problem disappears. Another possibility is to define a function which generates fresh names in some deterministic way. Then, translating the same thing twice will give you the exact same answer twice. – Andrej Bauer Dec 8 '16 at 8:59

One option could be adding more parameters to $\chi$ so to make both $\Gamma$ and a fresh name source $\phi \in {\sf Names}^\infty$ explicit:
$$\begin{array}{l} \chi(\Gamma, x, X;\phi) = X \mbox{ if } x \not\in\Gamma \\ \chi(\Gamma, x, \phi) = X \mbox{ if } x:X \in\Gamma \\ \chi(\Gamma, \lambda x. t, X;\phi) = abs(X, \chi(\Gamma;x:X, t, \phi)) \\ \chi(\Gamma, t_1 t_2, \phi) = app(\chi(\Gamma, t_1, \phi^1),\chi(\Gamma, t_2, \phi^2)) \\ \qquad \mbox{where } \phi = \phi^1_0 \phi^2_0 \phi^1_1 \phi^2_1 \phi^1_2 \phi^2_2 \ldots \end{array}$$
You can then state a form of injectivity as $$\chi(\Gamma, t_1, \phi) = \chi(\Gamma, t_2, \phi) \implies t_1 = t_2$$ and surjectivity as $$\forall T.\ \exists \Gamma, t, \phi.\ \chi(\Gamma, t, \phi) = T$$
Note that some stronger forms of injectivity do not hold. E.g. $$\chi(\Gamma_1, t_1, \phi) = \chi(\Gamma_2, t_2, \phi) \implies \Gamma_1 = \Gamma_2 \land t_1 = t_2$$ is false since $$\chi(x:X,x, \phi) = \chi(y:X,y, \phi) \land x:X \neq y:X$$ Similarly, this does not hold: $$\chi(\Gamma, t, \phi_1) = \chi(\Gamma, t, \phi_2) \implies \phi_1 = \phi_2$$ since only a finite portion on $\phi$ is needed by $\chi$.
• what $\mbox{where } \phi = \phi^1_0 \phi^2_0 \phi^1_1 \phi^2_1 \phi^1_2 \phi^2_2 \ldots$ means, explain to me? – alim Dec 8 '16 at 17:22
• @alim There I have split the infinite sequence $\phi$ into two infinite sequences $\phi^1,\phi^2$ by taking the elements in even/odd position. In such way from a source of infinitely many fresh names I got two similar sources. – chi Dec 8 '16 at 18:15