[Risord]

So how non-turing completeness work with infinite streams?

Many practical applications (like this) are working with possibly infinite stream of user inputs / requests etc. If we can guarantee that our server, browser or game application just stops eventually we know that something is wrong. However we like to guarantee that our application won't work infinitely with single request / input / time tick. So does this say that we want avoid using turing complete language mostly but turing complete part need to be handled somewhere maybe outside of our code? Something like how Haskell works with side effects. What you think?

[tom_mellior]

Coq is not Turing complete but has support for coinductive data types (= infinite streams) and (co-)recursion over them.

Simplifying a lot, it has a syntactic "guard condition" that says that you must produce some result before you're allowed to make a recursive call. For example, you can map over an infinite stream because a map produces a result for each element of the input stream. Unlike Haskell, you cannot write a fold over an infinite stream because you would need to look at all elements before producing a result.

So if you can structure your system as a transformation from an infinite stream of requests to an infinite stream of responses, you're fine in Coq even though it is not Turing complete.

The intuition is that, just like in Haskell, you don't actually end up doing an infinite computation if only a finite part of the final result is ever requested.

[pron]

If you have support for coinductive data types then you are Turing complete. Proof: you can simulate a Turing machine. However, Coq's term language is not Turing complete, meaning that every syntactic element in Coq evaluates to a terminating computation.

[lmm]

> So does this say that we want avoid using turing complete language mostly but turing complete part need to be handled somewhere maybe outside of our code? Something like how Haskell works with side effects.

Yes. E.g. you might have most of your logic in a turing-incomplete per-tick or per-request function, and then a single explicitly "unsafe" infinite loop at top level. In a language like Idris this happens naturally - you just have an explicit distinction between total and not-necessarily-total functions.

[colanderman]

See my sibling comment. Decidability by definition does not apply to infinite inputs (i.e., it is a nonsensical question to ask, like "what is the square root of potato?"). Some proof languages like Coq implicitly extend decidability to extend to infinite streams with finite representations (think generative regular expressions or state machines).

[dismantlethesun]

It won't. It will instead operate over the first googol items and then require a restart.