Computing Reviews

Fixed points in Cartesian closed categories
Barr M. (ed) Theoretical Computer Science70(1):65-72,1990.Type:Article
Date Reviewed: 06/01/91

Barr proposes to study domain theory using a semantic model general enough to include situations that cannot be covered by standard ZF set theory. The framework is a Cartesian closed category that has finite limits and a natural number object. Let &ohgr; be a natural number object with a partial order. We define D as an &ohgr;-complete partially ordered object if and only if an arrow V:[ &ohgr; → D ] → D exists such that, for any arrow f : A →[ &ohgr; → D ] with transpose : A × &ohgr; → D, we have f ( a , n ) ≤ V ○ f ( a ) for all ( a , n ) ∈ A × &ohgr;, and if g : AD is any arrow such that ( a , n ) ≤ g ( a ) for all ( a , n ) ∈ A × &ohgr;, then V ○ f ≤ g. In such a case, there is an operator fix:[ DD ] → D satisfying the usual properties of a least fixed point, namely that f (fix ( f ) ) = fix(f) and that if f ( d ) = d, then fix( f )≤ d .

On the whole, the approach is interesting and mathematically elegant. It would be useful, however, if the author elaborated on the advantages of this approach over other models. Inconsistencies in notation are a minor problem: for example, the author uses both &pgr; 1 and p 1 for projections, Inc and p for inclusions, id and A for identity functions, and < f , g > and ( f , g ) for maps from X to Y×Y. The paper also contains several typographical errors, such as confusions between f and , f0 and 0, f ○ n ○ s and f ○ s ○ n ○ g, g and g ○ p 1, and s0 and id×s0.

Reviewer:  T.H. Tse Review #: CR114623

Reproduction in whole or in part without permission is prohibited.   Copyright 2024 ComputingReviews.com™
Terms of Use
| Privacy Policy