Unary PCF

Unary PCF is a laughably small fragment of PCF, consisting of

• a single base type,
• a single value on base type, and
• a constant representing nontermination.

It is useless as programming language, but it has interesting semantic properties.

Definition

Unary PCF is a simply-typed \lambda-calculus with a single base type \omicron, functions, two constants, and a binary operator.

The types are given by

A, B \Coloneqq \omicron \mid A \to B

The typing rules are given by the usual rules for variables, \lambda-abstraction and application, along with

\frac{}{\Gamma \vdash \top : \omicron}
\quad
\frac{}{\Gamma \vdash \bot : \omicron}
\quad
\frac{
  \Gamma \vdash M : \omicron
  \quad
  \Gamma \vdash N : \omicron
}{
  \Gamma \vdash M \land N : \omicron
}

along with reduction rules

\top \land x \longrightarrow x
\qquad
\bot \land x \longrightarrow \bot

We can think of \top as an observable value. \bot as the usual nontermination, which taints anything it touches. The binary operator \land can be thought of as a "convergence test", which forces evaluation of its first argument, and gets stuck if that doesn't terminate.

The induced compatible notion of reduction is confluent and strongly normalizing.

Decidability

The key mathematical property of PCF is that its observational preorder is decidable.

We define the observational preorder \lesssim_A by induction on the type A as follows:

\begin{array}{lll}
  &M \lesssim_\omicron N
    &\quad\triangleq\quad
      &M \longrightarrow^\ast \top\;
        \Longrightarrow\;
       N \longrightarrow^\ast \top \\
  &M_1 \lesssim_{A \to B} M_2
    &\quad\triangleq\quad
      &\forall (N_1 \lesssim_A N_2).\;
        M_1(N_1) \lesssim_B M_2(N_2)
\end{array}

Then we have

Theorem (Loader 1998). \lesssim_A is decidable.

References

• Unary PCF and its decidability were both introduced in the article

@article{loader_1998,
	title = {Unary {PCF} is decidable},
	volume = {206},
	doi = {10.1016/S0304-3975(98)00048-6},
	number = {1-2},
	journal = {Theoretical Computer Science},
	author = {Loader, Ralph},
	year = {1998},
	pages = {317--329}
}