Why CTFE is context-sensitive?

[Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang at gmail.com>]

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.