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