Complete axioms for categorical fixed-point operators

被引:71
|
作者
Simpson, A [1 ]
Plotkin, G [1 ]
机构
[1] Univ Edinburgh, LFCS, Div Informat, Edinburgh EH9 3JZ, Midlothian, Scotland
关键词
D O I
10.1109/LICS.2000.855753
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:30 / 41
页数:12
相关论文
共 50 条