<div dir="ltr">Oh I see. Type checking a possibly infinite computation might itself take possibly infinite steps?<br></div><br><div class="gmail_quote"><div dir="ltr">Em sex, 31 de ago de 2018 às 17:13, Alexis King <<a href="mailto:lexi.lambda@gmail.com">lexi.lambda@gmail.com</a>> escreveu:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Detecting termination of an arbitrary program written in a<br>
Turing-complete language is (about as literally as can be) the halting<br>
problem:<br>
<br>
    <a href="https://en.wikipedia.org/wiki/Halting_problem" rel="noreferrer" target="_blank">https://en.wikipedia.org/wiki/Halting_problem</a><br>
<br>
This problem has been known to be unsolvable in general (assuming we<br>
don’t discover some form of computation more powerful than a Turing<br>
machine; that is, the Church-Turing thesis holds) since 1936, and is one<br>
of the most fundamental results in computer science.<br>
<br>
It’s possible to determine if programs halt if you restrict the language<br>
sufficiently, but then it won’t be Turing-complete. However, this does<br>
not make totality checking completely fruitless, as it turns out you can<br>
do a great deal of useful things even in a language that is not<br>
Turing-complete (which I find is often surprising to people).<br>
<br>
Alexis<br>
<br>
> On Aug 31, 2018, at 15:02, Rodrigo Stevaux <<a href="mailto:roehst@gmail.com" target="_blank">roehst@gmail.com</a>> wrote:<br>
> <br>
> which cannot be prohibited statically if we want both the language to<br>
> be Turing complete, and type inference to be decidable.<br>
> <br>
> <br>
> Could you be so kind as to give a hint on literature that could help<br>
> me understand this statement?<br>
</blockquote></div>