Correction on our FoSSaCS 2001 paper

Correction on our FoSSaCS 2001 paper (1 February 2001, by Masahito Hasegawa)

In Section 7 (Conclusion and Further Work), the dinaturality for the call-by-value fixpoint operator is wrongly stated:

must be

We do need these eta-expansions for the precise correspondence with the dinaturality on the corresponding iterator. We apologize for this sloppiness (we noticed this shortly after submitting the final camera-ready...).
In fact, one can show that the first equation is operationally wrong, by writing down simple ML programs F, G which invalidate it, e.g.,

  fun F (f:int->int) = (print "Hello"; fn x:int => x);
  fun G (f:int->int) = (print "Bye"; fn x:int => x);
  (* F, G : (int -> int) -> int -> int *)

Obviously, fix (G o F) 1 and G (fix (F o G)) 1 behave differently. On the other hand, the second (corrected) equation is valid as the eta-expansions prevent undesirable side-effects. Similar seemingly-correct equations like fix F = fix (F o F) are also invalidated by this example.

In the extended version (to appear in Higher-Order Symbolic Computation), this mistake has been corrected.

Back to Hassei's Research Page / Home Page