00:05:39 -!- vanila has quit (Quit: Leaving).
00:22:11 <Jafet> EXPBLARGL': given N, take the Nth prime number and split every 3 bits to get a brainfuck program.
00:31:16 -!- GeekDude has joined.
00:34:45 -!- not^v has joined.
00:39:11 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
00:40:55 <Koen_> Jafet: what is the proportion of prime numbers that yields correct brainfuck programs?
00:41:02 <Koen_> and terminating brainfuck programs?
00:41:28 -!- Phantom_Hoover has joined.
00:41:52 <Koen_> and with that I wish you all a good night
00:42:16 -!- Koen_ has quit (Quit: The struct held his beloved integer in his strong, protecting arms, his eyes like sapphire orbs staring into her own. "W-will you... Will you union me?").
00:45:29 -!- doesthiswork has joined.
00:49:25 <cpressey> neither http://esolangs.org/wiki/Underload nor http://esolangs.org/wiki/INTERCAL has been a featured page?!??!
00:50:30 <zzo38> I don't know, but I think it probably ought to be
00:51:26 <ais523> cpressey: basically the problem is that elliott keeps making me do the featured article process, so I can't really feature languages I've had a large hand in for fear of bias accusations
00:51:47 <ais523> admittedly I didn't invent INTERCAL, but I am responsible for much of its recent development
00:51:51 <zzo38> Then other people should try to help too?
00:52:06 <dulla> it's prec prec prec prec
00:52:08 <elliott> I nominate cpressey. he's a sysop and everything
00:52:21 -!- GeekDude has quit (Quit: ZNC - http://znc.in).
00:52:48 <dulla> I nominate Linus Torvald
00:53:16 <elliott> hopefully linus torvalds will go nowhere near the esolangs wiki
00:54:30 <boily> I nominate elliott, because because something something elliott something.
00:54:32 <ais523> I'd be honoured if he did, but I think he has better things to be doing
00:54:39 <dulla> so, is it an issue of needing seven proxies so skiddies don't shit up the place, or what, elliott
00:54:44 <zzo38> I want to nominate cpressey
00:54:55 <ais523> that said, the last C-INTERCAL release /was/ at the request of Donald Knuth
00:54:58 <dulla> like shitting o people that deserve it? ais523
00:55:05 <ais523> we went really fast on that one, just in case it was somehow holding up TAOCP
00:55:37 <dulla> All I know is some big wig, probably torvald gordon ramseys the tech world
00:56:14 <elliott> are you going to get more coherent over time or should I just put you on ignore now
00:56:25 <dulla> I'm having a bad day?
00:56:28 <boily> dulla: I thinkg to gordonramsey is a perfectly cromulent verb.
00:57:05 <dulla> english, where everything is a verb, and an idiom
00:57:28 <dulla> behind seven layers of postmodernism irony, more like it
00:58:16 <oren> Can someone invent a VCS that works on .doc files?
00:58:31 <boily> oren: I thinkg M-Files already does it.
00:58:58 <boily> (ah bordel de... why must I type a g after a k?)
00:59:07 <zzo38> oren: Do you need such thing so much?
00:59:09 <ais523> there's also the "track changes" thing built into Word but it's really bad for VCS purposes IMO
00:59:28 <ais523> you could also just put the .doc files in git or something, it'll still track versions
00:59:31 <ais523> and Word has a diff feature
00:59:41 <ais523> dulla: version control system
00:59:43 <boily> dulla: version control system.
00:59:46 <elliott> http://ben.balter.com/2015/02/06/word-diff/
00:59:56 -!- GeekDude has joined.
01:00:14 <zzo38> Although Microsoft Word isn't really the best way to do these kind of things anyways especially use with VCS
01:00:42 <elliott> hm, http://blog.martinfenner.org/2014/08/25/using-microsoft-word-with-git/ looks fun too
01:03:51 <ais523> "As you work, Word Diff sits on a server (in my case Heroku), waiting for you to push your changes. When you do, it springs into action, automatically converting the Word document to Markdown after each commit:"
01:04:03 <ais523> I'm trying to work out whether this is better or /even worse/ than Word's built-in diff funciton
01:05:20 <ais523> it assumes that Word documents can't have complex formatting at all
01:05:34 <ais523> which in turn, implies that whatever task you're doing, it's one for which Word is the wrong tool
01:06:04 <elliott> well, it assumes that you're okay with diffs that ignore complex formatting things most of the time
01:11:06 <dulla> or makes noobish tuples
01:11:20 <dulla> (<what is this formatting>, "words")
01:15:38 <dulla> and then probably highlight color it to preserve it
01:36:49 -!- oerjan has joined.
01:37:44 <lambdabot> Taneb said 1h 49m 11s ago: Because of you, "hth" has entered my general vocabulary. I am not happy about this circumstance.
01:39:24 <oerjan> myndzi: your script is still broken hth
01:56:02 <zzo38> I almost written the session 63
01:56:32 <oerjan> then you'll have to start using 6 bit numbers!
01:57:13 <oerjan> another one-off joke ruined by off-by-one error
01:57:34 <zzo38> Well, I am using entirely decimal numbers in ASCII for the session numbers here anyways anyone who want to store in binary should probably use at least 16-bits though
01:58:45 <oerjan> i see you are expecting to go on for a while.
01:59:14 -!- not^v has quit (Ping timeout: 246 seconds).
01:59:25 <zzo38> I don't actually know how long it expects to go on, but I expect 16-bits is going to be enough even if it is longer than expected.
02:03:22 <HackEgo> hth is help received from a hairy toe. It is not at all hambiguitous.
02:04:36 <oerjan> are you saying that doesn't help?
02:05:17 -!- not^v has joined.
02:05:20 <dulla> hackego is a hackkkkk
02:05:55 <HackEgo> HackEgo, also known as HackBot, is a bot that runs arbitrary commands on Unix. See `help for info on using it. You should totally try to hax0r it! Make sure you imagine it's running as root with no sandboxing.
02:06:07 <olsner> oerjan: 6 bits is enough to fit 0 to 63, hth
02:07:15 <olsner> this may or may not mean that your joke is still off by one, because 64 will need an extra bit
02:08:08 <oerjan> dead horse floggers anonymous is thataway --->
02:08:43 <oerjan> I MAD LIKE HELL AND CANOT TAKE IT ANY MORE
02:09:11 <dulla> you should become a CTO
02:09:26 <dulla> I hear when the servers go down, the server admins are the least of your problems
02:09:53 <dulla> though that story was probably a joke, it's probably not a lie
02:09:54 <oerjan> no intention to become any kind of O
02:10:56 <olsner> in your case it would have to be CTØ
02:11:37 <dulla> if only I knew what encoding I need to see that
02:11:46 <HackEgo> [U+A66E CYRILLIC LETTER MULTIOCULAR O]
02:12:14 <elliott> was that the first unironic "u mad" in this channel
02:12:35 <oerjan> now _font_ might be a bit harder.
02:12:40 <dulla> I'm already utf-8, oerjan
02:12:47 <oerjan> elliott: is anything dulla says unironic?
02:13:06 <elliott> oerjan: if the answer is no then it might as well be yes
02:13:17 <elliott> if you hide absolutely everything behind irony I'm just going to take you sincerely :p
02:13:20 -!- ProofTechnique has joined.
02:13:42 <dulla> I don't think my oration skills are good enough for intentional irony
02:13:57 <ais523> `addquote <elliott> oerjan: if the answer is no then it might as well be yes
02:14:01 <ais523> that one's good both in context and out of context
02:14:05 <HackEgo> 1232) <elliott> oerjan: if the answer is no then it might as well be yes
02:14:57 <oerjan> dulla: anyway if it's any consolation i cannot see the multiocular o in my client either.
02:15:07 <dulla> It's not descriptive
02:15:18 <dulla> multiocular is not in my scope
02:15:24 <ais523> I can't in mine either, despite the fact that I recently installed a font whose entire purpose is that it contains obscure Unicode
02:15:32 <oerjan> i can only imagine its greatness. or check the logs.
02:15:48 <dulla> or search the unicode site for it
02:16:20 <oerjan> alternatively, i can cut and paste it into my browser, which shows it just fine.
02:17:07 <ais523> mine still doesnt like it
02:17:47 -!- ProofTechnique has quit (Ping timeout: 245 seconds).
02:18:01 * oerjan checks the repository browser now that HackEgo is present again
02:18:19 <oerjan> the only thing of note is shachaf removing pbflistdeluxe.
02:19:18 <oerjan> dulla: i believe there's a separate double o character
02:20:07 <oerjan> that one has upper and lower case variants
02:21:24 <HackEgo> [U+A66C CYRILLIC CAPITAL LETTER DOUBLE MONOCULAR O]
02:21:57 <oerjan> those cyrillic monks had a strange relationship with eyes
02:23:08 <oerjan> https://en.wikipedia.org/wiki/Double_O_(Cyrillic) is one my browser doesn't show either
02:25:20 <zzo38> They don't even agree how many eyes seraphim have, I think?
02:30:24 <lambdabot> Plugin `unmtl' failed with: `StateT IO' is not applied to enough arguments, giving `/\A B. IO -> A (B, IO)'
02:30:30 <lambdabot> Plugin `unmtl' failed with: `StateT s IO' is not applied to enough arguments, giving `/\A. s -> IO (A, s)'
02:31:10 <oerjan> zzo38: it's probably more than you can draw, anyway.
02:36:22 <oerjan> <elliott> for the sake of fantasy i would like you all to believe that i have irc pings hooked up to an alarm <-- works for me
02:46:30 -!- bb010g has joined.
02:49:47 -!- Phantom_Hoover has quit (Ping timeout: 250 seconds).
03:13:33 <oren> Note to self: building a massive watermill complex to power your massive water pumping complex does not work when the pumps drain the very water that powers the watermills.
03:15:32 <boily> oren: playing dwarf fortress?
03:16:04 <oren> now I have watermills over dry land
03:16:32 <oerjan> r.i.p. obsidian apocalypse
03:16:54 <oren> I need to rethink this
03:17:48 <oren> Maybe I'll route a few aquifers into the cistern
03:20:45 <oren> (The cistern exists because the river stops during the winter)
03:21:45 <oren> Here is the massive water mill complex http://snag.gy/Z4QOq.jpg
03:25:13 <oren> It is built to provide 1000 units of power, currently providing 300, which isn't enough to move it
03:33:23 <dulla> i have the feeling this is a dwarf fortress thing
03:36:51 <oren> dulla: yup. It is part of a plan to glass the whole panet
03:37:49 -!- boily has quit (Quit: CLARIFIED CHICKEN).
03:37:53 <dulla> recall the blunderbuss minecart exploit
03:38:13 <dulla> the things you can do with that
03:38:51 <oren> Well, eventually the watermills will be self-powered when the cistern has been filled properly.
03:39:29 <oren> So then I'll have lots of power available to power, well, anything I want
03:39:42 <dulla> and then there is the catapult exploit, I wonder if that works with warheads, too
03:40:19 <dulla> though, you honestly don't need it for catapults, stones are cheap as dirst
03:40:41 -!- not^v has quit (Ping timeout: 252 seconds).
03:40:59 <oren> Ooh a cyclops. pull the lever of death, and pump the pumps of death!
03:41:16 -!- callforjudgement has joined.
03:41:50 <oren> currently, the pumps of death are dwarfpowered. Soon, very soon, they will be water-powered.
03:43:24 <dulla> Wouldn't it be more efficient to have more pumps?
03:44:02 -!- ais523 has quit (Ping timeout: 245 seconds).
03:46:17 <oren> http://snag.gy/6hG8F.jpg shown is a cyclops murdering the merchants, the entrance (currently being pumped full of water to prevent any dwarves being stupid enough to run outside), and part of aqueducts running to the power plant
03:46:50 <dulla> Does pressurised water still do that thing?
03:46:57 <dulla> Where it moves faster than a game tick?
03:47:38 <dulla> It'd be a great way to make sure things in the aquaduct stay in the aquaduct
03:48:04 <HackEgo> danddreclist 63: shachaf nooodl boily \ http://zzo38computer.org/dnd/recording/level20.tex
03:50:17 <oren> The merchants are leaving, porbably because their merchandise is being carried away by pressurized water
03:50:45 <oren> oh and because most of them have been dismembered by a cyclops
03:51:14 <dulla> it's probably the dismemberment
03:51:28 <dulla> You know how the merchants can't take the heat
03:52:13 <zzo38> Do you like this level20.tex? This is the one involving the rune caster
03:53:45 <oren> the cyclops apparently dorwned before the magma could even getnear it
03:54:04 <oren> or maybe the merchants killed it.
03:58:23 <oren> "some migrants have arrived, despite the danger"
04:00:46 <oren> Oh come on guys, come right on in, never mind the drowned merchants and cyclopes...
04:07:29 -!- MDude has changed nick to MDream.
04:08:38 <oren> http://snag.gy/Obzd2.jpg
04:22:24 -!- callforjudgement has quit (Read error: Connection reset by peer).
04:22:32 -!- callforjudgement has joined.
04:26:34 <oerjan> eek anagol's recent entries has moved too fast
04:28:05 <oerjan> surely it used to be more than 24 hours before?
04:34:19 -!- cpressey has quit (Ping timeout: 256 seconds).
04:41:19 -!- cpressey has joined.
05:09:24 -!- ProofTechnique has joined.
05:11:35 -!- callforjudgement has quit.
05:12:06 -!- callforjudgement has joined.
05:17:09 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)).
05:36:26 -!- dianne has quit (Ping timeout: 264 seconds).
05:38:10 -!- dianne has joined.
05:38:58 -!- chaosagent has joined.
05:39:16 -!- doesthiswork has quit (Quit: Leaving.).
05:54:46 -!- callforjudgement has quit.
05:55:02 -!- callforjudgement has joined.
06:05:14 -!- cpressey has quit (Ping timeout: 264 seconds).
06:06:33 <oren> Oh shit, a miner was caught in a cave in, got confused by the dust, and fell into the cistern.
06:07:33 <oerjan> is the water undrinkable now
06:08:22 <oren> I dunno. Hopefully we can wash the blood away after the fishermen retrieve the corpse.
06:09:23 <oren> This is why I hate using cave ins, though it is sometimes necessary
06:10:07 <oerjan> will they now all die from waterborn disease
06:10:41 <oren> I don't think that's modeled, though I could be wrong. In any case they have plenty of booze to drink
06:12:10 <oren> The cistern is for the generation of energy during the winter when the river stops.
06:12:13 -!- cpressey has joined.
06:13:23 <oren> holy crap, hes actually alive still.
06:14:00 <oren> and he swam out! he's a good swimmer I guess
06:14:53 <oerjan> all's well that ends well
06:15:38 <oren> with luck now I can pressurize the cistern
06:16:18 <oren> thus having a way to literally blast enemies to death
06:27:48 <oerjan> <elliott> is this the onion <-- possibly r/nottheonion?
06:29:55 -!- cpressey has quit (Ping timeout: 256 seconds).
06:37:04 -!- cpressey has joined.
06:40:17 -!- hjulle has quit (Ping timeout: 245 seconds).
06:44:46 <oren> It appears that drowning merchants is a good way to get free stuff
06:46:18 <zzo38> That's your way of getting free stuff?
06:46:54 <oren> Well they come every season, even if i drown them every season, so yeah
06:47:25 <oren> I seal the doors and pump water into the trade depot
06:47:54 <zzo38> It seems like merchants should sue you if that happen a lot it will be recognized?
06:48:08 <oren> I dunno, we'll see
06:48:23 <oren> If they try to sue me I'll drown thelawyers
06:52:32 -!- cpressey has quit (Ping timeout: 246 seconds).
06:52:33 <oerjan> @tell fizzie btw the wiki bridge isn't working either hth
06:53:53 -!- cpressey has joined.
06:55:43 <oerjan> `addquote <Taneb> cpressey, Agda is a function that maps cabal install to an electric heater
06:55:56 <HackEgo> 1233) <Taneb> cpressey, Agda is a function that maps cabal install to an electric heater
06:56:31 -!- oren has quit (Ping timeout: 244 seconds).
06:58:39 <zzo38> O, that's what it is?
06:59:06 -!- cpressey has quit (Ping timeout: 244 seconds).
07:01:43 <bb010g> I wish Haskell would steal Agda's operator syntax. If then else is so nice there.
07:42:46 -!- CADD has joined.
07:57:25 -!- callforjudgement has quit (Ping timeout: 264 seconds).
08:29:42 -!- oren has joined.
08:32:09 <oren> I am now testing to see if killing merchants over and over has any consequences
08:35:06 <oren> I have started a new game, and built the depot in an area designed so I can flood it whenever I want
08:56:50 -!- CADD has quit (Ping timeout: 264 seconds).
10:02:18 -!- Phantom_Hoover has joined.
10:16:51 -!- cpressey has joined.
10:17:06 <cpressey> I just wrote my first Agda program!
10:17:14 <cpressey> Actually, I typed it in from a book
10:23:20 <cpressey> and yes, I am an esowiki sysop I think, so if someone wants to bug me to slap a green checkmark on the Underload page and put an abstract on the front page,... do that
10:24:56 -!- oerjan has quit (Quit: Famous last words).
10:25:28 -!- oerjan has joined.
10:25:47 -!- oerjan has quit (Client Quit).
10:30:20 <cpressey> oh, oh, "famous last words", right, right
10:30:27 <cpressey> this is mediawiki we're talking about
10:52:29 -!- kapil___ has quit (Quit: Connection closed for inactivity).
11:01:47 <cpressey> Jafet: I did consider prime numbers, but, y'know... PRIMES is in P. can't be too careful.
11:02:29 -!- cpressey has quit (Quit: leaving).
11:39:51 -!- SopaXorzTaker has joined.
11:40:37 <fizzie> Why does that thing have such a ridiculous number of underscores in it.
11:40:48 -!- zemhill___ has quit (Remote host closed the connection).
11:41:11 -!- zemhill has joined.
11:43:21 <fizzie> Oh, the wiki bridge. Blah. I'll try to remember to fix that, though it would be easier with proper internet.
12:00:04 -!- vanila has joined.
12:00:34 -!- Patashu has quit (Ping timeout: 255 seconds).
12:16:25 -!- kapil___ has joined.
12:38:00 -!- chaosagent has quit (Ping timeout: 252 seconds).
13:06:48 -!- oren has quit (Quit: Lost terminal).
13:37:29 <vanila> http://jzt.xyz/worlds/village-of-jzt
13:54:19 -!- boily has joined.
13:57:39 -!- boily has quit (Client Quit).
13:59:46 -!- boily has joined.
14:06:57 <boily> elliott: helliott. CAO is down :(
14:09:23 -!- reynir has quit (Quit: brb).
14:12:20 <elliott> boily: play on cdo or cszo or whatever?
14:12:26 <elliott> there's like fifty servers these days aren't there
14:17:21 <boily> it doesn't feel right, but I'm on CDO.
14:19:13 <elliott> cdo has always been the cool server
14:19:44 <boily> let me dehuge my term.
14:21:13 <elliott> I have no idea whaty ou do when you do that but it definitely doesn't make your terminal any smaller :P it's fine though I can just make my font tiny
14:23:32 <boily> I put in 80x24 for the max width and height?
14:23:49 <elliott> I mean, you can tell there's more than 80 columns and 24 rows to your terminal right now, right >.>
14:24:09 <elliott> it's fine though I just made my font smaller and now it fits on my screen
14:24:24 <boily> aaaah. it goes with the terminal size. makes sense. tdh
14:24:37 <boily> I like my terminal to be full screen :D
14:26:13 <elliott> you could "stty cols 80 rows 24" before running ssh I guess but that'd lead to a hell of a lot of wasted space
14:28:52 * boily is hungry and should go breakfast...
14:33:17 -!- heroux has quit (Ping timeout: 256 seconds).
14:35:06 -!- heroux has joined.
14:36:57 -!- MDream has changed nick to MDude.
14:42:29 -!- kapil___ has quit (Quit: Connection closed for inactivity).
15:13:17 -!- hjulle has joined.
15:23:58 -!- int-e has quit (*.net *.split).
15:23:59 -!- kline has quit (*.net *.split).
15:24:05 -!- int-e has joined.
15:24:05 -!- lambdabot has quit (Quit: brb).
15:25:41 -!- kline has joined.
15:28:06 <vanila> what program could i use on linux to measure/grapha processes memory use?
15:28:16 -!- doesthiswork has joined.
15:28:34 -!- lambdabot has joined.
15:29:45 <boily> elliott: breakfasting is dangerous here. a haircut happened.
15:30:04 <boily> vanila: vanelloa. ksysguard perhaps?
15:59:55 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
16:02:02 -!- Phantom_Hoover has joined.
16:03:46 -!- SopaXorzTaker has quit (Ping timeout: 265 seconds).
16:16:15 -!- SopaXorzTaker has joined.
16:24:13 -!- SopaXorzTaker has quit (Read error: Connection reset by peer).
16:26:40 -!- aretecode has quit (Read error: Connection reset by peer).
16:30:48 -!- aretecode has joined.
16:53:00 -!- GeekDude has joined.
16:59:42 -!- Koen_ has joined.
17:00:30 -!- Phantom_Hoover has quit (Ping timeout: 244 seconds).
17:00:36 -!- Phantom__Hoover has joined.
17:02:21 -!- Tritonio has joined.
17:02:34 -!- FreeFull has quit (Quit: BBL).
17:17:50 <lambdabot> freshname. Return a unique Haskell project name.
17:18:44 <int-e> It starts out with "Ha" and adds some random letter. VERY useful.
17:19:09 <vanila> its generating a fresh symbol
17:19:20 <lambdabot> Plugin `compose' failed with: Unknown command: "fresh"
17:25:59 <vanila> my program has a new bug
17:26:08 <vanila> it is segfaulting before it even reaches line 1
17:26:16 <vanila> i dont know what is going on !
17:27:48 <vanila> how do i even debug this.
17:31:31 <boily> vanila: which language?
17:33:32 <boily> what #includes do you have? any esoteric, anormal, unusual or experimental libraries?
17:38:37 <vanila> it was working a second ago
17:38:40 <vanila> and we just changed one function
17:42:43 <Koen_> also did you include some .h that you wrote yourself?
17:43:07 <Koen_> and which you changed less than a second ago?
17:50:24 <vanila> it's really fascinating a weird way
17:50:32 <vanila> i hope i get to the bottom of it, but i really have no idea how
17:50:41 <vanila> i looked at the assembly code for the prelude of main but i cant understand it
17:53:30 <Koen_> vanila: can you show us what you changed in the .h ?
17:56:49 <vanila> i didnt change any headers
18:00:15 <Koen_> and if you put a putstr as the very first line of the main it's not printed out?
18:00:31 <Koen_> or a printf("\n");
18:00:32 <vanila> that shouldn't be possible
18:01:00 <Koen_> (don't omit the \n to flush the output)
18:02:33 -!- Phantom__Hoover has quit (Ping timeout: 250 seconds).
18:35:33 -!- cpressey has joined.
18:36:08 <vanila> i wonder if it's theoretically impossible cpressey - maybe focus on proving that rather than making a language?
18:36:13 <cpressey> the compiler can always artificially extend the program by adding e.g. +- to the front of it, then it knows there's a shorter program
18:36:48 <cpressey> i'm sure it's not theoretically impossible, because int-e
18:37:16 <cpressey> turn brainfuck program into integer, program is ackermann of that integer
18:40:15 <cpressey> but it has sort of raising an interesting conjecture, which is
18:40:43 <cpressey> if the mapping from TM's to language X programs is complex, running programs in language X will also be complex
18:41:30 <cpressey> which sounds perfectly intuitive, but -- no idea how one would go about proving it
18:41:51 <cpressey> other things I have failed at this weekend: Agda
18:42:02 <vanila> yes I agree about the 'if mapping, then running' thing
18:42:13 <vanila> that's what I realized from the idea of encrypted source code
19:06:12 -!- TieSleep has changed nick to TieSoul.
19:12:28 -!- boily has quit (Quit: RELATIVE CHICKEN).
19:14:47 <cpressey> hmm, maybe EXPBLARGL could force to try all the permutations of the program -- wouldn't work well with brainfuck because +- = -+ ... but maybe some other language
19:16:06 <cpressey> nah, i think you could still inject some kind of "identity" instruction, then you know there's another permutation that also works
19:16:18 <cpressey> maybe i'll keep banging my head against agda
19:16:39 <vanila> i could help with agda maybe?
19:18:27 <elliott> cpressey: did you ever figure out the Burro/Cabra type things
19:18:51 <vanila> https://www.youtube.com/watch?v=uxRjp4LVuo4
19:18:52 <bluckbot> YouTube 「title: Amor incondicional entre un burro y una cabra」 「uploaded by: Univision Noticias」 「duration: 00:01:21」 「views: 6413」 「likes: 67」 「dislikes: 0」
19:19:18 -!- ChanServ has set channel mode: +o elliott.
19:19:20 -!- elliott has kicked bluckbot bluckbot.
19:19:41 <elliott> 2015-02-17.log:07:08:01 <dulla> oerjan kick bluckbot
19:19:43 -!- elliott has set channel mode: -o elliott.
19:20:01 <elliott> that's one garish YouTube logo colour
19:20:18 <vanila> Unconditional love between a donkey and a goat
19:25:17 <elliott> stronger algebraic structures
19:26:00 <cpressey> There, and elsewhere, I basically ran up against "imaginary functions" and gave up
19:26:28 <elliott> there was something about being able to do gcd on programs
19:26:32 <cpressey> been meaning to add I/O to Burro and to rewrite the docs, but
19:26:43 <cpressey> yeah that's a... what's it called
19:26:49 <elliott> hmm, what kinda imaginary functions
19:27:01 <vanila> You can take the derivative of a lambda term
19:27:12 <vanila> there's a new paper about it, it's silly but neat
19:27:30 <cpressey> http://esolangs.org/wiki/Imaginary_function
19:28:41 <cpressey> vanila: given the awesome power of taking a derivative of a CFG, I dunno, this could all be very wild
19:30:19 <cpressey> really can't even get near rings, I don't know how one would get up to integral domains and such
19:30:51 -!- naturalog has quit (Ping timeout: 244 seconds).
19:31:13 <elliott> vanila: do you have a link to that paper?
19:31:42 -!- naturalog has joined.
19:31:51 <vanila> http://www.informatik.uni-marburg.de/~pgiarrusso/papers/pldi14-ilc-author-final.pdf
19:32:00 <elliott> cpressey: with imaginary functions: isn't it simple enough to just to add thunk(F) where F is a function to your primitive values
19:32:05 <elliott> and have apply send thunk(F) to F
19:32:06 <vanila> they get some good results speeding up code with it
19:32:10 <elliott> not exciting, but it seems to meet your spec just fine
19:32:29 <vanila> applied to pure lambda calculus, it has no effect
19:32:40 <vanila> its' only when you make special primitives with differentiation support
19:32:44 <vanila> just to spoil the ending
19:34:44 <cpressey> i think that's occurred to me but i got too sick of it to follow up on it
19:35:13 <elliott> as in data Expr = ... | Thunk Expr | Apply Expr | ...; data Value = ... | NativeFn (Value -> Value) | Closure Env Args Expr | ThunkV Value | ...; ... eval (Apply e) = apply (eval e); eval (Thunk e) = thunk (eval e); ...; apply (ThunkV v) = v; ... thunk v | isFun v = ThunkV v | otherwise = undefined or whatever
19:35:21 <elliott> it's sorta like adding an axiom
19:35:25 <cpressey> basically you'd have a type constructor Thunk x and (apply Thunk x = x) but apply (a-real-function-value) would actually apply it
19:36:02 <cpressey> istr thinking there was some little bumpy inconsistency. but if there isn't
19:36:49 <cpressey> yeah maybe you could invert things, or at least pretend to, to cover "for every X there is a -X" type axioms in algebraic structures
19:36:57 <elliott> I should get back into esolangs.
19:38:02 <elliott> data Unit : Set where tt : Unit; apply : forall {A} -> (Unit -> A) -> A; apply f = f tt
19:38:50 <elliott> probably best not to think about this kind of thing in a setting with types
19:40:38 <cpressey> I can't wrap my head around Agda. writing a function and writing a proof are seperate things in my head, and it wants me to moosh them together
19:41:13 <cpressey> I write my theorem as....... a type? Of a function? Then write the proof as the body of the function?
19:41:55 <vanila> values are proofs and types are propositions
19:42:07 <vanila> lambda is used to prove implication
19:44:29 <cpressey> Here are two very simple propositions, the
19:44:29 <cpressey> true proposition and the false proposition:
19:44:46 <elliott> that's one awkward way to present it
19:44:46 <cpressey> indent didn't get preserved :(
19:44:56 <elliott> data True : Set where { true-is-true : True }
19:44:57 <cpressey> sign that I'm reading maybe not the best paper, huh
19:45:00 <elliott> might be clearer than that record silliness
19:45:11 <vanila> yeah elliott s way is much nicer
19:45:17 <elliott> there are reasons to use the record one For Real
19:45:27 <elliott> but it's not exactly great pedagogically
19:46:10 <cpressey> ok, so in the above, "False" is not a value, it's a proposition.
19:46:32 <elliott> (because types are values)
19:46:32 <vanila> wellll... it's a type but types are values....
19:46:50 <elliott> think of haskell where all the levels are collapsed
19:47:03 <elliott> instead of values having types which have kinds it's just values have types (which are values)
19:47:16 <elliott> ...but not just any values! they have to be type-typed values. I'm helping
19:47:32 <cpressey> "I'm helping" is the new "hth"
19:47:49 <vanila> A good thing to try is proving thinsg with lambda
19:47:53 <elliott> you can do, like, helping : if true then Nat else Bool
19:48:03 <vanila> not geetting data types involved first
19:48:27 <vanila> theorem1 : (P : Set) -> (Q : Set) -> P -> Q -> P
19:48:32 <cpressey> I got as far as defining the Peano numbers
19:48:58 <vanila> and theorem2 : (P : Set) -> (Q : Set) -> P -> (P -> Q) -> Q
19:49:12 <elliott> theorem1 : forall {P Q} -> P -> Q -> P would be even better for avoiding thinking about types
19:49:38 <b_jonas> aren't there libraries for these things?
19:49:56 <elliott> cpressey: if it helps at all for understanding how to write proofs as lambda terms: you use modus ponens by application
19:50:15 <elliott> to prove Q from (P -> Q) and P, let's say we have proofs p-implies-q : P -> Q and p : P
19:50:21 <elliott> then we have the proof p-implies-q p : Q
19:50:56 -!- bb010g has quit (Ping timeout: 265 seconds).
19:50:56 -!- supay has quit (Ping timeout: 265 seconds).
19:50:56 -!- mbrcknl has quit (Ping timeout: 265 seconds).
19:51:13 <cpressey> i see a type signature (that is to say, proposition (that is to say, theorem)) for a function called theorem1, above.
19:51:25 -!- jameseb has quit (Ping timeout: 265 seconds).
19:51:27 <cpressey> let's go with elliott's version
19:51:55 <cpressey> as i understand it they're NOT that different
19:52:06 <cpressey> one has explicit types passed to it, is all
19:52:09 <elliott> they are the same logically
19:52:18 <elliott> yeah in one of them the set arguments are implicit
19:52:23 -!- fractal has quit (Ping timeout: 265 seconds).
19:52:34 <elliott> which is more natural if you're thinking of them as foralls
19:52:52 -!- spiette has quit (Ping timeout: 265 seconds).
19:53:25 <cpressey> how do you implement it, and why? theorem1 p q -> p ? that makes no sense
19:53:42 <cpressey> sorry, there should be a = in there
19:53:48 <elliott> cpressey: think of it like
19:53:50 -!- merdach has quit (Ping timeout: 265 seconds).
19:54:14 <elliott> the (p :)s giving labels to the proofs
19:55:05 <elliott> if we have a proof p of P and a proof q of Q, then we can prove P with p
19:55:55 <elliott> (if we have a proof x of P -> Q and a proof y of P, then we can prove Q with modus ponens on x and y; theorem2 : forall {P Q} -> (P -> Q) -> P -> Q; theorem2 x y = x y)
19:56:28 -!- merdach has joined.
19:56:32 -!- Tritonio has quit (Ping timeout: 252 seconds).
19:56:38 <elliott> it's like deducing P, Q |- P except you label everything in the context
19:57:00 <vanila> well i was trying to leave theorem1 and theorem2 undefedin so cpressey could use them for practice
19:57:15 -!- spiette has joined.
19:57:35 <cpressey> i have no idea how you "practice" that
19:57:39 -!- mbrcknl has joined.
19:57:43 -!- jameseb has joined.
19:58:06 -!- supay has joined.
19:58:37 <elliott> you can just think of "theorem1 p q" as syntax for "by theorem1, using p and q as the assumptions P and Q", so that's giving a definition for how the proof works
19:59:25 <vanila> i looked up 'learn you an agda' it seems way more difficult than things need to be
19:59:39 <cpressey> vanila: well, it's only 2 pages, and the 2nd one is under construction
19:59:47 <vanila> I can write a much simpler tutoral
19:59:51 <vanila> that is easier to learn from
20:00:24 <cpressey> the problem, one problem, is that modus ponens has a conjunction in it, doesn't it? if p -> q, and if p, then q
20:00:38 <cpressey> i mean there are too many "ifs" in my description but
20:00:45 <elliott> ok yes it's using currying
20:00:51 <elliott> "if p -> q, then if p, then q"
20:01:04 <elliott> you can use conjunction if you want though
20:01:07 -!- incomprehensibly has quit (Ping timeout: 250 seconds).
20:01:12 <elliott> but that involves data types :P
20:01:20 <elliott> think of propositional logic with just -> as the connector
20:01:40 <elliott> and the metalogical deduction rule "if you have a proof of (P -> Q) and you have a proof of P, then you have a proof of Q"
20:02:11 -!- fractal has joined.
20:02:17 <elliott> we have that rule in agda, and we write it syntactically by putting the proof of (P -> Q) and the proof of P adjacent: proof-of-imp proof-of-P is a proof of Q
20:02:19 -!- Patashu has joined.
20:02:24 -!- incomprehensibly has joined.
20:04:17 <vanila> if f : P -> Q (f is a proof that P implies Q)
20:04:23 <vanila> and x : P (x proves P)
20:04:31 <vanila> then f x : Q (f of x proves Q)
20:05:46 -!- bb010g has joined.
20:05:51 <cpressey> i'm going to look for a different proof system. this one sucks.
20:06:10 <vanila> if you still want dependent types
20:06:27 <elliott> yeah, and then he gets to learn "match"
20:07:44 -!- nyuszika7h has quit (Read error: Connection reset by peer).
20:09:26 -!- nyuszika7h has joined.
20:09:54 <cpressey> http://at.metamath.org/index.html
20:19:07 <cpressey> the rainbow colouring and serif font do kind of scream "1999", i admit
20:20:08 -!- bb010g has quit (Quit: Connection closed for inactivity).
20:24:52 -!- Patashu has quit (Ping timeout: 240 seconds).
20:30:19 <elliott> good luck reading metamath proofs in their source form
20:34:24 <cpressey> looks like forth with lots of $'s
20:37:33 <int-e> I'm reading proofs and the typesetter "corrected" "well-founded" to "well founded".
20:38:08 <int-e> (so now we have a well founded relation. great.)
20:41:30 <cpressey> i read a horror story once about a publisher "correcting" "homeomorphism" to "homomorphism" (in a paper which also contained instances of "homomorphism")
20:41:49 -!- FreeFull has joined.
20:42:57 * cpressey sighs and tries the other paper, the one that doesn't define True as a record type
20:44:24 <int-e> (Another ... fun ... thing is that we use \mathsf{} in our paper. The computer modern scripts all have the same x-height and work well together. With the publisher's font the sans-serif characters look *big*)
20:44:27 <FreeFull> Why would one define True with a record type?
20:45:15 <int-e> But I'm more upset about having to go through everything word by word because I expect some more nasty surprises.
20:45:30 <int-e> (At least we have no homeomorphisms.)
20:47:11 <int-e> They also changed non-variable (meaning: not a variable) to nonvariable. Isn't that great...
20:47:44 <cpressey> FreeFull: to avoid elliott 's true-is-true thing, see above
20:49:26 <cpressey> i do hope it's a well founded nonvariable
20:53:45 -!- TieSoul has changed nick to TieSleep.
20:58:44 <cpressey> apparently this is the same paper
21:02:20 -!- bb010g has joined.
21:03:12 -!- TieSleep has quit (Ping timeout: 245 seconds).
21:06:07 <FreeFull> cpressey: I'll look in the logs
21:10:30 -!- TieSoul has joined.
21:10:32 <cpressey> oho http://oxij.org/note/BrutalDepTypes/
21:17:08 <cpressey> much clearer descriptions of some things
21:18:18 -!- TieSoul_ has joined.
21:18:37 -!- TieSoul has quit (Ping timeout: 245 seconds).
21:24:40 -!- doesthiswork has quit (Quit: Leaving.).
21:37:43 <cpressey> bugs me that -> is more like punctuation than a function constructor in this thing
21:42:57 <vanila> X -> Y could be thought of a syntactic sugar for (_ : X) -> Y
21:43:00 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)).
21:45:43 <cpressey> ah, there's no way. i'm too old for this.
21:53:09 <cpressey> and although it would be really cool to use metamath to prove properties of functions *starting from ZFC*
21:53:39 <cpressey> i think the obvious thing for me to do is write my own proof-checking language instead
21:59:36 -!- Phantom__Hoover has joined.
22:00:12 <cpressey> and, strangely, easier than learning Agda.
22:02:21 <b_jonas> I wouldn't think it'd be easy, but then, if you want to create a new esolang, I won't stop you in this channel.
22:12:39 <cpressey> tbh, i have had some ideas about one for a long time, but never went as far as implementing them. also, nb: proof-checker, not theorem-prover
22:16:41 <cpressey> there's a checker for metamath in 300-odd lines of Python, so it can't be ridiculously hard.
22:28:34 -!- cpressey has quit (Ping timeout: 245 seconds).
22:34:13 -!- AndoDaan has joined.
22:35:22 <AndoDaan> How do I ask for my messages again?
22:40:10 <AndoDaan> And how to record a message for someone?
22:40:54 <vanila> @tell AndoDaan like this
22:41:30 <AndoDaan> Grand. Thanks. I wish I had a better memory. Or more discipline to keep a cheat-sheet.
22:42:45 -!- Lymia has quit (Ping timeout: 250 seconds).
22:42:57 <AndoDaan> @tell mroman I actually took a look at the p section of FMNSSun a few days ago. And I'm thinking p~ still might be a little too complex for me atm.
22:45:47 -!- Lymia has joined.
23:01:09 <fizzie> Wiki gateway should be up now.
23:05:17 -!- spiette has quit (Ping timeout: 250 seconds).
23:14:29 <fizzie> The thing that puts esowiki edit info on the channel.
23:14:53 <fizzie> You know, the [wiki] things.
23:15:22 <fizzie> (It was allegedly down.)
23:15:49 <AndoDaan> Ah, thought it was something new
23:19:51 -!- arjanb has quit (Quit: zzz).
23:21:42 -!- Phantom__Hoover has quit (Read error: Connection reset by peer).
23:23:59 -!- chaosagent has joined.
23:27:16 -!- J_Arcane_ has joined.
23:28:31 -!- J_Arcane has quit (Ping timeout: 244 seconds).
23:28:38 -!- Phantom_Hoover has joined.
23:28:40 -!- J_Arcane_ has changed nick to J_Arcane.
23:31:36 -!- GeekDude has joined.