> Then how does this example from a Hawk paper (Microprocessor
> Specification in Hawk) work? Any Hawk code with feedback would
> have this kind of definition.
It's a standard problem, so we don't need Hawk examples:
This won't work:
let
xs = map (+1) xs
in xs
This works (and may or may not be what you intended):
let
xs = 0 : map (+1) xs
in xs
None of these examples will terminate, but (thanks to Haskell's
non-strict semantics) the second will produce partial information
about xs while looping, whereas the first (if ghc would let it) would
just loop, trying to calculate information about xs, without ever
finding any..
In other words, you've got to make sure that your recursion can get
started. If not even partial information about the right-hand side is
available without knowing anything about the left-hand side (xs), then
no information will ever be produced (*).
Some implementations are able to flag some cases of non-productive,
non-terminating programs as a black hole, but the problem is in the
definition itself.
Presumably, Hawk uses a representation that ensures productivity of
recursive definitions, or a coding style that avoids non-productive
recursions (e.g., the `delay 0' guarding the feedback in your example
looks suspicious).
As your original question involved a recursive integral, you might also
want to take a closer look at Fran [1], which has exactly this problem,
and work-arounds for each of its implementations. It is not at all
obvious where the initial fragment of the recursive structure should
come from in some cases, potentially leading to rather arbitrary choices,
but you are in a much better position to make such choices than the
implementation.
Claus
[1] http://www.research.microsoft.com/~conal/Fran/
(*) formally, you have a fixpoint-calculation: you start with no
information about the lhs, then try to evaluate the rhs (with no
information about xs). If this gives you some information (such
as "xs is not empty"), you are in the game and can repeat the
process (now with a slightly better approximation of xs), trying
to get more information in each step.
