Tue 16 April 2013, 15:30-17:30
Keisuke Nakano (Univ. Electro-Communications), 2 Talks
理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7
Talk 1: Juggling meets coinduction
In this talk, I will present an application of coinduction, juggling. 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 talk, I will formalize their theory 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 certified. The result exposes a practical aspect of coinductive proofs. Most part of this talk has been presented in CPP 2012. Some open problems also will be introduced.
Talk 2: Metamorphism in jigsaw
In this talk, I will present a new computation model for metamorphism. A metamorphism is an unfold after a fold, consuming an input by the fold then generating an output by the unfold. It is typically useful for converting data representations, e.g., radix conversion of numbers. Bird and Gibbons have shown that metamorphisms can be incrementally processed in streaming style when a certain condition holds because part of the output can be determined before the whole input is given. However, whereas radix conversion of fractions is amenable to streaming, radix conversion of natural numbers cannot satisfy the condition because it is impossible to determine part of the output before the whole input is completed. In this talk, I present a jigsaw model in which metamorphisms can be partially processed for outputs even when the streaming condition does not hold. The jigsaw model allows us to process metamorphisms in a flexible way that includes parallel computation. We also apply our model to other examples of metamorphisms. Most part of this talk is recently published in Journal of Functional Programming. Additionally, I will present some further work on this work.