Please refer this link from page 177 to 184.

# 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

- If $e:\tau$ and $e\longmapsto e’$, then $e’:\tau$.
- 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 argumentto $e$ that it isinstantiatedto 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))))$.