< 1268179373 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but isn't the way board game players interact, taking turns to manipulate some state, game theoretical stuff < 1268179452 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i guess not really < 1268179485 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1268179504 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :A|(B C) = (A|B) (A|C), obviously < 1268179515 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but does A (B|C) = (A B)|(A C)? < 1268179523 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :where A B is common parts and A|B is combination < 1268179576 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :isn't the study of general properties of game trees an important part of game theory? at least the one book i've read talks about it a lot. < 1268179689 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: winning theory could be your chance to include all the ridiculous ideas you've ever thought of into mathematics < 1268179703 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so what's the symbol for A totally winning B? < 1268179711 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm not sure how that maps to what category theory is to algebra though < 1268179722 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Tw(A,B)? TW(A,B)? TwAB? A op B? < 1268179742 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :as always, A | B = A <==> A > B < 1268179753 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :or maybe more like >= < 1268179840 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :of course < 1268179843 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but totally winning is about strategy < 1268179877 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I think op is the best route as you know, operators are awesome and you can invent symbols for them < 1268179884 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :doesn't mean we should get too creative when defining the algebra of games < 1268179890 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Whyever not. < 1268179898 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :indeedso iguess not. < 1268179908 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :or do i mean yes < 1268179915 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Circled > would be nice. < 1268179922 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm not really following any of these conversations < 1268179923 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Might confuse with just >, but isn't that a good thing? < 1268179929 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::| < 1268179934 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah! < 1268180194 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268180356 0 :Oranjer!~HP_Admini@adsl-71-7-92.cae.bellsouth.net JOIN :#esoteric < 1268181042 0 :alise!~95fedb5c@gateway/web/freenode/x-edyqgzccoahjvfsh JOIN :#esoteric < 1268181055 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :what did i miss since what i last said? < 1268181125 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :beats me! < 1268181255 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :alise: < oklopol> yeah! < 1268181267 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that is it? :P < 1268181325 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well also "02:17… Oranjer has joined #esoteric" < 1268181326 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's sort of relevant to what Oranjer said < 1268181376 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :what is it with chess ais, you give them a huge amount of time because you don't wanna feel pressure and they just sit about doing nothing < 1268181387 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :you're a computer. you don't panic. stop wasting my time < 1268181470 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :chess is too hard anyway < 1268181503 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :what < 1268181517 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :lament: i don't care, it's entertaining < 1268181527 0 :Ilari!unknown@unknown.invalid QUIT :Ping timeout: 268 seconds < 1268181538 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oh I think i may just have set up the ai wrongly < 1268181541 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it just sat there and ran out of time < 1268181546 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :alise: AIs do use up time < 1268181562 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :coppro: yes but this one played fine with little time. also, as i said, it ended up not moving at all. < 1268181598 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :how does it end up not moving < 1268181619 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :lament: yeah i never learned how knights move < 1268181631 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION tries a different type of clock
< 1268181633 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oranjer: by not moving in the allocated time < 1268181642 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :I think they do the Kansas City Shuffle, oklopol < 1268181682 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :two steps this way and then one step this way oh and by the way YOU CAN FLY OVER OTHER PIECES, that's just insane < 1268181719 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :it's just a game after all < 1268181726 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :flying horses < 1268181745 0 :cal153!unknown@unknown.invalid QUIT : < 1268181767 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :Chess: the only playable Allegory of Islam < 1268181811 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :lament: your responses are really boring today, are you drunk on life? < 1268181834 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :i'm sober < 1268181840 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oranjer: you are way too postmodern < 1268181851 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :how so? < 1268181858 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :lament: < 1268181862 0 :Ilari!~user@2002:5871:273b::1 JOIN :#esoteric < 1268181865 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :Muhammed flys somewhere on a flying ass < 1268181893 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :Muhammad, sorry < 1268181926 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: empty string < 1268182164 0 :cal153!~cal@c-69-181-46-213.hsd1.ca.comcast.net JOIN :#esoteric < 1268182640 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1268182810 0 :coppro!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1268183511 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :In which I play Chess extremely shittily: < 1268183512 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :1. b4 c6 {+0.17/8} 2. Nc3 Nf6 {+0.31/9} 3. Na4 d6 {+0.21/9} 4. c4 g6 {+0.06/8} 5. d4 Be6 {+0.14/8} 6. c5 Na6 {+0.06/9} 7. d5 Nxd5 {+0.79/8} 8. b5 cxb5 {+1.70/10} 9. e4 Qa5+ {+1.61/10} 10. Bd2 Qxa4 {+1.71/11} 11. Qxa4 bxa4 {+1.98/10} 12. exd5 Bxd5 {+2.00/10} 13. a3 Nxc5 {+3.09/9} 14. Ba5 Nb3 {+3.00/9} 15. Rb1 Bg7 {+3.82/10} 16. Bc7 Rc8 {+5.19/10} 17. Ba5 Nxa5 {+5.87/10} 18. g4 Bxh1 {+10.37/10} 19. Nf3 Bxf3 {+13.43/11} 20. Be2 Bxe2 < 1268183526 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :23. Rb4 Rxa3 {+14.69/9} 24. Rb5 Rh3 {+14.96/8} 25. g5 a3 {+17.63/9} 26. f4 a2 {+22.11/9} 27. Rc5 bxc5 {+26.91/9} 28. f5 gxf5 {+27.85/9} 29. Ke1 Rxh2 {+79.98/28} 30. Kd1 a1=Q# {+79.99/28} < 1268183531 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Admittedly a few mistakes were due to the mouse slipping. < 1268183547 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :That probably made the already ridiculous difference in skill vs the computer vastly worse < 1268183558 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But hey, it was entertaining. I am awfully bad though. < 1268183628 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :how does one read this notation < 1268183628 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :can the computer give an estimate of how much you sucked? < 1268183776 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oranjer: ignore the bits in {}s < 1268183783 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and then just google chess move notation < 1268183787 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i'm white < 1268183789 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :obviously < 1268183790 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1268183798 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :lament: probably, but i don't feel like hating myself that badly < 1268183854 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise < 1268183871 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax < 1268183880 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hello < 1268183883 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hello < 1268183898 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I love finite calculus < 1268183907 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ok zeilberger < 1268183914 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ceil(burger) < 1268183918 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :failculus < 1268183927 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it isn't really very calculusy tbh :p < 1268183944 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it blows my mind that the are so many stiking similarities with the real calculus < 1268184005 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :it blows my mind that this blows your mind < 1268184023 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :given that calculus is obviously the limit of finite calculus < 1268184031 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well 1 is basically the infinitesimal of the integers :P < 1268184047 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :finite calculus isn't calculus on integers < 1268184056 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i know < 1268184069 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i know you know, i just like saying it < 1268184071 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it's catchy < 1268184078 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :?? < 1268184082 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it's not calculus on integers? < 1268184088 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :are you reading the same paper as me? :P < 1268184109 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh well it's calculus from integers < 1268184122 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but the functions still go to R < 1268184131 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: why not on booleans < 1268184132 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :mine are Z -> Z < 1268184137 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :boolean calculus, do it now < 1268184144 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, I am actually reading George Booles paper on this right now < 1268184148 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :er book < 1268184159 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :haha man I'm laughing too much at the idea of boolean calculus < 1268184173 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION frowns
< 1268184180 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: no you /must/ do it on Bool -> Bool where true : Bool, false : Bool and nothing else < 1268184183 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well the reason the paper doesn't talk about Z -> R, i think, is that integers always sum to integers, so you can restrict it that way, unlike normal calculus < 1268184191 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I guess I'm basically asking for calculus from naturals mod 2 < 1268184193 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so DO IT < 1268184196 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :>:3 < 1268184214 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 264 seconds < 1268184241 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well it could be Q -> Q also < 1268184243 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but that's not as elegant < 1268184252 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :why are you talking < 1268184257 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :boolean calculus < 1268184257 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :now < 1268184268 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, it's your idea, you do it! < 1268184281 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i don't have a cock compiler < 1268184290 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :just s/Z/Bool/ in your code, job done < 1268184296 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :um :P that wont do it < 1268184302 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i think it's very elegant from Z to R < 1268184306 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hey I just realized Bool is a field < 1268184324 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what's Bool? < 1268184327 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, why is Z -> R better than Z -> Z? < 1268184365 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :gf < 1268184368 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :true/true = true < 1268184371 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :true/false = undefined < 1268184377 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that's one fucking awesome field xD < 1268184379 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :"= undefined" *barf* < 1268184386 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :as in "is undefined" < 1268184387 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :because if we consider Z a measure space with cardinality as the measure, then sums are just integrals < 1268184389 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :false/true = false < 1268184392 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :false/false is undefined < 1268184400 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :*unbarf* < 1268184401 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :and with integration we usually have functions from our measure space to R. < 1268184402 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so basically X/true = X anything else is undefined < 1268184424 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, wait what < 1268184427 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so the multiplicative inverse is < 1268184430 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :true^-1 = true < 1268184432 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that's it < 1268184436 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :worst field ever < 1268184451 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, ooh I wonder if there's a Z[i] calculus with all the nice harmonic, holomorphic stuff < 1268184451 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :then again multiplication is boring on booleans anyway < 1268184453 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :whoa < 1268184458 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :multiplication is division on booleans < 1268184463 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :wait no < 1268184469 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :except for half of it (/false) >_< < 1268184473 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, unitary calculus!! < 1268184482 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :fax: the crazy dude's paper talked about discrete analytic functions < 1268184486 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :for all the cases where / is defined on bools it is identical to * < 1268184495 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :01:27 < alise> for all the cases where / is defined on bools it is identical to * < 1268184499 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oops < 1268184504 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: if you're using his notation you say R but you mean hZ_p < 1268184505 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :or mentioned them < 1268184506 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :looked neat < 1268184509 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(where Z is a finite set) < 1268184517 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :do not pervert /our/ discourse :P < 1268184532 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :tbh addition on booleans is pretty nice, being xor < 1268184537 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hmmmm < 1268184558 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :true - true = false; true - false = true; false - true = true; false - false = false; < 1268184559 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :heh - = + too < 1268184563 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :this is the best discovery I have made :)))))) < 1268184568 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: what is < 1268184568 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :finding this finite calculus < 1268184576 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :dude it's just some addition and subtraction < 1268184648 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hey fax DID YOU KNOW you also have exponentiation on booleans < 1268184654 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :x^true = x; otherwise undefined < 1268184664 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268184664 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in fact, you can even use the ackermann function on them. < 1268184667 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it's clear sums are integrals because every function is simple < 1268184667 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :from Z, with the usual measure < 1268184667 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :err wait what < 1268184667 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's bullshit, let me gather myself. < 1268184669 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay maybe it's not completely obvious < 1268184671 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :"Vladimir Arnold forcefully stated in one of his books that it is wrong to think about finite difference equations as approximations of differential equations. It is the differential equation which approximates finite difference laws of physics" < 1268184672 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :now you have INFINITE OPERATORS!!!!!!!!! < 1268184699 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so fax is now the fifth ultrafinitist i gather < 1268184920 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :this pleases me < 1268184930 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: I'll love you if you make a Coq module with ultrafinitist definitions of the following, paramaterised on the rational h and the prime p: Naturals, so that there is no prime greater than p; Integers, presumably with each half of the integers dedicated to a sign; Rationals, divided once more (h must fit into one of these); and Reals, defined as hZ_p. < 1268184948 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Along with associated operations, the calculus he defines, and properties. < 1268184951 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, I will help you do it :) < 1268184954 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And by love you, I mean hate you love you. < 1268184966 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: Well... I started writing it in my language but couldn't be bothered. < 1268184970 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, I should implement (normal) construtive reals though < 1268184981 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :those are easy < 1268184990 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :following the sketch in my constructie functional analysis text < 1268185027 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sigma (f:Q+->Q), Forall (e1,e2:Q+), abs (f e1 - f e2) <= e1 + e2 < 1268185028 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :boring < 1268185039 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: now do it, ultrafinitistic peon < 1268185193 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: Actually I suppose that all those sets don't neccessarily have to have the same size because they all coexist. < 1268185219 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So having the integers be twice the size of the naturals (minus 1, because there's only one 0...) and having rationals be the size of the naturals plus the integers would be OK. < 1268185231 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The reals have to be hZ_p by Order of Zeilberger. < 1268185350 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The nice thing is that we don't need any pesky functions or anything to define these because there's a simple, finite number of cases. < 1268185613 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :p would be what? The largest known* mersenne prime (* known by http://coqprime.gforge.inria.fr/ ) < 1268185630 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :p and h are parameters to the module < 1268185663 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :they are universal constants like physical ones but we don't know what they are (zeilberger says that the True Value either p or h - i forget which - is unknowable so uh whatever) < 1268185670 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so we just plug in values we like. < 1268185690 0 :augur!~augur@216-164-33-76.c3-0.slvr-ubr2.lnh-slvr.md.cable.rcn.com JOIN :#esoteric < 1268185702 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Time for a nick change. < 1268185719 0 :uorygl!unknown@unknown.invalid NICK :uorygl[hireMe] < 1268185723 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1268185725 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: if you have an awful lot of cpu time on your hands the largest mersenne prime would be a good choice for p, yes. < 1268185743 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :h would be the result of pressing 0., holding down 0 for a long while, then pressing 1, probably. < 1268185763 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :shouldn't h come from a physical/science experiment < 1268185768 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :like the fine structure constant or something < 1268185783 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Zeilberger claims they are separate to physical constraints and that he is a platonist. < 1268185801 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Since we are following his school of ultrafinitism, not the usual physical-constraints one, that is not required. < 1268185814 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :1/p is a good value for h if you have that in your system. < 1268185826 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :What is hZ_p? < 1268185830 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :p is a natural and rationals = size of naturals + size of integers, so < 1268185836 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :1/p should always be acceptable < 1268185842 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :uorygl[hireMe]: Z is the integers < 1268185844 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :_p is subscript p < 1268185854 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :And h is an h? < 1268185857 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Zeilberger, an ultrafinitist that believes no infinite sets exist, defines the reals as hZ_p < 1268185859 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :That explains so much. < 1268185866 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :where h is a very, very small number < 1268185869 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and p is a very, very large prime < 1268185882 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268185884 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :01:50 < uorygl[hireMe]> That explains so much. < 1268185886 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :^^^^ lol < 1268185899 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :So what does hZ_p mean? < 1268185910 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It means hZ_p. :-P < 1268185924 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :That is not a definition! < 1268185943 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :Or, if it is a definition, then your mom is a perfectly good model of hZ_p. < 1268185947 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :Since your mom is your mom. < 1268185949 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :'Tis true < 1268186017 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Z_p = Z/Zp I guess? < 1268186029 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Galois field < 1268186031 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :Yeah, I figure Z_p is the integers modulo p. < 1268186037 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :I have no idea what the h is supposed to be. < 1268186053 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :F_p = Z/pZ < 1268186067 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :h is the fundamental mesh constant, it's smaller than 1 < 1268186082 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :so hZ_p = {...-h,0,h,2h,3h,...} < 1268186096 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :h: It's Smaller Than One. < 1268186104 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :So you multiply each number by h? < 1268186168 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268186180 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise you should make slogans < 1268186182 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so if h is the fundamental mesh constant, what's the cool name for p < 1268186199 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :uorygl this is my interpretation, but I am by no mean an expert on this < 1268186261 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it doesn't actually do anything < 1268186262 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hmm, ultrafinitists don't even let you have a type of types. < 1268186274 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :After all, it's infinite. < 1268186280 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Unless you have a finite number of sets, which would be cool. < 1268186283 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: what doesn't? < 1268186401 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I guess the best thing is to have the integers be of size p. < 1268186443 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Which means that the naturals are of size (p+1)/2. < 1268186458 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :What does let you have a type of types? < 1268186465 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So the rationals are of size p+((p+1)/2). < 1268186471 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :I know of... not many systems under which that's possible. < 1268186472 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :uorygl[hireMe]: Anything? < 1268186474 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Nat : Set. < 1268186487 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :Yes, but Set !: Set. < 1268186498 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Obviously. < 1268186503 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But Set is still infinite. < 1268186528 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So, the reals have the same size as the integers. < 1268186536 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Which means that the reals are smaller than the rationals. < 1268186543 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :This Makes No Sense (not that ultrafinitism does); start over. < 1268186561 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The naturals are of size (p+1)/2. < 1268186564 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The integers are of size p. < 1268186572 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :your mom < 1268186572 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The rationals are of size p. < 1268186586 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Half negative, half positive. < 1268186591 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :also the h < 1268186599 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So (p-1)/2 each. < 1268186606 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :Here's some ultrafinitism for you: take ZFC, remove the axiom of infinity, add an axiom of non-infinity. < 1268186632 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: i don't know coq man I can't do this :( < 1268186794 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, (p-1)/2 is valid Coq < 1268186829 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yes it is < 1268186949 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1268186953 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :the size of the integers must be prime < 1268186981 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that would make integers a field - weird < 1268187001 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :isn't that awesome not weird :) < 1268187014 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :see these are the possibilities ultrafinitism gives you dude < 1268187028 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol I will ttyl < 1268187037 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I have to go < 1268187052 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION should have gotten an F on his history exam. Instead, I got a B+
< 1268187087 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :1234567890123456789012353 is a prime number < 1268187136 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: you've turned into a history person! < 1268187183 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :an historical personage < 1268187216 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I got a 36/50 < 1268187541 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Things about the rationals: 1/p is a rational. < 1268187554 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So, for every integer, there are p elements in the rationals for it. < 1268187566 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :p is the maximum size of a set. So, the rationals suck. < 1268187570 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So, I must sacrifice something. < 1268187574 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I sacrifice 1/p. < 1268187574 0 :Asztal!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268187683 0 :fax!unknown@unknown.invalid QUIT :Quit: 1234567890123456789012353 < 1268188694 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268188964 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It would be interesting to see how varied an ultrafinitist system is. < 1268188965 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :My bet: Not at all. < 1268189227 0 :oklopol!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268189514 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :http://sibeli.us/ < 1268190931 0 :uorygl[hireMe]!unknown@unknown.invalid PRIVMSG #esoteric :The best ultrafinitist system is a Galois field. < 1268190937 0 :uorygl[hireMe]!unknown@unknown.invalid NICK :uorygl < 1268190961 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :what language lends itself to reflection the most? < 1268190980 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :BackFlip. :P < 1268191016 0 :alise!unknown@unknown.invalid QUIT :Quit: Page closed < 1268191018 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :not that kind of reflectiong < 1268191561 0 :werdan7!unknown@unknown.invalid QUIT :*.net *.split < 1268191562 0 :rodgort!unknown@unknown.invalid QUIT :*.net *.split < 1268191562 0 :ttm!unknown@unknown.invalid QUIT :*.net *.split < 1268191698 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Aura! < 1268191704 0 :ttm!~daniel@130-94-161-238-dsl.hevanet.com JOIN :#esoteric < 1268191706 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :jamaica! < 1268191715 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Or whatever that's called. < 1268191743 0 :rodgort!~rodgort@li14-39.members.linode.com JOIN :#esoteric < 1268192439 0 :werdan7!~w7@freenode/staff/wikimedia.werdan7 JOIN :#esoteric < 1268193057 0 :Gracenotes!~person@wikipedia/Gracenotes JOIN :#esoteric < 1268194425 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Gah, I'm so unclear sometimes. < 1268194672 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :I'm tempted to throw neutrons at you. < 1268194682 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :But that wouldn't really help. < 1268194709 0 :jcp!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268194719 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :Sgisotype < 1268196208 0 :coppro!unknown@unknown.invalid QUIT :Read error: Operation timed out < 1268197192 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268197693 0 :coppro!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1268198670 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Hm, smeta.na is available for the low low price of $4,000/yr < 1268198738 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268199259 0 :Oranjer!unknown@unknown.invalid PART #esoteric :? < 1268199582 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION is half tempted to use PSOX with Scheme
< 1268199585 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :>:D < 1268199641 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION three-quarters tempted to mock Sgeo's use of fractional temptation.
< 1268201376 0 :skeeto!~user@c-98-204-92-42.hsd1.md.comcast.net JOIN :#esoteric < 1268201455 0 :skeeto!unknown@unknown.invalid PRIVMSG #esoteric :is it possible to write the identity function in Fractran? I don't think it's possible. < 1268202185 0 :skeeto!unknown@unknown.invalid PART #esoteric :? < 1268202804 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :So, what does PSOX look like? < 1268202824 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :One can not see PSOX. < 1268202830 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :One can only ... /experience/ PSOX. < 1268202836 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION decides that uorygl has been living in a bubble since the end of 2007
< 1268202839 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Does it provide the Unix standard library? < 1268202851 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :I don't think PSOX is famous. < 1268202873 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :It is infamous in these parts < 1268202911 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :It gives alise aneurysms < 1268202935 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :If it gives alise aneurysms, I'm almost bound to probably be slightly irritated by it. < 1268203505 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268203755 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268204170 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Isn't PSOX about as well-maintained as PEBBLE these days? < 1268204187 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :pikhq, if PEBBLE was abandoned, yes < 1268204205 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I've not touched it since, oh, 2007. < 1268204209 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :If people start showing interest, I may regain interest in maintaining PSOX < 1268204406 0 :kar8nga!~kar8nga@jol13-1-82-66-176-74.fbx.proxad.net JOIN :#esoteric < 1268204803 0 :tombom!tombom@wikipedia/Tombomp JOIN :#esoteric < 1268206172 0 :oerjan!unknown@unknown.invalid QUIT :Quit: leaving < 1268206782 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION goes to try Smalltalk
< 1268207504 0 :tombom!unknown@unknown.invalid QUIT :Quit: Leaving < 1268207573 0 :cheater2!unknown@unknown.invalid QUIT :Ping timeout: 246 seconds < 1268207999 0 :clog!unknown@unknown.invalid QUIT :ended < 1268208000 0 :clog!unknown@unknown.invalid JOIN :#esoteric < 1268208170 0 :cheater2!~cheater@ip-80-226-44-25.vodafone-net.de JOIN :#esoteric < 1268208799 0 :FireFly!unknown@unknown.invalid QUIT :Quit: Leaving < 1268208954 0 :cheater3!~cheater@ip-80-226-44-25.vodafone-net.de JOIN :#esoteric < 1268209075 0 :coppro!unknown@unknown.invalid QUIT :Quit: I am leaving. You are about to explode. < 1268209193 0 :cheater2!unknown@unknown.invalid QUIT :Ping timeout: 256 seconds < 1268209229 0 :zeotrope!unknown@unknown.invalid QUIT :Ping timeout: 256 seconds < 1268209264 0 :zeotrope!~zeotrope@bas3-kitchener06-1096649314.dsl.bell.ca JOIN :#esoteric < 1268209941 0 :OxE6!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268210004 0 :adu!unknown@unknown.invalid QUIT :Quit: adu < 1268210219 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1268210300 0 :MU!~mu@wireless-lsusecure-9.net.lsu.edu JOIN :#esoteric < 1268210309 0 :MU!unknown@unknown.invalid PART #esoteric :? < 1268211121 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1268212503 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1268212510 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1268216192 0 :kar8nga!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268216616 0 :oklopol!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268216728 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oerjan come quick < 1268217466 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :oklopol! :o < 1268217832 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1268217868 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :do the types by any chance form a quasigroup in your a/b b\a type thingie? < 1268217923 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :what < 1268217972 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'll take that as a no < 1268217981 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :no no, dont take it as anything < 1268217986 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :i dont know what you're asking < 1268217990 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh okay < 1268217992 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm talking about that < 1268218008 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :linguistics thing you tried to teach me and someone else and he was like whaaaaaa < 1268218026 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :(C)CG? < 1268218028 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :and you were like okay this is going nowhere i'm gonna go do something otherthing. < 1268218040 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :oh, right < 1268218052 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :lecomte and retore's minimalism < 1268218054 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it was about semiconflabulent grammars < 1268218059 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :ah minimalist < 1268218080 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :i dont know if the types for a well defined structure. i doubt it < 1268218084 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :form** < 1268218171 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :hmm minimalism has (a/b)*b = a, but does it have (a*b)/b? i guess that makes no sense < 1268218207 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :well, * is an operation on lexical items that bear types < 1268218217 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i just noticed a similarity when reading about quasigroups, but i haven't actually given it any thought < 1268218221 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :not a type constructor < 1268218225 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :right < 1268218233 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so a*b isn't even defined in general < 1268218241 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :well, it is < 1268218244 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :therefore it can't form an algebra < 1268218245 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh? < 1268218247 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :its just not a type constructor < 1268218257 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :look at it like this < 1268218258 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but is it defined no matter what the types of a and b are < 1268218267 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :thats correct < 1268218272 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :but / is a type constructor < 1268218275 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :* is not < 1268218289 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :so you cant do (a*b)/c < 1268218293 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :why? because a*b is not a type < 1268218303 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :so you cant use / on it < 1268218312 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh alright < 1268218318 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :think of it like haskell < 1268218324 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :a -> b is a type in haskell < 1268218331 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :a + b is not a type < 1268218337 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :so you cant have some type < 1268218339 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :(a + b) -> c < 1268218371 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so i can't really say (A/B)*B = A either, i can say c*d : B if c : (A/B) and d : B? < 1268218413 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :pretty but. i mean, (A/B)*B would be seen as just an operation over the type objects < 1268218417 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :which is fine < 1268218422 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :its just not a type constructor < 1268218432 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :its an operation on types. < 1268218438 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :brb < 1268218451 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but as an operation over type objects, isn't it partial? < 1268218501 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :say we just have the types A and B, how can A*B be defined if * isn't a type constructor < 1268218537 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :also how can it be defined on the objects or whatever, if a : A, b : B, what's the type of a*b? < 1268218613 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :it is indeed partial < 1268218651 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :A*B is undefined. only A/B * B and B * A\B are defined < 1268218663 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :for all types A and B < 1268218667 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay, so they do form an algebra, but it's partial < 1268218674 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :therefore it clearly can't be a quasigroup < 1268218675 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :its just function application dude < 1268218691 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :its literally beta reduction < 1268218697 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :on types instead of functions < 1268218707 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :and the types are directional < 1268218742 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what's the difference between type constructors and type operators? both are operators that take types to other types < 1268218755 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :constructors are used to define the universe of types, yes, but i don't see how that's relevant < 1268218774 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i probably shouldn't be looking at this quite this algebraically. < 1268218778 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :sure but a type constructor is, at least in this case, and i think in all cases, total < 1268218787 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :ah, well yes, okay < 1268218791 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :-> : T x T -> T < 1268218807 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :* : (T x T) x T -> T < 1268218874 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :theres also the tensor product thing that they had tho fight < 1268218887 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :they had a second type constructor, x < 1268218890 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so (T, /, \) forms an algebra, but it doesn't really have any structure... so i guess you should just think of those as type constructors instead of an algebra < 1268218901 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :well, it DOES have structure < 1268218905 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :its just not a well known one < 1268218928 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :or rather, its not an interesting one < 1268218963 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :if you did math, for instance, + or * over the integers has all sorts of fun properties < 1268218969 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well right, that's what i meant, it's the free algebra on two binary operations, sort of < 1268218971 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :like, sometimes you can get back what you gave it < 1268218978 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :or you can go in circles < 1268218983 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :etc < 1268218993 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric : / and \ are not like that < 1268219010 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah therefore free < 1268219027 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :which is to say, there are finite subsets of Z which are closed under + or * < 1268219043 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :there is no subset of T that is closed under / or \ < 1268219053 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :T as a whole is closed, but no subset of it is < 1268219064 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's not true < 1268219069 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :yes it is < 1268219075 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the subalgebra generated by A/B is a subset < 1268219077 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's closed < 1268219083 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :what? < 1268219099 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :sorry, no finite subset < 1268219105 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah that's true < 1268219113 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :obviously < 1268219133 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but it's freeness that's the point < 1268219139 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :but there ARE finite subsets of Z which are closed under *, lets say < 1268219142 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :{1} for instance < 1268219154 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :or {0} or {0,1} < 1268219166 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :why are you telling me this? < 1268219173 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :im just saying < 1268219181 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh well i guess that's allowed < 1268219185 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :the structure of Z under + or * is more interesting than \ and / < 1268219200 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :simply because you can get substructures that are interesting like this < 1268219291 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :you can do all sorts of fun stuff with * and + that you cant do with / and \ simply because / and \ are, you might say, information preserving < 1268219306 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah, you might even say it's free. < 1268219325 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :the result of addition is not something that has a uniquely identifiable origin < 1268219336 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :1 + 1 = 0 + 2 = -1 + 3 = ... < 1268219359 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :but A/B is just A/B. theres only one way to get A/B. < 1268219415 0 :Slereah!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1268219427 0 :comex!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1268219435 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i don't really know the exact definition of freeness, but that's exactly what i mean by free in the case of an algebra that doesn't have any sort of identities. < 1268219503 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :there's a base and there's only one way to get everything from it. in the case of no identities, we have the stronger thing that every individual operation is completely reversible < 1268219544 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :anyway < 1268219577 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :if you let * be a type operator (which it technically isnt; it operators on things _with_ types, but we can pretend it can operate on just types for convenience) < 1268219595 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :then you get \ / and * forming some sort of "non-free" object, as you might say < 1268219598 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :identities being where the structure comes from, in the free monoid we can still have ab*c = a*bc even though it's free, where {a,b,c} is the base, because we have an identity that makes them the same, but if the operation satisfies no identities, then it's fully information preserving < 1268219632 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :they form a partial algebra, if that's the term < 1268219646 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :e.g. (A/B * B)/B, ((A/B)/B)*B, etc. < 1268219672 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :might still be free though < 1268219679 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :hmmhmm < 1268219689 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :maybe. im just saying that there you now get the non-uniqueness of histories. < 1268219699 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :trues < 1268219750 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm actually literally atm reading a book that would completely explain the role of identities in universal algebra, if i just read like 20 pages ahead < 1268219760 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1268219773 0 :Slereah!~Slereah@ANantes-259-1-61-200.w92-135.abo.wanadoo.fr JOIN :#esoteric < 1268219905 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric ::) < 1268220040 0 :cal153!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1268220122 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :(which also might be why i'm obsessing about the algebraic side of these things) < 1268220427 0 :cal153!~cal@c-69-181-46-213.hsd1.ca.comcast.net JOIN :#esoteric < 1268221850 0 :cal153!unknown@unknown.invalid QUIT :Ping timeout: 248 seconds < 1268222079 0 :cal153!~cal@c-69-181-46-213.hsd1.ca.comcast.net JOIN :#esoteric < 1268224329 0 :fax!~none@unaffiliated/fax JOIN :#esoteric < 1268224572 0 :alise!~95feda53@gateway/web/freenode/x-iecmsuovvvlexyib JOIN :#esoteric < 1268225003 0 :oklopol!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1268225424 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: I finished sibeli.us < 1268225443 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Your score: 175822 / Points possible: 660500 / Grade: 26% (F) < 1268225450 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I couldn't go any swbps because of my kb matrix < 1268225452 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*do < 1268225460 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise is kool < 1268225560 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :augur: + /is/ an operation on types tyvm < 1268225560 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's (Either a b) in haskell syntax < 1268225594 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :a*b (same thing as cartesian product) = (a,b) < 1268226133 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :alise: oh, well ok. :P < 1268226150 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :i meant + as integer addition tho < 1268226160 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :thats all < 1268226262 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268226276 0 :alise!~95feda53@gateway/web/freenode/x-rtniaqmdeogeyjih JOIN :#esoteric < 1268226279 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :o hai < 1268226282 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Your score: 480612; Points possible: 660500; Grade: 72% (C-); this could do swbp (1234) most of the time, though I got some key-jammery there somewhere. I have to wonder if it would've been easier with the music, though. < 1268226320 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Your score: 380183 Points possible: 660500 Grade: 57% (F) < 1268226333 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :1234 would have worked too? That'd have made it easier < 1268226347 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :"Use the keys '1', '2', '3' and '4' (or 's', 'w', 'b' and 'p') for strings, woodwinds, brass and percussion." < 1268226352 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :That's what it says on the front page. < 1268226354 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Yeah, I missed that bit. < 1268226364 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I just pressed "play" without reading the instructions. < 1268226374 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Sounds exactly like the sort of thing you'd do! < 1268226413 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :swbp is highly inconvenient on Colemak; all left hand and in 2143 order < 1268226414 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :HA < 1268226414 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant loses at something! < 1268226429 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :A first! < 1268226460 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :XD < 1268226461 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But yeah, I started thinking ohh this is easy < 1268226461 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And then it was all, like, SSSWSWSWISBWndhFoiDSJpKAFPAJDOIHWDSOIWJD < 1268226484 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I dreaded the fast bits from the start :-P < 1268226485 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: It's worse with the music, trust me < 1268226502 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :With a 100+-key keyboard, though, shouldn't you be controlling just about every instrument? < 1268226564 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268226564 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: I've heard the whole thing like... once before < 1268226594 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :And I, several < 1268226594 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So a couple of times I thought "thank god, it's over" and then more shit popped up < 1268226644 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Being .fi, it's sort-of required reading, I think. < 1268226660 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Or listening. Anyway. < 1268226694 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It's rubbish < 1268226694 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You Finlanders suck :P < 1268226741 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: More automatic tweetery, though this is a bit Finnish-only: [2010-03-10 14:53:19] Tweeted: verikissanhiekka valtaa kanavia internetissä / akuutti rautaneito kuin laiteristiriita / laiminlyöty ja kukertava (runogen) < 1268226776 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :What. < 1268226783 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1268226820 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :It's automagical poetry-generation; a rather old (10 years?) bit of code that I was suggested to make auto-tweet too. < 1268226957 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :1234 was a lot more comfortable if not easier: Your score: 418757 Points possible: 660500 Grade: 63% (D) < 1268226972 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :alise: I don't think my poetic skills are up to a faithful translation, but if you want a mostly literal one... "blood-cat-litter takes over channels on the Internet / the acute iron maiden like a device conflict / neglected and colorful". < 1268226985 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Though "colorful" is a crappy word for "kukertava"; I don't really know what it should be. < 1268226995 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: xD < 1268227008 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Wiktionary's entry -- http://en.wiktionary.org/wiki/kukertaa#Finnish -- lacks a definition. < 1268227039 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: flowery? < 1268227109 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I'm not sure. Perhaps, though the connection to actual flowers is (at least to me) less there. < 1268227119 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :1. flowery -- (of or relating to or suggestive of flowers; "a flowery hat"; "flowery wine") < 1268227119 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :2. flowery, ornate -- (marked by elaborate rhetoric and elaborated with decorative details; "a flowery speech"; "ornate rhetoric taught out of the rule of Plato"-John Milton) < 1268227147 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :It's not sense #2, but it's maybe not exactly sense #1 either. < 1268227185 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Interwebs say: "It's a Finnish word for a colour that isn't of any particular colour, I think." < 1268227208 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :xD < 1268227211 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Right < 1268227221 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Weird-ass word; to me it suggests flowers < 1268227250 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Here's one poem I created earlier: "saatanan aarre ei ole valopuu / humanistien aurinko ymmärtää antaa kuin ruoska / kaipaus ei ole käytävä eikä brainfuck" < 1268227251 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :But evidently that's not what it means < 1268227267 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: :-D < 1268227269 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*word. < 1268227269 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: translayt < 1268227281 0 :kar8nga!~kar8nga@jol13-1-82-66-176-74.fbx.proxad.net JOIN :#esoteric < 1268227330 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :alise: "The treasure of Satan is not a light-tree / the sun of humanists knows to put out like a whip / longing is not a corridor, nor brainfuck". < 1268227351 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :"ymmärtää antaa" is another a bit difficult one. < 1268227354 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: I'd've said "insinuates" < 1268227387 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: But that's "antaa ymmärtää", isn't it? < 1268227403 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Yes, but with poetic license you can write it the other way around. < 1268227419 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Oh, but it's not that, in fact; that thing there in the poem is the other half from the saying "antaa ymmärtää, muttei ymmärrä antaa". < 1268227419 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I don't know, that just made more sense to me. < 1268227450 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :The translation used the "6. put out -- (be sexually active; "She is supposed to put out")" sense of "put out". < 1268227450 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Then I'd just say "understands to give" < 1268227465 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :And to me, that wasn't implied :-P < 1268227513 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Well, you'd have to know the guy whose irc behaviour was used as a model when constructing that particular wordlist. :p < 1268227514 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :those would make goodterrible lyrics < 1268227514 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :for a goodterribleterrible song < 1268227579 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: "ymmärtää antaa" is only in the "naula" wordset, c.f. http://www.pelulamu.net/naula/ < 1268227605 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I learned long ago not to visit pelulamu.net < 1268227628 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :So yeah, okay. :-P < 1268227629 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pelulamu.net? < 1268227660 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Anyway, that generator is a handcrafted CFG, mostly not by me; there's four wordsets ("poetic", "gothy", "funny" and "naula") you can tell it to use. < 1268227681 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :If you do "-w goth", you get out stuff like: "sinä olet pääkallo / risti kylpee veressä / pikkutyttö kylpee veressä tulvillaan kipua sydänyöllä" < 1268227688 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric ::-D < 1268227722 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pelulamu.net? < 1268227722 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :also TRANSLATE :| < 1268227730 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Do you have this available? I could put this in /etc/profile.d < 1268227756 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :alise: google.com/translate_t < 1268227783 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Sowwy, but there's only a binary-only version available; I'm supposed to clean up the code before release; have been for the last ten years. < 1268227786 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :no :| < 1268227789 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: http://maija.irtie.org/runogen/ anyway. < 1268227823 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :specially as i'm going in ... 20 seconds? < 1268227823 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but srsly what's pelulamu.net < 1268227823 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :like finnish rotten.com or sth? < 1268227828 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :alise: Well, the gothy one is approximately "you are a skull / a cross bathes in blood / a little girl bathes in blood full of pain at midnight". < 1268227845 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: Can you hook me up with a 64-bit binary? < 1268227847 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268227854 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Um, sure, I guess. < 1268227875 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Don't you have any 32-bit compatibility libs, though?-) < 1268227881 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :No, I do not < 1268227886 0 :alise_!~95feda53@gateway/web/freenode/x-lzesngqgkccgcwid JOIN :#esoteric < 1268227888 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I have a 32-bit chroot, which I'd rather avoid when possible < 1268227892 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what was said since um sure i guess < 1268227908 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Three lines that are available in the tunes.org clog log < 1268227925 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well as i'm leaving right now < 1268227926 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric ::p < 1268227936 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: It also generates the output in iso-8859-1; is that a problem, or can you pipe it through iconv or something manually? < 1268227951 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well bye < 1268227968 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Presumably something iconv-like is no problem < 1268227972 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :alise: Bye < 1268228020 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :http://zem.fi/~fis/runogen in that case -- the server will send it as text/plain, unfortunately. < 1268228064 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Awesome < 1268228085 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :It seems something between the program and my screen even automatically understands the 8-bittiness < 1268228095 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Cheers < 1268228110 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268228220 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268228230 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Yes, it's a bit strange; the output looked just fine in rxvt-unicode when I ran it directly, but when I had the Python script print it out, it came up as the missing-character ? signs. I guess Python might do something there, though I was under the impression that if I just used os.popen and read() to get a 'str'-type 8-bit string and then print that, it shouldn't go and alter the bytes. < 1268228252 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Though I had to manually utf-8ify it anyway for Twitter posting. < 1268228332 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Unless I'm mistaken, there was also one undocumented (by -h) command line option, though I can't remember what it did. < 1268228372 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Using "-v -v -v" will give you some printouts of the rule-parsing at least. :p < 1268228464 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Written in C, presumably? < 1268228473 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Written in very ugly C. < 1268228477 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric ::-) < 1268228480 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :That's the main reason there's only binaries. < 1268228495 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Gah, that thing's written in 2002; I'm ashamed of myself. < 1268228575 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Here's a representative snippet of code quality: http://pastebin.com/XvpEJHVv < 1268228588 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Looks good to me < 1268228605 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Maybe I'm overly critical. < 1268228611 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :;-) < 1268228633 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise is a girl < 1268228769 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Well... the win32 gui code at least is a mess. :p < 1268228779 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Ah, but it always is < 1268228890 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: http://pastebin.com/KMqHn2e6 < 1268228900 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: There's even a manually implemented checkbox-listbox thing. < 1268228930 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I like Outo virhe 1 and 2 < 1268228981 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Heh. I don't quite know what they mean. < 1268228982 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :And I wonder what's going on with the number 20000 in get_opts < 1268229002 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Also, the loop: for (i = 20002; i < 20013; ++i) { if (i == 20012) break; ... } is nice < 1268229137 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :At least the messages are cheerful < 1268229208 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I think the mapping there is that 20000+N (for N = 2 .. 10) means to generate a poem of N lines; and 20011 means that the length is taken from some textfield. < 1268229378 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Nnngh. Look at this nonsense: mii.dwTypeData = strdup("&Muu pituus... (xxxxxxxxxxxxxx)"); sprintf(mii.dwTypeData, "&Muu pituus... (%d)", dw); < 1268229424 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Nonsense? :-D < 1268229454 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Makes sense to me; strdup is just a not very efficient way of doing it < 1268229520 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :(And of course it assumes a 32-bit DWORD but I guess everybody does) < 1268229581 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I could've just used snprintf to calculate the length. Except that I guess MSVC calls that _snprintf and it doesn't actually return the number of bytes that were needed, so maybe not. < 1268229672 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :You should use the safer _snprintf_s! < 1268229714 0 :adu!unknown@unknown.invalid QUIT :Quit: adu < 1268229762 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I don't think MSVC6 had the _s functions yet, in fact. < 1268229769 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Probably not < 1268231976 0 :cpressey!~CPressey@173-9-215-173-Illinois.hfc.comcastbusiness.net JOIN :#esoteric < 1268233638 0 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1268234842 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :http://dpaste.com/hold/170444/ < 1268234973 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey its very long :| < 1268234996 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Yeah and it doesn't tell you much you didn't already know, either :) < 1268235008 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I don't really get why don't you just use types to do this proof.. < 1268235037 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But it helped me work out the system (so the comment is really the most valuable) < 1268235051 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :In short, because I don't want to be tied to any particular type system. < 1268235070 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :This method of (basically) pure rewriting lets you roll your own. < 1268235113 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Hm, I guess I could have just done 'nand' to make it shorter. < 1268235140 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268235247 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : oerjan come quick <-- er.. < 1268235465 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION should not have stayed up until 4 last night
< 1268235500 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: now you'll _never_ catch up < 1268235824 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey what does tied to a particular type system mean? what I am suggesting is that a type system could be on you side, rather than against you < 1268235872 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I guess there's no way to make a smalltalk system look like it's native? < 1268236424 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :wow alise is gonna love this http://www.paulkabay.com/#trivialism < 1268236643 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268236654 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1268236973 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: Well, people make up new type systems all the time, as research. I'd like to have something that supports that effort, rather than picking one type system and saying "That's all I got". < 1268236988 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I gotta say, I love trivialism already. < 1268236990 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :bbiab. < 1268236993 0 :cpressey!unknown@unknown.invalid PART #esoteric :? < 1268237133 0 :cpressey!~CPressey@173-9-215-173-Illinois.hfc.comcastbusiness.net JOIN :#esoteric < 1268237260 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: To me, type systems are just a special case of abstract interpretation. < 1268237273 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :isn't that true in general? < 1268237300 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Uh... yes? Not sure what you're referring to. < 1268237307 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well you don't need to say "to me" < 1268237317 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Oh, well < 1268237344 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why don't you have an abstract interpretation module and use it to prove this boolean stuff in a much more effecient way? < 1268237393 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :That was kind of the plan, but I think it turned out that this proof construct thing *is* my abstract interpretation module... < 1268237419 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Abstract interpretations can be mathematically modelled as Galois connections. < 1268237443 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :And these rewrite rules, with types going one way and evaluations going the other way, seem to be... close to that idea. < 1268237531 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :(I guess read my first statement as "Type systems are just a special case of abstract interpretation. Most people seem content to work inside the special case. But I want to design very general things.") < 1268237660 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Galois connections?? < 1268237707 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Oh, I barely understand it myself :/ < 1268237782 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :http://en.wikipedia.org/wiki/Galois_connection vs my shitty explanation http://catseye.tc/about/galois-connections.html < 1268237832 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Also, my examples are wrong, and I think I say "element" where I mean "subset" in one place. < 1268237833 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :abstract values (such as {int, even, odd, power-of-two, prime, ... }). < 1268237840 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :^ THIS AER TYPES!@! < 1268237855 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Yes, I know. < 1268238009 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :And "turing-machines-that-always-halt" is a type, too... < 1268238064 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Just, good luck proving that your function always evaluates to one. < 1268238238 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :aerotypes, just so much hot air? < 1268238388 0 :augur!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1268238436 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Is !x -> x just as inconsistent as !x = x ? In the former, every statement has the same normal form, but there's only one normal form. In the latter, there are no normal forms. < 1268238539 0 :Gracenotes!unknown@unknown.invalid QUIT :Quit: Leaving < 1268238592 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :with intuitionistic logic otherwise, it is. < 1268238606 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :!false -> false, for example < 1268238664 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or hm, x -> !!x is a theorem, so < 1268238677 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :x -> !!x -> !x follows < 1268238873 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :guess who's 24 today :D < 1268238893 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: I agree it's ... on the same level, I just don't know if there is terminology to distinguish between the two. < 1268238896 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :augur < 1268238921 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Hey, augur shares Chuck Norris's birthday. < 1268238931 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: they're equivalent by my argument, in intuitionistic logic < 1268239008 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: Well, maybe replace ! with @ to drop the connotation of "not" ... I'm just thinking symbolically. In both systems, you can pick any two arbitrary statements, like @@@@@x and @@x, and show they are equal. < 1268239039 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :without the connotation of "not" neither is inconsistent < 1268239045 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Only diff is the first says they're equal because they're both equal to x. The second doesn't have to pass through x. < 1268239078 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :er, by "pass through" I mean "refer to x directly" < 1268239100 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :um neither has to pass through x < 1268239104 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or wait < 1268239111 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Oh, you're right. < 1268239113 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well, ... < 1268239128 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1268239148 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I still think they're inconsistent. < 1268239155 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :when you say !x -> x do you mean that there _exists_ an x for which this is true? in which case !x -> x is not inconsistent, just take x = true < 1268239195 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: I mean, for all x, this is true. < 1268239206 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well, not "true" < 1268239228 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: @x = x is not inconsistent if @ has nothing to do with "not" < 1268239232 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :x is a valid evaluation of !x. < 1268239254 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: OK, then I totally don't understand formal logic. < 1268239258 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION goes back to school
< 1268239299 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: and by nothing to do with "not", i mean that you throw away all the other axioms of ! < 1268239300 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :?? < 1268239306 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what's !x? < 1268239311 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: not x < 1268239317 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :in a particular system? < 1268239322 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(if so, which one) < 1268239338 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: i don't think cpressey knows yet :D < 1268239342 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :maybe the problem is that the term "inconsistent" refers to logical systems and by discarding the "logical" meaning of the system, you can no longer use that term? < 1268239370 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: if you have just @x = x, you cannot prove x = y for all x and y < 1268239390 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :one of them has to be a number of @'s applied to the other < 1268239424 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(or to something common, but that happens to be the same thing in this case) < 1268239473 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I think we need to clarify the universe, like what x and y can be < 1268239498 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :clarify the universe by melting it down and seiving it < 1268239508 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :mmmmmm < 1268239510 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :tasty. < 1268239511 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: for example say that @x has the meaning !!x < 1268239536 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :then it is definitely consistent for @x = x to be true, because it's true in classical logic < 1268239565 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :although not necessary, since it is not always true in intuitionistic logic < 1268239576 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If x and y elem {0, @0, @@0, ...} then we can prove x = y for any choice. < 1268239583 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1268239613 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If you start picking them from {0, 1} or something, yeah, I see how you can't prove arbitrary things. < 1268239647 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :OK. Will mull this over. < 1268239856 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1268240009 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :fax D: < 1268240010 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268240011 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :D: < 1268240013 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268240016 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268240021 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION uses email instead
< 1268240025 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268240038 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :so slow :| < 1268240331 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :OK, let me restate. In a system where there is only one value (call it 0), is @x -> x considered just as "inconsistent" as @x = x (which is just shorthand for {@x -> x, x -> @x}), or are there two different terms for "everything reduces to the same normal form, so we can prove any statement" vs. "there are no normal forms, so we can prove any statement"? < 1268240380 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION 's jaw drops
< 1268240384 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :my unit tests actually passed < 1268240424 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: if there is only one value, then @x = x is obviously true < 1268240531 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I might need to rethink again. < 1268240640 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Like, what is a value. If we add another axiom #x = #x, then there are a bunch of irreducible terms #0, ##0, ###0, which are all distinct from 0, at least syntactically -- are they values? Is @@@0 not a value (well, it can't be distinguished from 0 or @0 or any other expression involving @, so maybe not?) < 1268240725 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :(Logic always was my least favourite esolang...) < 1268240768 0 :tombom!tombom@wikipedia/Tombomp JOIN :#esoteric < 1268240824 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: also it is not a requirement of logics to be defined by reductions or have normal forms... < 1268240868 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, oh I see what you mean, like adding a new 'function' as an axiom, without giving it reduction rules < 1268240868 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: Yeah, I realize that. Kind of. < 1268240939 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Kind of like saying it is not a requirement of graphs to be directed :D < 1268240966 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Or to have degeneracies < 1268241064 0 :oklopol!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268241067 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :how old am i? < 1268241077 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i just turned either 21 or 20 a few weeks ago < 1268241084 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :argh < 1268241099 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :http://en.wikipedia.org/wiki/Anus_language < 1268241135 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm almost sure it's 20 < 1268241141 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :didn't i talk about this here? < 1268241149 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm sure i've mentioned my age < 1268241158 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: you'd think that page should have been protected... < 1268241181 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: why donto you figure it out based on your date of birth < 1268241183 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: well i recall you turning 20 i think, and it was more than a few weeks ago < 1268241191 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay, good < 1268241197 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :fax: sounds like a lot of work < 1268241209 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :as in, quite possibly a year and a few weeks ago < 1268241223 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :... wtf. < 1268241229 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :also i think my memory problems are funny, which is also a reason to ask < 1268241260 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION checks what year it is
< 1268241275 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay so this year i turn 2010-1989 = 21 < 1268241280 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so in fact i just had to turn that. < 1268241314 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh right i had to be 20 and not 19 because of something alise said about 19 last year < 1268241327 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i would remember if it'd applied to me < 1268241339 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :clearly oklopol is a being outside time and space < 1268241349 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :with troubles adapting < 1268241353 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, quick, fetch a GPS! < 1268241367 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :Hmm < 1268241377 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :except that it depends on the location being on earth < 1268241383 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :which is a small subset of space < 1268241386 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :._. < 1268241402 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :FireFly: you'd think it should be usable in low earth orbit too < 1268241420 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :I guess, but still just a small subset < 1268241714 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :lol my compositions from ~6 years ago are craaaazy < 1268242284 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :in theory, you could use GPS to determine your location anywhere in space < 1268242291 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but it would be rather inaccurate far from the Earth < 1268242406 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :When you're far enough away that the Earth is basically a point, triangulating is hard :P < 1268246061 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268246353 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: success < 1268246381 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :lament: what is success < 1268246473 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :i mean failure < 1268246484 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :but you're unbanned in #Nm < 1268246497 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :n/m- < 1268246527 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :should i join it < 1268246565 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :of course not < 1268246577 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :you should take a stand < 1268246584 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :o < 1268247266 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: I just got one starting with "lohikäärme on lohikäärme ja lohikäärme on lohikäärme"... maybe you should've enforced a bit of variety ;-) < 1268247297 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Although I guess that's arguably validly poetic < 1268247304 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :`translate lohikäärme < 1268247312 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :dragon < 1268247316 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :dragon < 1268247614 0 :MizardX!unknown@unknown.invalid QUIT :Ping timeout: 256 seconds < 1268247720 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1268247983 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: I think there's supposed to be some sort of enforcement like that. < 1268248026 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Apparently not for that rule, though. < 1268248386 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Apparently :-P < 1268248985 0 :MizardX!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268248999 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1268249601 0 :oklopol!unknown@unknown.invalid QUIT :Read error: No route to host < 1268249624 0 :oklopol!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268250131 0 :augur!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1268250441 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: Actually I have other motivations for doing it this way, but they're... of questionable value < 1268250969 0 :kar8nga!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268251968 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1268252828 0 :Phantom_Hoover!~chatzilla@cpc4-sgyl29-2-0-cust108.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268252850 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Is there any need for a modern-day version of INTERCAL? < 1268252866 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I don't think there's been any need for INTERCAL all along < 1268252871 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's still fun to work with, though < 1268252876 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Is there any point, then? < 1268252888 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :there isn't a whole lot of point to much of what we do here < 1268252896 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :although, there's always the chance we might learn something about programming < 1268252897 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Would it be interesting? < 1268252898 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :besides, it's fun < 1268252902 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Or fun? < 1268252905 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Phantom_Hoover: have you seen C-INTERCAL and CLC-INTERCAL? < 1268252910 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Yes... < 1268252914 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :quite a lot of work has gone into modernising INTERCAL already < 1268252966 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :OK < 1268252968 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838] < 1268252975 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that was strange < 1268253034 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1268253233 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1268253515 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Practical INTERCAL for the modern enterprise programmer < 1268253535 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: you just _know_ you need to write that book < 1268253548 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :not now, though < 1268253809 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :there's always the chance we might learn something about the deepest fantasies of wombats, as well. < 1268253815 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :it's just much, much smaller < 1268253829 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :... probably < 1268254007 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hey we'll need to do _some_ animal testing of our telepathic sensors before using them on humans, wombats should be excellent. < 1268254132 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I just got back < 1268254134 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and read the line < 1268254138 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :" there's always the chance we might learn something about the deepest fantasies of wombats, as well." < 1268254141 0 :augur!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1268254142 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it was rather strange < 1268254147 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION tries to locate the context
< 1268254165 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i'm not entirely sure there was any < 1268254184 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, that is rather worrying < 1268254194 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: yep, it was completely out of context < 1268254196 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : although, there's always the chance we might learn something about programming < 1268254197 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :which is why it was so strange < 1268254208 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, and "INTERCAL for dummies"? < 1268254244 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oh I get it now < 1268254278 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well, sufficiently hyperintelligent dummies < 1268254308 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or possibly crash test dummies. that might fit even better, actually. < 1268254335 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric ::E < 1268254338 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :err < 1268254339 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric ::D* < 1268254365 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :...wherein AnMaster reveals himself as really being cthulhu. < 1268254370 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hah < 1268254385 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, or that I'm using qwerty < 1268254404 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well i have no idea if they're close in dvorak or not < 1268254416 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but that would be too simple of course < 1268254511 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :do crash test dummies dream of roadkill sheep? < 1268254690 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Do people in #esoteric dream of inflatable sheep? < 1268254699 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :not normally, no < 1268254702 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :at least, I don't < 1268254715 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :mystery of the cube? < 1268254724 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i cannot honestly say i'm sure i've ever done so < 1268254736 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I haven't dreamt about that either < 1268254765 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :flying and cardinal sheeps possibly. But if so I must have forgot about them < 1268254778 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :what's a cardinal sheep? < 1268254793 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, I believe that pun only works in Swedish < 1268254794 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :or rather < 1268254798 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :English/Swedish mix < 1268254811 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :what is the swedish < 1268254817 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :"karda" is a part of the process for making thread out of wool < 1268254825 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I'm somewhat fuzzy on what exactly it involves < 1268254840 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm karde in norwegian < 1268254843 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and the bits "kard" and "card" are produced the same in Swedish < 1268254847 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :well would be < 1268254853 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :we don't have the latter in any word afaik < 1268254957 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :inflatable sheep my be a cardinal sin < 1268254959 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*may < 1268255010 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :(A sin often practiced by cardinals) < 1268255209 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1268255458 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1268256009 0 :alise!~95fee1b3@gateway/web/freenode/x-zzobsjxhzwajnhzl JOIN :#esoteric < 1268256270 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268256415 0 :alise!~95fedb41@gateway/web/freenode/x-iwnjidfmgfxhgokm JOIN :#esoteric < 1268256418 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :05:41:13 Written in very ugly C. < 1268256421 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :the standard dialect of C < 1268256467 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :05:43:53 alise is a girl < 1268256468 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :inded. < 1268256468 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*indeed < 1268256645 0 :ais523!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268256726 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :07:53:44 wow alise is gonna love this http://www.paulkabay.com/#trivialism < 1268256727 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise http://www.paulkabay.com/#trivialism < 1268256740 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION applauds the psychic connection
< 1268256740 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sorry, I'm already a preëventualist (http://viewsourcecode.org/why/preeventualist/; some links broken) < 1268256876 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm a Stuckist, myself. < 1268256947 0 :pikhq!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268256963 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : /Philosophically/ I guess I cannot reject the proposition that all things are true. < 1268256975 0 :pikhq!~pikhq@75-106-100-139.cust.wildblue.net JOIN :#esoteric < 1268256976 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But only because the question is a bit meaningless: from what frame of reference? < 1268256990 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Even if you supply one, you must define the terms you use - and you cannot do that precisely. < 1268256999 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So perhaps I actually believe that truth doesn't really exist, rather. < 1268257092 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Nah, too easy. < 1268257101 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Something exists, else why am I doing this? < 1268257111 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :And if it exists, might it not be true? It might. < 1268257143 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise philosophically < 1268257145 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise #philosophically < 1268257168 0 :alise_!~95fedb41@gateway/web/freenode/x-cgommqqzrnjkoadn JOIN :#esoteric < 1268257260 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268257291 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :13:38:21 Something exists, else why am I doing this? < 1268257293 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I don't know why you're doing this. < 1268257298 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I gave (ack 4 1) half an hour, and it still didn't finish evaluating. It must hate me. < 1268257310 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Also, the things that exist for you might differ from the things that exist for me. < 1268257324 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Solipsism, while a ludicrously unlikely premise from inside our frame of reference, is still possible. < 1268257333 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And philosophy is all about the possible yet unlikely. < 1268257347 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But it's a sucky basis for action. < 1268257352 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If I assumed cogito-ergo-sum, that wouldn't really be valid in philosophy, since it'd only be valid for me. < 1268257360 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Solipsism, that is. < 1268257368 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And philosophy shouldn't really only work for the author, otherwise it's ... not philosophy. < 1268257375 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So objectively, nothing can be said to exist for certain; < 1268257377 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*certain. < 1268257391 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Truth is still ill-defined either way, though. < 1268257398 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :We have a rigorous definition of provability, but not truth. < 1268257407 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :We call things true if they seem to be true to us. < 1268257425 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Oh, the Axiom of Choice is probably true. But that doesn't really mean anything, it's just human folly. < 1268257433 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So, really, I guess I technically don't believe in anything. < 1268257451 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :In practice though, from this frame of reference, solipsism is bullshit, philosophical zombies don't exist, the universe is objective, and truth is a useful notion. < 1268257451 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey make ack doesn't terminated < 1268257499 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A must confusing jumble of tenses, fax. < 1268257516 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: ... I think I wrote it correctly, (ack 3 2) and such gave a result which corresponded with what I thought I saw when I had the impression I was looking at the Wikipedia page on the Ackermann function < 1268257710 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :or, what they *claim* is the Ackermann function < 1268257735 0 :Asztal!~asztal@host86-156-98-112.range86-156.btcentralplus.com JOIN :#esoteric < 1268258362 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I should probably disappear from IRC for a while. < 1268258385 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :what, again? < 1268258430 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Yes, again. < 1268258432 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Bye! < 1268258434 0 :cpressey!unknown@unknown.invalid PART #esoteric :? < 1268258514 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Bitchin' < 1268258520 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*most < 1268258553 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise_: muphry's law in action < 1268258582 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*Murhpy's < 1268258592 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I just caused a stack overflow of the meta tower. < 1268258608 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :no, yes, wait, argh < 1268258688 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :bufuhukfbawf < 1268258700 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1268258726 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: that's a very naughty word < 1268258735 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :my style is strictly ruude < 1268258738 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :aramakayhe < 1268258759 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION wonders what's a better name for "data" that more strongly suggests induction and not just boring... data
< 1268258766 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :"Inductive" is a bit too long. < 1268258774 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1268259479 0 :cheater2!~cheater@ip-80-226-239-158.vodafone-net.de JOIN :#esoteric < 1268259665 0 :cheater3!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268260229 0 :tombom!unknown@unknown.invalid QUIT :Quit: Leaving < 1268261172 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1268262165 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :doing classical logic in constructivist logic is fun < 1268262218 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :Try doing the non-contradiction theorem! < 1268262357 0 :oklopol!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268262468 0 :oklopol!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268262500 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Slereah: What, not (p and not p)? < 1268262513 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :Yeah < 1268262515 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :That's in constructivist logic too :P < 1268262521 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :IS IT? < 1268262534 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :Or am I thinking of p or not p < 1268262535 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1268262545 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268262547 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :We get rid of (p \/ ~p), not ~(p /\ ~p) < 1268262553 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :Ah yes < 1268262560 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :I often confuse them < 1268262561 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The way to do classical logic in constructivist logic is to write everything as (p \/ ~p) -> ... < 1268262565 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :Contradiction and... < 1268262569 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :What's the other name < 1268262579 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you can define classical P OR Q :<=> ~~(P \/ Q) < 1268262579 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Law of the excluded middle. < 1268262582 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and so on, < 1268262592 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :then you can prove classical tautologies < 1268262609 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :taut eulogies < 1268262610 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/864149.txt?key=efscdf3wmdhlbyfpnxqfdw < 1268262641 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :proof of (p->q) -> (~p->~q) -> q -> p classically < 1268262655 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :You have a taut body < 1268262656 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I love the beauty of just letting LEM hand us a contradiction, at which point we simply take its word and prove the thing we want to prove, whatever it is, from it. < 1268262660 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :I can tell from your taut pants < 1268262683 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :Trivial system ~ < 1268262685 0 :oklopol!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268262689 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :Everything is true! < 1268262716 0 :oklopol!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268262754 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :There are no trivial mathematics, just trivial mathematicians < 1268262776 0 :FireFly!unknown@unknown.invalid QUIT :Quit: Leaving < 1268262779 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :shut up < 1268262795 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268262796 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :lament feels singled out there < 1268262831 0 :alise__!~95fedb41@gateway/web/freenode/x-fcgnuruvcivvacuz JOIN :#esoteric < 1268262850 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION realises he redefined modus tollendo ponens in that proof
< 1268262890 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Well, almost. < 1268262914 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268263047 0 :Slereah!unknown@unknown.invalid PRIVMSG #esoteric :modus penis < 1268263118 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :alise__: are the implications left-associative or right-associative? < 1268263155 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :right-associative. Obviously. As they're also the function arrows. < 1268263179 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh. wait what? < 1268263195 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Curry-Howard isomorphism. Types = statements in constructivist logic. < 1268263203 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Values = proofs. < 1268263203 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :(In a dependently-typed language.) < 1268263204 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION explodes
< 1268263208 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :It's the future, mon. See: Agda, Coq, Epigram. < 1268263223 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :future < 1268263226 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :FUTURE < 1268263237 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I'll believe you when I see it in .NET :P < 1268263246 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :.NET: The Future < 1268263247 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :non-dependently typed too. just you only get propositional logic then, or thereabouts. < 1268263263 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :.NET is looking to be the future, regrettably < 1268263292 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: propositional logic is for butts < 1268263333 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i see an obvious pun but i'll leave it for Slereah < 1268263428 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :nice of you to throw him some scraps of meat that you can't be bothered to pick from the bones < 1268263499 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's more like it seems more his style < 1268263507 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(see above) < 1268263690 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :metastruct will be so cool :| < 1268263729 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :does anyone know a program that will simply ask X to clean up any temporary resources it has hanging around? < 1268263740 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i n *hit by falling anvil* < 1268263741 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :so that I don't have to write one myself < 1268263768 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1268263778 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :foo : (ProgDescription -> Prog) -> Prog < 1268263787 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :shutdown -r < 1268263793 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :foo p = englishDescr "ask X to clean up any temporary resources it has hanging around" < 1268263796 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1268263801 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :foo p = p (englishDescr "ask X to clean up any temporary resources it has hanging around") < 1268263813 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :the program is (foo _) < 1268263815 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :where _ is obvious. < 1268264001 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268264293 0 :oklopol!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1268265393 0 :oerjan!unknown@unknown.invalid QUIT :Quit: Good night < 1268265425 0 :oklopol!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268265446 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :coppro: kill -9 < 1268265456 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(note: all resources considered temporary) < 1268265467 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :haha < 1268265519 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Resources should totally include their extents.