Abstract
Buhler et al. presented a mathematical theory of toss juggling by regarding a toss pattern as an arithmetic function, where the function must satisfy a condition for the pattern to be valid. In this paper, the theory is formalized in terms of coinduction, reflecting the fact that the validity of toss juggling is related to a property of infinite phenomena. A tactic is implemented for proving the validity of toss patterns in Coq. Additionally, the completeness and soundness of a well-known algorithm for checking the validity is demonstrated. The result exposes a practical aspect of coinductive proofs. © 2012 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Nakano, K. (2012). Shall we juggle, coinductively? In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 160–172). https://doi.org/10.1007/978-3-642-35308-6_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
