From this question, the answerer states EAL-based languages can use arbitrary fixpoint types without losing strong normalization, because their normalization (and complexity) properties comes from linear types and the stratification of terms. I wonder, though, if the same can be done for value-level fixed-points; i.e., is it possible to express things such as infinite lists without losing strong normalization? If one could mechanically restrict the unrolling of fix in the same style that duplication is restricted by let and boxes, then, I believe, that could be doable. Is it?

  • $\begingroup$ Nobody? Basically the idea is to only allow fix to unroll lazily, and if the term is enclosed by a !, and the fixed variable only occurs inside exactly 1 !. That guarantees the fixed term always stays at the same level. Could that introduce non-termination? $\endgroup$
    – MaiaVictor
    Nov 13, 2017 at 12:42
  • $\begingroup$ I don't understant what you mean exactly. Your description seems to correspond to considering a construct $\mathsf{fix}\,f.M$ in which $f$ occurs only at exponential depth $1$ in $M$, with the reduction rule $$!\mathsf{fix}\,f.M\to M\{\mathsf{fix}\,f.M/f\}.$$ However, this is obviously non terminating (consider $!\mathsf{fix}\,f.!f$), so I don't think this is what you mean. It is hard to answer when the question is too vague... $\endgroup$ Nov 13, 2017 at 12:59


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.