07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:19:58 -!- kosmikus|away has changed nick to kosmikus. 08:38:03 -!- cmeme has quit (calvino.freenode.net irc.freenode.net). 08:38:03 -!- kosmikus has quit (calvino.freenode.net irc.freenode.net). 08:40:23 -!- kosmikus has joined. 10:38:59 -!- trman has joined. 10:41:02 -!- trman has quit ("Leaving"). 15:28:57 -!- cmeme has joined. 17:37:44 -!- calamari_ has joined. 17:37:47 hi 17:38:00 hi 20:15:19 know what's cool? 20:15:31 ice! 20:15:34 yes. 20:15:59 also, the non-turing-completeness of systems with finite memory makes it possible to prove whether a program halts in that system. 20:16:12 That's cool? 20:16:30 it's cool because at least Brainfuck does prescribe limited memory. 20:17:06 Taaus: I can play the C# minor fugue from WTC book I! 20:17:16 Okay, so have you made a program that tests/proves halting/non-halting for an arbitrary BF program? 20:17:28 no 20:17:33 a naive one would be trivial to implement 20:17:48 Ah, c# is a lot of fun. How many voices is it? 20:17:51 it would also require a fucking big computer 20:17:52 five 20:17:59 Ah, that's what I thought. 20:18:02 five voices and three subjects 20:18:14 s/subjects/themes 20:18:26 It's pretty unique in that respect. Like the two-voice e-minor fugue. 20:18:29 is that really on-topic? I didn't think c# was an especially esoteric language. 20:18:30 i can't say i understand it, but at least i can play it. 20:18:44 Taaus: the Bb-minor one is also five-part 20:18:49 i can play it as well 20:18:55 it only has one subject though. 20:19:23 (and there's another triple fugue in book II) 20:19:43 I know c# isn't the only 5-part fugue, but the vast majority in WTC I+II are 3- and 4-parters :) 20:19:56 WTC II is boring. It only has 3 and 4. 20:20:19 C# minor is probably the most complex one in the entire WTC, structurally. 20:21:26 for brainfuck 20:21:41 you could just execute the program 20:21:51 keeping track of all memory states that occured. 20:22:04 if a memory states repeats, you're done - the program won't halt. 20:22:08 *state 20:22:24 since there's only a finite number of memory states, you'll be done eventually. 20:22:26 Well... In theory, it's trivial... :P 20:22:42 Just 64000^256. Lovely. 20:22:52 plus the pointer position. 20:22:52 64000? not really 20:23:02 didn't mueller specify 4000? 20:23:15 or something like that. 20:23:16 64k is pretty popular though. 20:23:22 He did? My bad. 20:23:23 but yeah, it's still a big number. 20:23:40 bfvga is a funny toy. too bad it's awfully hard to do anything pretty with it. 20:24:07 still it would be interesting to try to prove haltingness of at least some programs that halt. 20:24:17 then you can compile them into a singe statement. 20:25:19 (naturally this doesn't apply to programs which use ,) 20:26:06 it's a reasonable, if not always valid, assumption for a compiler to make, that a program containing a ',' will not halt. 20:26:35 Alternatively, you could figure out how long (runtime-wise) the longest running halting program runs, then run all programs for that long. 20:26:52 Ah, yes... "," is bothersome. 20:27:08 the longest running halting program... 20:27:12 it would have to visit all states 20:27:41 fizzie needs to depart for an evening walk out there. is away. 20:28:25 Hehe, true... So actually, you can just run the program for memory * cell_size^memory, and see if it's halted. 20:28:33 yes. 20:28:55 how long would that take? :) 20:29:01 then you don't need a computer with heaps of memory, just lots of patienec. 20:29:10 yeah. It's a better approach. 20:29:14 lament: Constant time! :D 20:30:27 does this "halt"? +[++] 20:30:29 it's just 1e768 different states for 4000-byte memory 20:30:57 calamari_: depends on the semantics of our machine. Those would of course have to be agreed upon. 20:31:03 is brainf*ck's cell-size defined? 20:31:43 It's usually taken to be either 8 bit, or infinite. Of course, 'infinite' won't work here. 20:31:43 I could make a version that alternates between say, 1 and 2 that still wouldn't exit 20:32:04 calamari_: yes, but then it would be immediately seen that it repeats the memory state 20:32:12 oic 20:32:55 even the naive halting proofer will prove that in reasonable time 20:33:00 (i.e. almost instantly) 20:36:02 fizzie: where is the bfvga that you spoke of earlier? 20:40:00 i have once written a graphics extension for befunge. 20:40:08 but never wrote a single program for it :( 20:43:57 What techniques could be used to prove the haltingness of at least some programs that halt? 20:44:00 I was able to use ansi to extend bf a little, but that still managed to be standard bf 20:44:05 Clearly a program without loops will halt. 20:44:40 halt = exit? 20:44:44 Yes. 20:44:45 Yes. 20:45:05 And a program that only has balanced loops will probably halt as well. 20:46:07 er. 20:46:14 balanced loops? 20:46:15 no. 20:46:19 not just balanced. 20:46:33 i'm talking about loops that move numbers from one cell to another. 20:47:06 the loop has to decrement the starting cell and always end on the same cell it started on. 20:47:12 e.g. [->+>+<<] 20:47:32 [->+<+] clearly won't terminate. 20:47:40 which sucks. 20:48:44 lament: *[ ... *-] or *[- ... *] 20:48:52 (* = same memory cell) 20:49:06 not counting nested loops at the ... of course 20:49:09 calamari_: [->+<+] is a [- ...] 20:49:26 so is [->+] 20:49:33 lament: yes, specific case of it 20:49:44 calamari_: those loops don't halt. 20:50:14 lament: wait a sec, I thought you repeated yourself 20:50:32 lament: those don't fit the description of * = same memory cell 20:50:46 calamari_: [->+<+] does. 20:51:18 Uh, wrapping notwithstanding, can a [...+] loop terminate? Surely the cell is always non-zero due to the "+". 20:51:24 hmm.. good point.. however -+ really isn't - 20:51:40 Taaus: correct. 20:51:53 are negative numbers allowed? 20:52:26 Well... That depends on what semantics we choose :) 20:52:30 so [->+<+] is [>+<] and that doesn't fitthe pattern 20:52:31 deltab: not usually. 20:52:57 My favourite semantics is 20:53:05 8-bit unsigned cells 20:53:12 infinite memory space 20:53:20 going left of the origin crashes 20:53:32 overflow and underflow crashes 20:54:01 lament: if you have infinit memory space what do you do about something like +[>+] ? 20:54:40 calamari_: what do you mean "what do you do"? 20:54:51 calamari_: as taaus said, it's a loop that ends with a +. 20:55:02 it doesn't halt. 20:55:40 lament: what about [-]- 20:55:54 never mind 20:56:33 You don't have to subscribe to my favourite semantics, though. 20:56:43 Most people prefer to have wraparound instead of overflow/underflow 20:56:48 or so it seems. 20:56:49 actually, ending with a plus doesn't matter, it's the combined effect of the cell, right? .. for example +[>++-] 20:56:55 Unfortunately, [->++-] matches [...-] 20:57:01 Oh, heh. :) 20:57:03 GMTA. 20:57:19 that's because matching [...-] is silly. 20:57:35 lament: right, I just wanted to emphasize that :) 20:57:43 Any sequence of <>+- can be converted to a "normal form" 20:57:55 which is trivial to do and should be done prior to examining the program. 20:59:42 (existing optimizing compilers do it) 20:59:49 (hopefully) 20:59:55 * lament checks 21:01:20 no, they don't :( 21:01:38 well, they do to an extent 21:01:43 +[[>]<] 21:02:01 Ah, nested loops. We haven't even begun to worry about those yet! 21:02:10 nor about unbalanced loops 21:03:16 ok 21:03:34 the compiler bfc by Panu does it.- 21:03:40 sort of. 21:03:53 At which point do we realise the futility of this endeavour? 21:04:22 taaus: when we read that it's impossible to solve the halting problem? 21:04:48 bfc optimizes this [+>-<-] to this: 21:05:01 for(;a[p];p+=0){a[p+0]+=0;a[p+1]+=-1;} 21:05:10 Well... It depends on the semantics... We proved earlier that Urban's original BF is halting-decidable. 21:05:31 taaus: that was with a finite memory space 21:05:37 Yes. 21:05:46 calamari_: obviously you can't do it with infinite memory space. 21:05:49 Like I said, semantics :) 21:06:04 lament: " infinite memory space" 21:06:15 calamari_: that's just my favourite semantics. 21:06:33 What we're looking at now is better heuristics to check for halting-ness. Even though complete decidability is impossible :) 21:06:43 with finite space +[>+] this eventually exits 21:06:56 (assuming cell wraparound) 21:07:20 yes, and the halting prover would happily prove it. 21:07:32 how about better ways to optimize bf code -> bf code 21:07:54 that's a lot harder than optimizing compilation to c 21:08:48 but the aforementioned "converting -+<> sequences to their normal form" would be the first step. 21:08:59 right, but thats simple stuff 21:09:32 i've never heard of optimizing a language in that same language. 21:09:35 Has it ever been doen? 21:09:39 *done 21:09:53 automatic refactoring or something?.. 21:14:44 perhaps going to a higher level language and back again to bf? 21:15:06 Converting -+<> sequences to normal form (preferrably to shortest form) isn't trivial either 21:15:10 or so it seems 21:15:18 try doing it in BF: P 21:15:34 but, that doesn't seem very promising either, because higher level languages have other baggage problems 21:16:28 lament: aren't you talking about figuring out that +--++ is the same as + ? 21:16:48 that's part of it. 21:19:46 using the higher level form above, I get [+>-<-] => [>-<].. however if there were nested loops, that might not work right 21:20:48 nested loops clearly aren't parts of -+<> sequences. 21:20:52 Lunch. 22:20:59 hrm. 22:21:12 finding the 'normal form' isn't all that trivial. 22:21:21 it's annoyingly annoying 22:24:44 took me 53 lines of Python code! 22:24:50 >>> normal('+>+<-') 22:24:51 '>+<' 22:24:53 woohoo 22:26:13 what does it give for >>+>>++<-<-<-<- 22:26:42 '>>>>++<-<<-<-' 22:27:26 let's try >>+>>++<-<-<-<->>>> 22:27:36 '->->>->++' :) 22:28:10 it returns the provably shortest path, although i'm certainly not going to prove that. 22:28:11 cool 22:33:41 bfvga is a proggie which maps the vga 320x200x256 mode display memory as a 64k brainf*ck array. I think it was in scene.org somewhere. 22:34:47 http://www.pouet.net/prod.php?which=5060 I think. 22:48:31 i don't like the comments in that thread. 22:49:04 well, they are sceners. 22:49:09 not esoteric-language-people. 22:51:55 that makes them wrong! 22:51:59 my program doesn't quite work :( 22:52:41 but, i applied it to the BF mandelbrot generator and it didn't change anything at all. 23:01:34 re bfvga, I tried the analogous befvga, the befunge version of that, with a 320x200 playfield and the playfield positions mapped to the screen. 23:01:46 it wasn't any more fun than bfvga though. 23:06:00 oh actually 23:06:23 my program does make the mandelbrot generator 30 characters shorter :) 23:06:38 11421 vs. 11451 23:08:08 it also does a lot of funky rearrangement of questionable quality 23:08:14 for example, it converts this: 23:08:20 [->++>>>+++++>++>+<<<<<<] 23:08:22 into this: 23:08:28 [>>>>>>+<++<+++++<<<++<-] 23:08:48 maybe you should make it not apply the modifications if they are not shorter. 23:09:42 also this: 23:09:49 [->+<] 23:09:50 into this: 23:09:53 [>+<-] 23:10:17 maybe. 23:10:58 but then the original idea was to convert everything to a "normal form" that would make it easier to process by other tools. 23:11:40 but that task is probably not compatible with that of always writing the _shortest_ version. 23:20:29 -!- calamari_ has quit (Read error: 104 (Connection reset by peer)).