Complete Axioms For Categorical Fixed-Point Operators
LICS '00: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science(2000)
摘要
We give an axiomatic treatment of fixed-point operators br categories A nation of iteration operator is defined, embodying the equational properties of iteration theories. We prove a general completeness theorem for iteration operators, relying on a new: purely syntactic characterisation of the free iteration theory.We then show how iteration operators arise in axiomatic domain theory. One result derives them from the existence of sufficiently many bifree algebras (exploiting the universal property Freyd introduced in his notion of algebraic compactness). Another result shows that, in the presence of a parameterized natural numbers object and an equational lifting monad, any uniform fired-point operator is necessarily an iteration operator.
更多查看译文
关键词
iteration operator,free iteration theory,iteration theory,fixed-point operator,uniform fixed-point operator,axiomatic domain theory,axiomatic treatment,equational lifting monad,equational property,algebraic compactness,Categorical Fixed-Point Operators,Complete Axioms
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络