Structural equivalence of self-referential structures

Question

Given two types, T1 and T2, how does structural equivalence work when they're self-referential? Further, how do we go about proving it?

T1: struct { a: int, b: pointer to T2 }
T2: struct { a: int, b: pointer to T1 }

I was attempting to create a directed graph, and by proving the directed graphs are equivalent, we can prove the types are equivalent. For example:

$$G1: T1.b \rightarrow T2 \rightarrow T2.b \rightarrow T1 \rightarrow T1.b$$ $$G2: T2.b \rightarrow T1 \rightarrow T1.b \rightarrow T2 \rightarrow T2.b$$

I don't know if I'm the right track here or not.

Answer 1

Since your types both reference each other, these are not inductive types, but coinductive types.$^{1}$ That's because, if you expand out T1 and T2 (as you have done partially in the question), you get an infinite structure:

T1 = { a: int, { a: int, { a: int, { a: int , { ... } } } }

The phrase "coinductive types" may be scary, but all this means is that T1 and T2 represent infinite trees, rather than finite trees.

So your question is: how do you prove two coinductive types are structurally equivalent? The answer is with something called a bisimulation relation -- another scary word and formal concept that just means proving the two infinite trees are identical.

So in your example, we can write out the same type for T2 and get the infinite tree

T2 = { a: int, { a: int, { a: int, ... } } }

Since the infinite trees for T1 and T2 are the same, we know that types T1 and T2 are structurally equivalent.

How do we prove this formally? We would define the bisimulation relation $\sim$ -- a relation between the nodes of the infinite tree for T1 and nodes of the infinite tree for T2 -- as the set of the following three pairs: $(\text{a}, \text{a}), (T1, T2), (T2, T1)$. Here is the picture of what's going on:

  T1              T2
 /  \            /  \
a    T2         a    T1
    /  \            /  \
   a    T1         a    T2
       /  \            /  \
      a    T2         a    T1
             \               \
              ...             ...

Bisimulation relation (mapping between left nodes and right nodes):

  T1      ~      T2
  T2      ~      T1
  a       ~      a

Now notice that for any node (type) $T$, we can prove that $T \sim T'$ implies that both children of $T$ and children of $T'$ are also bisimilar: this is because the left child is always a and the right child alternates, for $T1 \sim T2$ the right children are $T2, T1$ and for $T2 \sim T1$ the right children are $T1, T2$. So the bisimulation relation is a bijection between the nodes of both trees that preserves their structure, which proves that the two trees are the same.

$^{1}$ NB: it's technically possible to interpret T1 and T2 as inductive types, but then they are both empty (have no elements) because there is no way to construct an element of T1 or T2 in an inductive manner (that is, in order to create a T1 or a T2, you need to already have a T1 or T2 for it to point to). So I assumed that's not what you meant here.

Answer 2

T1: struct { a: int, b: pointer to struct { a: int, b: pointer to T1 }}

and

T2: struct { a: int, b: pointer to struct { a: int, b: pointer to T2 }}

seem to be structurally equivalent.