<p>One approach to such questions is via <strong>encodings</strong>.  </p>

<p>Say you have a language $L_1$ and a language $L_2$ and you want to show that they are somehow "the same", you can do this by finding an encoding</p>

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

<p>and then show that for all $L_1$ programs $M, N$ the following holds:</p>

<p>$$
   M \cong_1 N
   \qquad \text{iff} \qquad
   \SEMB{M_1} \cong_2 \SEMB{M_2}
$$</p>

<p>Here $\cong_i$ is a chosen notion of program equivalence for $L_i$. In order to do this for typed languages, one typically also maps $L_1$-types to $L_2$ by way of a function $\SEMBTYPE{\cdot}$ which is extended to typing environments, such that
something like the following holds:</p>

<p>$$
   \Gamma \vdash_1 M : \alpha
   \qquad \text{implies} \qquad
   \SEMBTYPE{\Gamma} \vdash_2 \SEMB{M} : \SEMBTYPE{\alpha}
$$
Here $\vdash_i$ is the typing judgement for $L_i$. 
The whole approach is called <strong>full abstraction</strong>.</p>

<p>In order to avoid the "curse of Church-Turing universality", one typically imposes conditions on $\SEMB{\cdot}$, e.g. that it's compositional, or closed under injective renaming. The more conditions $\SEMB{\cdot}$ meets, the stronger the full abstraction result.</p>

<p>This is also Orchard &amp; Yoshida are attempting to do (Theorems 1- 5), although they don't quite achieve it.</p>

CC BY-SA 3.0
2016-08-08T14:26:20.860Z
2016-08-08T14:26:20.860Z
Martin Berger
<p>After reading <a href="https://www.doc.ic.ac.uk/~dorchard/publ/popl16-orchard-yoshida.pdf">Effects as Sessions, Sessions as Effects</a>, I was wondering how would a proof of equivalence between both take place, or even, a proof of Sessions types being a Type and Effect System.</p>

<p>In a more generic fashion, how one can prove a relation (e.g. equivalence) between different "classes"* of types? Would that expressiveness test as done by Orchard and Yoshida be enough?</p>

<p>[*]: I don't know how to correctly define it, I don't want to use "kinds of types" or "types of types".</p>

<type-theory><proofs><type-systems>
How to prove relations between "classes" of types?
cyberglot
# How to prove relations between "classes" of types?

(Asked by: username_0 on 2016-08-08)

After reading [Effects as Sessions, Sessions as Effects](https://www.doc.ic.ac.uk/~dorchard/publ/popl16-orchard-yoshida.pdf), I was wondering how would a proof of equivalence between both take place, or even, a proof of Sessions types being a Type and Effect System.

In a more generic fashion, how one can prove a relation (e.g. equivalence) between different "classes"\* of types? Would that expressiveness test as done by Orchard and Yoshida be enough?

[\*]: I don't know how to correctly define it, I don't want to use "kinds of types" or "types of types".

**Tags:** type-theory, proofs, type-systems

---

## 1 answers

### Answer by username_1 on 2016-08-08. Score: 6

One approach to such questions is via **encodings**.

Say you have a language $L\_1$ and a language $L\_2$ and you want to show that they are somehow "the same", you can do this by finding an encoding

$$
\newcommand{\SEMBTYPE}[1]{\ulcorner #1 \urcorner}
\newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack}
\SEMB{\cdot} : L\_1 \rightarrow L\_2
$$

and then show that for all $L\_1$ programs $M, N$ the following holds:

$$
M \cong\_1 N
\qquad \text{iff} \qquad
\SEMB{M\_1} \cong\_2 \SEMB{M\_2}
$$

Here $\cong\_i$ is a chosen notion of program equivalence for $L\_i$. In order to do this for typed languages, one typically also maps $L\_1$-types to $L\_2$ by way of a function $\SEMBTYPE{\cdot}$ which is extended to typing environments, such that
something like the following holds:

$$
\Gamma \vdash\_1 M : \alpha
\qquad \text{implies} \qquad
\SEMBTYPE{\Gamma} \vdash\_2 \SEMB{M} : \SEMBTYPE{\alpha}
$$
Here $\vdash\_i$ is the typing judgement for $L\_i$.
The whole approach is called **full abstraction**.

In order to avoid the "curse of Church-Turing universality", one typically imposes conditions on $\SEMB{\cdot}$, e.g. that it's compositional, or closed under injective renaming. The more conditions $\SEMB{\cdot}$ meets, the stronger the full abstraction result.

This is also Orchard & Yoshida are attempting to do (Theorems 1- 5), although they don't quite achieve it.


---

