When specializing a let-expression
Similix might choose to unfold or residualize it. If the binding-time of
the parameter V (and therefore also E) is static then Similix can
safely unfold the let-expression, but if the binding-time of V is
dynamic the situation is different. Uncritically unfolding a let whose
parameter is dynamic can lead to either code duplication or wrong residual
programs. Code duplication could occur when it turns out that the
parameter will be used more than once in the residual program. Depending on
the context, code duplication could lead to a slowdown, if the duplicated
code occurs on the same evaluation path in the residual program. A wrong
residual program is one for which the Mix-equation does not hold. If, by
unfolding a let, a non-terminating computation is discarded, then the
residual program terminates more often than the original program, and can
therefore not obey the Mix-equation
. The following is an example of such a case:
Notice that if the residual program had not contained the call (f-0-1 d_0) then it would terminate for negative values of d_0 which would not be the case for the original program when called as follows (goal 3 d) where d is a negative number. So in conclusion: a dynamic let-expression can only be unfolded when its actual argument is known to be executed exactly once in the specialized body of the let-expression.
When the expression E in the let expression contains a side-effecting subexpression, unfolding the let-expression may change the order of side-effects, so in that case Similix never unfolds the let-expression. In the next example we will demonstrate this:
If the let-expressions in this example were unfolded then not only would the order in which input is read be changed, but also the number of values read. So Similix does not unfold the let-expressions in this case. Sequences, i.e. begin-expressions, are handled as if these were let-expressions with dummy formal parameters, not occurring free in the body of the let-expression. Note also that here the order of evaluation is preserved.
