Advisors: Steven Schäfer
Sequences are commonly used in discrete mathematics and computer science. Stream calculus 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. It is highly inspired by generating functions.
We present a type-theoretic implementation of Rutten's stream calculus.
We use stream differential equations similar to behavioral differential equations in to define streams and operations on streams.
We show that every system of causal stream differential equation has a unique solution.
This is analogue to a result from Pous.
We prove that every causal operator stream differential equation has a unique and causal result.
Instead of bisimilarity as used by Rutten, we use induction on prefix equality as the main proof technique.
This fits well with our use of causality.
We formalize a ring of streams with convolution product, the multiplicative inverse and a square root.
We use this to prove a basic property about the Fibonacci sequence and derive the closed form of the stream of Catalan numbers.