# The continuation passing style transformation in the lambda calculus

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?