Abstract
A special final coalgebra theorem, in the style of Aczel's [2], 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 [12]. 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 [10].
Thomas Forster alerted me to Quine's work. Peter Aczel and Andrew Pitts offered considerable advice and help. Daniele Turi gave advice by electronic mail. I have used Paul Taylor's macros for commuting diagrams. K. Mukai commented on the text. Research funded by the ESPRIT Basic Research Action 6453 ‘Types.’
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S., The lazy lambda calculus, In Resesarch Topics in Functional Programming, D. A. Turner, Ed. Addison-Wesley, 1977, pp. 65–116
Aczel, P., Non-Well-Founded Sets, CSLI, 1988
Aczel, P., Mendier, N., A final coalgebra theorem, In Category Theory and Computer Science (1989), D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, A. Poigné, Eds., Springer, pp. 356–365, LNCS 389
Barr, M., Terminal coalgebras in well-founded set theory, Theoretical Comput. Sci. 114, 2 (1993), 299–315
Kunen, K., Set Theory: An Introduction to Independence Proofs, North-Holland, 1980
Milner, R., Communication and Concurrency, Prentice-Hall, 1989
Milner, R., Tofte, M., Co-induction in relational semantics, Theoretical Comput. Sci. 87 (1991), 209–220
Paulson, L. C., Set theory for verification: I. From foundations to functions, J. Auto. Reas. 11, 3 (1993), 353–389
Paulson, L. C., Set theory for verification: II. Induction and recursion, Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993, To appear in J. Auto. Reas.
Paulson, L. C., A fixedpoint approach to implementing (co)inductive definitions, In 12th Conf. Auto. Deduct. (1994), A. Bundy, Ed., Springer, pp. 148–161, LNAI 814
Quine, W. V., On ordered pairs and relations, In Selected Logic Papers. Random House, 1966, ch. VIII, pp. 110–113, Orginally published 1945–6
Rutten, J. J. M. M., Turi, D., On the foundations of final semantics: Non-standard sets, metric spaces, partial orders, In Semantics: Foundations and Applications (1993), J. de Bakker, W.-P. de Roever, G. Rozenberg, Eds., Springer, pp. 477–530, LNCS 666
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Paulson, L.C. (1995). A concrete final coalgebra theorem for ZF set theory. In: Dybjer, P., Nordström, B., Smith, J. (eds) Types for Proofs and Programs. TYPES 1994. Lecture Notes in Computer Science, vol 996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60579-7_7
Download citation
DOI: https://doi.org/10.1007/3-540-60579-7_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60579-9
Online ISBN: 978-3-540-47770-9
eBook Packages: Springer Book Archive