[maweki]

Now you have to talk about what a specification is.

If it is a relation from some function input to its output, that would be one step. And of course, functions are composable that way.

But say you have a system behaviour that is a stream of function applications, e.g. [f(0), f(f(0)), f(f(f(0)))...] and I forgot the name for this function. This infinite stream is your system behaviour.

Now we have a different behaviour [g(0), g(g(0)), g(g(g(0)))...]

You can (more or less) easily reason about the relation of g^n(0) to f^n(0) where both streams or behaviours are synchronous. But reasoning about the behaviour of all g^n(0) in relation to all f^m(0) is difficult.

All the useful properties for these streams, liveness, fairness, as well as other invariants, are not easily encoded.

[chriswarbo]

Co-inductive methods are useful for that sort of thing.

For example, we can prove two infinite streams are equal by showing that their definitions/generators are "bisimilar".

[maweki]

But the question is not whether their infinite extensions or limit are equal, but whether at each finite combination some property about the stream progress holds.

[bqmjjx0kac]

> and I forgot the name for this function.

I believe this is called `iterate` in Haskell.