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?


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.