Unary PCF is a laughably small fragment of PCF, consisting of
It is useless as programming language, but it has interesting semantic properties.
Unary PCF is a simply-typed -calculus with a single base type , functions, two constants, and a binary operator.
The types are given by
The typing rules are given by the usual rules for variables, -abstraction and application, along with
along with reduction rules
We can think of as an observable value. as the usual nontermination, which taints anything it touches. The binary operator 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.
The key mathematical property of PCF is that its observational preorder is decidable.
We define the observational preorder by induction on the type as follows:
Then we have
Theorem (Loader 1998). is decidable.
Loader, Ralph. 1998. ‘Unary PCF Is Decidable’. Theoretical Computer Science 206 (1–2): 317–29. https://doi.org/10.1016/S0304-3975(98)00048-6.
@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}
}