[clean-list] strong root normal form

[Marco Kesseler]

Hi Erik,

>I am at a point where I want to understand the concept of 'strong root
>normal form'. There are too many programs in which I turn lets into strict
>lets and stumble upon a version that appears to work as I had expected. But
>I don't understand what's happening. 

I may be able to give an alternative informal explanation. If this is 
not entirely accurate, anyone, please correct me. It has been a 
while. That being said, I doubt that you need all this to understand 
how Clean works. See the end of this mail.

>The Clean documentation says:
>
>"A pattern partially matches a graph if firstly the symbol of the root of
>the pattern equals the symbol of the root of the graph and secondly in
>positions where symbols in the pattern are not syntactically equal to
>symbols in the graph, the corresponding sub-graph is a redex or the
>sub-graph itself is partially matching a rule.

A partial match means: we know that the root of an expression matches 
the pattern, and for the rest of the graph we do not know yet whether 
it matches the rest of the pattern, because it has not yet been 
evaluated far enough to decide.

>A graph is in strong root
>normal form if the graph does not partially match any rule.

As long as a graph partially matches a rule, it may still be 
reducible by that rule (it can, as soon as we are able to establish a 
total match). Conversely, if a graph does not partially match ANY 
rule, this means that there is NO rule that will EVER be able to 
rewrite the root node to anything else.

>It is decidable
>whether or not a graph is in strong root normal form. A graph in strong root
>normal form does not partially match any rule, so it is also in root normal
>form.

The exact differences between strong root normal form and root normal 
form elude me right now. Root normal form basically means that the 
root will never reduce to anything else. This means that the root is 
known to be part of the final result.

In terms of Clean you could see it as follows: if you have a rule

f 1 = Cons 2 (f 2)
f 2 = Nil

then the rule pattern 'f 1' (partially) matches the expression 'f (0 
+ 1)', because f matches f, and for the rest of the pattern we do not 
know yet. After reducing (0 + 1) it totally matches 'f 1', turning it 
into a redex, that can be rewritten to 'Cons 2 (f 2)'. 'Cons' does 
not match any pattern, so it is part of the final result and can be 
delivered.

Looking at things this way seems a bit overkill though. I doubt that 
many programmers find comfort in the statement that 'f (0 + 1)' 
partially matches the patterns 'f 1' and 'f 2'.

>The default reduction strategy used in CLEAN is the functional reduction
>strategy. Reducing graphs ac-cording to this strategy resembles very much
>the way execution proceeds in other lazy functional languages: in the
>standard lambda calculus semantics the functional strategy corresponds to
>normal order reduction.

In the discussion above, we have seen that graphs can partially match 
a pattern. But before we can apply a rewrite rule, we have to know 
whether there is a rule that matches completely. In order to 
establish this, we may have to reduce some subgraph. This was the 
case with the '0 + 1' expression in the example above.

The point is now: we cannot just start reducing any subgraph we like, 
and repeat this until we we happen to have a match. If we choose the 
wrong subgraphs, we might end up in an infinite reduction, probably 
reducing graphs that are not needed for the final result.

So, we need a sensible order for choosing our rewrite rules. The 
normal order reduction strategy has been proven to be a sensible 
order. It will never cause a needless infinite computation.

>On graph rewrite rules the functional strategy
>proceeds as follows: if there are several rewrite rules for a particular
>function, the rules are tried in textual order; patterns are tested from
>left to right; evaluation to strong root normal form of arguments is forced
>when an actual argument is matched against a corresponding non-variable part
>of the pattern. A formal definition of this strategy can be found in (Toyama
>et al., 1991)."

Basically, this strategy means that you only evaluate a graph for as 
far as needed to establish whether it completely matches a pattern. 
And as you cannot write down infinite patterns, this process cannot 
CAUSE  an infinite computation either.

Others may call it common sense, but note that strict programming 
languages do not use this strategy. They will always evaluate 
function arguments before evaluating the function itself, even if 
they are not needed to establish the function result.

But wait: what if the functional strategy reduces a subgraph that 
leads to an infinite computation while matching for a pattern? Well 
in that case the function would have been undefined anyway. 
Programmer mistake.

>Well, to be honest, I understand not a word of this. Does anybody have some
>examples of expressions which are or are not in SRNF and why?

I hope this clears things up somewhat. If not, you may find comfort 
in the fact that I never think about these issues while programming 
in Clean. I just remember things like:

- Clean will normally evaluate its results top-down. First the root 
constructor, then its parts. Same for each substructure. As soon as 
an expression delivers its root constructor (Cons or Nil in case of 
lists), it is in root normal form.

- Without strictness annotations Clean will never evaluate more than 
is necessary to establish the part of the result that has to be 
delivered next.

- Derived strictness information may change the evaluation order, but 
this does not change the previous remark. Strictness will only be 
derived for expressions that are needed to compute the root result.

- Explicit strictness annotations will change the evaluation order, 
relative to other evaluations. What happens exactly is a bit depended 
on the kind of strictness annotation (and I do not know the latest 
details). I try to avoid them as much as possible (same with 
uniqueness by the way), but sometimes a program is just too 
inefficient without them.

Now the main question becomes: what is it that you need strictness 
for exactly? Is it needed for efficient execution, to reduce memory 
equirements, or for other reasons? Can you give an example of a 
surpising effect?

regards,
Marco