Theoretical Foundation of Typechecking Algorithm for Equi-Recursive Types

Definition[Induction and Coinduction]

  1. Principle of Induction: if X is \mathcal{F}-closed, then \mu\mathcal{F}\subseteq X
  2. Principle of Coinduction: if X is \mathcal{F}-consistent, then X\sube\upsilon\mathcal{F} 1

The intuition comes from the their definitions, that the greatest fixed point is the union of all \mathcal{F}-consistent sets and the least fixed point is the intersection of all \mathcal{F}-closed sets.

Definition[Tree Type]

  A tree type is a partial function T:\lbrace 1,2\rbrace^\ast\rightharpoonup\lbrace\to, \times, \top \rbrace such that T(\epsilon)\downarrow, T(\pi\rho)\downarrow implies T(\pi)\downarrow, T(\pi)=\to or T(\pi)=\times implies T(\pi1)\downarrow and T(\pi2)\downarrow. Let T(\epsilon)=\top. The tree type can also be expressed by the following BNF:

T ::= \top \ |\ T\times T\ |\ T\to T

The set of all finite tree types, denoted by \mathcal{T_f}, will be the least fixed point of T, and set of all tree types (including both finite and infinite), denoted by \mathcal{T}, is the greatest fixed point of T

The tree type function actually is a function that takes an argument which is of string form and only consists of 1 and 2 as path from the root of a binary tree to one of its nodes, where 1 means left child and 2 means right child

  The subtyping relation of a type system who tolerate recursive types is thus can be defined by subtying relation on finite tree types and infinite tree types

Definition[Subtyping of Finite Types]

  For any \tau,\rho\in\mathcal{T_f}, \tau<:\rho if (\tau, \rho)\in\mu \mathcal{S_f}, where the monotone function \mathcal{S_f}:\mathcal{P}(\mathcal{T_f}\times\mathcal{T_f})\to(\mathcal{T_f}\times\mathcal{T_f}) is defined by:

\mathcal{S_f}(R)=&\ \lbrace (\tau, \top)\ |\ \tau\in\mathcal{T_f} \rbrace \\
\cup&\ \lbrace (\tau_1\times\tau_2, \rho_1\times\rho_2)\ |\ (\tau_1, \rho_1), (\tau_2, \rho_2)\in R \rbrace \\
\cup&\ \lbrace (\tau_1\to\tau_2, \rho_1\to\rho_2)\ |\ (\rho_1, \tau_1), (\tau_2, \rho_2)\in R \rbrace

Definition[Subtyping of Infinite Types]

  For any \tau,\rho\in\mathcal{T}, \tau<:\rho if (\tau, \rho)\in\nu \mathcal{S}, where the monotone function \mathcal{S}:\mathcal{P}(\mathcal{T}\times\mathcal{T})\to(\mathcal{T}\times\mathcal{T}) is defined by:

\mathcal{S}(R)=&\ \lbrace (\tau, \top)\ |\ \tau\in\mathcal{T_f} \rbrace \\
\cup&\ \lbrace (\tau_1\times\tau_2, \rho_1\times\rho_2)\ |\ (\tau_1, \rho_1), (\tau_2, \rho_2)\in R \rbrace \\
\cup&\ \lbrace (\tau_1\to\tau_2, \rho_1\to\rho_2)\ |\ (\rho_1, \tau_1), (\tau_2, \rho_2)\in R \rbrace

  Notice that the generating function of finite and infinite types are the same, two definition only differs from the choice of fixed point.

Definition[Invertible Function]

  A generating function \mathcal{F} is said to be invertible if for all x\in\mathcal{U}, the family of sets G_x=\lbrace X\sube\mathcal{U}\ |\ x\in\mathcal{F}(X) \rbrace is strictly ordered and well-founded under the set inclusion. If \mathcal{F} is invertible, then we can define a partial function sup_{_\mathcal{F}}:\mathcal{U}\rightharpoonup\mathcal{P(U)} as:

X &\text{if } X = min(G_x)\\
\uparrow &\text{if } G_x = \empty

The sup_{\tiny\mathcal{F}} is basically a function that gives the set who can be used to generate, or provide its argument, if S is the mininal set satisfies S=\mathcal{F}(X) and x\in S, then sup_{_\mathcal{F}}(x)=S

  We can generalize sup_{_\mathcal{F}} to sets:

\bigcup_{x\in X}sup_{_\mathcal{F}}(x) &\text{if } \forall x\in X.sup_{_\mathcal{F}}(x)\downarrow \\
\downarrow &\text{elsewise}

Membership Checking

  We can check if a set X is the subset of the greatest fixed point of a function \mathcal{F} by leveraging the sup_{\tiny\mathcal{F}}, define gfp:\mathcal{P(U)}\to\lbrace true, false\rbrace as follow:

false &\text{if }sup_{\tiny\mathcal{F}}(X)\uparrow\\
true &\text{if } sup_{\tiny\mathcal{F}}(X)\sube X\\
gfp_{\tiny\mathcal{F}}(sup_{\tiny\mathcal{F}}(X)\cup X) &\text{elsewise}

and let gfp_{\tiny\mathcal{F}}(x)\equiv gfp_{\tiny\mathcal{F}}(X)

  For the next we will prove the correctness of function gfp_{\tiny\mathcal{F}}, make sure it really returns the correct result for arbitrary X.

Lemma 1

  X\sube\mathcal{F}(Y) iff sup_{\tiny\mathcal{F}}(X)\downarrow and sup_{\tiny\mathcal{F}}(X)\sube Y
  From the definition of sup_{\tiny\mathcal{F}} we can see that it is sufficient to prove for all x\in\mathcal{F}(Y), sup_{\tiny\mathcal{F}}(x)\downarrow and sup_{\tiny\mathcal{F}}(x)\in Y: since x\in\mathcal{F}(Y), it's clearly that G_x\neq \empty, which means by definition, sup_{\tiny\mathcal{F}}(x)\downarrow and sup_{\tiny\mathcal{F}}(x)\sube Y(since sup_{\tiny\mathcal{F}} returns the smallest element). Conversely, from the monotonicity of \mathcal{F} we get \mathcal{F}sup_{\tiny\mathcal{F}}(x))\sube \mathcal{F}(Y), however, x\in\mathcal{F(sup_{\tiny\mathcal{F}}(x))} by definition, thus x\in\mathcal{F}(Y)

This lemma basically inverses the definition of sup_{\tiny\mathcal{F}}

Lemma 2

  Suppose P is a fixed point of \mathcal{F}, then X\sube P iff sup_{\tiny\mathcal{F}}(X)\downarrow and sup_{\tiny\mathcal{F}}(X)\sube P
  By the definition of fixed point, X\sube P\equiv X\sube F(P), then the result is obvious from lemma 1.∎

  Now we can prove the partial correctness of gfp_{\tiny\mathcal{F}}, where "partial" means that the termination proof of gfp_{\tiny\mathcal{F}} requires further constraints which will be investigated later.

Theorem[Partial Correctness of Membership Checking Function]

  1. If gfp_{\tiny\mathcal{F}}(X)=true, then X\sube\nu\mathcal{F}
  2. If gfp_{\tiny\mathcal{F}}=false, then X\not\sube\nu\mathcal{F}

  By induction on the recursive tree of gfp_{\tiny\mathcal{F}}(X)=true

  1. If the result true is returned by the second clause of gfp_{\tiny\mathcal{F}}, which is sup_{\tiny\mathcal{F}}(X)\sube X then by lemma 1 we have X\sube \mathcal{F}(X), i.e., X is \mathcal{F}-consistent, by the principle of coinduction, we have X\sube\nu\mathcal{F}. If the result is returned by the third clause, which means gfp_{\tiny\mathcal{F}}(sup_{\tiny\mathcal{F}}(X)\cup X)=true, then by the induction hypothesis, sup_{\tiny\mathcal{F}}(X)\cup X\sube \nu\mathcal{F}, thus X\sube\nu\mathcal{F}.
  2. If the result is returned by the first clause of gfp_{\tiny\mathcal{F}}, which is sup_{\tiny\mathcal{F}}(X)\uparrow, then by lemma 2, X\not\sube\nu\mathcal{F}. If the result is returned by the third clause, which means gfp_{\tiny\mathcal{F}}(sup_{\tiny\mathcal{F}}(X)\cup X)=false, then by induction hypothesis, sup_{\tiny\mathcal{F}}(X)\cup X\not\sube\nu\mathcal{F}, we have subcases:
    1. The case for X\not\sube\nu\mathcal{F} is trivial.
    2. If sup_{\tiny\mathcal{F}}(X)\not\sube\nu\mathcal{F}, then by lemma 2, X\not\sube\nu\mathcal{F}.

  Now we are going to investivate the halt condition for gfp_{\tiny\mathcal{F}}.

Definition[Reachable Set]

  Define set rch_{\tiny\mathcal{F}}(X) to be the union of pred^n(X) (n composition of function pred) for all n\geqslant 0, where pred(X)=\bigcup_{x\in X}pred(x) such that pred(x) is defined by:

\empty &\text{if } sup_{\tiny\mathcal{F}}(x)\uparrow\\
sup_{\tiny\mathcal{F}}(x) &\text{if } sup_{\tiny\mathcal{F}}(x)\downarrow

and let rch_{\tiny\mathcal{F}}(x)\equiv rch_{\tiny\mathcal{F}}({x})

Be noticed that the set rch_{\tiny\mathcal{F}}(X) contains all the elements that are directly or indirectly required to generate elements in X

Definition[Finite State Function]

  A generating function \mathcal{F} is said to be finite state if rch_{\tiny\mathcal{F}} is finite for all x\in\mathcal{U}

Theorem[Termination of Membership Checking Function]

   gfp_{\tiny\mathcal{F}}(X)\downarrow only if rch_{\tiny\mathcal{F}}(X) is finite, i.e., if \mathcal{F} is finite state, then gfp_{\tiny\mathcal{F}} is guaranteed to terminates for any finite X\sube\mathcal{U}
  Notice that on each recursive call gfp_{\tiny\mathcal{F}}(Y) of the original call gfp_{\tiny\mathcal{F}}(X), we have Y\sube rch_{\tiny\mathcal{F}}(X) by definition, since size of Y is strictly incresing and rch_{\tiny\mathcal{F}}(X) is finite, the function must terminates when |Y|=|rch_{\tiny\mathcal{F}}(X)|.∎

Regular Trees and µ-Types

  Now we have defined the generating function \mathcal{S} for the subtyping relation of infinite types, and have already found a function to check the membership, now we need to implement the sup function for \mathcal{S}, to prove the correctness of this algorithm, we need to find all types that the algorithm will terminate.


  A tree type \rho is a subtree of a tree type \tau if \rho=\lambda\sigma. \tau(\pi\sigma), i.e., \rho can be obtained by adding a fixed prefix \pi to \tau. The prefix \pi is the path from the root of \tau to the root of \rho. We use subtrees(\tau) to denote all subtrees of \tau.∎

Since the tree type is a function that takes a path represented by string as argument and returns a node corresponding to the path, adding a fixed prefix to it means we always want to start from a particular node.

Definition[Regular Trees]

  A tree type \tau\in\mathcal{T} is regular if subtrees(\tau) is finite, i.e., \tau has finitely many distinct subtrees. The set of all regular trees is written \mathcal{T}_r.∎

  Note that the if we restrict the domain of \mathcal{S} to \mathcal{T_r}, denoted \mathcal{S_r},then it will be finite state, to prove this, observe that rch_{\tiny\mathcal{S_r}}(\tau, \rho)\sube subtrees(\tau)\times subtrees(\rho)(obvious from the three clause of \mathcal{S}), and since both subtrees(\tau) and subtrees(\rho) are finite, so is rch_{\tiny\mathcal{S_r}}(\tau, \rho).

Definition[Raw μ-Types]

  Let \lbrace X_1, X_2, ...\rbrace be a countable set of type variables, let set \mathcal{T_m^{raw}} be the set of raw \mu-Types defined by the following BNF:

\tau ::= &X\ |\ \top\ |\ \tau\times\tau\ |\ \tau\to\tau\ |\ \mu X.\tau

where \mu X.\tau is recursive type which can be unfolded once by [X\mapsto \mu X.\tau]\tau, however, all the unfoldings of a raw \mu-type are definitionally equal (that's the so-called "equi-recursive", the unfolding of a recursive type is equal to its folding). Intuitively, \mu X.\mathtt{Int}\to X is definitionally equals to the following scala type declaration(this is just some sort of pseudocode, real scala does not permit recursive occurences of X on both sides of =):

type X = Int -> X

We use FV(\tau) to denote the free type variables in a \mu-type \tau

  To establish the theorems based on the raw \mu-type, we first need to prove that raw \mu-type is somehow isomorphic to the tree type (since we define both finite and infinite types and their generating functions \mathcal{S} and \mathcal{S_f} based on the tree type representation, respectively), i.e., we can transform a raw \mu-type to a tree type and vice versa. Intuitively, the tree type can be constructed from the infinite unfolding of a \mu-type; however, this only holds under a specific circumstance, where a raw \mu-type is contractive:


  A raw \mu-type \tau is contractive, if for any subexpression of \tau' of \tau, its \mu-binders are not equal to corresponding bodies, e.g., \mu X.\mu X_1...\mu X_n.S, where S is not equal to any of X. A raw \mu-type is simply called \mu-type if it's contractive, and the set of all contractive raw \mu-types is denoted by \mathcal{T_m}

  To see why the contractivity is required, observe the \mu-type \mu T.T, the \mu-binder T is equals to its body T, unfolding it gives exactly the same type again, thus no tree type can be constructed.

Definition[Subtyping Relation of μ-Types]

  Two \mu-type \tau and \rho is in subtyping relation if (\tau, \rho)\in\nu\mathcal{S_m}, where \mathcal{S_m}:\mathcal{P(T_m\times T_m)\to P(T_m\times T_m)} is defined by:

\mathcal{S_m}(R) = &\ \lbrace (\tau, \top)\ |\ \tau\in\mathcal{T_m}\rbrace\\
\cup&\ \lbrace (\tau_1\times\tau_2, \rho_1\times\rho_2)\ |\ (\tau_1, \rho_1), (\tau_2, \rho_2)\in R\rbrace\\
\cup&\ \lbrace (\tau_1\to\tau_2, \rho_1\to\rho_2)\ |\ (\rho_1, \tau_1), (\tau_2, \rho_2)\in R\rbrace\\
\cup&\ \lbrace (\tau, \mu X.T)\ |\ (\tau, [X\mapsto \mu X.T]T)\in R\rbrace\\
\cup&\ \lbrace (\mu X.T, \tau)\ |\ ([X\mapsto \mu X.T]T, \tau)\in R, \tau\neq\top, \tau\neq\mu Y.T_1 \rbrace

The additional conditions in the last clause is used to make the function invertible, otherwise the generating set G will not be strictly ordered.
  Now we can define the sup_{\tiny\mathcal{S_m}} (which stands as a method to check the membership of gfp) as follow:

sup_{\tiny\mathcal{S_m}}(\tau, \rho)=
\empty &\text{if }\rho=\top\\
\lbrace (\tau_1, \rho_1), (\tau_2, \rho_2)\rbrace &\text{if } \tau=\tau_1\times\tau_2, \rho=\rho_1\times\rho_2\\
\lbrace (\rho_1, \tau_1), (\tau_2, \rho_2)\rbrace &\text{if }\tau=\tau_1\to\tau_2,\rho=\rho_1\to\rho_2\\
\lbrace (\tau, [X\mapsto \mu X.T_1]T_1)\rbrace &\text{if }\rho=\mu X.T_1\\
\lbrace ([X\mapsto \mu X.T_1]T_1, \rho)\rbrace &\text{if }\tau=\mu X.T_1, \rho\neq\mu Y.S_1,\rho\neq\top\\
\uparrow &\text{elsewise}

  It can be proven that \mu-type \tau<:\rho(i.e. (\tau, \rho)\in\nu\mathcal{S_m}) iff the corresponding tree type \tau'<:\rho'(i.e., (\tau', \rho')\in\nu\mathcal{S}), see p.301 to p.304 of the original book.

  Until now, the algorithm to checking the subtyping relation between to \mu-types is obvious: instantiate gfp with sup_{\tiny\mathcal{S_m}} (we do not use sup_{\tiny\mathcal{S}} because we have proved the isomorphism between \mu-types and tree types, so they are considered identical). However, since the function gfp(X) is defined only if the reachable set of X is finite, we have to prove that rch_{\tiny\mathcal{S_m}}(\tau,\rho) is finite for all pairs of \mu-types (\tau,\rho) to finish the correctness proof of the algorithm based on gfp. The proof sketch is that the reachable set of a pair of tree types \tau' and \rho' is basically the subtrees for them, respectively (as we have shown above), which is subexpressions for their corresponding \mu-types \tau and \rho, so basically we need to prove that the subexpressions of a \mu-type is finite. To do this, we develop two difference forms of subexpression, one called Top-down subexpression and the other called Bottom-up subexpression, we first prove that the reachable set of \mu-type pair is the subset of former one, then prove that the latter one is finite, finally, we prove that the former one is a subset of the latter one, then by the set inclusion, the reachable set must also be finite, the detailed proof can be found at p.305 to p.311 of the original book.