A Concrete Final Coalgebra Theorem for ZF Set Theory

Details A Concrete Final Coalgebra Theorem for ZF Set Theory A Concrete Final Coalgebra Theorem for ZF Set Theory

2001-03-29

arxiv.org/abs/cs/9511103v1

published in P. Dybjer, B. Nordstrm and J. Smith (editors), Types for Proofs and Programs '94 (Springer LNCS 996, published 19

Computer Science

Logic in Computer Science

a greatly revised version has appeared in Mathematical Structures in Computer Science 9 (1999), 545-567. This version uses dif

Scientific paper

A special final coalgebra theorem, in the style of Aczel's, is proved within standard Zermelo-Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel's Solution and Substitution Lemmas are proved in the style of Rutten and Turi. The approach is less general than Aczel's, but the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint. The theory is intended for machine implementation and a simple case of it is already implemented using the theorem prover Isabelle.

Affiliated with

Also associated with

No associations

Rating

A Concrete Final Coalgebra Theorem for ZF Set Theory does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A Concrete Final Coalgebra Theorem for ZF Set Theory, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Concrete Final Coalgebra Theorem for ZF Set Theory will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-418196