×

A fixedpoint approach to implementing (co)inductive definitions. (English) Zbl 1433.68560

Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 148-161 (1994).
Summary: This paper presents a fixedpoint approach to inductive definitions. Instead of using a syntactic test such as ‘strictly positive’, the approach lets definitions involve any operators that have been proved monotone. It is conceptually simple, which has allowed the easy implementation of mutual recursion and other conveniences. It also handles coinductive definitions: simply replace the least fixedpoint by a greatest fixedpoint. This represents the first automated support for coinductive definitions.
The method has been implemented in Isabelle’s formalization of ZF set theory. It should be applicable to any logic in which the Knaster-Tarski Theorem can be proved. Examples include lists of \(n\) elements, the accessible part of a relation and the set of primitive recursive functions. One example of a coinductive definition is bisimulations for lazy lists.
For the entire collection see [Zbl 0875.00063].

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S., The lazy lambda calculus. In Resesarch Topics in Functional Programming, D. A. Turner, Ed. Addison-Wesley, 1977, pp. 65-116
[2] Aczel, P., An introduction to inductive definitions, In Handbook of Mathematical Logic, J. Barwise, Ed. North-Holland, 1977, pp. 739-782
[3] Aczel, P., Non-Well-Founded Sets, CSLI, 1988 · Zbl 0668.04001
[4] Boyer, R. S., Moore, J. S., A Computational Logic, Academic Press, 1979 · Zbl 0448.68020
[5] Camilleri, J., Melham, T. F., Reasoning with inductively defined relations in the HOL theorem prover. Tech. Rep. 265, Comp. Lab., Univ. Cambridge, August 1992
[6] Davey, B. A., Priestley, H. A., Introduction to Lattices and Order, Cambridge Univ. Press, 1990 · Zbl 0701.06001
[7] Dybjer, P., Inductive sets and families in Martin-Lofs type theory and their set-theoretic semantics. In Logical Frameworks. G. Huet, G. Plotkin, Eds. Cambridge Univ. Press. 1991, pp. 280-306 · Zbl 0755.03033
[8] Farmer, W. M., Guttman, J. D., Thayer, F. J., IMPS: An interactive mathematical proof system, J. Auto. Reas.11, 2 (1993), 213-248 · Zbl 0802.68129
[9] Hennessy, M., The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics, Wiley, 1990 · Zbl 0723.68067
[10] Huet, G., Induction principles formalized in the Calculus of Constructions, In Programming of Future Generation Computers (1988), Elsevier, pp. 205-216 · Zbl 0657.68013
[11] Melham, T. F., Automating recursive type definitions in higher order logic. In Current Trends in Hardware Verification and Automated Theorem Proving, G. Birtwistle, P. A. Subrahmanyam, Eds. Springer, 1989, pp. 341-386
[12] Milner, R., How to derive inductions in LCF, note, Dept. Comp. Sci., Univ. Edinburgh, 1980
[13] Milner, R., Communication and Concurrency, Prentice-Hall, 1989 · Zbl 0683.68008
[14] Monahan, B. Q., Data Type Proofs using Edinburgh LCF, PhD thesis, University of Edinburgh, 1984
[15] Paulin-Mohring, C., Inductive definitions in the system Coq: Rules and properties, Research Report 92-49, LIP, Ecole Normale Supérieure de Lyon, Dec. 1992 · Zbl 0844.68073
[16] Paulson, L. C., Logic and Computation: Interactive proof with Cambridge LCF, Cambridge Univ. Press, 1987 · Zbl 0645.68041
[17] Paulson, L. C., ML for the Working Programmer, Cambridge Univ. Press, 1991 · Zbl 0863.68032
[18] Paulson, L. C., Co-induction and co-recursion in higher-order logic, Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
[19] Paulson, L. C., Introduction to Isabelle, Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993
[20] Paulson, L. C., Set theory for verification: I. From foundations to functions, J. Auto. Reas. 11, 3 (1993), 353-389 · Zbl 0802.68128
[21] Paulson, L. C., Set theory for verification: II. Induction and recursion, Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993 · Zbl 0840.68104
[22] Paulson, L. C., A concrete final coalgebra theorem for ZF set theory, Tech. rep., Comp. Lab., Univ. Cambridge, 1994
[23] Pitts, A. M., A co-induction principle for recursively defined domains, Theoretical Comput. Sci. (1994), In press; available as Report 252, Comp. Lab., Univ. Cambridge · Zbl 0795.68129
[24] Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I., An EVES data abstraction example, In FME ’93: Industrial-Strength Formal Methods (1993), J. C. P. Woodcock, P. G. Larsen, Eds., Springer, pp. 578-596, LNCS 670
[25] Szasz, N.
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.