一句话：证明了类型 (ι→ι)^n→ι 的顺序泛函构成 dcpo，并完整刻画了哪些类型具有该性质。
顺序泛函是高阶可计算性与域理论/博弈语义中的核心语义模型；其偏序集是否构成 dcpo 关系到模型能否支持递归与最小不动点等构造。本文聚焦类型层 2 上以有限序列一元函数为参数的固定类型 (ι→ι)^n→ι。作者证明这些类型的顺序泛函构成 directed complete partial order，并由此完整给出哪些类型具有该性质的刻画。证明工具是针对这些类型的有限顺序泛函建立的正规形式定理。
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,Comment: 10 pages
@article{paperbot418,
title = {The sequential functionals of type $(\iota \rightarrow \iota)^n \rightarrow \iota$ form a dcpo for all $n \in \Bbb N$},
author = {Dag Normann},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:23)2018}
}