×

A co-induction principle for recursively defined domains. (English) Zbl 0795.68129

Summary: This paper establishes a new property of predomains recursively defined using the cartesian product, disjoint union, partial function space and convex powerdomain constructors. We prove that the partial order on such a recursive predomain \(D\) is the greatest fixed point of a certain monotone operator associated to \(D\). This provides a structurally defined family of proof principles for these recursive predomains: to show that one element of \(D\) approximates another, it suffices to find a binary relation containing the two elements that is a post-fixed point for the associated monotone operator. The statement of the proof principles is independent of any of the various methods available for explicit construction of recursive predomains. Following R. Milner and M. Tofte [ibid. 87, No. 1, 209-220 (1991; Zbl 0755.68100)], the method of proof is called co-induction. It closely resembles the way bisimulations are used in concurrent process calculi [R. Milner, Communication and concurrency, Prentice Hall, New York (1989; Zbl 0683.68008)].
Two specific instances of the co-induction principle already occur in the work of S. Abramsky [Inf. Comput. 92, No. 2, 161-218 (1991; Zbl 0718.68057)] in the form of “internal full abstraction” theorems for denotational semantics of SCCS and lazy lambda calculus. In the first case post-fixed binary relations are precisely Abramsky’s partial bisimulations, whereas in the second case they are his applicative bisimulations. The co-induction principle also provides an apparently useful tool for reasoning about equality of elements of recursively defined datatypes in (strict or lazy) higher-order functional programming languages.

MSC:

68Q55 Semantics in the theory of computing
06B35 Continuous lattices and posets, applications

Software:

ML; Haskell
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S., The lazy lambda calculus, (Turner, D., Research Topics in Functional Programming (1990), Addison-Wesley: Addison-Wesley Reading, MA), 65-116
[2] Abramsky, S., A domain equation for bisimulation, Inform. and Comput., 92, 161-218 (1991) · Zbl 0718.68057
[3] S. Abramsky and C.-H.L. Ong, Full abstraction in the lazy lambda calculus, Inform. and Comput.; S. Abramsky and C.-H.L. Ong, Full abstraction in the lazy lambda calculus, Inform. and Comput. · Zbl 0779.03003
[4] Bird, R.; Wadler, P., Introduction to Functional Programming (1988), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ
[5] Freyd, P. J., Algebraically complete categories, (Carboni, A.; etal., Proc. 1990 Como Category Theory Conf.. Proc. 1990 Como Category Theory Conf., Lecture Notes in Mathematics, Vol. 1488 (1991), Springer: Springer Berlin), 95-104 · Zbl 0815.18005
[6] D. Howe, Equality in lazy computation systems, pp.198-203 in [8]; D. Howe, Equality in lazy computation systems, pp.198-203 in [8]
[7] (Hudak, P.; Peyton Jones, S.; Wadler, P., Report on the Programming Language Haskell: Version 1.1. Report on the Programming Language Haskell: Version 1.1, Tech. Report (1991), Yale University and Glasgow University)
[8] (Proc. 4th IEEE Ann. Symp. on Logic in Computer Science. Proc. 4th IEEE Ann. Symp. on Logic in Computer Science, Asilomar, CA (1989))
[9] Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[10] Milner, R.; Tofte, M., Co-induction in relational semantics, Theoret. Comput. Sci., 87, 209-220 (1991) · Zbl 0755.68100
[11] Milner, R.; Tofte, M.; Harper, R., The Definition of Standard ML (1990), MIT Press: MIT Press Cambridge, MA
[12] E. Moggi Computational lambda-calculus and monads, 14-23 in [8]; E. Moggi Computational lambda-calculus and monads, 14-23 in [8]
[13] Moggi, E., An Abstract View of Programming Languages (1989), Stanford University, Lecture Notes
[14] Park, D., Fixpoint induction and proofs of program properties, Mach. Intell., 5, 59-78 (1970) · Zbl 0219.68007
[15] Paulson, L. C., ML for the Working Programmer (1991), Cambridge Univ. Press: Cambridge Univ. Press Cambridge · Zbl 0863.68032
[16] Pitts, A. M., Relational properties of recursively defined datatypes, (Proc. 8th IEEE Ann. Symp. on Logic in Computer Science. Proc. 8th IEEE Ann. Symp. on Logic in Computer Science, Montréal (1993)), 86-97
[17] Plotkin, G. D., A powerdomain construction, SIAM J. Comput., 5, 452-487 (1976) · Zbl 0355.68015
[18] Plotkin, G. D., (Lecture Notes for Postgraduate Course on Domain Theory (1981/1982), Dept. of Computer Science, University of Edinburgh)
[19] Plotkin, G. D., (Lectures on Predomains and Partial Functions, Notes for a course at CSLI (1985), Stanford University)
[20] Smyth, M. B.; Plotkin, G. D., The category-theoretic solution of recursive domain equations, SIAM J. Comput., 11, 761-783 (1982) · Zbl 0493.68022
[21] Winskel, G.; Larsen, K. G., Using information systems to solve recursive domain equations effectively, (Kahn, G.; etal., Semantics of Data Types. Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173 (1984), Springer: Springer Berlin), 109-130 · Zbl 0539.68019
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.