Daniel Freiermuth: Bachelor's Thesis

Saarland University Computer Science

Formalizing stream calculus using coinduction

Advisors: Steven Schäfer

Abstract:

Sequences of elements of some type T are common in discrete mathematics and computer science. Stream Caculus is a powerful and clean tool for dealing with those, capable even of handling more involved ones (like non-trivial recurrence relations) and not only useful for proving propositions, but even deriving them.
Streams are often given by Stream differential equations. Regarding the soundness of such equations, it turns out that Causality is a key property that allows us to use corecursion to solve Stream differential equations.
Having a ring structure on T, we can introduce more structure on Stream of type T, namely a ring structure and squareroot. We can use that to reason on the level of Streams. This is highly motivated by ordinary and exponential generating functions.

References:

Downloads:


Legal notice, Privacy policy