On Monday, 27 January 2014 at 22:40:19 UTC, Simen Kjærås wrote:
> My computer has 16GB of RAM. You try keeping track of all the possible states.

Wrong reasoning.

The issue is that the proof for the halting problem does assume non-finite resources. That means that the proof that you cannot prove termination for an arbitrary program does not hold for programs that run on your computer. :^)

Anyway, the reasoning does not hold anyway, because there is an inifinite number of programs that can be proved to terminate… So you just do those instead!

> computers. It's technically true, yes. It also does not matter, for the reason described above.

When people try to be theoretical smartasses they should fess up to a theoretical response!

From a pragmatic position speculative precomputation is quite acceptable, works well with profiling on typical datasets and whole program analysis.

Even if the compution does not terminate you can run it as far as you can and then freeze the result, and use that as a starting point.

A cheap version of this has been used for decades to speed up program initialization: run the program until it reads input, then core dump. Run a program on the core dump that turns it into an executable. This is a nice way to speed up the initialization of interpreted programs. Java needs this badly!

> Lastly, deadalnix didn't even bring up the halting problem, so why even mention it?

He did implicitly, it was referenced in d.learn. This thread runs in two forums.

Ola

On 28.01.2014 10:42, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>"@puremagic.com wrote:
> On Monday, 27 January 2014 at 22:40:19 UTC, Simen Kjærås wrote:
>> My computer has 16GB of RAM. You try keeping track of all the possible states.
>
> Wrong reasoning.

Correct reasoning. My reasoning is that this is infeasible, not impossible in theory.


> The issue is that the proof for the halting problem does assume non-finite
> resources. That means that the proof that you cannot prove termination for an
> arbitrary program does not hold for programs that run on your computer. :^)

I am well aware what the halting problem is. I'm just saying that actually *proving* non-termination is impossible in practical situations. "This takes too much time, let's do something else" is not a proof, but more than good enough for most porpoises.


 Anyway, the reasoning does not hold anyway, because there is an inifinite number
> of programs that can be proved to terminate… So you just do those instead!

I assume you mean finite.


>  From a pragmatic position speculative precomputation is quite acceptable, works
> well with profiling on typical datasets and whole program analysis.

Absolutely. But just as the halting problem says that the question of whether a program with infinite memory terminates is undecidable in general, it is infeasible to *prove* whether a program will terminate even if memory today is actually not infinite.

The fact that the halting problem does not apply to computers with finite memory has no effect on deadalnix's question - it's still impossible to prove, just for a different reason.

-- 
  Simen

On Tuesday, 28 January 2014 at 15:49:14 UTC, Simen Kjærås wrote:
> Correct reasoning. My reasoning is that this is infeasible, not impossible in theory.

A refutal of a proof is not required to be executed? That's not the purpose.

> "This takes too much time, let's do something else" is not a proof, but more than good enough for most porpoises.

Then you agree with me. Good. :)

>  Anyway, the reasoning does not hold anyway, because there is an inifinite number
>> of programs that can be proved to terminate… So you just do those instead!
>
> I assume you mean finite.

No, only if you assume finite resources. Proof is trivial: you can just add an infinite number of NOPs (like a= a+1-1) without affecting semantics.

> Absolutely. But just as the halting problem says that the question of whether a program with infinite memory terminates is undecidable in general, it is infeasible to *prove* whether a program will terminate even if memory today is actually not infinite.

Correction: it is infeasible to prove the termination aspects of ALL programs. There are plenty of programs (or functions) where you can prove it.

It depends on the program, but that doesn't matter. That was my main point. Theoretical computer science isn't pragmatic, but optimization is always pragmatic.

> with finite memory has no effect on deadalnix's question - it's still impossible to prove, just for a different reason.

I thought we agreed that we don't need to prove anything? You can just bail out or do some kind of partial evaluation.

You might even want to speculatively calculate non-compile-time functions for given parameters after profiling. Like if f(x) is called 50% with the value x=32, then precompute and emit a switch(x) statement with f(x) as the default and the value for f(32) as a case.

Profiling really changes how you view these things.

On 01/28/2014 04:49 PM, Simen Kjærås wrote:
>
> On 28.01.2014 10:42, "Ola Fosheim Grøstad"
>  <ola.fosheim.grostad+dlang@gmail.com>"@puremagic.com wrote:
>  [...] there is an inifinite number
>> of programs that can be proved to terminate… [...]
>
> I assume you mean finite.

He meant infinite. (Which is correct.)

On 01/28/2014 05:18 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>
>>  Anyway, the reasoning does not hold anyway, because there is an
>> inifinite number
>>> of programs that can be proved to terminate… So you just do those
>>> instead!
>>
>> I assume you mean finite.
>
> No, only if you assume finite resources. Proof is trivial: you can just
> add an infinite number of NOPs (like a= a+1-1) without affecting semantics.

_Now_ you mean finite. :o)

(In any case, there is even an infinite number of programs that are not behaviourally equal but can be automatically proved to terminate by one and the same algorithm.)

On Tuesday, 28 January 2014 at 16:29:24 UTC, Timon Gehr wrote:
> _Now_ you mean finite. :o)

I just tried to make things easy…

> (In any case, there is even an infinite number of programs that are not behaviourally equal but can be automatically proved to terminate by one and the same algorithm.)

Oh… don

On Tuesday, 28 January 2014 at 17:01:24 UTC, Ola Fosheim Grøstad
wrote:
> On Tuesday, 28 January 2014 at 16:29:24 UTC, Timon Gehr wrote:
>> _Now_ you mean finite. :o)
>
> I just tried to make things easy…
>
>> (In any case, there is even an infinite number of programs that are not behaviourally equal but can be automatically proved to terminate by one and the same algorithm.)
>
> Oh… don

Woops. The program terminated without a proof! :-]

I am sooo not going to start on a rant on program transformations and the relevance to the real world. Let's just agree that real world compilers are pragmatic and that you can write tractable programs if you want (like choosing a functional programming style).

On Monday, 27 January 2014 at 21:12:30 UTC, deadalnix wrote:
> On Monday, 27 January 2014 at 18:30:43 UTC, Pierre Talbot wrote:
>> On Monday, 27 January 2014 at 04:07:04 UTC, Andrei Alexandrescu wrote:
>>> On 1/26/14 3:22 AM, Pierre Talbot wrote:
>>>> Hi,
>>>>
>>>> I was wondering why CTFE is context sensitive, why don't we check
>>>> every expressions and run the CTFE if it applies?
>>>
>>> Compilation would get awfully slow (and sometimes won't terminate).
>>>
>>> Andrei
>>
>> So it is theoretically possible? I mean if the compilation doesn't terminate, the execution won't either for at least one program input, so we can detect an infinite loop at compile-time. Moreover, isn't the same problem with context-sensitive CTFE?
>>
>> Pierre
>
> lolwut ? How do you make the difference between a program that won't terminate ever and one that will terminate eventually (say, in several years) ?

With resource bounds (such as memory, time or number of operations) but from what others said I understand now that it's a bad idea. Moreover, I just thought there were programs designed to not terminate (for example server).
Thanks to all.