×

Foundations of regular coinduction. (English) Zbl 07471662

Summary: Inference systems are a widespread framework used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. In this paper, we consider a middle way interpretation, called regular, which combines advantages of both approaches: it allows non-well-founded reasoning while being finite. We show that the natural proof-theoretic definition of the regular interpretation, based on regular trees, coincides with a rational fixed point. Then, we provide an equivalent inductive characterization, which leads to an algorithm which looks for a regular derivation of a judgment. Relying on these results, we define proof techniques for regular reasoning: the regular coinduction principle, to prove completeness, and an inductive technique to prove soundness, based on the inductive characterization of the regular interpretation. Finally, we show the regular approach can be smoothly extended to inference systems with corules, a recently introduced, generalised framework, which allows one to refine the coinductive interpretation, proving that also this flexible regular interpretation admits an equivalent inductive characterisation.

MSC:

03B70 Logic in computer science
68-XX Computer science

Software:

CoCaml; Paco; coFJ
PDFBibTeX XMLCite
Full Text: arXiv Link

References:

[1] Peter Aczel, Jir´ı Ad´amek, Stefan Milius, and Jiri Velebil. Infinite trees and completely iterative theories: a coalgebraic view.Theoretical Computer Science, 300(1-3):1-45, 2003.doi:10.1016/ S0304-3975(02)00728-4. · Zbl 1028.68077
[2] Davide Ancona, Pietro Barbieri, Francesco Dagnino, and Elena Zucca. Sound regular corecursion in coFJ. In34nd European Conference on Object-Oriented Programming, ECOOP 2020, volume
[3] Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor,Handbook of Mathematical Logic, volume 90 ofStudies in Logic and the Foundations of Mathematics, pages · Zbl 0324.02009
[4] Davide Ancona and Agostino Dovier. A theoretical perspective of coinductive logic programming. Fundamenta Informaticae, 140(3-4):221-246, 2015.doi:10.3233/FI-2015-1252. · Zbl 1348.68028
[5] Davide Ancona, Francesco Dagnino, and Elena Zucca. Extending coinductive logic programming with co-facts. In Ekaterina Komendantskaya and John Power, editors,Proceedings of the First · Zbl 1468.68054
[6] Davide Ancona, Francesco Dagnino, and Elena Zucca. Generalizing inference systems by coaxioms. In Hongseok Yang, editor,Programming Languages and Systems - 26th European Symposium on · Zbl 1485.68053
[7] Jir´ı Ad´amek, Stefan Milius, and Jiri Velebil. Iterative algebras at work.Mathematical Structures in Computer Scienc, 16(6):1085-1131, 2006.doi:10.1017/S0960129506005706. · Zbl 1112.18005
[8] Davide Ancona and Elena Zucca. Corecursive Featherweight Java. In Wei-Ngan Chin and Aquinas Hobor, editors,Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, · Zbl 0982.68809
[9] Henning Basold, Ekaterina Komendantskaya, and Yue Li. Coinduction in uniform: Foundations for corecursive proof search with horn clauses. In Lu´ıs Caires, editor,Programming Languages and
[10] Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. A general account of coinduction up-to.Acta Informatica, 54(2):127-190, 2017.doi:10.1007/s00236-016-0271-4. · Zbl 1371.68186
[11] James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Bernhard Beckert, editor,Automated Reasoning with Analytic Tableaux and Related Methods, International · Zbl 1142.03366
[12] James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent.Journal of Logic and Computation, 21(6):1177-1216, 2011.doi:10.1093/logcom/exq052. · Zbl 1242.03084
[13] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Robert M. Graham, Michael A. Harrison, and Ravi Sethi, editors,The 4th ACM Symposium on Principles of · Zbl 1149.68389
[14] Bruno Courcelle. Fundamental properties of infinite trees.Theoretical Computer Science, 25:95- 169, 1983.doi:10.1016/0304-3975(83)90059-2. · Zbl 0521.68013
[15] Francesco Dagnino. Generalizing inference systems by coaxioms. Master’s thesis, DIBRIS, University of Genova, 2017. Best italian master thesis in Theoretical Computer Science 2018. URL: http://eatcs.org/images/it/theses/Dagnino_thesis.pdf.
[16] Francesco Dagnino. Coaxioms: flexible coinductive definitions by inference systems.Logical Methods in Computer Science, 15(1), 2019.doi:10.23638/LMCS-15(1:26)2019. · Zbl 1432.68251
[17] Francesco Dagnino, Davide Ancona, and Elena Zucca. Flexible coinductive logic programming. Theory and Practice of Logic Programming, 20(6):818-833, 2020. Issue for ICLP 2020.doi: · Zbl 1468.68054
[18] Amina Doumane.On the infinitary proof theory of logics with fixed points. (Th´eorie de la d´emonstration infinitaire pour les logiques ‘a points fixes). PhD thesis, Paris Diderot University,
[19] Brian A. Davey and Hilary A. Priestley.Introduction to Lattices and Order. Cambridge University Press, 2 edition, 2002.doi:10.1017/CBO9780511809088. · Zbl 1002.06001
[20] J´erˆome Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Simona Ronchi Della Rocca, editor,Computer Science Logic 2013, CSL 2013, volume 23 ofLIPIcs, pages 248-262. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.doi: 10.4230/LIPIcs.CSL.2013.248. · Zbl 1356.03098
[21] Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. In Roberto Giacobazzi and Radhia Cousot, editors,The 40th Annual ACM · Zbl 1301.68220
[22] Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Language constructs for nonwell-founded computation. In Matthias Felleisen and Philippa Gardner, editors,Program · Zbl 1381.68034
[23] Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Cocaml: Functional programming with regular coinductive types.Fundamenta Informaticae, 150(3-4):347-377, 2017.doi:10.3233/ FI-2017-1473. · Zbl 1374.68098
[24] Xavier Leroy and Herv´e Grall. Coinductive big-step operational semantics.Information and Computation, 207(2):284-304, 2009.doi:10.1016/j.ic.2007.12.004. · Zbl 1165.68044
[25] Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion - the locally finite fixpoint and its properties. In Bart Jacobs and Christof L¨oding, editors, · Zbl 1475.68196
[26] Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion and iterative algebras.Information and Computation, page 104456, 2019.doi:10.1016/j.ic. 2019.104456. · Zbl 1435.68208
[27] Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In Mogens Nielsen and Uffe Engberg, editors,Foundations of Software Science and Computation Structures - 5th · Zbl 1077.03515
[28] Davide Sangiorgi.Introduction to Bisimulation and Coinduction. Cambridge University Press, USA, 2011. · Zbl 1252.68008
[29] Luke Simon, Ajay Bansal, Ajay Mallya, and Gopal Gupta. Co-logic programming: Extending logic programming with coinduction. In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors,Automata, Languages and Programming, 34th International Colloquium, · Zbl 1171.68404
[30] Luke Simon, Ajay Mallya, Ajay Bansal, and Gopal Gupta. Coinductive logic programming. In Sandro Etalle and Miroslaw Truszczynski, editors,Logic Programming, 22nd International · Zbl 1131.68400
[31] R´egis Spadotti.A mechanized theory of regular trees in dependent type theory. (Une th´eorie m´ecanis´ee des arbres r´eguliers en th´eorie des types d´ependants). PhD thesis, Paul Sabatier
[32] Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications.Pacific Journal of Mathematics, 5(2):285-309, 1955. · Zbl 0064.26004
[33] Tarmo Uustalu and Niccol‘o Veltri. Finiteness and rational sequences, constructively.Journal of Functional Programming, 27:e13, 2017.doi:10.1017/S0956796817000041. · Zbl 1418.68069
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.