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 '17 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$ – Damiano Mazza Nov 13 '17 at 12:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.