1
$\begingroup$

I have an issue understanding the following definition (from https://tel.archives-ouvertes.fr/tel-00783245/document , p.82) of the continuation-passing style (CPS) transformation in the lambda calculus ($NB$: the author stipulates on p.277 that $\to$ associates to the right):

[CPS-transformation] Let $o$ be a distinguished type. For each term $t$ of type $\rho$, it is possible to construct its CPS-transformation $\overline{t}$ of type $\overline{\rho}$ in the following way:

$$\overline{x} = \lambda \Phi^{\,\rho \to o}. \Phi x^{\rho} $$ $$\overline{\lambda x^{\alpha}. N^{\beta}} = \lambda \Phi^{\,(\alpha \to \beta)' \to o}.\Phi(\lambda x^{\alpha'}. \overline{N}^{\overline{\beta \to o}})$$ $$\overline{M^{\alpha \to \beta} N^{\alpha}} = \lambda\Phi^{\beta' \to o}.\overline{M}^{\overline{\alpha \to \beta}}(\lambda m^{(\alpha \to \beta)'}. \overline{N}^{\overline{\alpha}}(\lambda n^{\alpha'}.mn\Phi)) $$ where $\Phi$ is of type $(\rho' \to o)$ is a $continuation$ of $t$. Each type $\overline{\rho}$ is defined as $(\rho' \to o) \to o$, where $\rho'$ is defined as follows: $$\rho' = \begin{cases} \rho & \text{if $\rho$ is basic} \\ \alpha' \to ((\beta' \to o) \to o), & \text{if $\rho = \alpha \to \beta$} \end{cases} $$

According to these definitions $(\alpha \to \beta)'$ is an abbreviation of $\alpha' \to ((\beta' \to o) \to o)$ and $\overline{\beta \to o}$ is of type $((\beta \to o)' \to o) \to o$, which is of type $([\beta' \to ((o' \to o) \to o)]\to o) \to o$. Accordingly we have:

$$\overline{\lambda x^{\alpha}. N^{\beta}} = \lambda \Phi^{(\alpha' \to (((\beta' \to o) \to o) \to o)}. \Phi(\lambda x^{\alpha'}. N^{([\beta' \to ((o' \to o) \to o)]\to o) \to o}) $$

I cannot see how the types match. How do $\Phi^{(\alpha' \to (((\beta' \to o) \to o) \to o)}$ and $\lambda x^{\alpha'}. N^{([\beta' \to ((o' \to o) \to o)]\to o) \to o}$ combine via function application, given that the former is of the form $ (a,(((b,c),c),c)$ and the latter of the form $a,(((b,(c,c),c), c), c)$ (we use here ',' an abbreviation for $\to$)?


$Edit$: the types seem to 'match' if we take $\Phi^{(\alpha' \to (((\beta' \to o) \to o) \to o)}$ and $\lambda x^{\alpha'}. N^{\beta \to o}$ (i.e of type $\alpha' \to (\beta \to o)$), so that $[\Phi^{(\alpha' \to (((\beta' \to o) \to o) \to o)}(\lambda x^{\alpha'}. N^{\beta \to o})]$ is of type $o \to o$. Is this the intended reduction of this term?

$\endgroup$

Your Answer

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

Browse other questions tagged or ask your own question.