Someone's Intermediate Representation

0%

# Intros on System FPC and Recursive Types

FPC is a language with products, sums, partial functions, and recursive types.

Recursive types are solutions to type equations $t\cong\tau$ where there is no restriction on $t$ occurrence in $\tau$. Equivalently, it is a fixed point up to isomorphism of associated unrestricted type operator $t.\tau$. When removing the restriction on type operator, we may see the solution satisfies $t\cong t\rightharpoonup t$, which describes a type is isomorphic to the type of partial function defined on itself.

Types are not sets: they classify computable functions not arbitrary functions. With types we may solve such type equations. The penalty is that we must admit non-termination. For one thing, type equations involving functions have solutions only if the functions involved are partial.

A benefit of working in the setting of partial functions is that type operations have unique solutions (up to isomorphism). But what about the inductive/coinductive type as solution to same type equation? This turns out that based on fixed dynamics, be it lazy or eager:

• Under a lazy dynamics, recursive types have a coinductive flavor, and inductive analogs are inaccessible.
• Under an eager dynamics, recursive types have an inductive flavor, but coinductive analogs are accessible as well.

# Solving Type Equations

The syntax table of recursive type is defined as follows
\begin{aligned} \text{Typ}&&\tau&&::=&&t&&t&&\text{self-reference}\\ &&&&&&\text{rec}(t.\tau)&&\text{rec }t\text{ is }\tau&&\text{recursive type}\\ \text{Exp}&&e&&::=&&\text{fold}\lbrace t.\tau\rbrace(e)&&\text{fold}(e)&&\text{fold}\\ &&&&&&\text{unfold}(e)&&\text{unfold}(e)&&\text{unfold} \end{aligned}

Recursive types have the same general form as inductive/coinductive types.

## Statics

$$\dfrac{\Delta,t\text{ type}\vdash\tau\text{ type}}{\Delta\vdash\text{rec}(t.\tau)\text{ type}}\\ \dfrac{\Gamma\vdash e:\lbrack\text{rec}(t.\tau)/t\rbrack\tau}{\Gamma\vdash\text{fold}\lbrace t.\tau\rbrace(e):\text{rec}(t.\tau)}\\ \dfrac{\Gamma\vdash e:\text{rec}(t.\tau)}{\Gamma\vdash\text{unfold}(e):\lbrack\text{rec}(t.\tau)/t\rbrack\tau}$$

## Dynamics

$$\dfrac{\lbrack e\text{ val}\rbrack}{\text{fold}\lbrace t.\tau\rbrace(e)\text{ val}}\\ \Big\lbrack\dfrac{e\longmapsto e’}{\text{fold}\lbrace t.\tau\rbrace(e)\longmapsto\text{fold}\lbrace t.\tau\rbrace(e’)}\Big\rbrack\\ \dfrac{e\longmapsto e’}{\text{unfold}(e)\longmapsto\text{unfold}(e’)}\\ \dfrac{\text{fold}\lbrace t.\tau\rbrace(e)\text{ val}}{\text{unfold}(\text{fold}\lbrace t.\tau\rbrace(e))\longmapsto e}$$

## Safety Theorem

1. If $e:\tau$ and $e\longmapsto e’$, then $e’:\tau$.
2. If $e:\tau$, then either $e\text{ val}$ or $\exists e’,e\longmapsto e’$.

# Inductive and Coinductive Types

Recursive types may be used to represent inductive types such as natural numbers and natural number list.

## Example First on Natural Number

Use an eager dynamics for FPC, the recursive type $\rho=\text{rec }t\text{ is }\lbrack z\hookrightarrow\text{unit},s\hookrightarrow t\rbrack$ satisfies the type equation $\rho\cong\lbrack z\hookrightarrow\text{unit},s\hookrightarrow\rho\rbrack$, and is isomorphic to the type of eager natural numbers.

Introduction and elimination forms defined on $\rho$ is defined with following equations
\begin{aligned} z&\triangleq\text{fold}(z\cdot\langle\rangle)\\ s(e)&\triangleq\text{fold}(s\cdot e)\\ \text{ifz }e\lbrace z\hookrightarrow e_0\shortmid s(x)\hookrightarrow e_1\rbrace&\triangleq\text{case unfold}(e)\space\lbrace z\cdot\underline{}\hookrightarrow e_0\shortmid s\cdot x\hookrightarrow e_1\rbrace \end{aligned}
On the other hand, with an lazy dynamics of natural numbers in PCF, the same recursive type $\rho’=\text{rec }t\text{ is }\lbrack z\hookrightarrow\text{unit},s\hookrightarrow t\rbrack$ satisfying $\rho\cong\lbrack z\hookrightarrow\text{unit},s\hookrightarrow\rho\rbrack$ is not the type of natural numbers.

Consider what chapter 15 mentioned, $\rho’$ contains infinity number $\omega$ which is not natural number.

## Another Example on Natlist

Using an eager dynamics for FPC, the natlist is defined by recursive type $\text{rec }t\text{ is }\lbrack z\hookrightarrow\text{unit},c\hookrightarrow\text{nat}\times t\rbrack$, satisfying the type equation $\text{natlist}\cong\lbrack n\hookrightarrow\text{unit},c\hookrightarrow\text{nat}\times\text{natlist}\rbrack$.

Introduction and elimination forms are given by equations
\begin{aligned} \text{nil}&\triangleq\text{fold}(n\cdot\langle\rangle)\\ \text{cons}(e_1;e_2)&\triangleq\text{fold}(c\cdot\langle e_1,e_2\rangle)\\ \text{case }e\lbrace\text{nil}\hookrightarrow e_0\shortmid\text{cons}(x;y)\hookrightarrow e_1\rbrace&\triangleq\text{case unfold}(e)\space\lbrace n\cdot\underline{}\hookrightarrow e_0\shortmid c\cdot\langle x,y\rangle\hookrightarrow e_1\rbrace \end{aligned}
Consider the same recursive type under a context of lazy dynamics for FPC. Then we can see a value of such recursive type has the form $\text{fold}(e)$, where $e$ is an unevaluated computation of the sum type.

## Redefine (Co)Inductive Type

Consider the recursive type $\tau\triangleq\text{rec }t\text{ is }\tau’$ and the associated inductive type and coinductive type $\mu(t.\tau’)$ and $\nu(t.\tau’)$. We redefine these types consistently with statics of inductive and coinductive types here
\begin{aligned} \text{fold}\lbrace t.\tau’\rbrace(e)&\triangleq\text{fold}(e)\\ \text{rec}\lbrace t.\tau’\rbrace(x.e’;e)&\triangleq(\text{fix }r\text{ is }\lambda(u: \tau)\space e_{rec})(e),\text{ where}\\ e_{rec}&\triangleq\lbrack\text{map}\lbrace t.\tau’\rbrace(x.r(x))(\text{unfold}(u))/x\rbrack e’\\ \text{unfold}\lbrace t.\tau’\rbrace(e)&\triangleq\text{unfold}(e)\\ \text{gen}\lbrace t.\tau’\rbrace(x.e’;e)&\triangleq(\text{fix }g\text{ is }\lambda(u:\rho)\space e_{gen})(e),\text{ where}\\ e_{gen}&\triangleq\text{fold}(\text{map}\lbrace t.\tau’\rbrace(x.g(x))(\lbrack u/x\rbrack e’)) \end{aligned}

Dynamics is ill-behaved. Under eager interpretation, the generator may not converge, depending on choice of $e’$; under lazy interpretation, the recursor may not converge, depending on choice of $e’$.

The outcome shows that in the eager case the recursive type is inductive, not coinductive; whereas in the lazy case the recursive type is coinductive, not inductive.

## Coinductive Signal Transducer

We can define type Sig for signal to be the coinductive type of infinite streams of booleans, then we can also define the type of a signal transducer as $\text{Sig}\rightharpoonup\text{Sig}$.

Sig as a coinductive type can have form $\nu(t.e’)$ follows previous redefined coinductive type. In each of its unfold and generate, it gets a new boolean value out. Thus it can have definition $\nu(t.\text{bool}\times t)$.

The definition applies in lazy dynamics, whereas under an eager definition one may use $\nu(t.\text{unit}\rightharpoonup\text{bool}\times t)$. Maybe we just need to feed it with something we do not care in case it won’t stop.

The NOR here can have the type of $\text{Sig}\times\text{Sig}\rightharpoonup\text{Sig}$, with definition as
$$\lambda(a,b)\text{gen}\lbrace t.\text{bool}\times t\rbrace(\langle a,b\rangle.\langle e_{nor}\langle\text{hd}(a),\text{hd}(b)\rangle,\langle\text{tl}(a),\text{tl}(b)\rangle\rangle;a,b)$$

# Self-Reference

In general recursive expression $\text{fix}\lbrace\tau\rbrace(x.e)$, the variable $x$ stands for the expression itself. Self-reference is effected by the unrolling transition and it substitutes itself for $x$ in its body during execution.
$$\text{fix}\lbrace\tau\rbrace(x.e)\longmapsto\lbrack\text{fix}\lbrace\tau\rbrace(x.e)/x\rbrack e$$

It is useful to think $x$ as an implicit argument to $e$ that it is instantiated to itself when expression is used.

Type of self-referential expressions given by the syntax table
\begin{aligned} \text{Typ}&&\tau&&::=&&\text{self}(\tau)&&\tau\text{ self}&&\text{self-referential type}\\ \text{Exp}&&e&&::=&&\text{self}\lbrace\tau\rbrace(x.e)&&\text{self }x\text{ is }e&&\text{self-referential expression}\\ &&&&&&\text{unroll}(e)&&\text{unroll}(e)&&\text{unroll self-reference} \end{aligned}

## Statics and Dynamics

The statics of these constructs is defined as
$$\dfrac{\Gamma,x:\text{self}(\tau)\vdash e:\tau}{\Gamma\vdash\text{self}\lbrace\tau\rbrace(x.e):\text{self}(\tau)}\\ \dfrac{\Gamma\vdash e:\text{self}(\tau)}{\Gamma\vdash\text{unroll}(e):\tau}$$
The dynamics is given by
$$\dfrac{}{\text{self}\lbrace\tau\rbrace(x.e)\text{ val}}\\ \dfrac{e\longmapsto e’}{\text{unroll}(e)\longmapsto\text{unroll}(e’)}\\ \dfrac{}{\text{unroll}(\text{self}\lbrace\tau\rbrace(x.e))\longmapsto\lbrack\text{self}\lbrace\tau\rbrace(x.e)/x\rbrack e}$$

The main difference, compared to general recursion, is that we distinguish a type of self-referential expressions, instead of having self-reference at every type. It’s all a matter of taste.

## Recursive Type Defined Self-Reference

We can define the $\text{self}(\tau)$ with recursive type since a self-referential expression of type $\tau$ depends on the expression itself. It satisfies the isomorphism $\text{self}(\tau)\cong\text{self}(\tau)\rightharpoonup \tau$.

The type equation can be solved by type operator $t.t\rightharpoonup\tau$, where $t\notin\tau$ is a type variable. Required fixed point is just the recursive type $\text{self}(\tau)\triangleq\text{rec}(t.t\rightharpoonup\tau)$. Redefinition on type is shown as follows
\begin{aligned} \text{self}(\tau)&\triangleq\text{rec}(t.t\rightharpoonup\tau)\\ \lambda(x)\space e&:\space\space\text{self}(\tau)\rightharpoonup\tau\equiv\lbrack\text{rec}(t.t\rightharpoonup\tau)/t\rbrack(t\rightharpoonup\tau)\\ \text{self}\lbrace\tau\rbrace(x.e)&:\space\space\text{rec}(t.t\rightharpoonup\tau)\equiv\text{self}(\tau)\\ \text{self}\lbrace\tau\rbrace(x.e)&\triangleq\text{fold}(\lambda(x:\text{self}(\tau))\space e)\\ \text{unroll}(e:\text{self}(\tau))&:\space\space\tau\\ \text{unroll}(e:\text{rec}(t.t\rightharpoonup\tau))&\triangleq(\text{unfold}(e:\text{rec}(t.t\rightharpoonup\tau)):\lbrack\text{rec}(t.t\rightharpoonup\tau)/t\rbrack(t\rightharpoonup\tau))(e)\\ &\equiv\text{unfold}(e)(e) \end{aligned}
It is easy to check that final line of redefinition is correct by $\text{unroll}(\text{self}\lbrace\tau\rbrace(y.e))\longmapsto^\ast\lbrack\text{self}\lbrace\tau\rbrace(y.e)/y\rbrack e$.

## Self-Reference Defined Fixed Point

We may define $\text{fix}\lbrace\tau\rbrace(x.e)$ to stand for the expression $\text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))$.

\begin{aligned} \text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))&\equiv\lbrack\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e)/y\rbrack(\lbrack\text{unroll}(y)/x\rbrack e)\\ &\equiv\lbrack\text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))/x\rbrack e \end{aligned}

Also in $\text{fix}\lbrace\tau\rbrace(x.e)$ form, we can see that
\begin{aligned} \text{fix}\lbrace\tau\rbrace(x.e)&=\text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))\\ &\longmapsto^\ast\lbrack\text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))/x\rbrack e\\ &=\lbrack\text{fix}\lbrace\tau\rbrace(x.e)/x\rbrack e \end{aligned}

In this way we define factorial as $\text{fact}\triangleq\text{self }f:\text{nat}\to\text{nat}\text{ is }\lambda(n:\text{nat})\text{ ifz }n\space\lbrace z\hookrightarrow s(z)\shortmid s(n’)\hookrightarrow n\times \text{unroll}(f)(n’)\rbrace$.

# The Origin of State

The concept of state in computation has its origins in the concept of recursion, or self-reference.

RS latch as an example maintains its output at logic level of zero or one in response to a signal on the R or S inputs. We can implement an RS latch using recursive types.

The idea is to use self-reference to model the passage of time, with the current output being computed from its input and its previous output. It is a value of type $\tau_{rsl}$ given by
$$\text{res }t\text{ is }\langle\text{X}\hookrightarrow\text{bool},\text{Q}\hookrightarrow\text{bool},\text{N}\hookrightarrow t\rangle$$

The X and Q components of the latch represents its current outputs. (Q represents the current of latch), and N represents the next state of the latch.

If $e:\tau_{rsl}$, then we define e @ X to mean $\text{unfold}(e)\cdot \text{X}$, and e @ Q and e @ N are defined similarly.

• e @ X and e @ Q evaluate to boolean output of latch $e$
• e @ N evaluates to another latch representing its evolution over time based on its inputs

For given value $r$ and $s$, a new latch is computed from an old latch by the recursive function $rsl$ with definition
$$\text{fix }rsl\text{ is }\lambda(l:\tau_{rsl})\space e_{rsl}$$
where $e_{rsl}$ is the expression
$$\text{fix }this\text{ is fold}(\langle\text{X}\hookrightarrow e_{NOR}(\langle s, l@\text{Q}),\text{Q}\hookrightarrow e_{NOR}(\langle r,l@\text{X}\rangle)),\text{N}\hookrightarrow rsl(this) \rangle)$$

## Coinductive RS Latch

According to the previous settings of lazy dynamics with PCF, we can try to interpret RS latch expression with coinductive type, which still follows the previous $\tau_{rsl}$ type.

Consider an initial state type $\rho\triangleq\langle\text{X}\hookrightarrow\text{bool},\text{Q}\hookrightarrow\text{bool}\rangle$ and we initialize them with $\langle\text{false},\text{false}\rangle$. Then we can get the RS latch expression
\begin{aligned} e_{rsl}&\triangleq\text{gen}\lbrace t.\tau_{rsl}’\rbrace(\langle\text{X}\hookrightarrow x,\text{Q}\hookrightarrow q\rangle.e_{rsl}’;\langle\text{X}\hookrightarrow\text{false},\text{Q}\hookrightarrow\text{false}\rangle),\text{ where}\\ e_{rsl}’&\triangleq\langle\text{X}\hookrightarrow x,\text{Q}\hookrightarrow q,\text{N}\hookrightarrow\langle e_{nor}\langle s,q\rangle,e_{nor}\langle x,r\rangle\rangle\rangle \end{aligned}
Then we can simplify previously stated self-reference expression of RS latch like
$$\text{fix }g\text{ is }\lambda(\langle\text{X}\hookrightarrow x,\text{Q}\hookrightarrow q)\text{ fold}(e_{rsl}’’), \text{ where}\\ e_{rsl}’’\triangleq\langle\text{X}\hookrightarrow x,\text{Q}\hookrightarrow q,\text{N}\hookrightarrow g(e_{nor}\langle s,q\rangle,e_{nor}\langle x,r\rangle)$$

# SKI Combinator as Recursive Type

Consider the type $\text{D}\triangleq\text{rec }t\text{ is }t\rightharpoonup t$, then we can try to define element $\text{k}:\text{D}$ and $\text{s}:\text{D}$ and application that satisfying:

• $x:\text{D},y:\text{D}\vdash x\cdot y:\text{D}$
• $\text{k}\cdot x\cdot y\longmapsto^\ast x$
• $\text{s}\cdot x\cdot y\cdot z\longmapsto^\ast (x\cdot z)\cdot(y\cdot z)$

We can easily find definition of $\text{k}\triangleq\text{fold}(\lambda(x:\text{D})\space\text{fold}(\lambda(y:\text{D})\space x))$ follows the application convention $x\cdot y\triangleq(\text{unfold}(x))(y)$.

Then $s\triangleq\text{fold}(\lambda(x:\text{D})\space\text{fold}(\lambda(y:\text{D})\space\text{fold}(\lambda(z:\text{D})\space(x\cdot z)\cdot(y\cdot z))))$.