The sequential functionals of type $(\iota \rightarrow \iota)^n \rightarrow \iota$ form a dcpo for all $n \in \Bbb N$

TL;DR

This paper characterizes when the set of sequential functionals at certain type levels forms a dcpo, providing a normal form theorem for finite sequential functionals to understand their order-theoretic properties.

Contribution

It offers a complete characterization of types for which the set of sequential functionals forms a dcpo, along with a normal form theorem for finite sequential functionals.

Findings

Sequential functionals of certain types form a dcpo.

A normal form theorem for finite sequential functionals is established.

The characterization applies to types at level 2 with finite sequences of unary functions.

Abstract

We prove that the sequential functionals of some fixed types at type level 2, taking finite sequences of unary functions as arguments, do form a directed complete partial ordering. This gives a full characterisation of for which types the partially ordered set of sequential functionals has this property. As a tool, we prove a normal form theorem for the finite sequential functionals of the types in question,