On behavioural pseudometrics and closure ordinals

A behavioural pseudometric is often defined as the least fixed point of a monotone function F on a complete lattice of 1-bounded pseudometrics. According to Tarskiʼs fixed point theorem, this least fixed point can be obtained by (possibly transfinite) iteration of F, starting from the least element ⊥ of the lattice. The smallest ordinal α   such that Fα(⊥)=Fα+1(⊥)Fα(⊥)=Fα+1(⊥) is known as the closure ordinal of F. We prove that if F is also continuous with respect to the sup-norm, then its closure ordinal is ω. We also show that our result gives rise to simpler and modular proofs that the closure ordinal is ω.

► We show that the closure ordinal of a monotone and continuous function on a complete lattice of 1-bounded pseudometric spaces is omega. ► We show that this result gives rise to simpler proofs. ► We show that this result gives rise to modular proofs.