00:00:03 btw is it even possible to write a non-trivial 2/3 polygot 00:00:04 ? 00:00:08 Yes. 00:00:16 import sys; prunt = sys.stdout.write 00:00:20 prunt('Hello, world!\n') 00:00:21 ehird, maybe it wasn't, maybe it was just in #esoteric 00:00:25 It's not hard if you keep within the boundaries. 00:00:48 ehird, it is harder writing a C extension that works with both indeed 00:00:54 AnMaster: so don't do that 00:00:55 usually i want my randomization done in interesting and novel ways 00:00:59 since nobody uses 3 00:01:00 ehird, why not? :/ 00:01:09 well nobody uses 3 because nothing supports it 00:01:18 Untrue: work is underway. 00:01:20 It's not too stable yet. 00:01:28 the only way to make more people use it would be to support it 00:01:49 ehird, well I found a crash bug in python 3 thanks to porting a C extension 00:02:39 -!- M0ny has quit ("Quit"). 00:02:51 because of a bug in one of the the C API functions that tried to convert a PyUnicode to PyByterray twice, in an unchecked way 00:03:35 Reported it? 00:03:58 yes 00:04:58 ehird, yes I tried to, but the bug reporting system never managed to send me the confirmation email 00:05:05 so I was unable to report it 00:05:09 -!- Gracenotes has joined. 00:05:15 probably the issue is at my isp 00:05:16 meh 00:05:41 Hey, when I get bogons I can be pretentious about my ISP. 00:05:43 It's the little things! 00:05:50 hah 00:06:11 ehird, anyway I forgot what exact API call it was by now. I worked around it in some way iirc 00:07:09 ehird, I did report it in #python with a note about that the bug tracker was broken for me. 00:07:54 night 00:08:08 (really, I need to go up early tomorrow so...) 00:08:45 Another installment in the "That classes as _music_?" series: http://www.youtube.com/watch?v=_po0RTKjsC8&fmt=18 00:16:29 okay that's awesome 00:19:12 oklopol_: it goes on for 30 minutes 00:19:15 in the real shows 00:19:18 apparently it reaches 120dB 00:19:48 oh it actually sounds like that 00:19:51 coool 00:20:00 :D 00:21:30 http://forum.slicehost.com/comments.php?DiscussionID=3234&page=1#Item_0 00:21:32 Fail. 00:24:15 Hm. 00:24:21 As far as I can tell, bogons is just two people. 00:24:21 XD 00:31:10 so i go into a huge directory and grep foo -R . 00:31:20 this takes like 3 minutes 00:31:36 but grepping a tarball of the same directory only takes 15 seconds 00:33:23 bsmntbombdood: directory iteration is slow 00:33:30 and, well, files in general. 00:34:13 there's a stat,open,and close for every single file :/ 00:34:46 how can i make this faster? 00:34:56 bsmntbombdood: don't grep a directory tree. 00:35:03 consolidate multiple files. 00:35:12 that's annoying 00:35:15 yes. 00:35:17 Filesystems are. 00:38:19 ... 00:40:42 -!- oerjan has joined. 00:40:48 bsmntbombdood: What? 00:41:00 that's not a soluiton 00:41:11 ehird: koalas 00:41:15 bsmntbombdood: Well, there's no other solution. 00:41:19 That's how the fs apis are. 00:42:11 -!- FireFly has quit ("Later"). 00:42:11 ... 00:42:27 bsmntbombdood: Do you have a language impediment? 00:43:26 ... 00:43:31 Clearly. 00:44:01 there's got to be a good way to do it 00:44:13 bsmntbombdood: sorry to disappoint 00:44:42 was just wondering could there be an infinite vector space for which there is no linearly independent subset which generates the space 00:45:09 oerjan: so whether they always have a basis 00:45:18 but found out yes they do 00:45:24 13:29:18 Intuition says 'no' 00:45:24 13:29:27 But I guess with the AoC anything can happen ;-P 00:45:26 but just write your response 00:45:33 in fact AoC is used in the proof 00:45:44 heh. 00:45:47 and it's "yes" 00:46:24 wait the axiom of death is used in it and it's on the same course as me 00:46:29 sounds dangerous 00:46:33 axiom of death :D 00:46:47 the axiom of death: exists P. P&~P 00:47:34 or more directly, you use Zorn's lemma 00:48:10 ah that's actually just a few pages down the material 00:48:19 i think i'll leave it for next week 00:48:22 basically, if you have an independent set which does _not_ generate all, you can always extend it, and you can take the union of a chain of them 00:48:45 ah 00:48:54 and then you just take the smallest supremum 00:48:55 so Zorn's lemma applies to say a maximal chain generates all 00:49:15 or is it infimum 00:49:21 there's no _the_ smallest supremum, because the extension is not unique 00:49:28 hmm true 00:49:37 hmm wait 00:49:43 does exists P. P&~P actually break anything 00:49:44 (also supremum is always smallest by definition 00:49:45 ) 00:49:48 I mean you still can't get to a P 00:50:01 ehird: yes you can 00:50:07 orl 00:50:08 y 00:50:08 how 00:50:17 ehird: assume there exists P such that P&~P, then true=false => everything is true 00:50:38 well right 00:50:42 oklopol_: that's not quite a first order proof though 00:50:43 I was concentrating on the 'exists P.' part 00:50:50 oerjan: indeed is not. 00:51:16 i want a "schaum's mathematical handbook with proofs" 00:51:44 oklopol_: also, Zorn's lemma is needed exactly to know that a maximal set exists 00:52:22 ah yes 00:52:31 P => (A => P) is an axiom 00:53:03 or can be, anyway 00:53:40 er it is? 00:53:44 so you get for that P, A => (P & ~P) 00:53:47 oerjan: that's not true, because what if P is true by an axiom 00:53:51 then there's no A 00:54:08 huh 00:54:18 ehird: em now i'm also using the P&~P hypothesis 00:55:02 -!- neldoreth has quit ("Lost terminal"). 00:55:19 maybe this is overkill 00:55:42 ~P = P => false 00:55:54 so P & ~P => false 00:56:07 and false => A is an axiom 00:56:51 that's pretty much what i was going for 00:57:15 yeah 00:57:31 yes but there's a reason I said 'exists' 00:57:33 * ehird shrug 00:57:34 so P & ~P => A (which could also be an axiom) 00:57:37 i'mw rong :) 00:57:54 well then you need to use the quantifier rules 00:58:44 ah yes 00:59:10 exists P. P & ~P => exists P. A 00:59:18 if that's not an axiom, it's close 00:59:34 finally, you can remove existentials if the variable is unused 01:00:03 err what does that mean? 01:00:15 exists P. A => A 01:00:23 ah 01:00:29 * (exists P. A) => A 01:00:42 yes ofc 01:02:12 of course since the set of axioms can vary by formulation, this is all a bit wishy-washy 01:02:44 *axioms/deduction rules 01:03:18 P => ~P ← tip: Use "really untrue" things. 01:03:34 yes kinda like a broken washing machine 01:03:53 P => ~P is equivalent to ~P, anyway 01:04:22 more like ~P & ~P 01:05:10 well in principle, but A => B = ~A \/ B (in classical logic), not & 01:05:36 point is the redundancy was relevant to ehird's weird point 01:05:50 also P => ~P is equivalent to ~P with just intuitionist logic 01:05:55 i was formulating new logic 01:06:00 you have regular true things which are untrue 01:06:04 so you have to use really untrue things 01:06:06 to distinguish 01:06:09 really untrue = ~~~ 01:06:39 oerjan: what do you mean with just intuitionistic logic? 01:06:42 *intuitionist 01:06:49 oh 01:07:06 actually isn't intuitionist logic a well-known logic, probably referred to that 01:07:08 intuitionist logic is a logic where the excluded middle doesn't hold, among other things 01:07:16 yeah 01:07:29 and where you cannot rewrite => & \/ in terms of each other 01:07:37 i've just had one course in logic, and it was more about proving stuff than the general philosophical issues 01:07:39 although ~P = P => false still 01:07:50 and by philosophy i mean other kinds of logics 01:08:37 Under the Curry-Howard isomorphism, Peirce's law is the type of continuation operators, e.g. call/cc in Scheme[1]. 01:08:41 that's fucking hot 01:08:48 yes 01:09:01 Peirce's law? 01:09:13 oklopol_: ((p->q)->p)->q 01:09:19 curry-howard isomorphism is like the best ting to happen to programming 01:09:44 intuitionistic logic corresponds to ordinary typed lambda calculus, while classical logic (with peirce's law etc.) corresponds to a lambda calculus with continuations 01:09:46 hard to say, i don't understand it. 01:09:53 oklopol_: 01:10:00 modusPonens :: (p -> q, p) -> q 01:10:01 proof: 01:10:05 modusPonens (f,x) = f x 01:10:08 (,) = and 01:10:10 Either = or 01:10:14 (->) = guess 01:10:27 Not a = a -> Void 01:10:30 (where "data Void") 01:11:05 yeah i've seen the definitions in many forms 01:11:13 so how don't you understand it 01:11:19 type = proposition, non-bottom implementation = proof 01:11:33 ah well that makes more sense 01:12:06 falseImpEverything :: Void -> a 01:12:12 i mean just seeing a syntactical mapping between types and logic doesn't really tell me much. 01:12:17 falseImpEverything x = case x of {} 01:12:25 oerjan: cheat 01:12:28 that's a bottom implementation 01:12:29 not allowed 01:12:33 ehird: no it is not 01:12:36 err k 01:12:46 because Void has no constructors 01:12:47 (although you can't get any (Not a) with no-bottom rule, so maybe we need a better definition) 01:12:56 (i mean maybe I am wrong) 01:13:14 hm sure you can 01:13:17 how 01:13:25 there's no value of type Void that isn't bottom 01:13:36 but Not a is not Void 01:13:45 it's (a -> Void) 01:13:52 oerjan: youc an't implement that 01:13:53 surely 01:13:54 so you need to start with a contradiction 01:14:06 well you said _any_ Not a 01:14:17 there are specific a's you can get 01:14:22 oerjan: liek? 01:14:23 Not Void being one 01:14:28 well okay 01:14:41 i guess you have to go into axiom land to get more 01:14:43 another would be ~(p & ~p) 01:14:47 which involves bottom, I guess 01:14:50 oerjan: hmm 01:14:58 ((p, p -> Void) -> Void) 01:15:00 -> Void 01:15:10 prove with fix, I assume? 01:15:17 err no 01:15:20 how can you prove that 01:15:31 f (p, q) = q p 01:15:43 oerjan: you don't have a (p,q) 01:15:47 you have a ((p,q)->Void) 01:15:55 no 01:15:55 ~(p&~p) 01:15:55 = 01:16:00 Not (p, Not p) 01:16:00 = 01:16:05 ((p, p -> Void) -> Void) 01:16:12 so how can you prove 01:16:15 f :: ((p, p -> Void) -> Void) 01:16:20 ohh 01:16:24 you mean proving ~(p&~p) 01:16:25 f (p, q) = q p 01:16:29 yes 01:16:33 instead of proving Not ~(p&~p) 01:16:33 sorry 01:16:35 brainfart 01:16:36 right, right 01:16:38 okay 01:17:14 okay i think i get it now 01:17:27 for anything of the form Not a, the intuitionist and classical tautologies are the same btw. 01:17:44 oklopol_: yeah it's pretty hot isn't it, every piece of code you write is a proof of some proposition 01:18:21 what logic would python be 01:18:37 oklopol_: erm python doesn't really have types as such... 01:18:46 so... none :D 01:19:04 it works best with functional languages 01:19:23 well i was mainly hoping for a fun pun answer 01:19:27 functional strongly typed langs 01:19:27 so 01:19:28 haskell 01:19:30 and ml 01:19:54 oklopol_: the serpent calculus 01:20:05 thank you ! 01:20:15 i'm sure that is fun if you get the obscure logic reference 01:20:24 i don't really 01:20:41 but i'll just assume it is really something. 01:20:42 sequent calculus is a way of axiomatizing logics 01:21:10 ...so s/q/rp/? 01:21:26 *qu 01:21:54 right was too busy correcting my keyboard's errors to see mine 01:21:56 You agree that neither you nor any person using the Service with your permission shall use the Service: for any fraudulent, criminal or unlawful purpose; to send unsolicited advertising or promotional material (or to engage in any "spamming" activity); to transmit any virus, worm, trojan horse or other harmful material; for the purpose of intimidating, harassing or causing annoyance to any third party 01:22:02 being annoying = illegal 01:25:12 so err f (q, p) = p q proves f :: ((p, p -> Void) -> Void), but can't you prove the inverse, f :: (p, p -> Void), with simply having f be a pair of (some value, function that bottoms) 01:25:20 no i don't think i still get it. 01:25:37 bottom = no 01:25:44 oklopol_: you cant use bottom 01:25:48 bottom -> a 01:27:17 i don't know what you mean 01:27:24 oklopol_: using bottom isn't allowed 01:27:39 where did i use it incorrectly? 01:27:49 i was thinking f = (value, mockingbird) 01:27:58 (some value, function that bottoms) 01:28:01 you used bottom 01:28:03 you lose 01:28:06 it is not allowed 01:28:11 in any circumstance 01:28:31 only terminating functions allowed 01:28:40 yep 01:28:45 otherwise your logic is inconsistent 01:30:08 so how isn't f (q, p) = p q wrong then, p bottoms 01:30:13 also, the mockingbird doesn't type in ordinary haskell 01:30:20 ... o rly oklopol_? 01:30:27 oklopol_: it's an argument 01:30:53 ehird: wut? that was a question 01:30:56 yes, Void values bottom, so you cannot produce them, but you can still look at what happens if you get them in 01:31:07 oerjan: okay makes sense 01:31:12 i was just going by ehird 01:31:16 's definition 01:31:43 i mean (value, mockingbird) is a terminating implementation 01:31:48 but right makes sense 01:32:01 awesome, bogons.net cofounder posted about how he hates Phorm on a mailing list 01:32:02 it needs to be well-typed in the logic too 01:32:58 there _are_ ways to type the mockingbird, but they involve letting an expression have two types simultaneously 01:33:01 oerjan: well okay mockingbird was a bad idea 01:33:50 (\a -> a a) :: (A /\ (A => B)) => B 01:34:02 but that's not a haskell or ML type 01:34:51 (/\ here has a different meaning than the (,) one, it means a should _actually_ be both types simultaneously) 01:38:21 oh it's 4 am 01:38:25 that's kinda cool. 01:38:34 guess it's no sleep for me 01:39:11 need to go give a friend a book at the railway station at exactly 8 am 01:39:19 "no sleep today, the milk has run awaaay" 01:39:28 or do i remember that wrong 01:40:05 i knew it, oklopol_ is a terrorist! 01:40:24 -!- oklopol_ has changed nick to oklopol. 01:40:27 wait i am? 01:40:55 who but a terrorist would show up at railway stations at exactly 8 am to give friends books 01:41:03 well you see 01:41:07 this guy has an exam on monday 01:41:11 and has 600 pages to read 01:41:15 i guess you _could_ be a secret agent 01:41:26 so it's somewhat crucial to get the book to him as early as possible 01:41:30 bomb making is no easy course 01:42:46 like, at least two weeks ago? 01:43:51 you don't need a railway station, you need a time machine 01:43:59 :P 01:44:19 coolness is not only a top clicker, he's a dedicated reader too 01:44:48 /whois coolness 01:44:56 pointless game reference 01:45:03 #pokenet? is that some pokemon thing? 01:45:28 hmm err different coolness 01:45:39 i'm talking about the guy who played ehird's fun clickery game 01:46:28 hm indeed it is 01:46:44 he recently spent a week reading 16-20 hours a day, i have a long way to go. 01:50:22 and why are our university's pages constantly broken, i want to stare at my exam schedule :< 01:51:23 must be all the hackers doing exercises 01:52:30 sadly we don't have any explicit hacking courses 01:52:53 how can you be a successful terrorist university without hacking courses 01:53:38 i'm not sure i can parse that. 01:53:52 hmm 01:53:54 no i can 01:54:43 there are implicit hacking courses, you need to learn some non-hacking too 01:55:12 maybe it's so you can pretend you're not a terrorist when necessary 01:55:40 ah 01:58:40 also maybe it's the university pretending that. 01:59:46 somehow deciding to stay awake because i'd only get a few hours of sleep reminds me of the story of the guy who threw all the eggs away because he dropped one. 02:00:16 such random associations. 02:00:57 * oklopol decides he probably shouldn't read because he didn't reach his quote anyway 02:01:00 *quota 02:03:06 wow i beat computer level 1 in reversi 02:03:44 * oerjan plays a fanfare 02:04:10 =@==<| 02:22:22 -!- Sgeo has joined. 02:56:54 A campfire hanging by a knotted string. 02:58:58 oklopol: that's not a random association at all. 02:59:16 It's a precisely appropriate association. 02:59:41 Mot juste, in fact. 03:00:32 Or mō zhōos, as we reformers like to spell it. (The macrons are optional, but consider adding silent e's to compensate.) 03:02:25 what happened to the poor t 03:02:56 My English teacher failed to pronounce it. 03:03:02 I think the French don't or something. 03:03:41 i think your english teacher had a speech impediment 03:04:06 -!- Sgeo has quit (Read error: 104 (Connection reset by peer)). 03:04:13 http://en.wiktionary.org/wiki/mot_juste does not agree in either english or french 03:04:14 -!- Sgeo has joined. 03:05:14 nor does http://www.merriam-webster.com/dictionary/mot+juste 03:06:35 -!- olsner has joined. 03:09:41 kerlo: it was? i must be smarter than i thought. 03:10:14 in fact it is not the exact same thing, half of the reason not to sleep is being afraid of not waking up in time 03:10:22 * kerlo puts the Humble Hat on oklopol. 03:10:31 but the other half is that egg thing. 03:10:44 i always do it 03:10:54 it is very bad to wake up with egg on your face 03:11:03 Okay. Mō zhōost. 03:11:38 stop being moose 03:11:56 interesting use of o 03:12:19 stop being abtoose 03:13:04 *abstroose 03:13:32 or possibly *obtoose 03:13:46 thought you meant the latter 03:14:02 o 03:14:02 o 03:14:15 in a self-referential way 03:14:58 What's an interesting use of o? 03:15:13 ōkləpŏl 03:16:15 a use that is pronounced nowhere near lower back afaik 03:17:39 the french is of course an upper front rounded vowel 03:19:08 By "lower" and "upper", do you mean... well, no, I don't know what you mean. 03:19:27 tongue position 03:19:28 Oh, low is open and high is close. 03:19:49 So the open-mid back rounded vowel is indeed near lower back. 03:19:56 terminology is so forble 03:20:32 And the "o" in "mot juste" is open-mid back rounded, if Wiktionary is trustworthy. 03:20:36 words are pretty useless 03:21:04 but the u is definitely not 03:21:11 that was the interesting part 03:21:11 -!- olsner has quit ("Leaving"). 03:23:40 So the "u" isn't like the stereotypical "u" at all. 03:24:21 unless you mean stereotypically french, in which case it is 03:24:36 * kerlo looks 03:25:48 Oh, I see. 03:26:41 I guess the anglicisation preserved the roundedness rather than the frontness. 03:26:47 Thus, ōo. 03:26:50 huh? 03:27:49 Using ōo to mean the vowel in "goose". 03:29:15 i don't read either wiktionary or merriam-webster that way. 03:29:39 although the latter has its own strange set of pronunciation symbols 03:30:17 * oerjan suddenly realizes his typing is nowhere near touch these days 03:30:27 Well, Wiktionary's representation of that vowel is more like ōō. 03:30:34 unless i concentrate 03:30:39 A long macron that goes right over both o's. 03:31:58 what i am saying is that neither actually says mot juste is pronounced with an oo sound in english 03:39:07 True.' 03:39:20 But hey, we're anglophones. We anglicise. 03:43:53 i think i'm going to save one egg by sleeping for an hour 03:44:24 wake me up at 7:30 if i'm not awake yet, current time being 5:54 03:44:32 thanks in advance -> 03:45:15 oklopol, your clock is off by approximately 10 minutes. 03:45:19 Or maybe my clock sucks. 03:46:00 oklopol: and then you can have egg and bacon for breakfast! well, assuming you have bacon. 03:46:29 * kerlo creates bacon. 03:46:30 of course i have bacon! 03:46:33 kerlo: it's a vacuum clock? 03:46:37 well actually i don't. 03:46:51 kerlo: three clocks here show the exact same time 03:47:00