Como provar relações entre "classes" de tipos?

Depois de ler Efeitos como Sessões, Sessões como Efeitos , fiquei pensando como seria uma prova de equivalência entre os dois, ou mesmo uma prova dos tipos de Sessões como sendo um Sistema de Tipo e Efeito.

De uma maneira mais genérica, como se pode provar uma relação (por exemplo, equivalência) entre diferentes "classes" * de tipos? Esse teste de expressividade feito por Orchard e Yoshida seria suficiente?

[*]: Não sei como defini-lo corretamente, não quero usar "tipos de tipos" ou "tipos de tipos".

Uma abordagem para essas questões é através de codificações .

Digamos que você tenha um idioma $L_1$ e um idioma $L_2$ e queira mostrar que eles são de alguma forma "iguais", você pode fazer isso encontrando uma codificação

$$\newcommand{\SEMBTYPE}[1]{\ulcorner #1 \urcorner} \newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack} \SEMB{\cdot} : L_1 \rightarrow L_2$$

e, em seguida, mostre que, para todos os programas o seguinte é válido:$L_1$$M, N$

$$M \cong_1 N \qquad \text{iff} \qquad \SEMB{M_1} \cong_2 \SEMB{M_2}$$

Aqui é uma noção escolhida de equivalência de programa para . Para fazer isso nos idiomas digitados, normalmente também é tipos para por meio da função que é estendida aos ambientes de digitação, de forma que algo como o seguinte seja válido:$\cong_i$$L_i$$L_1$$L_2$$\SEMBTYPE{\cdot}$

$$\Gamma \vdash_1 M : \alpha \qquad \text{implies} \qquad \SEMBTYPE{\Gamma} \vdash_2 \SEMB{M} : \SEMBTYPE{\alpha}$$ Aqui é o julgamento de digitação para . Toda a abordagem é chamada de abstração completa .$\vdash_i$$L_i$

Para evitar a "maldição da universalidade de Church-Turing", normalmente impõe-se condições em , por exemplo, que seja de composição ou seja fechado com renomeação injetiva. Quanto mais condições , mais forte será o resultado completo da abstração.$\SEMB{\cdot}$$\SEMB{\cdot}$

Isso também é o que Orchard e Yoshida estão tentando fazer (Teoremas 1 a 5), ​​embora não o alcancem.