## Solving first order stream equations

May 10th, 2010 by fybI 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`d`

`tail (d :: s)`

reduces to`s`

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

where the `d_i`

are either constants from the domain or equal to some element `x_k`

of the stream `x`

.

We get `n`

equations: `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 `abs(n-j)`

.

Solving the `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.

May 10th, 2010 at 3:14 pm

Maybe i’m wrong but the example equation has many solutions :

x = 2 :: ? :: 3 :: x

you could replace ? by any value.

July 13th, 2010 at 1:57 pm

I agree. The equations have at least one solution, my procedure tells when they don’t have more than one. Actually in this simple context, the algorithm gives a representation of ALL the solutions in the form of a template.