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
next sibling 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
next 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 next 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 parent 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
prev sibling next sibling parent "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
prev sibling 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 next sibling parent "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
prev sibling next sibling parent "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
prev sibling next sibling parent =?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
prev sibling next sibling parent "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
prev sibling next sibling 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 next sibling parent "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
prev sibling next sibling parent =?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
prev sibling next sibling parent "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
prev sibling next sibling parent "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
prev sibling next sibling 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 "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