Why CTFE is context-sensitive?

[Simen Kjærås]

On 28.01.2014 10:42, "Ola Fosheim Grøstad" 
<ola.fosheim.grostad+dlang at 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