<p>From <a href="https://cstheory.stackexchange.com/questions/36767/can-elementary-affine-logic-be-used-as-the-core-type-system-of-a-practical-progr">this question</a>, 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 <code>fix</code> in the same style that duplication is restricted by <code>let</code> and boxes, then, I believe, that could be doable. Is it?</p>

CC BY-SA 3.0
2017-11-13T12:42:35.987Z
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?
MaiaVictor
CC BY-SA 3.0
2017-11-13T12:59:30.833Z
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...
Damiano Mazza
<lambda-calculus><functional-programming><linear-logic>
Is it possible to use arbitrary fixpoint values on EAL without losing strong normalization?
MaiaVictor
# Is it possible to use arbitrary fixpoint values on EAL without losing strong normalization?

(Asked by: username_0 on 2017-09-01)

From [this question](https://cstheory.stackexchange.com/questions/36767/can-elementary-affine-logic-be-used-as-the-core-type-system-of-a-practical-progr), 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?

**Tags:** lambda-calculus, functional-programming, linear-logic

> **Comments:**
> **username_0**: 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?  
> **username_1**: 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...  

---

## 0 answers

