00:02:59 -!- contrapumpkin has changed nick to copumpkin. 00:12:42 Today- well, yesterday- I made some paper boats then went to the cinema 00:13:19 nice 00:13:36 now I want to make paper boats 00:15:41 I was making the best out of a printing error 00:16:57 Which led me to have about 30 sheets of paper with 4 black squares on each side 00:17:19 -!- ProofTechnique has quit (Ping timeout: 245 seconds). 00:25:02 -!- ProofTechnique has joined. 00:25:58 4 eh? 00:35:48 -!- ProofTechnique has quit (Ping timeout: 245 seconds). 00:38:06 blockzombie, yes 00:38:12 I was trying to print of some slides, 4 per page 00:38:14 Double sided 00:38:19 So I guess 8 per sheet 00:39:59 -!- Adrop has joined. 00:41:22 -!- Adrop has left. 00:41:24 -!- hjulle has quit (Ping timeout: 250 seconds). 00:41:31 -!- not^v has quit (Ping timeout: 255 seconds). 00:56:45 -!- skj3gg has quit (Quit: ZZZzzz…). 01:02:38 -!- chaosagent has joined. 01:15:18 -!- boily has joined. 01:20:33 @metar CYUL 01:20:33 CYUL 130100Z 27012KT 8SM -SN SCT035 OVC060 M12/M16 A2989 RMK SC3SC5 SLP123 01:33:19 -!- Froo has quit (Quit: *bubbles away*). 01:35:08 -!- skj3gg has joined. 01:39:00 @metar ENVA 01:39:00 ENVA 130120Z 13008KT CAVOK M04/M06 Q1014 RMK WIND 670FT 14008KT 01:42:24 hellørjan. still enjoying tropical weather? 01:42:38 @massages-loud 01:42:39 shachaf said 23h 45m 7s ago: not much of a hello when you quit within a few seconds! 01:43:07 @tell shachaf sorry. I had to disappear toward a pre-work shower. 01:43:07 Consider it noted. 01:44:14 still enjoying the flu, possibly 01:45:07 oh. the sickness disproved? 01:45:22 (what's the opposite of improved? I'm seriously drawing a blank here...) 01:45:37 "worsened" hth 01:45:41 thanks. 01:45:46 * boily is an idiot. 01:45:51 i'm pretty sure disproved means something completely different 01:46:43 yes, but I had a long day, and my mental hamster is sprawled besides its wheel, lightly twitching. 01:47:05 is it epileptic spasms 01:47:13 -!- skj3gg has quit (Quit: ZZZzzz…). 01:47:28 perhaps. I'm drinking diet coke. 01:48:00 * oerjan is drinking orange juice, might change to coke zero later 01:48:48 also eating 01:49:20 i suppose not having nausea is good 01:49:44 * dulla gets oerjan a Coke Orange 01:49:53 Welcome to Americlap 01:49:58 -!- Lymia has quit (Ping timeout: 245 seconds). 01:50:01 argh 01:50:24 we don't generally mix coke and orange in norway afaik 01:50:28 * boily glares at dulla “no corrupting Scandinavians!” 01:50:52 Hey, you can put your own god damn oj in your own god damn cocaine cola 01:51:06 unless you mean coke in the "americans have a different word for fizzy drinks dependent on region and time of day" sense 01:51:37 i believe i've read there's no trace of cocaine in coke since the 1930s or thereabouts 01:51:46 it's become the coca cola company versus pepsi co 01:51:55 pepsi is better. 01:51:58 you have root beer, or dr pepper 01:52:27 regardless, the automated drink machines are really weird, they allow you to make your own cola flavors 01:52:38 > orange vanilla coke 01:52:40 Not in scope: ‘orange’ 01:52:40 Perhaps you meant ‘range’ (imported from Data.Ix)Not in scope: ‘vanilla’Not ... 01:53:27 ;_; 01:54:11 i do not believe lambdabot yet has a vending machine attached 01:54:50 Well, now I have a goal 01:55:31 obviously what we truly want is launchMissiles :: IO () 01:59:13 I'd be more worried about a launchMissiles :: (). 01:59:33 This is going to be the start of a strategy game, oerjan 01:59:39 Are you realy willing? 02:00:16 the answer to that should be obvious to anyone who has been here in the channel for a while 02:00:25 ("heck no, far too much work") 02:00:56 boily: no, that would be unsafeLaunchMissiles, which you have to construct yourself hth 02:01:35 meh... 02:01:41 i think intuitively the type should be Void rather than () 02:01:50 because, there won't be anything left to return. 02:03:05 I would not be opposed to a proc chance of the missiles simply exploding on you for being so unsafe 02:03:14 oerjan: ^^ 02:03:26 dulla: those are missiles we are talking about. missiles are reliable. 02:04:41 Not when they are from kazahkstan 02:05:02 or is uzbekistan more apropos 02:05:15 àpropostan. 02:05:40 a'postrophestan 02:09:48 Missiles of this size, apocalypstrophestan 02:11:52 -!- adu has joined. 02:17:28 -!- Frooxius has joined. 02:17:48 -!- ^v has quit (Read error: Connection reset by peer). 02:18:15 -!- ^v has joined. 02:20:30 -!- dianne has quit (Quit: Lost terminal). 02:21:22 -!- dianne has joined. 02:23:49 -!- boily has quit (Quit: TEXTURED CHICKEN). 02:24:38 -!- Sprocklem has joined. 02:25:04 -!- Lymia has joined. 02:25:31 -!- arjanb has quit (Quit: .). 02:27:17 -!- skj3gg has joined. 02:30:18 -!- AndoDaan has joined. 02:36:10 -!- oren has joined. 02:40:15 -!- skj3gg has quit (Quit: ZZZzzz…). 03:14:26 That is a problem with the definition of "turing complete", not with C, tswett... 03:15:12 That is, no real computer can ever be "turing complete", thus some algorithms that theoretically "work" don't actually 03:15:28 * elliott sighs 03:16:54 -!- skj3gg has joined. 03:17:01 elliott, are there models of computability that take the limits of physics into account? 03:19:14 linear bounded automaton with tape fixed to 10^90 bits 03:20:16 nys: I think there are more restrictions than that. Consider the maximum speed of information propagation, and the energy supply, for example. 03:21:32 Personally, I think there is in theory a tradeoff between the size of memory and the speed of the computer. 03:21:40 oren: http://arxiv.org/abs/quant-ph/0110141 03:24:16 nys: cool. So there will never, even in theory, be a need for pointers longer than 90 bits. We can saefly assume that 03:24:30 sorry, digits 03:25:03 (assuming C) 03:25:17 so 300 bits 03:25:44 pikhq: right. 03:26:40 -!- skj3gg has quit (Quit: ZZZzzz…). 03:39:00 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 04:35:25 this is why we have a hierarchical cache structure, and coproccessing, oren 04:36:33 -!- skj3gg has joined. 04:49:01 -!- skj3gg has quit (Quit: ZZZzzz…). 04:52:26 -!- skj3gg has joined. 04:52:41 -!- Sketra has joined. 04:53:06 -!- nys has quit (Quit: quit). 04:58:18 'Sup 04:59:11 *ACHOO* 04:59:32 Bless you 04:59:33 `olist 975 04:59:53 olist 975: shachaf oerjan Sgeo FireFly boily nortti 05:00:10 (courtesy of shachaf) 05:00:30 I saw it but forgot to olist 05:01:21 What is Olist? 05:01:36 order of the stick announcements 05:01:51 `? olist 05:01:56 Update notification for the webcomic Order of the Stick. 05:02:16 Shachaf is a stalker? 05:02:18 HackEgo: you're, like, slow, tdnh 05:02:20 That's weird 05:02:25 Oh wrong chat 05:02:31 no, he sent me a lambdabot message 05:02:45 I've heard of lambdabot 05:02:57 @nixon 05:02:57 Always remember that others may hate you but those who hate you don't win unless you hate them. And then you destroy yourself. 05:03:16 What 05:03:29 That makes Not a lick o' sense 05:04:38 -!- Sprocklem has quit (Ping timeout: 246 seconds). 05:04:39 nixon often didn't hth 05:05:06 @pinhead 05:05:06 Unknown command, try @list 05:05:17 @zippy 05:05:18 Unknown command, try @list 05:05:22 hm what was it 05:05:27 @listmodules 05:05:27 activity base bf check compose dice dict djinn dummy elite eval filter free fresh haddock help hoogle instances irc karma localtime metar more oeis offlineRC pl pointful poll pretty quote search slap source spell system tell ticker todo topic type undo unlambda unmtl version where 05:05:32 @list quote 05:05:32 quote provides: quote remember forget ghc fortune yow arr yarr keal b52s pinky brain palomer girl19 v yhjulwwiefzojcbxybbruweejw protontorpedo nixon farber 05:05:45 @pinky 05:05:45 I think so, Brain, but me and Pippi Longstocking -- I mean, what would the children look like? 05:06:13 @yow 05:06:13 Vote for ME -- I'm well-tapered, half-cocked, ill-conceived and TAX-DEFERRED! 05:06:32 Vile creature of the internet begone from this sacred land of code and drama 05:06:50 wat 05:07:10 Sorry, I spout often words of wimsical use 05:07:35 @fortune 05:07:36 Occurs check: cannot construct the infinite kind 05:09:13 What 05:09:49 By the hymen of Olivia newton John that is a big bot lib for lambdabot 05:11:16 what do you expect of a bot more than a decade old 05:11:58 I feel young now 05:12:03 Thanks, Sir 05:12:25 yw 05:13:13 Who are you btw & what do you do for program wise 05:13:23 > nixon 05:13:25 Not in scope: ‘nixon’ 05:13:32 > quote.nixon 05:13:33 Not in scope: ‘quote’ 05:13:33 Perhaps you meant one of these: 05:13:33 ‘quot’ (imported from Prelude), 05:13:39 > [ y | y ] 05:13:40 Ambiguous occurrence ‘y’ 05:13:41 It could refer to either ‘L.y’, defined at L.hs:153:16 05:13:41 or ‘Debug.SimpleReflect.Vars.y’, 05:13:52 I haven't haskelled in years 05:13:54 you need an input set, Sketra 05:14:12 Its ok I gave up in fifth grade 05:14:14 > is just an abbreviation for @run it doesn't have access to the other commands 05:14:15 > [y|y <- "aeiou" 05:14:16 can't find file: L.hs 05:14:16 Not in scope: ‘is’ 05:14:16 Perhaps you meant one of these: 05:14:16 ‘id’ (imported from Data.Function), 05:14:18 > [y|y <- "aeiou"] 05:14:20 "aeiou" 05:14:49 Remember ten years from now oerjan you make lambdabot into an artificial intelligance 05:15:00 I don't 05:15:05 HAHaHhahahhHahHahahh 05:15:14 * Sketra sobs internally 05:15:37 @run text " (@nixon) " 05:15:38 (@nixon) 05:15:43 I forget the syntax... 05:16:02 @run text " @nixon " 05:16:03 @nixon 05:16:14 It makes a space 05:16:15 fk 05:17:37 oh 05:17:39 > [ y|y <- "gacen" ] 05:17:40 "gacen" 05:17:42 @@ run text " (@nixon) " 05:17:42 run text " (@nixon) " 05:17:46 Thanks 05:17:48 @@ @run text " (@nixon) " 05:17:49 (@nixon) 05:17:52 I give up 05:18:10 $say @Nixon 05:18:14 pfft 05:18:36 is it bad if I had a bot use lambdabot to do nefarious deeds 05:19:06 that's pretty traditional actually >_> 05:19:22 lol well then 05:19:26 -!- skj3gg has quit (Quit: ZZZzzz…). 05:19:36 Doesn't have a good security system? 05:20:52 @show test 05:20:52 "test" 05:20:53 its security system is really terrible 05:20:58 -!- GeekDude has quit (Quit: ZNC - http://znc.in). 05:21:07 @@ @run text @show @nixon 05:21:08 I brought myself down. I impeached myself by resigning. 05:21:10 there are some very bad exploits that I doubt got fixed that I'm not going to tell anyone about 05:21:21 @@ @ run text . reverse $ @show @nixon 05:21:21 Plugin `compose' failed with: Unknown command: "" 05:21:24 @@ @run text . reverse $ @show @nixon 05:21:25 .era yeht ,ti ecaf s'tel ,woN .seert eht fo tuo tsuj era ,yllacisab , meht ... 05:21:28 yay 05:21:32 lol well then 05:22:24 them basically are just out of the trees Now lets face they are 05:22:40 Sketra: lambdabot only got a proper sandbox last month after we found that security bug 05:22:42 I can read backwards 05:22:51 well somewhat proper 05:23:07 Ooo a sandbox?! 05:23:10 That's cool 05:23:20 before that it tried to trust haskell's type system 05:23:34 Lol nope 05:24:17 Sketra: um you don't know what sandbox means for a bot? 05:24:23 Nope 05:24:30 I think 05:24:36 it means putting it in a more secure environment 05:25:31 OH 05:25:41 yeah well you may have could said that 05:26:04 My friend did that to our currency bot 05:28:03 Prod bots are nice 05:28:51 ... Who is oerjan? 05:29:21 you're sounding seriously crazy today. 05:29:54 What? 05:30:27 I'm just asking a question 05:30:45 i'm a norwegian who does pretty much nothing. 05:30:51 I wish to know what you've done in your life As a programming 05:30:57 Go to war oerjan? 05:31:15 How come Germany took over Norway but Sweden?! 05:31:20 not* 05:32:04 sweden didn't have a long atlantic coastline or a stupid policy of downsizing the military (not sure about the latter) 05:33:46 Who are nords 05:33:51 Nordic? 05:34:17 Geometery confuses me oerjan 05:36:01 you just have to look at it from the right angle 05:37:04 I learned a new today 05:37:09 -///- 05:37:18 nordics are people living in northern europe. some of their ancestors were vikings. 05:37:26 ouo" I heard from a friend that.. 05:37:32 you guys are smart 05:38:03 you're Eolus. you should have noticed by now. 05:38:11 Ofc in some fields you may not be as smart 05:38:21 true. 05:38:28 Eoly is best friend 05:38:42 i don't actually believe that but whatever. 05:38:52 Believe what 05:39:15 that you're not the exact same person as Eolus. 05:39:29 Physically 05:39:39 or legal birth name? 05:39:50 physically. 05:40:01 Male 05:40:10 Mentally 15 persons 05:40:51 whatever 05:40:55 Second split of third tri quarter of the Median system Sketra Split from Zetsu Female alter Mental age 17 05:40:58 Like that 05:41:04 I log a lot of stuff 05:41:55 Should I have everyone introduce themselves like that? I assume it would be easier 05:42:56 we aren't going to distinguish you into personae anyhow. 05:42:58 4000 newtons psi to shatter bones 05:43:45 Its ok just call us by the nick that is displayed and you should be spared any type of discontent and murderous anger from sprouting 05:44:28 Like int-e always calling us By lilax 05:45:25 * Sketra pets Oerjan 05:45:31 you never do that anyways 05:45:41 You are good friend I guess 05:45:44 i almost did above. 05:46:23 Probably would forgive since you only did it once 05:46:50 -!- MDude has quit (Read error: Connection reset by peer). 05:46:58 Its just hhhh titles matter cuz ugh idk we just hate being called by eachothers names 05:47:11 Albiet confusing just call us by our nicks 05:48:07 i'll do that, but only because i'd be doing that anyway. if you start making me want to follow rules i consider pointless, i might run out of patience myself. 05:48:24 Make... LOL 05:48:39 *start making me follow 05:48:47 well no oerjan you don't have to follow the rules you are nice and funny 05:48:53 We forgive you 05:49:15 Also you remind of us our grandpa so its ok 05:49:15 ...that kind of talk doesn't help, either. 05:50:12 As long as you don't say anything rash in anger lol Cuz lots of us are emotionally unstable and you might never hear from me again or us for that matter 05:50:38 -!- bb010g has joined. 05:50:53 -!- pikhq has quit (Remote host closed the connection). 05:51:34 HaskellCEO: TOO MUCH! Just found out that these dickwads belong to some Christian denomination known as the Alonzo Church of God in Christ or some shit. 05:51:50 Wair what?! 05:52:10 domination 05:52:24 It's a joke about the famous mathematician Alonzo Church 05:52:42 oh 05:52:57 what's RGB for pink? 05:53:14 Roy Gee Biv? 05:54:19 255 192 203 pink 05:54:25 according to X11 05:55:10 (/usr/share/X11/rgb.txt) 05:55:13 cool 05:55:43 really 05:55:51 k 05:56:00 Sketra: Red Green Blue 05:56:20 I'm colour blind to Blue and Green 05:56:26 color numbers for a monitor 05:56:43 Oh mai 05:56:58 probably somewhat randomly assigned 05:57:04 Thas cool I haven't coded since 10th grade 05:57:06 (the names) 05:57:25 hhhhhh 05:57:28 I'm gonna go with "deep pink" 255 20 147, for the color of bad links, and "Purple" 160 32 240 for the good links 05:57:50 Oh I see what you are doing 05:58:18 this all probably depends on monitor calibration and stuff, something i only know the vaguest part about 05:58:38 -!- ProofTechnique has joined. 05:58:44 Sketra: writing a primitive hypertext browser for my game 06:05:17 -!- pikhq has joined. 06:11:24 Sketra: you know 06:13:44 hm iirc today's freefall seems to miss the direct order the mayor's assistant gave... 06:16:20 http://freefall.purrsia.com/ff2200/fc02155.htm 06:28:50 I do? 06:44:32 *ACHOO* 07:28:27 http://www.noulakaz.net/weblog/2007/03/18/a-regular-expression-to-check-for-prime-numbers/ 07:31:59 -!- Patashu has joined. 07:32:44 -!- blockzombie has quit (Remote host closed the connection). 07:35:48 -!- oerjan has quit (Quit: leaving). 07:44:55 http://webcache.googleusercontent.com/search?q=cache%3Awww.monohaskell.com&oq=cache%3Awww.monohaskell.com&aqs=chrome..69i57j69i58.1240j0j4&sourceid=chrome&es_sm=122&ie=UTF-8 07:47:48 -!- Sketra has quit (Ping timeout: 250 seconds). 07:54:43 -!- int-e has set topic: What is the land-speed velocity of a migrating fungot? | The many faces of Lilax | ZFC is a ChuChu rocket. | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/. 07:57:55 Oh, early GG comic today. 08:03:30 Ah I guess collateral damage is no fun if you're it. http://www.schlockmercenary.com/2015-02-13 08:13:07 -!- spupuser has joined. 08:15:44 woohoo it't working 08:23:41 http://postimg.org/image/8upxjp4rz/ 08:27:41 See, it detected that the "element" link's file exists and made that link blue 08:30:29 Now to reinvent web forms 08:33:08 [wiki] [[Ttml]] http://esolangs.org/w/index.php?diff=41901&oldid=41860 * Orenwatson * (+24) update spec to include hyperlinks 08:38:08 -!- bb010g has quit (Quit: Connection closed for inactivity). 08:51:50 -!- shikhin has joined. 08:53:00 -!- elliott has set topic: What is the land-speed velocity of a migrating fungot? | ZFC is a ChuChu rocket. | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/. 08:53:15 int-e: can you stop being a dick to 16 year olds, it's getting really old 08:55:35 it's the most ridiculous feud in this place since whenever I cared enough to feud with people 09:09:18 oren: do you pick a new terminal font for every sreenshot 09:09:26 that one is actually cute though 09:10:25 *screenshot 09:15:40 -!- adu has quit (Quit: adu). 09:26:29 elliott: well, not every screenshot, but I do acquire new terminal fonts every week or so 09:26:56 elliott: He strokes (pets? pats?) me the wrong way, it's hard not to bite. 09:27:12 But You're right. 09:28:47 -!- shikhin_ has joined. 09:31:32 -!- shikhin has quit (Ping timeout: 245 seconds). 09:47:24 -!- ais523 has joined. 09:49:10 -!- ais523 has quit (Read error: Connection reset by peer). 09:49:28 -!- ais523 has joined. 10:02:20 -!- chaosagent has quit (Ping timeout: 252 seconds). 10:23:47 Wife made me new jewelry: https://twitter.com/J_Arcane/status/566173919770869760 10:40:29 -!- Phantom_Hoover has joined. 10:57:32 -!- ^v has quit (Read error: Connection reset by peer). 10:57:59 -!- ^v has joined. 11:18:27 -!- shikhin_ has changed nick to shikhin. 11:25:35 -!- boily has joined. 11:33:04 -!- ais523 has quit (Quit: computer is malfunctioning). 11:46:59 -!- ais523 has joined. 11:47:03 -!- AndoDaan has quit (Ping timeout: 252 seconds). 11:59:33 -!- ais523 has quit (Read error: Connection reset by peer). 11:59:47 -!- ais523 has joined. 11:59:56 -!- AnotherTest has joined. 12:04:17 @massages-loud 12:04:17 You don't have any messages 12:11:39 -!- Lymia has quit (Remote host closed the connection). 12:15:04 -!- Phantom_Hoover has quit (Ping timeout: 252 seconds). 12:15:10 -!- boily has quit (Quit: CARBONATED CHICKEN). 12:16:02 where can you find law texts of us laws? 12:16:03 like 12:16:08 on cities? 12:16:14 apparentely some cities have some weird laws 12:16:23 but nobody seems to have an actual source 12:18:05 -!- Lymia has joined. 12:18:06 The libraries of those cities, perhaps. 12:18:17 So weird question: does immutability simplify the prospect of building a compiler for a dynamically typed language? 12:19:10 Well, you no longer need to convert the program to SSA. 12:23:14 (Compilers for imperative languages like gcc already use immutable IRs, so the passes after that wouldn't really change.) 12:25:49 So I'm trying to figure out what kind of hypercomputer you'd need to do the Henkin construction. 12:26:56 Define a level-1 hypercomputer as a Turing machine attached to a halting oracle for Turing machines. 12:27:11 Jafet: Yeah, that was my thought; the risk of a name changing in type gets smaller if it can't change (local override notwithstanding, and potentially workaroundable). Polymorphic functions seem like they could still be stickier, but maybe not so much? 12:27:22 Jafet: so... no online :( 12:27:39 I should really do SICP, and look into the source code of Bones. 12:28:45 So our L1H starts with a consistent theory, such as ZFC (assuming ZFC is consistent). It then enumerates every statement in the language; whenever it gets to a statement consistent with the theory so far, it adds it to the theory. 12:29:00 It can check if a statement is consistent with the theory or not by seeing if a Turing machine halts. 12:29:05 And that's stage 1. 12:30:07 Now, the way I just said it, stage 1 will go on forever, meaning we'll never start on stage 2. Aye? 12:30:14 There are a hundred counties in Kansas, which is probably about as regressive as america gets, and each of them can enact strange ordinances. I don't think there's a good chance you will find them all online (especially any recently-passed ones). 12:30:42 Jafet: damn :( 12:31:02 State-wide laws should be available though (google suggests http://www.usa.gov/Topics/Reference-Shelf/Laws.shtml) 12:32:53 -!- Patashu has quit (Ping timeout: 245 seconds). 12:32:59 I could be wrong... https://library.municode.com/index.aspx?clientId=14166 12:33:17 Anyhoo, stage 2 begins by adding a constant to the language for every "there exists" statement we added in stage 1. 12:33:37 Then we add a statement saying that the constant is an example of the "there exists" statement. 12:34:02 Then we do the same thing we did in stage 1, enumerating all the statements and adding the consistent ones. 12:34:37 But now how do you check if a statement is consistent with all the previously added statements? 12:34:39 J_Arcane: in a unityped language, all functions (or perhaps no functions?) can essentially be polymorphic 12:35:43 Anyway, whether "local variables" (if your language has them) are immutable is mostly immaterial because of SSA transform. 12:35:45 Jafet: Hmm. That makes me think of the Write Yourself a Scheme implementation; where there's a union type of 'LispValue' that can be either of number, symbol, etc. 12:36:14 If your compiler goes to the trouble of SSA transform for performance, that is 12:38:47 I think that involves checking if an L1H halts, meaning you need an L2H. And stage 3 will require an L3H, and so on. 12:39:43 "In functional language compilers, such as those for Scheme, ML and Haskell, continuation-passing style (CPS) is generally used where one might expect to find SSA in a compiler for Fortran or C. SSA is formally equivalent to a well-behaved subset of CPS (excluding non-local control flow, which does not occur when CPS is used as intermediate representation), so optimizations and transformations for 12:39:45 mulated in terms of one immediately apply to the other." Hm. 12:40:10 After you've done all the infinitely many stages, your model is just the set of all constants. 12:40:14 Great discussion, everyone. 12:41:20 Is that a countable model? 12:42:27 Yeah. 12:54:11 Why do you need an oracle for that construction, though 12:54:29 Just test all statements in parallel in stage 1, and accumulate the ones proven to be consistent 12:54:45 When you find any existentially quantified ones, thread them through stage 2, etc. 12:56:25 This will eventually give you every (finitely provably) consistent finite statement 13:17:32 -!- GeekDude has joined. 13:22:36 -!- graSP has joined. 13:27:29 -!- graSP has quit (Quit: ChatZilla 0.9.91.1 [Firefox 35.0.1/20150122214805]). 13:28:00 -!- graSP has joined. 13:28:03 -!- copumpkin has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz…). 13:28:31 -!- SopaXorzTaker has joined. 13:42:27 -!- sorch has joined. 13:45:43 -!- skj3gg has joined. 13:47:24 -!- sorch has quit (Quit: Leaving). 13:49:34 -!- ais523 has quit (Read error: Connection reset by peer). 13:49:48 -!- ais523 has joined. 13:52:53 -!- graSP has quit (Ping timeout: 244 seconds). 14:06:29 -!- TieSoul has joined. 14:19:49 -!- skj3gg has quit (Quit: ZZZzzz…). 14:31:06 -!- Tritonio has quit (Ping timeout: 252 seconds). 14:40:06 -!- Guest50274 has joined. 14:54:27 -!- skj3gg has joined. 14:57:16 -!- skj3gg has quit (Client Quit). 15:11:27 -!- adu has joined. 15:14:15 -!- `^_^v has joined. 15:19:25 -!- adu has quit (Quit: adu). 15:21:17 -!- callforjudgement has joined. 15:22:48 -!- ais523 has quit (Ping timeout: 252 seconds). 15:23:03 -!- callforjudgement has changed nick to ais523. 15:28:55 -!- spupuser has quit (Ping timeout: 255 seconds). 15:32:44 -!- shikhin has quit (Ping timeout: 265 seconds). 15:49:44 -!- adu has joined. 15:58:37 Jafet J_Arcane What is SSA if it's a "well-behaved" CPS? 15:59:59 Also what is an oracle? 16:00:02 is anyone here capable of getting paywalled papers and doesn't have the morals to prevent sharing it afterwards 16:00:18 yes, thanks ais523, I thought of you too 16:01:57 -!- SopaXorzTaker has quit (Ping timeout: 250 seconds). 16:13:57 I can do it 16:14:07 UofT library has a lot 16:14:31 uh I just mean like online ACM paywall kinda things 16:14:34 unless you mean a digital library 16:15:59 -!- mihow has joined. 16:17:10 Morals? Perhaps "legals" is a better term. 16:17:40 Hmm, this spell checker agrees 16:17:44 @wn legals 16:17:45 No match for "legals". 16:18:15 fair 16:18:20 -!- bb010g has joined. 16:18:27 I meant more "doesn't have a moral system s.t. ..." 16:19:31 Chaotic Good FTW 16:19:50 it's "Natural Deduction and Weak Normalization for Full Linear Logic", anyway. 16:20:29 http://jigpal.oxfordjournals.org/content/12/6/601.abstract 16:21:58 elliott, I find often googling the title works 16:23:18 Taneb: tried that :/ 16:23:42 Are there any interesting concurrency esolangs? 16:24:07 -!- ProofTechnique has quit (Ping timeout: 256 seconds). 16:24:22 "All of them" 16:25:30 I got it 16:25:48 * elliott waits anxiously in the get-away car 16:26:01 * elliott glances around for cops 16:28:24 * dulla arrests elliott 16:29:47 How would you rate π-calculus as 1) interesting 2) esolang 16:31:58 -!- ProofTechnique has joined. 16:34:13 -!- Guest50274 has quit (Remote host closed the connection). 16:36:18 I am not familiar with it, Jafet 16:36:58 * dulla brings elliott to the combination sex dungeon and creamery 16:37:57 um... what kind of cream are we talking here 16:38:08 -!- shikhin has joined. 16:38:38 Ice cream 16:40:10 A number of researchers are, but it's fairly safe to rate them as esoteric 16:41:59 -!- oerjan has joined. 16:43:20 https://esolangs.org/wiki/Ziim looks interesting 16:51:57 -!- oren has quit (Ping timeout: 245 seconds). 17:04:10 -!- oren has joined. 17:21:30 -!- GeekDude has changed nick to GeekDudesBopt. 17:21:31 -!- GeekDudesBopt has changed nick to GeekDudesBot. 17:21:49 -!- GeekDudesBot has changed nick to GeekDude. 17:23:06 -!- GeekDude has quit (Changing host). 17:23:06 -!- GeekDude has joined. 17:23:31 -!- GeekDude has changed nick to GeekDudesBot. 17:32:27 -!- GeekDudesBot has changed nick to GeekDude. 17:32:39 -!- GeekDude has quit (Changing host). 17:32:39 -!- GeekDude has joined. 17:50:28 -!- perrier has quit (Remote host closed the connection). 17:51:40 -!- perrier has joined. 17:53:36 -!- Phantom_Hoover has joined. 17:56:17 -!- J_Arcane has quit (Quit: ChatZilla 0.9.91-rdmsoft [XULRunner 32.0.3/20140923175406]). 17:56:34 -!- J_Arcane has joined. 17:58:18 -!- Phantom_Hoover has quit (Ping timeout: 244 seconds). 17:59:25 -!- callforjudgement has joined. 18:02:22 -!- ais523 has quit (Ping timeout: 245 seconds). 18:02:36 -!- callforjudgement has changed nick to ais523. 18:18:08 -!- bb010g has quit (Quit: Connection closed for inactivity). 18:58:36 -!- arjanb has joined. 19:05:23 -!- oren has quit (Ping timeout: 245 seconds). 19:06:03 -!- Phantom_Hoover has joined. 19:10:23 -!- nortti has changed nick to lawspeaker. 19:12:06 -!- lawspeaker has changed nick to nortti. 19:15:25 > let herpes = 1:1: zipWith (\a b -> a + b + 1) herpes (tail herpes) in herpes 19:15:26 [1,1,3,5,9,15,25,41,67,109,177,287,465,753,1219,1973,3193,5167,8361,13529,21... 19:15:44 > let herpes = 1:1: zipWith (\a b -> a + b + 1) herpes (tail herpes) in take 8 herpes 19:15:45 [1,1,3,5,9,15,25,41] 19:16:08 :t intersperse 19:16:09 a -> [a] -> [a] 19:16:40 > let herpes = 1:1: zipWith (\a b -> a + b + 1) herpes (tail herpes) in intersperse ' ' . (take 8) $ herpes 19:16:41 No instance for (GHC.Num.Num GHC.Types.Char) 19:16:41 arising from a use of ‘herpes’ 19:17:01 > let herpes = 1:1: zipWith (\a b -> a + b + 1) herpes (tail herpes) in intersperse ' ' . map show . (take 8) $ herpes 19:17:03 Couldn't match type ‘[GHC.Types.Char]’ with ‘GHC.Types.Char’ 19:17:03 Expected type: a0 -> GHC.Types.Char 19:17:03 Actual type: a0 -> GHC.Base.String 19:17:16 > let herpes = 1:1: zipWith (\a b -> a + b + 1) herpes (tail herpes) in intersperse " " . map show . (take 8) $ herpes 19:17:17 ["1"," ","1"," ","3"," ","5"," ","9"," ","15"," ","25"," ","41"] 19:17:20 -!- oren has joined. 19:17:27 > let herpes = 1:1: zipWith (\a b -> a + b + 1) herpes (tail herpes) in unwords . intersperse " " . map show . (take 8) $ herpes 19:17:29 "1 1 3 5 9 15 25 41" 19:18:50 hmm 19:19:10 -!- ais523 has quit. 19:19:21 do the ratios approach phi? 19:19:21 -!- ais523 has joined. 19:20:07 make it print more terms 19:21:50 -!- ais523 has quit (Read error: Connection reset by peer). 19:22:03 -!- ais523 has joined. 19:24:26 quintopia: of course they do. it's just 2*F_n - 1 [with n counting from 1] 19:25:34 (uhm and using F_n to denote Fibonacci numbers) 19:26:32 quintopia they are leonardo numbers 19:26:48 they can be described in terms of that, afaik 19:27:30 besides, you can compile it yourself on compile online, quintopia 19:27:46 http://rextester.com/BQA14775 19:29:29 also it's L(n)=2F(n+1)-1, /wikipedia int-e 19:31:05 J_Arcane what is an orcale in that talk you have about SSA and CPS? 19:31:11 had* 19:31:11 -!- zzo38 has joined. 19:31:26 Hmm? 19:33:28 i figured it would but wasnt sure if the +1 would throw it off somehow 19:33:49 Nice. Rust 1.0 by May, and beta end of next month. 19:33:55 did you know fibonacci's first name is actually leonardo, confusing that 19:34:10 how do you prove the ratio approaches phi in the limit 19:34:21 dulla: so what. the code doesn't really indicate whether the first index is 0 or 1. 19:35:15 You can have a zero in it, but to reuse the lazy list construction of the fibb numbers, I had to start at 1:1 19:35:52 -!- oren has quit (Ping timeout: 240 seconds). 19:35:55 by the looks of it L(0)=1 19:36:06 dulla: *oracle 19:36:23 whoop 19:36:31 er, Oracle* J_Arcane 19:37:06 Dunno what you mean. There were a couple convos going at once though, perhaps there's some confusion there? 19:38:15 quintopia: you can absorb the +1 into the terms instead. 19:38:34 Um, something about hypercomputers, and oracles resolving or optimising SSA's or halting problems 19:39:11 (a + b + 1) + 1 = (a + 1) + (b + 1) 19:40:04 and then you have the usual fibonacci recursion 19:40:10 *recurrence 19:40:17 i aint seeing it 19:41:15 dulla: ahh, yeah, no someone was working on a proof of ... something. I was just talking about immutability and compiling. 19:41:23 basically, take your sequence fulfilling a_n = a_(n-1) + a_(n-2) + 1 and define b_n = a_n + 1 19:42:04 ah okay i see it now 19:42:21 And oracles are? 19:42:25 wise 19:42:33 but mysterious 19:42:58 dulla: an oracle is an extra instruction you add to your turing machine / whatever which does something arbitrary you decide on. 19:43:16 in this case, testing whether an ordinary turing machine halts 19:43:16 So more or less external or side influence 19:43:21 yep 19:43:28 alright 19:43:42 the thing is, a lot of the theory works the same if you add an oracle to things 19:43:50 So Buterin wasn't pulling Oracle out his ass when talking about news tickers 19:44:16 just, instead of not being able to decide halting problem for ordinary TMs, you're now unable to decide it for a TM with your oracle 19:45:57 I also thought of adding a oracle operation into a sequent calculus, where |- Oracle X is an axiom if and only if |- X is not a theorem of the system (even if it cannot be proven that it isn't a theorem). 19:45:59 So you can exit a loop? 19:47:21 well you can detect an infinite loop 19:47:45 dulla: Well, the oracles are often hypothetical. The one that solves the halting problem cannot, as far as we know, exist. (It would require computing power that goes beyond Turing machines, which goes against the Church-Turing thesis) 19:48:49 see e.g. https://esolangs.org/wiki/Banana_Scheme which is an esolang applying this to scheme 19:49:21 (Not all oracles are hypothetical. It's interesting to think of polynomial time algorithms that can query oracles that solve (at least conjecturally) harder problems like satisfiability of boolean formulas) 19:49:52 (just as an example) 19:50:04 a big part of why the P = NP problem is so hard is that the answer to it can change if you add an oracle. 19:50:06 -!- Sprocklem has joined. 19:50:38 which means that many of the easy methods for proving complexity results simply cannot work for it 19:51:17 zzo38: is that oracle circular? 19:51:29 int-e: How does that mean? 19:52:17 zzo38: does the system in "not a theorem of the system" refer to the system with those axioms? 19:52:26 zzo38: (produced by the oracle) 19:52:56 int-e: I would think so. Maybe there might be some systems where this doesn't work although I expect it to work in most cases. 19:54:25 Hmm, actually, what good is such an axiom schema? Knowing Oracle X doesn't tell you much. 19:55:17 I don't actually know the answer of that question. 19:57:56 so an oracle of x? 19:59:28 Although |- Oracle Oracle X would indicate that |- X is a theorem, I think. 20:00:06 go intuintionistic on it 20:00:11 x is better than not not x 20:06:39 -!- oren has joined. 20:08:05 zzo38: tricky. it almost fails if the theory is inconsistent, but then X is a theorem anyway... 20:08:32 classically, at least. 20:14:09 -!- dorei has joined. 20:17:28 -!- hjulle has joined. 20:21:27 Man, I've been on board with this for years: http://www.stopusinglinkedin.com/ 20:25:22 stop using web 2.0 xD 20:25:28 "With these changes in place, developers can no longer build tools that allow you to better leverage your own professional connections." ... err, right, sure. 20:26:02 "Linkedin prevents *US* from earning money with your data." ... cry me a river, baby. 20:27:11 (I agree with the idea of not using LinkedIn, but these are the wrong reasons.) 20:27:14 well true, the latest complaint is not the most compelling. 20:27:30 the part where it's little more than a spam pyramid is the bigger one for me. 20:31:17 -!- nycs has joined. 20:32:53 -!- `^_^v has quit (Ping timeout: 256 seconds). 20:35:16 -!- ais523 has quit (Read error: Connection reset by peer). 20:35:30 -!- ais523 has joined. 20:36:53 ok guys 20:37:02 the dawn machine: yea or nay? 20:37:54 -!- drdanmaku has joined. 20:38:25 -!- drdanmaku has quit (Client Quit). 20:42:20 ??! 20:42:31 too late, i already decided 20:44:29 the dream machine: yea :-P 20:47:22 Tell the people that made PDJSON that I fixed the bug in it. 20:51:44 -!- AnotherTest has quit (Ping timeout: 246 seconds). 20:51:59 -!- GeekDude has quit (Changing host). 20:52:00 -!- GeekDude has joined. 20:52:45 -!- GeekDude has quit (Changing host). 20:52:45 -!- GeekDude has joined. 20:58:27 -!- Tritonio has joined. 20:59:01 -!- callforjudgement has joined. 21:03:29 -!- ais523 has quit (Ping timeout: 256 seconds). 21:04:12 -!- callforjudgement has changed nick to ais523. 21:11:29 -!- mihow has quit (Quit: mihow). 21:22:58 -!- mihow has joined. 21:23:41 -!- Patashu has joined. 21:24:35 -!- ais523 has quit. 21:24:47 -!- ais523 has joined. 21:27:30 J_Arcane: I'm aheadof the game, I never started using Linkedin. 21:27:49 Neither do I 21:28:10 -!- ais523 has quit (Client Quit). 21:28:17 -!- callforjudgement has joined. 21:29:07 -!- callforjudgement has changed nick to ais523. 22:13:46 -!- nycs has quit (Quit: This computer has gone to sleep). 22:14:04 -!- nycs has joined. 22:18:26 -!- callforjudgement has joined. 22:18:28 -!- ais523 has quit (Read error: Connection reset by peer). 22:18:30 -!- callforjudgement has quit (Changing host). 22:18:30 -!- callforjudgement has joined. 22:30:51 -!- nys has joined. 22:36:02 -!- shikhin_ has joined. 22:39:07 -!- shikhin has quit (Ping timeout: 255 seconds). 22:47:05 I made up a format that can be used in a HTML comment inside of a HTML form, which can be used to make the form to work with interactive command-line interfaces; for example this can be used to login to OpenID servers which support it. An example can be: 22:47:57 ? 22:48:04 (The client would need to parse the form method and action too, as well as any hidden fields in the form) 22:49:00 It might be used for example now you can login to stuff other than webpages using OpenID too. 22:49:37 -!- mihow has quit (Quit: mihow). 22:49:52 (Assuming there is a reason you still want to use OpenID for this) 23:01:52 -!- nycs has quit (Quit: This computer has gone to sleep). 23:02:05 dulla: one of the tricks with this channel is, there doesn't really have to be a reason 23:02:59 oh, everyone, eso question that came up in another channel: what's the minimum number of transistors needed to have a functioning CPU, assuming you don't care about performance? 23:03:07 basically a Turing tarpit but with transistors 23:03:30 we have to assume that there's some sort of external memory for this to work, but presumably we can rig the details as appropriate (e.g. by use of a magnetic tape drive) 23:03:31 I want to know too the answer. Perhaps might TOGA computer do it? 23:04:20 it's got to be some sort of simple Turing machine, hasn't it? you don't want to waste transistors storing addresses 23:04:22 Jafet: you want *all* the consistent statements, not just the provably consistent ones. 23:04:32 the (2,3) machine doesn't count because it requires an infinite initialization 23:05:21 Taneb: also, Al Dente is totally an interesting concurrency esolang. 23:05:43 I like "Al Dente" esolang too 23:05:54 There's no flow control. Stuff just spontaneously happens. 23:05:55 what about My Unreliable Past? that's a concurrency esolang really, even though it doesn't look like one 23:06:12 (I don't think anyone's guessed the original inspiration for that one yet) 23:07:09 As for the CPU, bitwise cyclic tag might be the winner. 23:07:30 Now write out all of the transistors of it please 23:08:33 Mmm I don't feel like it. 23:09:01 tswett: BCU requires /two/ queues 23:09:17 even one is going to be awkward to attach to a CPU 23:09:26 people don't just sell unlimited-size queues 23:10:29 -!- oren has quit (Ping timeout: 264 seconds). 23:12:34 -!- Lymia has quit (Remote host closed the connection). 23:13:09 -!- Lymia has joined. 23:13:38 People don't sell unlimited-size RAM, either. 23:14:04 right 23:14:08 which is why you need the tape drive 23:14:19 Say each queue has four pins. Input, output, enqueue, dequeue. 23:14:26 so you can add more tape when you run out, without needing an infinite number of address bits 23:14:33 but sure, I'll buy that 23:14:39 err, plus two power pins 23:14:42 but those don't need transistors 23:14:51 Right. 23:15:02 even if we assume our infinite queues are self-powering, they still need power pins to know what logic levels to use 23:15:03 Does the clock count towards transistor count? 23:15:14 hmm 23:15:23 well it's very hard to make a clock with nothing but transistors 23:15:34 I think you can make a clock with one transistor plus a bunch of extra components 23:15:56 although I think that might give you a sine wave rather than a square wave? probably good enough, anyway 23:16:21 So lemme think how this ultra-tiny CPU would work. 23:17:24 I think the state could just be stored in a single flip-flop or whatever. 23:18:16 i hear this guy named babbage had an idea to make a computer with no transistors at all 23:18:20 Mm, maybe two. Execute one command per two clock cycles. 23:19:12 oerjan: yes, but the implication is that we're making one with /only/ transistors 23:19:19 + the minimum of other required components 23:19:24 probably need a few capacitors and resistors 23:19:49 Okay, so you have a one-bit register S, where zero means we're about to read the first bit of a command and one means we're about to read the second bit of a 1 command. 23:20:18 As well as, I dunno, T, where zero means we're about to read a bit and one means we're about to write one. 23:20:20 Something like that. 23:20:32 can we do the read and write simultaneously? 23:21:32 Even if the queue supports that, I'm not sure if the CPU logic could handle that. 23:21:56 Well, this is what it is. 23:22:10 T = 0 means we're about to read a bit. T = 1 means we're about to enqueue or dequeue a bit. 23:22:17 You can't dequeue a bit and read a bit in the same clock cycle. 23:23:58 remember we have two queues 23:24:01 BCT doesn't work with just one 23:24:04 So, upon clock positive edge, if T = 0 and S = 0, then we dequeue the data queue, enqueue the program queue, and subsequently dequeue the program queue. 23:24:19 Except can you enqueue and dequeue in the same clock cycle? 23:24:34 Maybe we can make it so that you enqueue on positive edge and dequeue on negative edge. 23:25:00 I guess we're using two-phase logic as is anyway 23:25:31 The program queue's input and output pins can just always be shorted together. The enqueue and dequeue pins can be controlled by a single wire, but one of the pins needs to have a not gate before it. 23:27:29 which can be implemented with one transistor and a resistor 23:27:37 if you don't mind the current drain, which we don't 23:28:25 Which logic style (or whatever you call it) are we using? 23:28:55 whichever works 23:29:05 so an infinite without infinite addressing is more or less tape + some instruction storage? 23:29:08 er 23:29:10 I think RTL is going to be cheapest in most cases? or randomly changing between NMOS and PMOS? 23:29:13 infinite tape without* 23:29:38 you don't want a logic style that drives both up and down because that needs twice as many transistors, even if it is more efficient 23:32:54 -!- scarf has joined. 23:33:32 And are these real transistors governed by calculus, or idealized ones which act kinda like relays? 23:33:45 Digital transistors? 23:34:52 -!- callforjudgement has quit (Ping timeout: 245 seconds). 23:35:19 tswett: real analog transistors, but I don't see why we can't use them in the digital range 23:35:26 -!- scarf has changed nick to ais523. 23:36:05 (for people who don't know, there are a range of ways to use transistors, but some make them act quite like amplifiers, and others make them act very digitally) 23:39:26 dulla: an infinite tape + a controlling finite state automaton, that's what a turing machine is. 23:39:38 well shit son 23:42:07 -!- Sprocklem has quit (Ping timeout: 255 seconds). 23:53:53 -!- chaosagent has joined. 23:54:25 You know what my favorite analog electronic component is? 23:54:31 The Fourier transformer. 23:59:30 how complex is one of those?