4
$\begingroup$

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?

$\endgroup$
  • 4
    $\begingroup$ 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$). $\endgroup$ – chi Dec 7 '16 at 16:07
  • $\begingroup$ @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? $\endgroup$ – alim Dec 8 '16 at 7:10
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Dec 8 '16 at 8:59
1
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – alim Dec 8 '16 at 17:22
  • $\begingroup$ @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. $\endgroup$ – chi Dec 8 '16 at 18:15

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.