I presented a solver for first order stream equations. Those are simple equations of the form:
x = 2 :: head (tail x) :: head (3 :: head x :: x) :: tail (4 :: x)
The solver is parametric in the domain type. It turns out that unless the domain is empty, those equations always have solutions. Given a term representing the right hand side of an equation, it builds a template which is a finite representation of its solutions. A template is instantiated by providing an environment in which the under-constrained elements of the stream get a value.
There are two steps: first reduce the term to a normal form by eliminating redexes:
head (d :: s)reduces to
tail (d :: s)reduces to
Then, solve the problem for normal forms. An equation whose right hand side is in normal form looks like:
x = d_1 :: ... :: d_n :: tail^j x
d_i are either constants from the domain or equal to some element
x_k of the stream
x_i = d_i. We get also a condition on the rest of the stream: if
j = n, then there is no constraint on the remaining elements of the solutions (after the
n-th), otherwise, there will be a loop of length
n conditions boils to extracting the strongly connected components of a graph whose vertices are the
x_1 ... x_n and the edges are the dependencies between them. The problem is actually simpler than the general one because each vertex is target of at most one edge.
I implemented such an algorithm in Agda but chickened out from writing the proofs in Agda that the algorithm produced a template whose instances are exactly the solutions of the given equation. I wrote the proofs in English instead.