www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Why CTFE is context-sensitive?

reply "Pierre Talbot" <ptalbot**mustberemoved** hyc.**thisto**io> writes:
Hi,

I was wondering why CTFE is context sensitive, why don't we check
every expressions and run the CTFE if it applies?

PS: I'm sorry for the double post, I just noticed that D.learn 
wasn't the right place to ask this question. It'd be great if 
someone could delete this misplaced post. Thanks.
Jan 26 2014
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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?

 PS: I'm sorry for the double post, I just noticed that D.learn wasn't
 the right place to ask this question. It'd be great if someone could
 delete this misplaced post. Thanks.


Compilation would get awfully slow (and sometimes won't terminate).

Andrei
Jan 26 2014
parent reply "Pierre Talbot" <ptalbot**mustberemoved** hyc.**thisto**io> writes:
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
Jan 27 2014
next sibling parent "Xinok" <xinok live.com> writes:
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


Just because code runs for a long time doesn't mean that it will 
run forever. This is known as the Halting problem [1]. We could 
have configurable switches to halt CTFE if it runs for more than 
N seconds or allocates more than N MiB.

However, this still doesn't take away from the point that it 
would make compilation awfully slow with presumably little 
benefit. There are further issues in that CTFE isn't exactly 
stable yet (I've had it produce incorrect results in a few 
cases), so relying on it to produce correct, optimized code is a 
bad idea.

I would be in favor of some "lite-CTFE" for the sake of 
optimization. Simply halting if the interpreter encounters a loop 
or function recursion should make it pretty snappy. But I think 
many compilers / optimizers already do this to some extent.

[1] https://en.wikipedia.org/wiki/Halting_problem
Jan 27 2014
prev sibling parent reply "deadalnix" <deadalnix gmail.com> writes:
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) ?
Jan 27 2014
next sibling parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Monday, 27 January 2014 at 21:12:30 UTC, deadalnix wrote:

 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) ?


1. The halting problem does not apply to finite resources. The 
proof is trivial: just record all state. You are in an infinite 
loop when you revisit a state your program already has been in. 
The halting problem only applies if you have non-finite storage.

2. You can set a timeout and use heurististics (and profiling) 
for what computations you want to try to precompute. Perfectly 
doable.
Jan 27 2014
next sibling parent reply =?UTF-8?B?U2ltZW4gS2rDpnLDpXM=?= <simen.kjaras gmail.com> writes:
On 2014-01-27 21:37, "Ola Fosheim Grøstad" 
<ola.fosheim.grostad+dlang gmail.com>" puremagic.com wrote:

 On Monday, 27 January 2014 at 21:12:30 UTC, deadalnix wrote:

 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) ?


 1. The halting problem does not apply to finite resources. The proof is
 trivial: just record all state. You are in an infinite loop when you
 revisit a state your program already has been in. The halting problem
 only applies if you have non-finite storage.


My computer has 16GB of RAM. You try keeping track of all the possible 
states.

Now, I know DMD cannot use 16GB of RAM, so let's limit ourselves to 3GB 
or so. We then make a bit array for all permutations of 3*2^30 bits. 
That would take 2^(3*2^30) bits. All the hard drives in the world may be 
on the order of 10 zettabytes. When I ask Mathematica what multiple of 
this number we need to keep track of all the possible permutations of 
3GB, it gives up and calls me an asshole. Some jotting on a piece of 
paper indicates 2^3,221,225,399 is fairly close. Even if Kryder's Law[0] 
continues to hold, it will take 2.5 billion years before the entire 
world has enough storage capacity to do what you suggest, and even then, 
searching all that data will *still* be prohibitively expensive.

In simpler terms: Just because something is not theoretically 
impossible, it may still be so ridiculously computationally expensive it 
might as well be impossible. Stop making the argument that the halting 
problem does not apply to regular computers. It's technically true, yes. 
It also does not matter, for the reason described above.

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


[0]: http://en.wikipedia.org/wiki/Mark_Kryder

--
   Simen
Jan 27 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
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
Jan 28 2014
parent reply =?UTF-8?B?U2ltZW4gS2rDpnLDpXM=?= <simen.kjaras gmail.com> writes:
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
Jan 28 2014
next sibling parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
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.
Jan 28 2014
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
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.)
Jan 28 2014
parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
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
Jan 28 2014
parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
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).
Jan 28 2014
prev sibling parent Timon Gehr <timon.gehr gmx.ch> writes:
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.)
Jan 28 2014
prev sibling next sibling parent reply "Tofu Ninja" <emmons0 purdue.edu> writes:
On Monday, 27 January 2014 at 21:37:58 UTC, Ola Fosheim Grøstad 
wrote:

 On Monday, 27 January 2014 at 21:12:30 UTC, deadalnix wrote:

 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) ?


 1. The halting problem does not apply to finite resources. The 
 proof is trivial: just record all state. You are in an infinite 
 loop when you revisit a state your program already has been in. 
 The halting problem only applies if you have non-finite storage.

 2. You can set a timeout and use heurististics (and profiling) 
 for what computations you want to try to precompute. Perfectly 
 doable.


I don't think that is quite right, you can have an infinite loop 
without there being any repeated states. Simple example is

for( i = 1; i>0 ; i++) {...}

This will run forever while still never repeating state, assuming 
that i never wraps around. After all you said that we don't have 
finite resources which is the same as saying we have unlimited 
resources.
Jan 27 2014
parent =?UTF-8?B?U2ltZW4gS2rDpnLDpXM=?= <simen.kjaras gmail.com> writes:
On 2014-01-27 23:18, Tofu Ninja wrote:

 On Monday, 27 January 2014 at 21:37:58 UTC, Ola Fosheim Grøstad wrote:

 On Monday, 27 January 2014 at 21:12:30 UTC, deadalnix wrote:

 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) ?


 1. The halting problem does not apply to finite resources. The proof
 is trivial: just record all state. You are in an infinite loop when
 you revisit a state your program already has been in. The halting
 problem only applies if you have non-finite storage.

 2. You can set a timeout and use heurististics (and profiling) for
 what computations you want to try to precompute. Perfectly doable.


 I don't think that is quite right, you can have an infinite loop without
 there being any repeated states. Simple example is

 for( i = 1; i>0 ; i++) {...}

 This will run forever while still never repeating state, assuming that i
 never wraps around. After all you said that we don't have finite
 resources which is the same as saying we have unlimited resources.


I assume i is a bigint then, and that you have infinite memory for it. 
Otherwise, you'll have repeated state when i overflows.

--
   Simen
Jan 27 2014
prev sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 1/27/14 1:37 PM, "Ola Fosheim Grøstad" 
<ola.fosheim.grostad+dlang gmail.com>" wrote:

 On Monday, 27 January 2014 at 21:12:30 UTC, deadalnix wrote:

 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) ?


 1. The halting problem does not apply to finite resources. The proof is
 trivial: just record all state. You are in an infinite loop when you
 revisit a state your program already has been in. The halting problem
 only applies if you have non-finite storage.


Somebody please give him a T-shirt :o).

Andrei
Jan 27 2014
prev sibling parent "Pierre Talbot" <ptalbot**mustberemoved** hyc.**thistoo**io> writes:
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.
Jan 28 2014