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.

Leave a Reply