Detecting termination of an arbitrary program written in a

Turing-complete language is (about as literally as can be) the halting

problem:

https://en.wikipedia.org/wiki/Halting_problemThis problem has been known to be unsolvable in general (assuming we

don’t discover some form of computation more powerful than a Turing

machine; that is, the Church-Turing thesis holds) since 1936, and is one

of the most fundamental results in computer science.

It’s possible to determine if programs halt if you restrict the language

sufficiently, but then it won’t be Turing-complete. However, this does

not make totality checking completely fruitless, as it turns out you can

do a great deal of useful things even in a language that is not

Turing-complete (which I find is often surprising to people).

Alexis

> On Aug 31, 2018, at 15:02, Rodrigo Stevaux <

[hidden email]> wrote:

>

> which cannot be prohibited statically if we want both the language to

> be Turing complete, and type inference to be decidable.

>

>

> Could you be so kind as to give a hint on literature that could help

> me understand this statement?

_______________________________________________

Haskell-Cafe mailing list

To (un)subscribe, modify options or view archives go to:

http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post.