Wie kann man Beziehungen zwischen „Klassen“ von Typen beweisen?

Nachdem ich Effekte als Sitzungen, Sitzungen als Effekte gelesen hatte , fragte ich mich, wie ein Äquivalenznachweis zwischen beiden stattfinden würde oder sogar ein Beweis dafür, dass Sitzungstypen ein Typ- und Effektsystem sind.

Wie kann man allgemeiner eine Beziehung (z. B. Äquivalenz) zwischen verschiedenen "Klassen" * von Typen nachweisen? Wäre dieser Ausdruckstest von Orchard und Yoshida ausreichend?

[*]: Ich weiß nicht, wie ich es richtig definieren soll, ich möchte keine "Arten von Typen" oder "Arten von Typen" verwenden.

Ein Ansatz für solche Fragen ist die Codierung .

Angenommen, Sie haben eine Sprache $L_1$ und eine Sprache $L_2$ und möchten zeigen, dass sie irgendwie "gleich" sind. Sie können dies tun, indem Sie eine Codierung finden

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

und zeigen Sie dann, dass für alle Programme Folgendes gilt:$L_1$$M, N$

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

Hier ist ein gewählter Begriff der Programmäquivalenz für . Um dies für typisierte Sprachen zu tun, ordnet man Typen normalerweise auch über eine Funktion die auf Typisierungsumgebungen erweitert ist, so dass etwa Folgendes gilt:$\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}$$ Hier ist das Typisierungsurteil für . Der gesamte Ansatz wird als vollständige Abstraktion bezeichnet .$\vdash_i$$L_i$

Um den "Fluch der Church-Turing-Universalität" zu vermeiden, werden typischerweise Bedingungen auferlegt , z. B. dass es kompositorisch ist oder unter injektiver Umbenennung geschlossen wird. Je mehr Bedingungen erfüllt, stärker ist das vollständige Abstraktionsergebnis.$\SEMB{\cdot}$$\SEMB{\cdot}$

Dies versuchen auch Orchard & Yoshida (Theoreme 1-5), obwohl sie es nicht ganz erreichen.