Recursive types, PCF, domains, and finite observations

Eager iso-recursive calculus.

The eager fragment inherits $\mathbf{1}$, products, sums, arrows, and the call-by-value rules of the simple calculus, and locally adds $\mathbb{N}$, numerals, type variables bound by $\mu$, and explicit fold/unfold: The complete local formation and typing delta is

$\mathrm{\Delta }⊢\mathbb{N}\mathsf{type}$

$\mathrm{\Gamma }⊢n:\mathbb{N}$

$\mathrm{\Delta },X⊢A\mathsf{type}$

$\mathrm{\Delta }⊢\mu X.A\mathsf{type}$

$\mathrm{\Gamma }⊢e:A[\mu X.A/X]$

$\mathrm{\Gamma }⊢{\mathsf{fold}}_{\mu X.A}e:\mu X.A$

$\mathrm{\Gamma }⊢e:\mu X.A$

$\mathrm{\Gamma }⊢\mathsf{unfold}e:A[\mu X.A/X]$

Values and evaluation contexts gain $$\begin{array}{c}v::=\cdots \mid n\mid {\mathsf{fold}}_{\mu X.A}v,\\ E::=\cdots \mid {\mathsf{fold}}_{\mu X.A}E\mid \mathsf{unfold}E,\end{array}$$ and their sole new root is

$\mathsf{unfold}({\mathsf{fold}}_{\mu X.A}v)⟼v$

The list instance and its canonical folded-cell abbreviation are $$\begin{array}{c}\mathsf{ListNat}=\mu X.(\mathbf{1}+\mathbb{N}\times X),\\ \mathsf{cell}(n,e)={\mathsf{fold}}_{\mathsf{ListNat}}(\mathsf{inr}⟨n,e⟩).\end{array}$$ Thus $\mathsf{cell}(n,v)$ is a value when $v$ is a value, whereas the curried term $\mathsf{cons}nv$ takes two beta steps to that syntax.

Contractive regular equality.

A binder $\mu X.A$ is admitted to the equality algorithm only when every free occurrence of its bound $X$ in $A$ lies strictly below a product, sum, or arrow constructor. Closed admitted types are finite directed graphs. Writing $\mathsf{head}(a)$ for the first constructor reached by following recursive back-edges, the worklist transitions are as follows. A visited pair is discarded: $$((a,b)::W^{\prime },V)⟼(W^{\prime },V)((a,b)\in V).$$ An unvisited pair rejects when its exposed heads differ in constructor or arity. Otherwise it takes the transition $$((a,b)::W^{\prime },V)⟼(\mathsf{children}(a,b)++W^{\prime },V\cup \{(a,b)\}).$$ The initial state is $([(a,b)],\varnothing )$; an empty worklist accepts. The judgment $A{\equiv }_{\mu }B$ means bisimilarity of the two unfolded ordered constructor trees, not a term reduction or a subtyping judgment.

Call-by-name PCF.

The separate language ${\mathsf{PCF}}_{\mathsf{n}}$ has Besides the inherited variable, numeral, lambda, and application rules, its typing rules are

$\mathrm{\Gamma }⊢e:\mathbb{N}$

$\mathrm{\Gamma }⊢\mathsf{succ}e:\mathbb{N}$

$\mathrm{\Gamma }⊢e:\mathbb{N}$$\mathrm{\Gamma }⊢e_0:A$$\mathrm{\Gamma },x:\mathbb{N}⊢e_s:A$

$\mathrm{\Gamma }⊢\mathsf{ifz}e\mathsf{then}{e}_0\mathsf{else}x.e_s:A$

$\mathrm{\Gamma },x:A⊢e:A$

$\mathrm{\Gamma }⊢\mathsf{fix}x:A.e:A$

Values, the complete context grammar, and roots are $$v::=n\mid \lambda x:A.e,E::=[]\mid \mathsf{succ}E\mid \mathsf{ifz}E\mathsf{then}{e}_0\mathsf{else}x.e_s\mid Ee,$$

$(\lambda x:A.e)d⟼e[d/x]$

$\mathsf{succ}n⟼n+1$

$\mathsf{ifz}0\mathsf{then}{e}_0\mathsf{else}x.e_s⟼e_0$

$\mathsf{ifz}(n+1)\mathsf{then}{e}_0\mathsf{else}x.e_s⟼e_s[n/x]$

$\mathsf{fix}x:A.e⟼e[\mathsf{fix}x:A.e/x]$

There is no argument context. Write $e\Downarrow n$ for $e{⟼}^{\ast }n$, and $e\Uparrow$ for an infinite reduction.

Omega-cpos and constructors.

For an omega-chain $(d_i)$, its least upper bound is $\underset{i}{⨆}{d}_i$. A pointed omega-cpo has a least element $\mathrm{\perp }$. A map is continuous when it is monotone and preserves these lubs. An element $c$ is compact exactly when $$c{⊑}_{\mathsf{D}}\underset{i}{⨆}{d}_i⟹\mathrm{\exists }j.c{⊑}_{\mathsf{D}}{d}_j.$$ The orders used in the list equation are with distinct sum tags incomparable, and $$\mathrm{\perp }{⊑}_{\mathsf{D}}z,\uparrow d{⊑}_{\mathsf{D}}\uparrow d^{\prime }⟺d{⊑}_{\mathsf{D}}{d}^{\prime }$$ for the lifting $D_{\mathrm{\perp }}$. Chain lubs are componentwise for products, remain in one tag for separated sums, and are bottom or the lifting of the eventual payload lub for liftings. Continuous function spaces $[D\to E{]}_c$ have the pointwise order and pointwise omega-chain lubs.

For continuous $F:D\to D$ on a pointed omega-cpo, $$\mathrm{lfp}(F)=\underset{n\ge 0}{⨆}{F}^n(\mathrm{\perp }),F(\mathrm{lfp}F)=\mathrm{lfp}F.$$ If $F(d){⊑}_{\mathsf{D}}d$, then $\mathrm{lfp}(F){⊑}_{\mathsf{D}}d$. If $\mathrm{\Phi }:P\times D\to D$ is continuous, then $$F_p(d)=\mathrm{\Phi }(p,d),\mu \mathrm{\Phi }(p)=\mathrm{lfp}(F_p)$$ defines a continuous map $\mu \mathrm{\Phi }:P\to D$. An admissible predicate contains bottom and is closed under omega-chain lubs; if it is preserved by $F$, it contains $\mathrm{lfp}(F)$.

The partial-list solution.

The cpo $\mathcal{L}$ consists of finite words ending in a hole, finite words ending in $\mathsf{nil}$, and infinite words. Its order is generated by $$\mathrm{\perp }{⊑}_{\mathsf{D}}d,\mathsf{cons}(n,d){⊑}_{\mathsf{D}}\mathsf{cons}(n,d^{\prime })⟺d{⊑}_{\mathsf{D}}{d}^{\prime }.$$ The truncations are Finite elements are exactly the compact ones. The continuous inverse maps solving the selected equation are $$\mathcal{L}\underset{\mathsf{in}}{\stackrel{\mathsf{out}}{\rightleftarrows }}(\{\ast \}+\mathbb{N}\times \mathcal{L}{)}_{\mathrm{\perp }}$$ with

PCF denotation and adequacy relation.

Types are interpreted by $$[[\mathbb{N}]]={\mathbb{N}}_{\mathrm{\perp }},[[A\to B]]=[[[A]]\to [[B]]{]}_c.$$ The strict natural operations are Variables, numerals, lambda, and application use projection, the numeral injection, continuous currying, and evaluation. The remaining clauses are Logical approximation is For closed $e:\mathbb{N}$, adequacy is $$e\Downarrow n⟺[[e]]=n,e\Uparrow ⟺[[e]]=\mathrm{\perp }.$$

Indexed eager observation.

For the exact fragment in convention 24.40, index zero relates all closed values of the same type. Positive indices compare unit and natural values, products, and equal sum tags structurally; arrows and recursive types use The symmetric term observation is The endpoints quantified here are values. Related substitutions satisfy $\gamma {\approx }_n^{\mathrm{\Gamma }}\delta$ componentwise. The relation is downward closed, admits two-sided finite anti-reduction, is compatible with related substitution, and is preserved by every well-typed closing evaluation context of the fragment.

Tail observation and proof recursion.

Finite tail observation in $\mathcal{L}$ is generated by

$d\stackrel{0}{⇝}d$

$\mathsf{out}(d)=\uparrow \mathsf{inr}(n,d_1)$$d_1\stackrel{k}{⇝}{d}^{\prime }$

$d\stackrel{k+1}{⇝}{d}^{\prime }$

The optional unrestricted propositions-as-types extension is exactly

$\mathrm{\Gamma },p:P⊢e:P$

$\mathrm{\Gamma }⊢\mathsf{fix}p:P.e:P$

$\mathsf{fix}p:P.e⟼e[\mathsf{fix}p:P.e/p]$

It is not part of a total proof core: at every $P$, including the empty type $0$, the term $\mathsf{fix}p:P.p$ is a closed self-loop of type $P$.