The sequential functionals of type $(\iota \to \iota {)}^n\to \iota$ form a dcpo for all $n\in \mathbb{N}$

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,

10 pages