00:00:03 oerjan: hmm, I think you sent me a message earlier... I may have intended to answer 00:00:41 maybe it was not important? 00:00:55 kmc: what if you want rust not to do it 00:01:04 imo doubleplusunsafe { ... } 00:02:06 `pastelogs oerjan> @.* olsner 00:02:41 danger(10000) { ... } 00:02:54 http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.32727 00:03:23 do badness(10000) { ... } 00:04:13 oerjan: ah! then I would guess "yes" 00:04:20 pwned boxes 00:04:46 though I'm not sure how much asbestos contamination does to fireproof a spider 00:05:02 olsner: we are all doomed hth 00:07:36 oerjan: hopefully only wales is doomed hth 00:08:11 hm well as long as they cannot swim 00:08:34 p. sure wales can swim 00:10:29 it's hard to argue with a pun based on a misspelling. 00:15:59 but if they wash up on the beach they're property of the queen 00:16:36 -!- Sgeo has joined. 00:16:43 hi Sgeo 00:20:07 -!- Sprocklem has joined. 00:21:11 -!- mroman_ has quit (Read error: Operation timed out). 00:21:25 -!- mroman_ has joined. 00:21:26 kmc: so that's how england got wales in the first place? 00:21:40 -!- ter2 has joined. 00:21:45 -!- tertu has quit (Ping timeout: 265 seconds). 00:22:02 yep 00:22:15 thx it all makes sense now 00:36:24 -!- muskrat has quit (Ping timeout: 246 seconds). 00:42:58 -!- Phantom_Hoover has joined. 00:43:01 -!- Zuu has joined. 00:55:28 -!- Zuu_ has joined. 00:56:42 -!- Zuu_ has quit (Remote host closed the connection). 00:57:54 ruddy: hutenosa 00:57:54 hutenosa 00:58:32 hi ruddy 00:58:32 hi hi 00:58:38 ruddy: are you enjoying finnish independence day 00:58:39 because i'm `thanks independence day also it's independence day 00:58:46 ruddy: have you declared yourself independent from finland 00:58:47 i think that is true independent of number of cells 00:58:55 ruddy: escargot 00:58:55 No clue what you mean. What do you think, fungot? 00:59:02 -!- Zuu_ has joined. 01:01:19 -!- drlemon has quit (Read error: Connection reset by peer). 01:02:50 -!- drlemon has joined. 01:06:29 -!- MindlessDrone has quit (Quit: MindlessDrone). 01:07:07 `thanks independence day also it's independence day 01:07:09 Thanks, independence day also it's independence day. Thindependence day also it's independence day. 01:16:33 -!- Halite has quit (Ping timeout: 250 seconds). 01:19:46 why is there no dramatic reading of the call of cthulhu for beginning readers on the internet 01:21:19 -!- conehead has joined. 01:21:56 coppro: they keep mysteriously disappearing together with the readers 01:22:42 oerjan: but I can find the *regular* version fine 01:22:46 I just want the seussized one 01:24:11 coppro: just read through the iwc christmas comics hth http://www.irregularwebcomic.net/archive.html 01:24:46 (Dec 24th) 01:25:18 One cthulhu, two cthulhu, red cthulhu, blue cthulhu. 01:26:12 The reason must be that dramatic readers who like to post stuff on internet don't like that book or do not know how to read it for some reason. Either that or they are hiding it. 01:27:04 happy independence day, nooodl 01:27:28 sinterklaas "basically that" 01:27:57 sinterklaas = basically cthulhu 01:34:02 `? science 01:34:04 Semi-automatic text generation. 01:34:15 oh come on, that doesn't even backronym. 01:34:31 I notice that too. 01:35:05 `? zzo38 01:35:07 zzo38 is not actually the next version of fungot, much as it may seem. 01:35:11 `? fungot 01:35:12 fungot cannot be stopped by that sword alone. 01:35:16 `? ruddy 01:35:17 `? shachaf `? shachaf 01:35:18 ruddy? ¯\(°_o)/¯ 01:35:18 HackEgo? ¯\(°_o)/¯ 01:35:25 hi ruddy 01:35:26 hi hi 01:35:33 ruddy: you show that bot! 01:35:34 eille! no violence against my peaceful bot! 01:35:40 ruddy hi ruddy 01:35:41 hi hi 01:35:46 loop, ruddy, loop 01:35:47 and in 01:35:47 ruddy: today is the day i am going to sleep 01:35:51 got to 01:35:59 ruddy: you gotta do what you gotta do 01:36:01 gotta get 01:36:54 `run echo "HackEgo? ¯\(°_o)/¯" >wisdom/ruddy 01:36:55 `run echo 01:36:58 No output. 01:39:17 -!- Zuu_ has quit (Remote host closed the connection). 01:41:25 * int-e blames lambdabot <-- ok how did lambdabot get you here 01:42:06 -!- Zuu_ has joined. 01:43:25 -!- Zuu_ has quit (Remote host closed the connection). 01:43:38 -!- Zuu_ has joined. 01:44:18 oerjan: I looked at the list of channels that it joins automatically 01:44:39 -!- yorick_ has joined. 01:44:49 -!- yorick has quit (Ping timeout: 246 seconds). 01:44:51 fiendish! 01:45:15 -!- Zuu_ has quit (Remote host closed the connection). 01:46:08 -!- Zuu_ has joined. 01:48:16 -!- Zuu_ has quit (Remote host closed the connection). 01:48:36 -!- Zuu_ has joined. 01:49:02 -!- Zuu_ has quit (Remote host closed the connection). 01:49:27 -!- Zuu_ has joined. 01:50:08 -!- Zuu_ has quit (Remote host closed the connection). 01:50:26 -!- Zuu_ has joined. 01:51:23 Zuu_: fix your connection thx 01:51:50 -!- elliott_ has changed nick to elliott. 01:53:18 oerjan: tis fine, i was just configuring something :/ 01:53:29 good, good 01:53:47 is there some canonical algorithm for assigning binary codes to each node of a state diagram 01:54:16 Bike: it's called "counting" hth 01:54:51 i mean, that minimizes the logic 01:55:28 wat 01:55:57 like in a circuit implementing the state diagram. 01:56:10 minimizing hamming distance between connected nodes for instance 01:56:14 there's an algorithm for minimizing the number of states iirc 01:56:22 -!- Zuu_ has quit (Remote host closed the connection). 01:56:24 not what i mean 01:57:06 -!- Zuu has quit (Read error: Connection reset by peer). 01:57:25 sounds messy anyway. 01:57:53 enough that i expect the answer is "no" 01:58:30 well there are multiple constraints you could optimize for, like size of the state 01:59:01 -!- Zuu has joined. 01:59:01 yes, but it sounds like something NP-complete or worse. 01:59:29 so whatever algorithm you find won't be "canonical". 01:59:43 size of state is easy, but I expect that often you'll want to use more bits than are strictly required, to encode some features of states. 01:59:47 unless it happens to be for surprising reasons. 01:59:58 --> it's a hard problem. 02:04:13 -!- yorick_ has quit (Remote host closed the connection). 02:04:13 i'm wondering this because my homework gave constraining hamming distance to one as a rule of thumb but also said it was usually impossible 02:04:16 ~engineering~ i guess 02:04:16 (a nice example of such features comes up when your automaton is the result of a powerset construction; it may be better to implement the nondeterministic automaton and use one bit per original state) 02:04:39 What's a powerset construction. 02:05:03 https://en.wikipedia.org/wiki/Powerset_construction 02:19:53 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 02:21:53 In a 6502 code, if I have the accumulator being zero, what is an efficient way to make the zero flag cleared if some value in the zero-page is zero, and set if it is nonzero? 02:26:04 what instructions alter the zero flag again 02:27:21 Loads, transfers, arithmetic. 02:28:27 ADC, AND, ASL, BIT, CMP, CPX, CPY, DEC, DEX, DEY, EOR, INC, INX, INY, LDA, LDX, LDY, LSR, ORA, PLP, ROL, ROR, SBC, TAX, TAY, TSX, TXA, TXS, TYA. 02:29:00 loads huh 02:29:30 obviously LDA whatever gives the opposite flag setting of what you want 02:29:47 oerjan: Yes I can see that 02:30:36 hm, no xor 02:30:42 Bike: EOR 02:31:09 has everyone used the 6502... 02:31:24 anyway i have no idea. 02:31:52 way back. although the manual for the assembly was missing instructions... 02:32:10 hm what's PLP 02:32:17 I wonder if just pushing the flags onto the stack and then testing the zero flag with BIT or AND, would be best way. 02:32:25 oerjan: The opposite of PHP. 02:32:27 (HTH) 02:32:31 oerjan: PLP is pop flags from stack 02:32:32 fizzie: THX 02:32:46 hm right 02:35:24 hey zzo38, i'm planning on making some CPUs with my FPGA. do you have any fun ISAs to recommend 02:35:54 Bike: imo make mmix 02:36:08 i guess that would make sense 02:36:32 though i don't remember anything about it other than that it drops the crazy decimal stuff and has a zillion registers. 02:39:05 -!- doesthiswork has joined. 02:39:44 Bike: Yes, MMIX is one possibility; GCC supports it, even. 02:40:14 i'm not actually sure how i should go about getting code onto the thing, there's no serial port. guess i'll have to get another cable and figure out uart 02:41:12 You can also try 6502 if you want to program it in assembly language (and if it is the variant used in the Famicom, then there is no decimal arithmetic either) 02:42:07 any more esoteric ideas? 02:42:23 imo make your own isa 02:42:28 hi 02:42:29 i was thinking of trying imlementing the processor from 'lambda the ultimate opcode'. no alu 02:42:32 himc 02:55:37 apparently there was an asynchronous RISC called "AMULET", i'm thinking of finding some specs 02:55:49 -!- doesthiswork has quit (Quit: Leaving.). 03:30:09 I guess to formalize a statement like "C is Turing complete" you would talk about a family of languages C_i where sizeof(void *) = i, and require that the languages have a uniform description 03:30:13 so I think that doesn't work 03:30:39 because any given TM (that you would try to implement in C_i for some i) can take arbitrarily large inputs and use arbitrarily much tape, even a vastly more than superexponential function of the input length 03:31:26 intptr_t rather puts a damper on things, eh 03:31:59 -!- tertu3 has joined. 03:32:10 What if a "char" cell can contain an arbitrary integer, and it is C89 rather than C99? 03:32:28 can you have a C where malloc never fails and just keeps giving you new pointers 03:33:30 zzo38: what's the relevant difference between C89 and C99? 03:34:14 kmc: I think C99 defines a lot of stuff that tells you how many bits everything is, isn't it? 03:34:45 c89 doesn't have char_bit? 03:35:26 -!- ter2 has quit (Ping timeout: 240 seconds). 03:56:27 -!- pikhq has quit (Ping timeout: 260 seconds). 03:56:35 -!- pikhq has joined. 04:09:33 -!- pikhq has quit (Ping timeout: 252 seconds). 04:09:43 -!- pikhq has joined. 04:14:50 -!- pikhq has quit (Ping timeout: 245 seconds). 04:15:53 -!- pikhq has joined. 04:27:33 -!- Sorella has quit (Remote host closed the connection). 04:46:02 Is there an editor for 6502 assembly language files (even if the file includes macros and other stuff) that will also display the generated hex codes and the bytes and cycles of each line, and the bytes and cycles of any highlighted block, and the addresses, etc? 04:49:56 -!- Slereah_ has quit (Read error: Connection reset by peer). 04:50:13 -!- Slereah has joined. 04:58:53 -!- nooodl_ has joined. 05:01:51 -!- nooodl has quit (Ping timeout: 240 seconds). 05:08:47 http://slashdot.org/story/13/11/06/1323223/mozilla-backtracks-on-third-party-cookie-blocking 05:08:54 Said as though third-party cookies are evil 05:08:56 *sigh* 05:09:17 because they are? 05:09:22 They can be 05:11:13 i think i would be happier if i hung out in a channel where when people said stuff like that they were talking about politics or such 05:11:39 I have legitimate use cases for third-party cookies :/ 05:11:51 (non-advertising uses, I mean) 05:12:01 i have legitimate use cases for mah diiiiick 05:15:19 http://kingjamesprogramming.tumblr.com/ 05:17:19 -!- oerjan has quit (Quit: leaving). 05:33:12 -!- pikhq has quit (Ping timeout: 246 seconds). 05:35:08 -!- pikhq has joined. 06:04:34 Bike: ^5 06:12:43 Did you see what Famicom Z-machine programming I have made up so far? http://wiki.nesdev.com/w/index.php/User:Zzo38/Famicom_Z-machine 06:13:23 -!- Sgeo_ has joined. 06:14:15 kmc: i don't know this notation. does it mean that you as well have legitimate use cases for mah dick 06:15:10 it means "high five" 06:15:15 so, kinda? 06:16:15 -!- Sgeo has quit (Ping timeout: 246 seconds). 06:16:26 cool 06:17:07 -!- Sgeo has joined. 06:17:34 diiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiickdiiiiick 06:17:38 -!- Sgeo_ has quit (Ping timeout: 246 seconds). 06:18:18 zzo38: why did you choose famicom as the machine you want to develop this for 06:19:04 nice kmc 06:23:04 -!- SingingBoyo has joined. 06:23:09 thx 06:23:40 quintopia: It is one computer that doesn't have Z-machine interpreter on it, is one reason. 06:24:01 zzo38: you think every computer should be able to interpret Z-machine? 06:25:40 @tell ais523 it looks like James Parsons has decided not to make a FLARP! language, you should delete the page. 06:25:40 Consider it noted. 06:26:54 quintopia: It may be intended. Infocom didn't do it since Famicom is by Nintendo of Japanese, but now other people can make it too. Also, to practice to write such programs. 06:27:42 zzo38: what other kinds of programs like that do you plan on writing in the future 06:28:50 quintopia: I am not exactly sure by now. 06:29:06 Did you find any mistakes in this program or any other comment/questions? 06:35:59 i don't have the assembler or the emulator or test programs. in short, i am a poor alpha tester. sorry. 06:36:41 It isn't complete enough for testing the program; I mean if you noticed anything wrong with the program just by looking at it. 06:38:05 nope! i 06:38:12 i'm not smart enough to do that either 06:40:10 Do you know anything about Z-machine programming, Famicom programming, and/or 6502 programming? 06:40:28 NOPE 06:40:47 you've found yourself a very esoteric niche 06:41:08 That wiki contains a lot of information about programming NES and Famicom. 06:41:31 (and other related systems, such as Vs.Unisystem) 06:44:21 One thing a bit unusual about this Z-machine interpreter is that several things are decided at compile-time; this may make the program more efficient in some ways. 06:49:48 The CPU chip used in that computer is the 2A03, which contains two cores which is the CPU core and APU core. The CPU core is a 6502 but with BCD arithmetic disabled (the logic is still there, it is just disconnected from the rest of the circuit). the APU core is used for audio (two square waves, one triangle wave, one noise, one DPCM) but also I/O ports and a DMA transfer. 06:50:11 how is the apu controlled 06:50:38 The APU is controlled by memory-mapped registers $4000-$4020. 06:53:03 The address of the DMA transfer is hard-coded and cannot be changed; you can change the source address to any 256-byte boundary, and when activated it reads the data from all 256 addresses in that page and writes the results all to a single address (not to 256 separate addresses). 06:58:29 why disable BCD 06:58:47 -!- tertu3 has changed nick to tertu. 06:59:24 don't most z-machine games expect a somewhat wider screen than the famicom has 07:01:05 tertu: Yes, but I do with what we have. (Also, this program is only version 1 to 3 Z-machine) 07:02:03 http://en.wikipedia.org/wiki/File:Z-machine480.jpg 07:02:22 iirc wasn't the bcd part of the chip still on it, just with the wires cut so you couldn't access it 07:02:34 Bike: Yes, it is like that. 07:03:23 why tho 07:04:11 -!- L8D has quit (Ping timeout: 252 seconds). 07:04:49 Due to overscan, the visible area is only 30x26, but if no words are longer than 30 then it would fit. However you probably will need to scroll the screen a lot. 07:07:27 Also, for simplicity, everything is displayed in uppercase (which is OK in version 1-3 only, as long as it can be distinguished internally in all cases that matter) 07:09:50 -!- pikhq has quit (Ping timeout: 240 seconds). 07:10:57 kmc: Apparently due to patents on the 6502 CPU design. 07:11:36 -!- pikhq has joined. 07:13:24 In addition, it doesn't implement the status line (there is a bit in the header to indicate this), and the SPLIT and SCREEN operations are not supported (there is also the bit in the header to indicate this too). 07:16:48 -!- nooodl_ has quit (Ping timeout: 246 seconds). 07:38:30 -!- ^v has quit (Remote host closed the connection). 07:39:29 -!- conehead has quit (Quit: Computer has gone to sleep.). 08:01:28 -!- Taneb has joined. 08:03:50 -!- upgrayeddd has joined. 08:35:43 zzo38: heh 09:54:30 -!- zzo38 has quit (Remote host closed the connection). 10:19:15 -!- MindlessDrone has joined. 10:20:43 -!- Sprocklem has quit (Ping timeout: 246 seconds). 10:49:27 -!- Sorella has joined. 10:50:00 -!- Sorella has quit (Changing host). 10:50:00 -!- Sorella has joined. 11:05:04 -!- SingingBoyo has quit (Ping timeout: 250 seconds). 11:14:38 -!- carado has joined. 11:44:06 -!- Phantom_Hoover has joined. 12:11:47 Huh, there's really no NES Z-machine interpreter? That is quite surprising. 12:20:46 -!- int-e has quit (Ping timeout: 246 seconds). 12:21:43 -!- int-e has joined. 12:30:11 -!- nooodl has joined. 12:35:02 surely there is 12:35:05 somewhere 12:40:36 -!- ais523 has joined. 12:43:09 x - y = 12:43:14 er, oops 13:16:15 -!- carado has quit (Ping timeout: 252 seconds). 13:20:42 -!- nooodl has quit (Quit: Ik ga weg). 13:21:03 -!- nooodl has joined. 14:02:56 -!- Taneb has quit (Quit: Leaving). 14:05:25 -!- L8D has joined. 14:09:26 -!- pikhq has quit (Ping timeout: 240 seconds). 14:10:05 -!- pikhq has joined. 14:24:24 -!- MindlessDrone has quit (Ping timeout: 250 seconds). 14:39:43 -!- MindlessDrone has joined. 15:42:43 anyone here have advice on how to read a line from a file without using stdio? 15:43:49 like, I can think of a few ways, was wondering what the best way is 15:43:58 byte-at-a-time is pretty slow, I'd hope to avoid that 15:45:15 -!- pikhq has quit (Ping timeout: 245 seconds). 15:45:29 is it ok to read more than the first line? can you seek? 15:45:47 -!- pikhq has joined. 15:45:58 olsner: I can seek, and I can over-read 15:46:14 also I have an advisory read lock on the file and everything that touches the file respects advisory locks 15:46:21 so I can guarantee it won't change while I'm reading 15:46:24 hmm, how about mmap and strchr/memchr? 15:46:39 huh, I hadn't thought of that at all 15:46:47 although, this should work on Windows too 15:46:58 I believe there's some sort of compatibility layer somewhere translating lseek, read, etc 15:47:07 but it almost certainly doesn't translate mmap 15:47:32 `olist 934 15:47:36 olist 934: shachaf oerjan Sgeo FireFly 15:48:36 Windows certainly can mmap files, but it probably doesn't have a function called mmap 15:48:55 yeah, it's not a case of "can Windows do that", but "can I do that without writing a bunch of Windows-specific code" 15:50:48 hmm, why can't you just use stdio though? (not that stdio has a portable and safe getline function that I know of) 15:52:07 olsner: because there's a huge amount of jumping around seeking and locking and unlocking and so on, stdio buffering would screw this up 15:54:41 Just read into a growing buffer and stop when strchr('\n') isn't -1. 15:56:20 yeah, that's what I was planning 16:00:24 Also, surely fgets on Windows has correct behavior? 16:00:43 Oh, without using stdio. 16:00:44 Hyuk. 16:00:51 So, reimplementing stdio for no good reason. 16:01:16 Gregor: yeah, pretty much 16:01:34 or, "reimplementing stdio because it doesn't like files unexpectedly shrinking while you're writing to them" 16:02:07 * Gregor thinks for a second... 16:02:26 If a file unexpectedly shrinks while you're writing to it, stdio's correct behavior should be to re-expand the file with zeroes. 16:02:28 What are you seeing? 16:03:07 Gregor: re-expanding the file with zeroes 16:03:22 whereas the behaviour that I /want/ is to abort the write 16:03:25 which implies no buffering 16:03:33 because I need to know what has and hasn't been written at any given point 16:08:15 or put it this way: the previous code used stdio, it kept failing in bizarre ways because trying to keep track of buffering on top of everything else was just too much 16:19:11 Does the halting problem imply, that there actually is a program where it is undecidable if it halts or not? 16:19:20 Or does it just state, that no algorithm can decide it 16:19:47 or are those statements equivalent? 16:21:44 usually one proofs that for any would be decision procedure for the halting program there is some input which it gets wrong (either giving a wrong answer or failing to terminate). 16:21:48 *proves 16:23:12 mroman_: In a sense, whether those statements are equivalent is philosophical. If you believe that humans are super-Turing, then they're not. If humans are not super-Turing, then they are. 16:24:47 mroman_: Gödel's Theorem actually does explicitly construct an undecidable program 16:37:14 I'm searching for a proof of the halting problem that is actually understandable :) 16:37:23 since like 6 years 16:37:27 and I haven't found a single one 16:38:36 The ones that don't make use of crazy math feed the program to itself 16:38:38 like uhm 16:39:19 L(Q,x) halts, if Q(x) does not and does not halt, if Q(x) halts 16:39:29 then L(L,L) and stuff goes boom 16:39:48 and my brain just keeps yelling: How the fuck would that work 16:40:14 huh? 16:40:18 where's the problem with it 16:40:21 Well 16:40:29 if L(L) halts, L(L) does not halt 16:40:33 L computes whether Q halts for Input X 16:40:37 yeah 16:40:51 so L(L,L) computes whether L(L) halts 16:41:01 exactly 16:41:04 but what's the input of the second L? 16:41:38 the second L is actually the description of L 16:41:46 so it does not need any input 16:43:00 Yeah. But what are you actually deciding then? 16:43:19 Assuming f(x) is a function 16:43:35 L(Q,x) should test whether Q(x,x) halts. 16:43:36 and L(f,x) tries to state whether f(x) can actually be computed 16:43:58 then L(L,L) does test termination of L(L,L) and all works out as claimed. 16:44:01 so it computes L(f,f) 16:44:03 which is f(f) 16:44:07 and that don't make sense 16:44:44 well 16:45:02 -!- Sgeo has quit (Read error: Connection reset by peer). 16:45:13 it is not actually f(f), it is more like f(written down definition of f) 16:45:32 as i.e. gödel number or the like 16:45:35 yeah, the "how do you write down the definition of f" is the main mathematical content of the proof 16:45:36 I have no idea what that definition is supposed to be 16:45:39 everything else is pretty trivial 16:45:47 The definition does not have any input 16:46:06 the defintion is just a number or a string or whatever 16:46:15 so for what input are you actually trying to calculate whether it halts or not 16:46:16 and as such does not need any kind of input 16:47:06 at L(Q,x) you test Q with input x,x as int-e stated 16:47:16 so it will never ever come to f(f) there 16:47:36 so 16:47:41 L(L,L) computes L(L,L) 16:47:48 yes, and inverts it 16:47:55 (doesn't it?) 16:48:00 yeah 16:48:15 so, if L(L,L) halts, L(L,L) does not halt 16:48:21 therefore, L cannot exist 16:48:40 What if L is like universes in type theory? 16:49:20 So you would actually have L_i(L_i-1,L_i-1) 16:49:27 I don't know if that would help 16:49:27 bleh… actually what I really want is a scanf that gives pointers into the original string and decodes base 64 and decompresses zlib 16:50:08 What if I assume that there are two turing machines that are able to decide the halting problem 16:50:10 or, no 16:50:15 I don't know what i Want 16:50:16 L(Q,x) and G(Q,x) 16:50:17 ais523: What you actually want is a program that writes all your software for you, as you want it 16:50:24 Even if you don't know how you want it 16:50:25 and then do L(G,G) and G(L,L) 16:50:28 FreeFull: yeah, that'd be nice, but it'd take too long to impl 16:50:53 Well, you wouldn't be the one to impl it 16:50:55 L(L,L) won't work 16:50:57 It'd already be impld 16:51:07 but maybe L(G,G)? 16:51:25 L(G,G) would by definition be G(G,G) 16:51:49 hm yeah 16:52:32 L(G,L) would be G(L,L) would be L(L,L) 16:53:16 mroman_: you can play such tricks, but you need more arguments, L(G,L) and G(G,L), where L(G,L) tests whether G(G,L) terminates and G(G,L) tests where L(G,L) terminates. 16:53:59 and these things become tedious soon. 16:55:43 -!- Sgeo has joined. 17:27:13 -!- oerjan has joined. 17:38:13 http://codepad.org/Z6Z4ZT3b <- you can also argue that way 17:38:26 but it leaves unclear whether P(i) actually exists or not 17:38:53 but we know, that if it does, that no program can decide that stuff 17:41:10 "i put something undecideable into something that does decides everything, therefore it can't exists" sounds pretty strange 17:46:34 -!- doesthiswork has joined. 17:48:17 elan's dad is starting to get annoying. 17:50:07 ais523: you managed to make an `olist that wasn't duplicate, this is _highly_ irregular hth 17:51:15 -!- SingingBoyo has joined. 17:51:45 luckily they seem to be on their way of his subplot 17:51:47 I think 17:51:57 s/of/away from/ 17:52:04 FireFly: um did you even _read_ today's update. 17:52:26 yeees 17:52:34 well, we'll see 17:52:36 what are you reading? 17:52:45 order of the stick 17:52:50 ah. 17:54:31 I have a bookmark on #726, haven't read it since. 17:56:14 oerjan: well the forum thread was only at 4 pages, and I'd checked like half an hour before 18:01:12 but what's the input of the second L? <-- i think you are a bit confused. L should only take one argument, and L(Q) should decide whether Q(Q) halts. 18:02:04 (and do the opposite.) 18:02:44 -!- doesthiswork has quit (Quit: Leaving.). 18:02:50 it's the initially assumed halting function which takes two arguments, not L. 18:04:29 it's quite possible your source was confused about this, wouldn't be the first time. 18:13:48 What if L is like universes in type theory? <-- then you get lots of nice proofs about separation in complexity hierarchies. 18:14:01 Guys 18:14:06 I wanted to ask a question 18:14:09 But I forget what it is 18:14:18 Can we find my question using some sort of programming trick 18:14:28 good, good, as i should be leaving now. 18:14:31 -!- oerjan has quit (Quit: leaving). 18:14:48 oerjan: And of course you always need a higher hierarchy to prove something about the one right below 18:17:38 found on Reddit: someone's trying to translate Haskell's Prelude into pure GNU Make (i.e. no shelling out or scripting): https://github.com/PiPeep/prelude.mk/blob/master/prelude.mk 18:18:06 although it seems pretty partial atm 18:20:38 What 18:21:01 Ok, that is rather incomplete 18:21:38 yeah 18:21:44 I'd probably upvote it if it were more complete 18:21:59 like, how does PiPeep plan to handle lists of lists, for instance? 18:36:15 -!- Phantom__Hoover has joined. 18:38:19 -!- conehead has joined. 18:39:39 -!- Phantom_Hoover has quit (Ping timeout: 246 seconds). 18:43:06 -!- muskrat has joined. 19:17:02 -!- conehead has quit (Ping timeout: 240 seconds). 19:26:07 -!- Taneb has joined. 19:32:36 -!- ^v has joined. 19:43:38 -!- doesthiswork has joined. 19:45:00 -!- muskrat has quit (Quit: Leaving). 19:51:51 -!- Phantom_Hoover has joined. 19:52:58 -!- Phantom__Hoover has quit (Ping timeout: 246 seconds). 20:03:54 Is there a language that is directly based on set theory? 20:04:09 LISP is pretty close but it is not really 20:04:23 And there are a lot of languages based on axiomatic systems 20:04:32 But I can't think of any from ZFC 20:06:07 most sets being unrepresentable doesn't hel. 20:06:08 p 20:07:03 Well all sets are representable in ZF-NC 20:07:47 But well, µ-recursive functions are based on some axiomatic system of integers 20:07:58 Logical combinators as well, and lambda calculus 20:08:09 So I'm wondering if there's any for some flavor of set theory 20:08:31 http://en.wikipedia.org/wiki/Axiom_of_choice#Statements_consistent_with_the_negation_of_AC iunno 20:10:24 Hm 20:11:02 I think constructive set theory requires both the negation of choice and of the excluded middle 20:11:04 zfc isn't constructive, i guess is what i mean. 20:12:24 http://plato.stanford.edu/entries/set-theory-constructive/ oh good. 20:12:57 -!- carado has joined. 20:13:28 A lot of people feel strongly about axiomatic systems, which I always find weird 20:13:40 Like one of them is truer than another 20:13:48 Is there any reason I shouldn't treat Red Bull as slightly weaker coffee that tastes much, much better? 20:14:09 I do that, actually 20:14:10 But 20:14:16 Redbull has a Stigma 20:14:33 People basically seem to treat it like DRUUUUGS 20:14:41 Also the taurine is kind of a boogey man 20:14:44 -!- keoni29 has joined. 20:14:57 Does the taurine even do anything? Also, I treat coffee as a drug, so 20:15:13 I drink coffee to get a specific effect 20:15:17 Not a clue 20:16:23 well it is a drug. 20:16:44 Also, I want something that has the taste of Red Bull without the caffeine, so I could drink it constantly without using it in drug mode. Technically still a drug I guess, but less dangerous to overconsume 20:17:11 Yeah, but I mean drug as in 20:17:13 Social stigma 20:21:44 I always assumed Red Bull was stronger than either 20:21:53 err, than coffee 20:21:55 I don't drink either 20:22:15 (in fact, I haven't drunk caffeinated drinks for like 8 years now) 20:22:30 -!- conehead has joined. 20:22:51 Redbull has about the same amount of caffeine as regular coffee 20:23:14 I'll stick to tea & occasional soft drinks 20:23:33 I'll stick with heroine 20:33:17 Does anyone here have experience with Forth? 20:33:30 some 20:34:00 I am building a microcomputer based on an eZ8 microcontroller and I have to decide what it boots into 20:34:13 We were thinking about Forth. 20:34:29 At the moment I just have this shell from which you can run programs: 20:35:38 http://www.youtube.com/watch?v=4DyPKRJV9PI&feature=player_embedded 20:35:56 This is an old version of the current firmwae 20:35:59 *firmware 20:37:32 -!- nisstyre has quit (Quit: Leaving). 20:51:59 keoni29: yeah, Forth seems vaguely appropriate for that 20:52:12 its main uses are as a bootstrap language, and on embedded systems, and for making DSLs 20:52:20 and your use seems to fit into two out of three of those categories 20:57:31 -!- conehead has quit (Ping timeout: 254 seconds). 20:57:39 I already wrote routines for comparing strings with a list of tokens 20:57:52 So writing an interpreter would not be a huge deal 20:58:04 -!- impomatic has quit (Quit: http://corewar.co.uk). 20:58:09 It's all written in Z8 assembler 20:58:16 ais523, one of the people at my university seems to know you from b nomic 21:05:28 Taneb: hmm, interesting 21:05:32 there aren't that many B players 21:05:41 what's their name? or do you have a reason to keep it secret? 21:06:23 actually, considering the list of people who would say B rather than Agora 21:06:26