Solving first order stream equations

May 10th, 2010 by fyb

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

2 Responses to “Solving first order stream equations”

1. axel.walker Says:

Maybe i’m wrong but the example equation has many solutions :
x = 2 :: ? :: 3 :: x

you could replace ? by any value.

2. Florent Says:

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.