Abstract
Proofs by induction on some inductively defined structure, e. g., finitely-branching trees, may appeal to the induction hypothesis at any point in the proof, provided the induction hypothesis is only used for immediate substructures, e. g., the subtrees of the node we are currently considering in the proof. The basic principle of structural induction can be relaxed to course-of-value induction, which allows application of the induction hypothesis also to non-immediate substructures, like any proper subtree of the current tree. If course-of-value induction is not sufficient yet, we can resort to define a well-founded relation on the considered structure and use the induction hypothesis for any substructure which is strictly smaller with regard to the constructed relation.
You have full access to this open access chapter, Download conference paper PDF
Similar content being viewed by others
Proofs by induction on some inductively defined structure, e. g., finitely-branching trees, may appeal to the induction hypothesis at any point in the proof, provided the induction hypothesis is only used for immediate substructures, e. g., the subtrees of the node we are currently considering in the proof. The basic principle of structural induction can be relaxed to course-of-value induction, which allows application of the induction hypothesis also to non-immediate substructures, like any proper subtree of the current tree. If course-of-value induction is not sufficient yet, we can resort to define a well-founded relation on the considered structure and use the induction hypothesis for any substructure which is strictly smaller with regard to the constructed relation. At a closer look, however, this well-founded induction is just structural induction on the derivation of being strictly smaller. This means that in a logical system that allows us to construct inductive predicate and relations, such as, e. g., Martin-Löf Type Theory (Nordström et al. 1990) or the Calculus of Inductive Constructions (Paulin-Mohring 1993), structural induction is complete for any kind of inductive proof.
In all these flavors of induction, validity of induction hypothesis application can be checked easily and locally, independent of its context. In proof assistants, in principle a structural termination checker (Giménez 1995; Abel 2000) sufficesFootnote 1 to check such inductive proofs, which looks at the proof tree, extracts all calls to the induction hypotheses, and checks that they happen only on structurally smaller arguments. In practice, mutual induction is supported as well, based on a simple static call graph analysis (Abel and Altenkirch 2002; Barras 2010; Ben-Amram 2008; Hyvernat 2014).
Dually to structural induction, in a coinductive proof of a proposition defined as the greatest fixed-point of a set of rules, we may appeal to the coinduction hypothesis to fill the premises of the rule we have chosen to prove our goal. For instance, two infinite streams may be defined to be bisimilar if their heads are equal and their tails are bisimilar, coinductively. Our goal might be to show that bisimilarity is reflexive, i. e., any stream is bisimilar to itself. To establish bisimilarity, we use the sole rule with the first subgoal to show that the head of the stream is equal to itself. After this breath-taking enterprise, we are left with the second subgoal to show that the tail of the stream is bisimilar to itself, which we solve by appeal to the coinduction hypothesis. At this point, it is worth noting that not the stream got smaller (the tail of an infinite stream is still infinite), but the coinductive hypothesis is guarded by a rule application. This means that the coinductive proof can unfold into a possibly infinitely deep derivation without getting into a “busy loop”, meaning the proof is productive.
In a similar way as for induction, we seek to relax the criterion for well-formed coinductive proofs, which states that only the immediate subgoals of the final rule application can be filled by the coinductive hypothesis. We can allow several rule applications until we reach the coinductive hypothesis from the root of the derivation. This is dual to course-of-value induction and could be called guarded coinduction.Footnote 2
In contrast to induction, checking the validity of calls to the coinduction hypothesis requires us to look at the context of the calls rather than the call arguments. We have to check that the calls to the coinductive hypotheses happen in a constructor context, i. e., a context of coinductive rule applications only. This lack of locality also leads to a loss of compositionality of proofs by guarded coinduction. For instance, consider a coinductive proof of the bisimilarity of two streams through a bisimilarity chain, i. e., via some intermediate streams and the use of transitivity of bisimilarity. Transitivity is not a constructing rule for bisimilarity,Footnote 3 but an admissible rule proven by coinduction. As transitivity is not a constructor, we cannot use the coinduction hypothesis under transitivity nodes in the proof tree. In practice, often a severe restructuring of a natural informal proof is necessary to make it guarded and please a structural guardedness checker. The resulting proofs may be highly non-compositional and bloated, especially if proofs of previous lemmata have to be inlined and fused into the current proof.
To regain compositionality, we have to relax the contexts of coinductive hypothesis applications to include admissible rules and lemma invocation in general, without jeopardizing productivity. Such contexts need to produce one more rule constructor than they consume, which must be easily verifiable by the productivity checker. Sized types (Hughes et al. 1996; Amadio and Coupet-Grimal 1998; Barthe et al. 2004; Abel 2008; Sacchini 2013) offer the necessary technology. Coinductive types, propositions, and relations are parameterized by an ordinal \(i \le \omega \) which denotes the minimum definedness depth of their derivations. Semantically, this idea is already present in Mendler’s work (Mendler et al. 1986; Mendler 1991), and it is implicit in the principle of ordinal iteration to construct the greatest fixed point of a monotone operator F. We define the approximants \(\nu ^i F\) of the greatest fixed-point \(\nu ^\omega F\) by induction on ordinal i as follows:
For monotone F, we obtain a descending chain \(\nu ^0 F \sqsupseteq \nu ^1 F \sqsupseteq \cdots \sqsupseteq \nu ^\omega F\). The greatest fixed point of F is reached at stage \(\omega \) if F is continuous in the sense that \(\sqcap _{i \in I} F(A_i) \sqsubseteq F(\sqcap _{i \in I} A_i)\). For instance, all strictly positive type transformers correspond to continuous operators (Abel 2003, Theorem 1).
An alternative construction of the greatest fixed-point uses deflationary iteration (Sprenger and Dam 2003; Abel 2012; Abel and Pientka 2013),
which gives a descending chain without the monotonicity of F. However, the same conditions on F are needed to reach the fixed point at stage \(\omega \).
Giving names to the approximants \(\nu ^i F\) of coinductive type \(\nu ^\omega F\), we can express through the type system when a term t, which acts as the context for the coinductive hypothesis, produces one more constructor than it consumes: it needs to have type \(\forall i.\; \nu ^i F \rightarrow \nu ^{i+1} F\) polymorphic in “size” (depth) i. Such a context is called guarding. A weaker, but very common and useful property of a function t is to be guardedness preserving, i. e., having type \(\forall i.\; \nu ^i F \rightarrow \nu ^i F\). For instance, consider bisimilarity on streams, which is defined using relation transformer \(F(X)(x,y) = (\mathsf {head}\,x \equiv \mathsf {head}\,y) \times X\,(\mathsf {tail}\,x)\,(\mathsf {tail}y)\). The symmetry lemma of bisimilarity \(\forall i.\, \nu ^i F (x,y) \rightarrow \nu ^i F (y,x)\) is guardedness preserving: to produce one constructor of the requested bisimilarity derivation, it only needs to inspect the last constructor of the given bisimilarity derivation. Analogously, transitivity of bisimilarity receives type \(\forall i.\; \nu ^i F (x,y) \rightarrow \nu ^i F (y,z) \rightarrow \nu ^i F (x,z)\). Here, to produce the last rule of the output derivations we only need to inspect the last rule of the two input derivations. This typing allows us to freely use transitivity in coinductive proofs without jeopardizing the validity of the coinductive hypothesis.
Tracking guardedness levels in the type systems through “sized” coinductive types gives us compositional coinduction, as we can freely abstract out, for instance, guardedness-preserving contexts without upsetting some structural productivity checker who can only deal with concretely given code.
Recently, guardedness-preserving functions have been rediscovered in the context of Isabelle/HOL as friendly operations (Blanchette et al. 2015). Prototypical implementations of type-based termination with sized types exist for Coq (Sacchini 2015) and Agda. The latter has been subjected to a larger case study: an implementation of normalization by evaluation using the coinductive delay monad (Abel and Chapman 2014). Compositional coinduction with sized types seems to be a promising alternative to parameterized coinduction (Hur et al. 2013) and up-to techniques (Pous and Sangiorgi 2012).
Notes
- 1.
Even for induction, type-based termination offers significant advantages for compositionality and robustness, as argued, e. g., by Barras and Sacchini (2013). However, at this point there is no mature implementation in proof assistants based on dependent types.
- 2.
- 3.
In fact, it is well-known that every coinductive relation with a transitivity rule is trivial, i. e., the total relation. The proof of relatedness of arbitrary objects is just the infinite tree all of whose nodes are applications of the transitivity rule. This problem can be overcome with mixed coinductive-inductive types (Abel 2007; Nakata and Uustalu 2010), to allow only finitely many applications of the transitivity rule in a row (Danielsson and Altenkirch 2010).
References
Abel, A.: Specification and verification of a formal system for structurally recursive functions. In: Coquand, T., Nordström, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol. 1956, pp. 1–20. Springer, Heidelberg (2000). http://dx.doi.org/10.1007/3-540-44557-9_1
Abel, A.: Termination and productivity checking with continuous types. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 1–15. Springer, Heidelberg (2003). http://dx.doi.org/10.1007/3-540-44904-3_1
Abel, A.: Mixed inductive/coinductive types and strong normalization. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 286–301. Springer, Heidelberg (2007). http://dx.doi.org/10.1007/978-3-540-76637-7_19
Abel, A.: Semi-continuous sized types and termination. Log. Methods Comput. Sci. 4(2:3), 1–33 (2008). http://dx.doi.org/10.2168/LMCS-4(2:3)2008, CSL 2006 special issue
Abel, A.: Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. In: Miller, D., Ésik, Z. (eds.) Proceedings of 8th Workshop on Fixed Points in Computer Science (FICS 2012), Electronic Proceedings in Theoretical Computer Science, vol. 77, pp. 1–11 (2012). http://dx.doi.org/10.4204/EPTCS.77.1 , invited talk
Abel, A., Altenkirch, T.: A predicative analysis of structural recursion. J. Funct. Program. 12(1), 1–41 (2002). http://dx.doi.org/10.1017/S0956796801004191
Abel, A., Chapman, J.: Normalization by evaluation in the delay monad: a case study for coinduction via copatterns and sized types. In: Levy, P., Krishnaswami, N. (eds.) Proceedings of 5th Workshop on Mathematically Structured Functional Programming, MSFP 2014, Grenoble, France, Electronic Proceedings in Theoretical Computer Science, vol. 153, pp. 51–67, 12 April 2014. http://dx.doi.org/10.4204/EPTCS.153.4
Abel, A., Pientka, B.: Wellfounded recursion with copatterns: a unified approach to termination and productivity. In: Morrisett, G., Uustalu, T. (eds.) Proceedings of 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pp. 185–196. ACM Press, Boston, MA, USA, 25–27 September 2013. http://doi.acm.org/10.1145/2500365.2500591
Amadio, R.M., Coupet-Grimal, S.: Analysis of a guard condition in type theory (extended abstract). In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, p. 48. Springer, Heidelberg (1998). http://dx.doi.org/10.1007/BFb0053541
Barras, B.: The syntactic guard condition of Coq. In: Talk at the Journée “égalité et Terminaison” du 2 février 2010 in Conjunction with JFLA 2010 (2010). http://coq.inria.fr/files/adt-2fev10-barras.pdf
Barras, B., Sacchini, J.L.: Type-based methods for termination and productivity in Coq. In: Mahboubi, A., Tassi, E. (eds.) The 5th Coq Workshop, A Satellite Workshop of ITP 2013, Rennes, 22 July 2013. https://coq.inria.fr/coq-workshop/2013#Sacchini
Barthe, G., Frade, M.J., Giménez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Math. Struct. Comput. Sci. 14(1), 97–141 (2004). http://dx.doi.org/10.1017/S0960129503004122
Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst. 30(3) (2008). http://doi.acm.org/10.1145/1353445.1353450
Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In: Fisher, K., Reppy, J.H. (eds.) Proceedings of 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp. 192–204. ACM Press, Vancouver, BC, Canada, 1–3 September 2015. http://doi.acm.org/10.1145/2784731.2784732
Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994). http://dx.doi.org/10.1007/3-540-58085-9_72
Danielsson, N.A., Altenkirch, T.: Subtyping, declaratively. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 100–118. Springer, Heidelberg (2010). http://dx.doi.org/10.1007/978-3-642-13321-3_8
Giménez, E.: Codifying guarded definitions with recursive schemes. In: Dybjer, P., Nordström, B., Smith, J. (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1994). http://dx.doi.org/10.1007/3-540-60579-7_3
Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Boehm, H.J., Jr., G.L.S. (eds.) Conference Record of POPL 1996: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 410–423. ACM Press, St. Petersburg Beach, Florida, USA, 21–24 January 1996. http://doi.acm.org/10.1145/237721.240882
Hur, C., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 193–206. ACM Press, Rome, Italy, 23–25 January 2013. http://doi.acm.org/10.1145/2429069.2429093
Hyvernat, P.: The size-change termination principle for constructor based languages. Log. Methods Comput. Sci. 10(1) (2014). http://dx.doi.org/10.2168/LMCS-10(1:11)2014
Mendler, N.P., Panangaden, P., Constable, R.L.: Infinite objects in type theory. In: Proceedings, Symposium on Logic in Computer Science, pp. 249–255. IEEE Computer Society, Cambridge, Massachusetts, USA, 16–18 June 1986
Mendler, N.P.: Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Log. 51(1–2), 159–172 (1991). http://dx.doi.org/10.1016/0168-0072(91)90069-X
Nakata, K., Uustalu, T.: Resumptions, weak bisimilarity and big-step semantics for while with interactive I/O: an exercise in mixed induction-coinduction. In: Aceto, L., Sobocinski, P. (eds.) Proceedings of 7th Workshop on Structural Operational Semantics, SOS 2010, Paris, France, Electronic Proceedings in Theoretical Computer Science, vol. 32, pp. 57–75, 30 August 2010. http://dx.doi.org/10.4204/EPTCS.32.5
Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin Löf’s Type Theory: An Introduction. Clarendon Press, Oxford (1990). http://www.cs.chalmers.se/Cs/Research/Logic/book/
Paulin-Mohring, C.: Inductive definitions in the system Coq - rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993). http://dx.doi.org/10.1007/BFb0037116
Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, Cambridge (2012)
Sacchini, J.: Co\(\widehat{q}\): Type-based termination in the Coq proof assistant (2015). project description, http://qatar.cmu.edu/ sacchini/coq.html
Sacchini, J.L.: Type-based productivity of stream definitions in the calculus of constructions. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pp. 233–242. IEEE Computer Society Press, New Orleans, LA, USA, 25–28 June 2013. http://dx.doi.org/10.1109/LICS.2013.29
Sprenger, C., Dam, M.: On the structure of inductive reasoning: circular and tree-shaped proofs in the \(\mu \)-calculus. In: Gordon, A.D. (ed.) FOSSACS 2003 and ETAPS 2003. LNCS, vol. 2620, pp. 425–440. Springer, Heidelberg (2003). http://dx.doi.org/10.1007/3-540-36576-1_27
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 IFIP International Federation for Information Processing
About this paper
Cite this paper
Abel, A. (2016). Compositional Coinduction with Sized Types. In: Hasuo, I. (eds) Coalgebraic Methods in Computer Science. CMCS 2016. Lecture Notes in Computer Science(), vol 9608. Springer, Cham. https://doi.org/10.1007/978-3-319-40370-0_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-40370-0_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40369-4
Online ISBN: 978-3-319-40370-0
eBook Packages: Computer ScienceComputer Science (R0)