< 1268092802 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :But your proofs aren't proofs and if they were they'd be nothing in particular. If I'm reading your snippet right. < 1268092807 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :fundamental theorem was solutions of XY = YX? < 1268092815 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok, okay but can you give me one hint on OR? < 1268092825 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :because right now I am just sort of lost < 1268092843 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok but this finite calculus is so cool! < 1268092844 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: How would you prove that pop(push(X,Stack)) == Stack ? < 1268092853 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Also, I assume that your proofs are first-class values. So how do you create a function taking a function from a positive rational to a rational, and also a proof that for all positive rationals e1 and e2, |f e1 - f e2| < e1 + e2? < 1268092874 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Or could you give me an example of something more interesting that could be proved (but still under a page of derivation)? < 1268092877 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i.e., a function taking (f, |f e1 - f e2| < e1 + e2), also known as a computable real < 1268092880 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :yeah fundamental theorem was your pet name for the commutation thing < 1268092881 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, in dependent type theory this would be a trivial proof, because pop(push(X,Stack)) would compute down to Stack, so all you really need to prove is Stack == Stack < 1268092883 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: depends < 1268092883 0 :bsmntbombdood_!~gavin@174-16-89-136.hlrn.qwest.net JOIN :#esoteric < 1268092908 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: A better example to prove would be most welcome, then < 1268092912 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey (if P reduces to P' then a proof of P is a proof of P') < 1268092920 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: I gave you one. < 1268092930 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: I don't have functions in my language < 1268092936 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :okay for OR, the first thing is to reduce it to a=b OR a=c. < 1268092937 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :or reals, for that matter < 1268092944 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: You don't need reals. < 1268092945 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok, I think it has something to do with sequence of lydon words.. (because you told me that) < 1268092945 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I just defined the reals. < 1268092953 0 :bsmntbombdood!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1268092959 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok, okay byebye! < 1268092961 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :at least i think that's the easiest way < 1268092962 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: You're too quick for me. < 1268092974 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: The tuple (f : Q+ -> Q, forall e1, e2 : Q+, |f e1 - f e2| < e1 + e2) is a computable real. < 1268092983 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(Which is just like the reals, except without things like chaitin's constant) < 1268092987 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :fax: nope, lyndon's aren't useful at all, i just like them. < 1268092995 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok, oh :p < 1268092999 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: The second element is a property of the first, a function. < 1268093002 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I thought they were integral to this < 1268093014 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :ah, sorry if i gave you that impression < 1268093024 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: (Basically pi 0.1 = 3.1, pi 0.01 = 3.14, etc) < 1268093025 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268093040 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: So, substitute whatever is the best analogue for a function. < 1268093047 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :How do you construct the proof? < 1268093055 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: I'm not going to be able to prove that without defining some axioms for ordering and stuff. < 1268093070 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: You don't need any axioms above the standard for this < 1268093085 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :i've basically lectured you parts of the "introduction" chapter of our combinatorics on words course, so things don't necessarily progress that linearly yet! < 1268093109 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Basically, we have term rewriting. We say, "X rewrites into Y"! The proof is simply to list the derivation. Maybe this isn't very impressive to *you*, but remember what world *I'm* living in. < 1268093116 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :oh well actually chapters 1 and 2 < 1268093125 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: So construct the computable reals. < 1268093141 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :where "lectured" == "listed theorems as exercises" ;) < 1268093143 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: No. What am I proving about them? Their existence? < 1268093143 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :anyway I better go to bed < 1268093149 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :me too < 1268093159 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: No. < 1268093169 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Okay, let me express this in Haskell-ish things for you. < 1268093175 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"for all positive rationals e1 and e2, |f e1 - f e2| < e1 + e2" is closer, but requires, like, numbers and shit. < 1268093181 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Symbolic. < 1268093196 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data Real = Real (Q+ -> Q) (forall (e1:Q+), (e2:Q+). abs (f e1 - f e2) < e1 + e2) < 1268093200 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The latter bit is the dependent part. < 1268093205 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So, to construct a computable real, we do < 1268093210 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Real f (proof of that property of f) < 1268093222 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So a Real is a function that satisfies a certain property; you must prove it does. < 1268093235 0 :fax!unknown@unknown.invalid QUIT :Quit: Lost terminal < 1268093238 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So if we have p : (forall (e1:Q+), (e2:Q+). abs (f e1 - f e2) < e1 + e2), p is a proof of that. < 1268093253 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If A is a rational, and B is a rational, and f is a function(?), the absolute value of the difference between f(A) and f(B) is less than the sum of A and B. ? < 1268093256 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Since all your proofs are just simply proving that x evaluates to x', it's pointless. < 1268093264 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The proof is nonexistent; x equiv-to x' by virtue of evaluating to it. < 1268093267 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So the proof is that x = x. < 1268093277 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: *positive rational, not rational. < 1268093278 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 264 seconds < 1268093279 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Also, no. < 1268093285 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Sigh. < 1268093300 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It is only true for some functions. Obviously. < 1268093312 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Our constructor takes a function f, and a proof that that holds /for only the single function f that we give/. < 1268093332 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :That's a proof *schema* in my book. < 1268093332 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Any function that satisfies that property is a /computable real/, so to create a computable real we must /supply a proof that the function we give obeys the property/. < 1268093344 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So, how would you structure such a thing? < 1268093353 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I bet you can't, because your proof construct is uber-limited. < 1268093365 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1268093398 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Nowhere did I say I was writing a *prover*, only a *proof checker* < 1268093412 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :What is the problem with specifying f in my proof? < 1268093413 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Irrelevant. < 1268093425 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You cannot even /express the proof/ in your language, because you can only prove things of the form x = eval x < 1268093437 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And you cannot check a proof you can't express. < 1268093451 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If there are some values for f where it holds, and others where it doesn't, then it's not a proof! < 1268093497 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You prove it for some given function f. < 1268093506 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Right, so give me some function f. < 1268093512 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :And I'll write the proof. < 1268093517 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If you don't, I can't. < 1268093538 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i : Q -> R; i q = (\_. q, ...proof...) < 1268093541 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Like I said, what you gave sounds like a proof schema to me. < 1268093544 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Really simple there. < 1268093547 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Write the proof in your language. < 1268093557 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :\x. e being lambda, of course. < 1268093625 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :How am I supposed to read that? < 1268093650 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :i takes the rationals to the reals; i is some function... < 1268093664 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :... which contains a proof... < 1268093688 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i : Q -> R -- i is a function from rationals to reals. < 1268093692 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Digression: < 1268093723 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :type R = (f : Q+ -> Q, forall (e1,e2 : Q+). abs (f e1 - f e2) < e1 + e2) < 1268093724 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so < 1268093733 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i q = (\_. q, ...) < 1268093742 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :\_.q is a function taking one argument, ignoring it, and returning q < 1268093760 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you must now prove that for all positive rationals e1 and e2, |(\_. q) e1 - (\_. q) e2| < e1 + e2 < 1268093761 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i.e. < 1268093770 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you must now prove that for all positive rationals e1 and e2, |e1 - e2| < e1 + e2 < 1268093773 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but you can't just assume that < 1268093778 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :do it methodically with your proof construct < 1268093780 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(I don't believe you can) < 1268093821 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"you must now prove that for all positive rationals e1 and e2, |e1 - e2| < e1 + e2" - that sounds at least closer to a sane request, but it still will require me defining rationals, to do it completely symbolically. < 1268093845 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well, no. I mean, |a - b| = a + b < 1268093851 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I assume you meant <= < 1268093859 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well, no. < 1268093868 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I mean, could = a + b < 1268093875 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Oh wait, positive. < 1268093882 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: also, no < 1268093884 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you must now prove that for all positive rationals e1 and e2, |(\_. q) e1 - (\_. q) e2| < e1 + e2 < 1268093890 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I did it wrong :D < 1268093899 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :What is q in that statement? < 1268093909 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the argument to the function i. pay attention < 1268093912 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :=> for all positive rationals e1 and e2, |q - q| < e1 + e2 < 1268093916 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :=> for all positive rationals e1 and e2, |0| < e1 + e2 < 1268093920 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :=> for all positive rationals e1 and e2, 0 < e1 + e2 < 1268093931 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(prove so) < 1268093933 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :=> for all positive rationals e1 and e2, true < 1268093935 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :=> true < 1268093942 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but you must prove it /with your proof construct/ < 1268093944 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :=> QED < 1268093947 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that's the whole point; it's verified < 1268093986 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :OK, if a > 0, and b > 0, then a + b > 0, I can do. I *still* do not know what you are talking about with your function i. Do you want this quantified over all possible functions i? < 1268094016 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION sigh
< 1268094023 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You know Haskell. Correct? < 1268094032 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Assume that I do not. < 1268094063 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Look, actually forget it. Thanks for your feedback. If I'm making a huge error I'm sure I'll figure it out myself. < 1268094068 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Later, folks. < 1268094070 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Seems to be more functions of the type (i :: a -> R) < 1268094070 0 :cpressey!unknown@unknown.invalid PART #esoteric :? < 1268094109 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :No, wait, more specific, :: Q -> R. Anyways. < 1268094141 0 :alise!~d4b78c32@gateway/web/freenode/x-vdlhcriannubqqsb JOIN :#esoteric < 1268094149 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :If you didn't know Haskell I couldn't explain it in a million years. < 1268094184 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Sounds like a personal problem. < 1268094190 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sure you could. You could give a Haskell tutorial. < 1268094255 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Do you have any idea what dependent type theory is? < 1268094260 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Haskell is utter peanuts in comparison. I have to assume some baseline. < 1268094284 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268094308 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I have no formal experience with dependent type theory, only indirect. < 1268094316 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Erm, indirect isn't the right word. < 1268094319 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Informal, I suppose. < 1268094321 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :i don't remember what peanuts taste like, but i'm sure i love them < 1268094393 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :What a tragic statement :P < 1268094430 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :thank you about me. < 1268094566 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I keep looking down, not seeing a tie, and thinking "?!" < 1268094568 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Silly bowtie. < 1268094610 0 :werdan7!unknown@unknown.invalid QUIT :Ping timeout: 624 seconds < 1268094778 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268094795 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :do you like clothes? < 1268094842 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Clothes are for the weak. < 1268094858 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :sooooo... you don't? < 1268094877 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :he wears a barrel < 1268094880 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :and a bear skin < 1268094884 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :i mean you wear all sorts of different clothes, which is weird if you, like normal humans, hate wearing clothes < 1268094896 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :And a necktie. < 1268094903 0 :werdan7!~w7@freenode/staff/wikimedia.werdan7 JOIN :#esoteric < 1268094914 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Just a barrel, a bear skin and a necktie. < 1268094915 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :That's me. < 1268094926 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Well, on a dressier day. < 1268094932 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I lose the barrel on average days. < 1268094943 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :which days are the average days? < 1268094947 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :somehow i feel i'm the only one being serious < 1268094950 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :how does one calculate that < 1268094955 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Pretty much anything other than going to a wedding or whatnot. < 1268094966 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :weddings are the outliers of my life! < 1268094979 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Hence why they're not the normal days. < 1268095440 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/real.pdf < 1268095444 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The ramblings of a crazy man. < 1268095578 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I learned something great from Ruby: Fibers! < 1268095593 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :"Andrew Wiles's alleged `proof' of FLT, while a crowning human achievement, is not rigorous, since" < 1268095594 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I think Fibers would be very useful in the C# project I'm working on < 1268095602 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :"it uses continuous analysis, which is meaningless." < 1268095604 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: fibers are shit < 1268095624 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :yeah looking at this pdf... it's crazy < 1268095625 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Howso? And is there ANYTHING that isn't? < 1268095802 0 :FireFly!unknown@unknown.invalid QUIT :Quit: Leaving < 1268095805 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :Well, for instance, he's telling us stuff like "sqrt(2) doesn't exist" < 1268095813 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1268095816 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :he is talking to me < 1268095821 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: because fibers are like continuations and coroutines but shittier < 1268095852 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :ph < 1268095854 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1268095878 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Well, I want something that lets me resume the current .. thing later < 1268095893 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I'm willing to work with whatever exists the most in .NET < 1268095898 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: continuations. coroutines. < 1268096130 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Continuations exist in .NET? < 1268096150 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :no, but .net is almost useless for programming. < 1268096175 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :.net is the best < 1268096184 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :if you hate yourself. < 1268096191 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Continuations can be done in .Net. < 1268096202 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :By which I of course mean CPS. < 1268096210 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Only via... yeah. < 1268096219 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I understand call/cc better than CPS < 1268096251 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: CPS is simply the act of transforming the usage of return values to a function that takes a value. < 1268096277 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Instead of "x = function_call(bar);", you do "function_call(bar, \x -> ...);" < 1268096294 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And that was a delicously odd hybrid of C and Haskell syntax. < 1268096601 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :So, Chrome maps the numpad keys, with numlock on, to the keyCodes 97 etc. < 1268096611 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :97, for the non-ASCII-inclined, is lower-case 'a'. < 1268096621 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :(The key 'A' sends a capital A, 65) < 1268096638 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :That's ... confusing. < 1268096726 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Oh look, Firefox does it too. < 1268096727 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Weird. < 1268096782 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268096791 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :grop < 1268097188 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268098105 0 :Asztal!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268098151 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :weird html5 keyboard handling? < 1268098505 0 :oklokok!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268099560 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Weird blaming of HTML5 for totally irrelevant things? :P < 1268099619 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1268100298 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1268100444 0 :Oranjer!unknown@unknown.invalid QUIT :Quit: Leaving. < 1268103661 0 :Oranjer!~HP_Admini@adsl-71-7-92.cae.bellsouth.net JOIN :#esoteric < 1268104092 0 :OxE6!~mu@wireless-lsusecure-9.net.lsu.edu JOIN :#esoteric < 1268104806 0 :Oranjer!unknown@unknown.invalid QUIT :Quit: Leaving. < 1268105751 0 :Oranjer!~HP_Admini@adsl-71-7-92.cae.bellsouth.net JOIN :#esoteric < 1268106144 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ugh, people in #latex treating me like I've never used a text editor before; much less LaTeX < 1268106217 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :I've never used LaTeX < 1268106591 0 :myndzi\!myndzi@tengototen.net JOIN :#esoteric < 1268106618 0 :myndzi\!unknown@unknown.invalid NICK :myndzi < 1268106806 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :anyone know a LaTeX equivalent of OO.o Math's csub? < 1268106847 0 :coppro!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268107020 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268107066 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric : a "tnx you badass" would have been appreciated... < 1268107137 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: firefox crashed < 1268107177 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Ah < 1268108476 0 :GreaseMonkey!~gm@unaffiliated/greasemonkey JOIN :#esoteric < 1268111564 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268112811 0 :adu!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268113132 0 :pikhq!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268113356 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1268113425 0 :Oranjer!unknown@unknown.invalid PART #esoteric :? < 1268113437 0 :pikhq!~pikhq@75-106-100-139.cust.wildblue.net JOIN :#esoteric < 1268113466 0 :bsmntbombdood_!unknown@unknown.invalid NICK :bsmntbombdood < 1268113770 0 :Gracenotes!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268114230 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I discovered http://www.periodicvideos.com/ today :( < 1268114475 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :now I'll never get to sleep < 1268114885 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :the one guy looks like your stereotypical professor < 1268114887 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :and he is < 1268115324 0 :coppro!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268115326 0 :Halph!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268115334 0 :Halph!unknown@unknown.invalid NICK :coppro < 1268115335 0 :werdan7!unknown@unknown.invalid QUIT :Ping timeout: 619 seconds < 1268115389 0 :yetifoot!~user@unaffiliated/yetifoot JOIN :#esoteric < 1268115413 0 :yetifoot!unknown@unknown.invalid PART #esoteric :? < 1268115681 0 :werdan7!~w7@freenode/staff/wikimedia.werdan7 JOIN :#esoteric < 1268115944 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1268116937 0 :oerjan!unknown@unknown.invalid QUIT :Quit: leaving < 1268117329 0 :MizardX!unknown@unknown.invalid QUIT :Ping timeout: 268 seconds < 1268118179 0 :tombom!tombom@wikipedia/Tombomp JOIN :#esoteric < 1268118537 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : anyone know a LaTeX equivalent of OO.o Math's csub? <--- what does csub do? < 1268118551 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :nevermind, found it < 1268118569 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :coppro, but I'm genuinely interested! < 1268118572 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :busy watching videos that tell me things I already know in humourous manner < 1268118583 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: positions a subscript directly below the principal < 1268118590 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :done with \underset < 1268118595 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION will attempt to learn E tomorrow
< 1268118595 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :right < 1268118598 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :E? < 1268118610 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :D done correctly :P < 1268118619 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :http://www.erights.org/elang/ < 1268118636 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Supposed to be secure distrubuted language thingy < 1268118656 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :sure that isn't Erlang? < 1268118662 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :(that you're thinking of; not the site) < 1268118721 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I'm pretty sure < 1268118833 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :G'night < 1268119009 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Morning. < 1268119029 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : I discovered http://www.periodicvideos.com/ today :( <--- looks interesting < 1268119044 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :it is < 1268119086 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : Supposed to be secure distrubuted language thingy sure that isn't Erlang? <-- "secure" isn't a way I would describe erlang. Not insecure either though. < 1268119104 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I mean, it isn't specifically geared towards security < 1268119108 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :bbl < 1268119111 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :that's true < 1268119130 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I mentioned it specifically because it's 'elang' < 1268119162 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Bot-tweets are getting a bit suspicious: "About IRC: for sex.. assembly language reminds you at very instruction. at http://paste.lisp.org/display/UNK" < 1268119225 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :sulphur is a really good video < 1268119238 0 :fungot!~fungot@momus.zem.fi JOIN :#esoteric < 1268121228 0 :tombom!unknown@unknown.invalid QUIT :Quit: Leaving < 1268121317 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :you must watch iron < 1268121322 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :the story is hilarious < 1268121599 0 :clog!unknown@unknown.invalid QUIT :ended < 1268121600 0 :clog!unknown@unknown.invalid JOIN :#esoteric < 1268121973 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 264 seconds < 1268122038 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1268122873 0 :madbr!unknown@unknown.invalid QUIT :Quit: Radiateur < 1268123290 0 :oklokok!~oklopol@dsl-tkubrasgw1-fe27dc00-89.dhcp.inet.fi JOIN :#esoteric < 1268123848 0 :Asztal!~asztal@host86-159-105-237.range86-159.btcentralplus.com JOIN :#esoteric < 1268124728 0 :coppro!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1268125653 0 :adu!unknown@unknown.invalid QUIT :Quit: adu < 1268126128 0 :GreaseMonkey!unknown@unknown.invalid QUIT :Quit: HydraIRC -> http://www.hydrairc.org <- Nobody cares enough to cybersquat it < 1268126578 0 :oklokok!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1268127622 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1268129077 0 :Asztal!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268129399 0 :amca!~amca@CPE-121-208-82-97.cqzr1.cha.bigpond.net.au JOIN :#esoteric < 1268129531 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268131851 0 :oerjan!unknown@unknown.invalid QUIT :Quit: leaving < 1268131913 0 :amca!unknown@unknown.invalid QUIT :Quit: Farewell < 1268137448 0 :alise!~d4b78c25@gateway/web/freenode/x-jvetrjubbqhpthfm JOIN :#esoteric < 1268137473 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hypothesis: It is impossible to be comfortable. < 1268137560 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :19:42:24 ugh, people in #latex treating me like I've never used a text editor before; much less LaTeX < 1268137572 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Most users of LaTeX are near computer-illiterate, I think. < 1268137579 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Mostly mathy people. < 1268137623 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: E is interesting but not nearly as magical as you think. < 1268137637 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And it requires a good understanding of its principles to use. < 1268137652 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :wow < 1268137656 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :thanks asshole alise < 1268137671 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :What? < 1268137690 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :I am in #LATEX < 1268137703 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :and too bad coppro isn't here; I could help him < 1268137704 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You mean my LaTeX remark? "Most users of LaTeX are near computer-illiterate" = >50% of LaTeX users are computer-illiterate. < 1268137706 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :I love latekz < 1268137716 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :LaTeX is fine. < 1268137723 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: thank you, you're saying there's a >50% chance I'm computer illiterate < 1268137740 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: No, because there is a large deluge of other evidence to suggest you are not. < 1268137744 0 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1268137748 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :okay I am happy then :))) < 1268137749 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :For instance, anyone in #esoteric is almost certainly highly computer literate. < 1268137760 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hi ais523. < 1268137803 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1268137824 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I have a seminar in half an hour, but am happy to talk until then < 1268137840 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: about Feather. < 1268137860 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, if you have questions... < 1268137867 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I haven't thought much further on it, though < 1268137872 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: What is Feather, in detail? < 1268137874 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :>:) < 1268137894 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : god dammit, you asshole! < 1268137898 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, I'm not sure myself < 1268137901 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : We were sane for a while there! < 1268137929 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :let's see... you start with a very small TC language < 1268137936 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I'm planning to use lambda calculus + continuations < 1268137950 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and a very small bootstrap program, written in that language < 1268137998 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :originally, the bootstrap is just an implementation of that language; simplicity is more important here than correctness or features or anything, so long as it remains TC < 1268138009 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :wait, it has to be correct < 1268138017 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but it doesn't matter if it has no error handling or something like that < 1268138037 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :now, the bootstrap program has to be written in a vaguely object-oriented style < 1268138057 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it doesn't need to be actual OO or even a C++ level of OO, but it needs to have parts which are vaguely identifiable as objects < 1268138073 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :lambda calculus + continuations; interesting < 1268138078 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and the property, that each of those parts can be retroactively replaced < 1268138079 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'm going to implement that < 1268138118 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the easiest way to do this seems to be to make each part the return from a call/cc, or somehow otherwise have a continuation that goes back in time to when it was created and replaces it < 1268138130 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: are you sure you absolutely need lambda if you have continuations? < 1268138133 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :calculus of continuations! < 1268138152 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: I'm not, but it's likely to make the self-interp shorter and easier to write < 1268138159 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: also, LC sucks, make it combinator calculus < 1268138173 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :LC has syntactic stupidities like (\f x.f x) vs f < 1268138174 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and Subtle Cough was proved non-TC, so you need /something/ other than call/cc, at least < 1268138180 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and (\x. x) vs (\y. y) < 1268138188 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :de bruijn indexes solve the latter but you still need n-conversion < 1268138203 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: planned Feather syntax is [ x | f x ] < 1268138208 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :for \x.(f x) < 1268138213 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So what? < 1268138222 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :semantics (\f x. f x) = semantics f < 1268138223 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but < 1268138223 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: because if I didn't say, AnMaster would ask < 1268138228 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(\f x. f x) =/= f < 1268138240 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, semantics (\x. f x) = semantics f < 1268138247 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :semantics (\x. x) = semantics (\y. y) < 1268138249 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but etc < 1268138252 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :De Bruijn indexes solve that one: < 1268138257 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :semantics (\0) = semantics (\0) < 1268138259 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :\0 = \0 < 1268138263 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but not n-conversion: < 1268138272 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the same problem happens even with combinators < 1268138278 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :n conversion? < 1268138281 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :ETA CONVERSION? < 1268138284 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :erm oops I wrote it wrong < 1268138292 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :semantics (\x. f x) < 1268138293 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and, well, in general because you can't compare functions in general in a TC language < 1268138305 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: you compare syntactic structure < 1268138317 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :anyway n-conversion + de bruijn indexes make it work < 1268138319 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, ``skk is semantically equal to i, for instance < 1268138320 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but n-conversion is ugly < 1268138326 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :converting (\{f} 0) to {f} < 1268138332 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :where {f} is f's current identifier number < 1268138349 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: that's irrelevant though < 1268138361 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(\x. f x) is literally /the same function/ as f < 1268138364 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :just written a different way < 1268138370 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :skk is more like a different implementation of the same thing as i < 1268138387 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I'm not convinced that (\x. f x) is the same function < 1268138404 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it certainly isn't in a strict lang if determining the value of f has side effects < 1268138415 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :then f isn't a value :P < 1268138461 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep; this argument only works if f is a function constant < 1268138466 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :this is such a weird discussion < 1268138474 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :perhaps the issue here is, that constant folding on functions is a fool's errand < 1268138488 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :because you end up evaluating the whole program at compile time, and if it contains an infinite loop you're in trouble < 1268138493 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: it's the sort of discussion we have here < 1268138543 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :ais523: I know < 1268138548 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :But this needs to be more interesting < 1268138558 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: let's put it this way - eta-conversion + n-reduction and then comparing syntactic structure is the kind of thing we do in our fancy functional langs :P < 1268138562 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :although I credit alise and him talking about de bruijn seqs < 1268138562 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :anyway, anything remotely related to Feather is inherently weird < 1268138573 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: de bruijn indexes < 1268138576 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :different thing < 1268138578 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: as an optimisation? < 1268138579 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :idxs, yeah < 1268138581 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :that's what I meant < 1268138591 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: no < 1268138606 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :why, then? < 1268138614 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hmm... the type of continuations is really strange < 1268138635 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well, of callCC, specifically < 1268138654 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :continuations have a relatively simple type (function from some type to bottom) < 1268138661 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :((a -> X) -> a) -> a < 1268138665 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :where X is forall b. b < 1268138668 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :call/cc, yes, that's weird < 1268138675 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :which is actually exists b. b < 1268138684 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :which is actually isomorphic to () :-) < 1268138693 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but we have it as forall for convenience... < 1268138719 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: the isomorphism there is misleading, I think < 1268138731 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's true, though < 1268138734 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :type-theoretically < 1268138740 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes, but rather vacuous < 1268138749 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :no, actually < 1268138759 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :T (except the opposite of _|_) really is the supertype of all types, theoretically < 1268138764 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in practice, you implement it like data T = T < 1268138771 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because they're the same thing < 1268138773 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(it also represents truth) < 1268138782 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(where false is the empty type, _|_) < 1268138808 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : App :: LC (a -> b) -> LC a -> LC b -- it annoys me that you can't do this < 1268138820 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because it stops you writing `semantics :: LC a -> a` < 1268138871 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :top bot < 1268138891 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :modal logic is weird; it has _|_, T, 0, and 1 as logic values < 1268138907 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :where 0 and 1 vaguely correspond to false and true, T to both, and _|_ to neither < 1268138913 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The fundamental theorem of type theory: all types are sandwiched between an act of gay sex, top to bottom. < 1268138924 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: hahahahaha < 1268138928 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :that is great < 1268138948 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, "bottom" is a stupid name for it < 1268138953 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's not < 1268138962 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's at the bottom of the type hierarchy < 1268138964 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I've seen "eet" used for the same symbol ("tee" spelt backwards), for instance < 1268138982 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: I know why it has that name; but it's too many syllables and looks nothing like the symbol < 1268139009 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :I just like to call them top and bot < 1268139013 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :literally "bot" < 1268139020 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :like bot fly :( < 1268139078 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: Maybe I should recruit you for helping me design my language < 1268139097 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :since you seem more competent about type theory and stuff than I originally imagined < 1268139107 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: alise is an expert on that sort of stuff < 1268139111 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : App :: LCC (a -> b) -> LCC a -> LCC (b -> c) -> LCC c -- I wonder how to modify this type to (apart from making it possible to compile) enforce CPS-style. < 1268139114 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I tend to care more about the practice than the theory < 1268139128 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hey, I'm no expert. < 1268139129 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :I like practice too. < 1268139136 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Practice is very, very important. < 1268139152 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hmm. I could fold App's type into Lam. < 1268139161 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So we have LamApp and LamVar. < 1268139168 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But then we can't have a top-level application. < 1268139174 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But I can model that to applying the main function to, say, id. < 1268139215 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : LamApp :: LCC (a -> b) -> LCC (b -> c) -> LCC (a -> c) -- Hey, look. It's compose. < 1268139438 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Yeah, this model isn't workable. < 1268139600 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh well, time for my seminar < 1268139610 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Seminyarrrrrrrr < 1268140034 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Aw man, my HOAS broke cwcc < 1268140045 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION is probably going to have potato chips for breakfast
< 1268140448 0 :Asztal!~asztal@host86-156-98-112.range86-156.btcentralplus.com JOIN :#esoteric < 1268140714 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 268 seconds < 1268140727 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I now have an interpreter for the Lambda Calculus of Continuations, but no pretty-printer, so I can't test it. < 1268141058 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :So, put differently, you have nothing. < 1268141097 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Well, I'm going to write a type-inferrer so that I can see the sort of results. < 1268141103 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Any hey, I can make it loop forever. < 1268141126 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Wait, all LC expressions have the type a = a -> a. < 1268141130 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Um. < 1268141145 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The AST isn't terribly conducive to pretty-printing: < 1268141150 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :data LCC t where < 1268141152 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : App :: LCC Lam -> LCC Lam -> LCC Lam -> LCC App < 1268141154 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : Lam :: (LCC Lam -> LCC Lam -> LCC t) -> LCC Lam < 1268141210 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, should I learn Common Lisp or Scheme [I think I may have asked you this before]. Although Scheme seems attractive, there's pretty much no large standard library < 1268141222 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Don't know if CL has one, but from what I gathered.. < 1268141287 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'm not even going to answer because you seem to value a language based on how many BSD socket libraries it has, and this is poisonous. < 1268141323 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Scheme (R5RS, not R6RS) is clearly the superior language. Common Lisp doesn't have standard sockets either. It does have Roman Numeral support, though. < 1268141360 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :...who said anything about sockets? < 1268141423 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The prototypical example of a "practical" "standard" "library"> < 1268141423 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*. < 1268141559 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: So, uh, tell me about your language. < 1268141670 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, Quadrescence and Gregor seem to hate PLT Scheme, I'm still not sure why. Do you have any comments on PLT Scheme? < 1268141683 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :It is a language that is intended to be practical for general programming, but will be particularly designed for building a computer algebra system with it. I want it strictly statically typed, however, if a certain type can't be proven/shown, that should NOT error, but be left for run-time resolution < 1268141690 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :PLT Scheme [...] is rubbish. < 1268141706 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Use SISC, or Scheme48, or Chicken, or ... < 1268141724 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: Computer algebra system: You want a term rewriting language. (Trust me.) < 1268141740 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :A typed one is an endeavour I've looked into before, and one that is very interesting. < 1268141747 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: Yes definitely < 1268141757 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :I've read my fair share of TRS junk < 1268141764 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: But as for the untyped-leave-to-runtime... Why not just have a more powerful type system? < 1268141799 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :In what way is PLT rubbish? < 1268141812 0 :ztirf4!~ztirf@HSI-KBW-085-216-050-047.hsi.kabelbw.de JOIN :#esoteric < 1268141837 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: To understand the reasons why you'd have to understand Scheme. < 1268141837 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Catch-22. < 1268141842 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Trust ze sexperts. < 1268141860 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Every single implemented dependent type system is annoying as ! to use, at least in my opinion. I don't want the programmer to fight with the compiler; I want him/her to work with it. This is NOT to say the type system can't be powerful! I am just saying things should be optional in a sense. < 1268141883 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, how well do I have to understand Scheme? I think I understand the basics at this point < 1268141894 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: Well, I agree that most dependently-typed languages aren't too nice to use. < 1268141897 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: almost entirely. < 1268141906 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Knowing some functions and stuff won't make you "know" scheme < 1268141910 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: But, I mean, my main project is to make dependently-typed languages nice. < 1268141913 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :You really have to "see the light" to know scheme < 1268141917 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: So you must understand that I'll push for that. :-) < 1268141931 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: Of course. I *want* dependent types. < 1268141936 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Also, even something like Haskell's type system can be extended a little bit to make it lenient for anything you'd want. < 1268141938 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :So, what Scheme is most recommended for newbies? < 1268141949 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: Right. My opinion is that you can make them nice /and/ mandatory. < 1268141965 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Well, not SISC, too barebones... Scheme48 or Chicken. Chicken has more librarooz. < 1268141968 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: That might be possible, and if so, I'd probably enforce that < 1268141989 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: You might agree that less libraries = better for a new schemer < 1268141996 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: But dependent types for term rewriting is in fact a project I had! (I gave up on it because it was really hard >_>) < 1268142011 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: Yes, but Sgeo's obsessed with libraries. And really most eggs are fine. < 1268142015 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Besides, SISC is Java. :-P < 1268142022 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Nothing is wrong with libraries < 1268142029 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :but I think the "point" of Scheme will be missed < 1268142034 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :True. < 1268142042 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Just at the start. < 1268142049 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Is "SRFI" what is meant by libraries? < 1268142053 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :I'd use Scheme48 or so < 1268142059 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: They are "standard" libraries < 1268142067 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: The problems with typing a term rewriting language are basically: One, identifying what you're typing (There's no nameable function, since we simply put little holes of free variables into an expression and rewrite it), and two, dealing with the extensibility (you can add to a "function" at any time just by creating a rule). < 1268142082 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I think I know how to solve the second one (with an entirely new type system). The first may just be a syntactic fluff. < 1268142085 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*a bit of < 1268142095 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: Oh, I forgot S48. < 1268142098 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Use Scheme48. < 1268142132 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :The Windows distribution is "experimental" < 1268142135 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: Right. My rule was going to be this: you can't create a new function/constructor unless it can be typed < 1268142159 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Oh, you're on windows, no wonder why you are attached to dr scheme < 1268142164 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Oh. < 1268142166 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Windows. < 1268142170 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Is Notepad++ any good with Scheme? < 1268142177 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Emacs. Only. < 1268142179 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :emacs is good for scheme < 1268142179 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Or Edwin, even, lol. < 1268142179 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :;) < 1268142185 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :with Quack, I suggest. < 1268142190 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Anything else will fail. Horribly. Do not even bother. < 1268142195 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Bla just use dr scheme < 1268142204 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Set to R5RS at least < 1268142206 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Since you're on windows, there's little you can really do < 1268142209 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Think of the /children/ < 1268142212 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :and yes, set it to R5RS < 1268142227 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Notepad++ seems to have Scheme support < 1268142238 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: Should we move discussion of this language elsewhere so I can blab a lot about the type system for term rewriting I half-thought up? < 1268142241 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: It has rudimentary highlighting, probably. < 1268142242 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Scheme highlighting isn't the important part < 1268142245 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :And no nice indentation thingy < 1268142254 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :If you are not going to trust the opinions of people who /know/ what they're talking about, why ask? < 1268142255 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I typed (let ((a 5) and hit enter < 1268142256 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: Sure < 1268142259 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :It didn't autoindent < 1268142273 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Same with Emacs. Technically. (Ctrl-J :P) < 1268142278 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Just use PLT/whatever < 1268142282 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: Name it < 1268142297 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yeah dr scheme at least has a workable editor for newbz < 1268142299 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: (the channel) < 1268142303 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :ummmmmmm < 1268142347 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Does PLT in r5rs mode support the SRFIs that PLT is supposed to support? < 1268142370 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: Well I wouldn't want to usurp your holy rights as a Platonic-space-excavator. :P < 1268142378 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Yes. < 1268142379 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: #~math < 1268142384 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION is happy now
< 1268142401 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: No, Libster and base3 will just start attempting to troll me again. < 1268142402 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Keyword "attempting". < 1268142426 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: No. < 1268142429 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Libster is banned < 1268142437 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hah, really? < 1268142439 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :base3 is gone < 1268142441 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :yes really < 1268142454 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Anyway, let's just do #rewritetypes so there's no flood. < 1268142460 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Unless someone /else/ has that channel... < 1268142471 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :No one is talking < 1268142485 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :but we can make a new channel if you so desire < 1268142490 0 :augur!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1268142502 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The holy institution of making a new channel, a.k.a. /j #foo :-P < 1268142661 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Um... >.> < 1268142674 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Are there any socket thingies in any SRFIs? < 1268142733 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I shouldn't have even bothered. < 1268142768 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I'll take that as a "No, and you're completely missing the point" < 1268142780 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Not no. < 1268142795 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But not yes. Actually not even mu, I meant exactly what I said. But yes, you are missing the point. < 1268142936 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :.. < 1268143044 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :What is the point, exactly? < 1268143057 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Maybe I should just stick with Haskell >.> < 1268143107 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I doubt you get Haskell's point either. < 1268143113 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :woo < 1268143115 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :xv < 1268143117 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :tomorrow i turn 2^3 * 3 years old. :D < 1268143302 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You'll be 512! < 1268143355 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :That spacing is misleading, since the exclusive-or binds less tightly than multiplication there. < 1268143375 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::-D < 1268143401 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :He'll be 11. < 1268143429 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Or 3, if you interpret it like he said. < 1268143437 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm... INTERCAL can do Roman Numerals, at least for output < 1268143452 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :maybe Common Lisp was just making implementing it easier? < 1268143470 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::-) < 1268143483 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Have you any opinions on how to best represent an Othello board? < 1268143486 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(Functional language.) < 1268143510 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'm thinking of some sort of function-based representation, something that reifies the concept of the continuous line into the way you access the board. < 1268143532 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: I don't think I can come up with correct opinions < 1268143542 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :alise: not exclusive or. < 1268143544 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :exponentiation. < 1268143545 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric ::| < 1268143546 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :based on what I'm doing at work atm, I'd come up with a functional translation of the OO way to represent it < 1268143547 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Incorrect ones are fine too, ais523. < 1268143551 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :augur: Ohh you don't say < 1268143554 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :#boring, that way < 1268143558 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no matter what the correct representation actually was < 1268143563 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :true < 1268143570 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :i could've done something more interesting < 1268143588 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Wilful misinterpretation is the norm here, isn't it? < 1268143593 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :so basically, you'd have a function with arguments (method of accessing the board, argument to that method) < 1268143597 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION fails to see PLT on http://people.csail.mit.edu/jaffer/SLIB.html
< 1268143600 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :wow, that is terrible < 1268143617 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :nicely abstracted and extensible, but otherwise terrible < 1268143660 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: slib sucks < 1268143671 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence will back me up on this... i hope < 1268143696 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Ok, so what doesn't suck? < 1268143710 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Nothing! < 1268143735 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Me! It'd be illegal. < 1268143784 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Speaking of which, where does the "put a sock on it" expression come from? (And don't reply with a line number.) < 1268143847 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Condoms. < 1268143861 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :OBVIOUSLY. < 1268143878 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Oh, that "it". < 1268143879 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: hahahahaha < 1268143880 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :slib < 1268143882 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :slib blows < 1268143901 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :slib blows... anuses < 1268143957 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :So... does this mean for networking stuff, I'd be using the implementation's stuff? < 1268143966 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Or is there anything else? < 1268144140 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Just learn scheme < 1268144142 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :then do cool stuff < 1268144282 0 :MizardX!unknown@unknown.invalid QUIT :Ping timeout: 248 seconds < 1268144288 0 :ztirf4!unknown@unknown.invalid QUIT :Quit: Nettalk6 - www.ntalk.de < 1268144341 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION gibbers a bit
< 1268144993 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :axiom interact : Interaction pre final transform result → (ω:Worldish) → pre ω → (result → transform ω → Φ Worldish (λω₁ → final ω₁)) < 1268144995 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :"Or something." < 1268145004 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I think Worldish has to be an opaque type. < 1268145021 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :That still lets us use the old world, though... < 1268145023 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oh, perhaps: < 1268145115 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :axiom interact : Interaction pre final transform result → (c:Conditions) → pre c → (result → transform c → Φ Conditions (λc₁ → final c₁)) → (ω:World) → (conditions ω ≡ c) → World < 1268145118 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Except with all the bits involving World omitted. < 1268145129 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Except then you just move the problem of worlds to the conditions. < 1268145147 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I think I'm going to try learning Common Lisp < 1268145324 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hah. < 1268145401 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Although I already know for a fact that I hate the names of some of the functions [saw a chart contrasting Scheme and CL] < 1268145454 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :AFK < 1268146279 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1268146447 0 :ais523!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268146485 0 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1268146515 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ouch < 1268146528 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :my entire system was being really slow, for some reason < 1268146542 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the DNS server in particular; I'm not sure if that's deliberate or not, but I changed the DNS to level3's < 1268146719 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fop < 1268146754 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fop? < 1268146803 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : alise: planned Feather syntax is [ x | f x ] <-- yay Feather! < 1268146825 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: I thought you only had one line of scrollback? or did alise invent that? < 1268146845 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, it's from the esoteric false rumours file < 1268146849 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :didn't you know? < 1268146860 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :haha, #esoteric so needs a rumors.tru and rumors.fal < 1268146861 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: he read the logs < 1268146866 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :not scrollback < 1268146879 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I read highlights and their context in logs < 1268146879 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :rumors.tru: alise is a girl pretending to be a man pretending to be a girl. < 1268146886 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :latex genii: how do i make an invisible char the same width as another given char? < 1268146888 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :rumors.fal: #esoteric's logs come from sustainable forest < 1268146898 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh, I'll look it up < 1268146906 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I know it's possible, and where to find out how, but not the actual command < 1268146918 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, \hphantom? < 1268146923 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :rumors.mu: This rumour is false. < 1268146928 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: that sounds right, yes < 1268146934 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, what? < 1268146936 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hphantom, I think ,yes < 1268146939 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*think, yes < 1268146941 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :well < 1268146942 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :even works in TeXmacs < 1268146946 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it is horizontal < 1268146952 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :there is a vertical version too iirc < 1268146961 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: gah, but it seems to treat it as not italic < 1268146963 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :or just \phantom generally < 1268146964 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and possible one that does both vertical and horizontal (not sure about that) < 1268146967 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, what? < 1268146974 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :very, very subtle spacing issues < 1268146983 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: you could italicise inside the \phantom, or doesn't that work? < 1268146995 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, did I mention I put a -6 em vertical spacer at the top of a minipage yesteday? < 1268147001 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :yes a negative one < 1268147006 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: no, or at least not to me < 1268147040 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :nope, it's still too long < 1268147050 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, needed two mini pages side by side, one contained a display style formula, which some tests showed was responsible for causing it to be put below the other mini box < 1268147051 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'm trying to make _! look the same as the n! in the definition < 1268147052 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :_! : ... < 1268147053 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :n! = ... < 1268147064 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so I'm doing \underline{\phantom{n}}, but the first line is too long < 1268147066 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :so I had to move it up using negative spacer < 1268147081 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: oh, try \phantom{$n$} < 1268147086 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that's a math n, not an italic n, presumably < 1268147120 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, err? does phantom inside math mode exit math mode? < 1268147146 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: I don't actually know; is it a math mode command, though? < 1268147176 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, I think it works in either < 1268147223 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, and since I normally use LyX, and LyX has support for phantoms without needing "insert tex code" it may abstract such things away < 1268147225 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, apparently so < 1268147268 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: maybe it's a kerning issue? I can sort-of imagine that \phantom would block kerning, and some typefaces will attempt to kern together any two italic characters < 1268147374 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :what exactly is alise trying to do? < 1268147404 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I mean, I saw what he said, but he didn't say what part of it should align < 1268147407 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: ! isn't italic < 1268147411 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : _! : ... < 1268147411 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : n! = ... < 1268147413 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: < 1268147414 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1268147415 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :_! : ... < 1268147417 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :n! = ... < 1268147422 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :_ and n should have same width < 1268147422 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, if you want those to align on the : and = ? < 1268147425 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i.e., ! and ! should align < 1268147426 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1268147430 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: no, I already handle that < 1268147449 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, I was about to suggest eqnarray environment or something < 1268147457 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yeah, doing that < 1268147468 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, also since n and _ are not in monospace there I assume? < 1268147481 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :then it might be hard to make them equal width < 1268147506 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :they're not < 1268147509 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :they're italicy variably thingy < 1268147519 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: why are you even suggesting monospace for a TeX-typeset document? < 1268147522 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's not an actual _ character < 1268147526 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in the tex < 1268147527 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, I'm not < 1268147528 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i'm trying < 1268147532 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :\underline{\phantom{n}} < 1268147537 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but that's wider than n, somehow < 1268147540 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :perhaps the underline has padding < 1268147542 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1268147558 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, perhaps, why not add a negative spacer in there to compensate! < 1268147567 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: because that is missing the point of TeX < 1268147585 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, LyX goes out of its way to make it hard to make semantically incorrect documents, but it seems that people still manage somehow < 1268147597 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: because i'd have to get it totally exact < 1268147610 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, I would quote fizzie from yesterday on that, but I'm too lazy to grep the log file < 1268147614 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268147619 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, wrt. negative spacers and latex that is < 1268147639 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :even positive spacers are normally semantically incorrect < 1268147643 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, also I have used mono space in a LaTeX document, for a code listing < 1268147651 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :also, this is texmacs; so almost identical but slightly different typesetting algo < 1268147656 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but that is the only case I can think of < 1268147657 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i imagine it's the same in tex thogh < 1268147659 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*though < 1268147673 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, why not LyX btw? < 1268147686 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :(/me remembers the Wikipedia advice to use positive space and negative space that cancel each other out to prevent LaTeX math rendering as HTML, and force it to render as an image, even if people have set their preferences to render as HTML) < 1268147705 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: because sometimes, it's faster not to use an IDE < 1268147710 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :whether for programming, or for typesetting < 1268147718 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, he said texmacs, not emacs < 1268147733 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and texmacs has the same idea as lyx basically < 1268147765 0 :alise_!~d4b78c25@gateway/web/freenode/x-trwpbpmdrntkwnir JOIN :#esoteric < 1268147771 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: because lyx is harder to use < 1268147776 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :however, my impressions of TeXmacs last I tried it were: sluggish user interface, blurry font rendering when editing (this might have been a fontconfig issue, I don't know), buggy import from LaTeX (this might not matter so much), much fewer features than LyX or similar < 1268147777 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Someone paste the last few lines to me < 1268147777 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :got disconnected < 1268147786 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : (/me remembers the Wikipedia advice to use positive space and negative space that cancel each other out to prevent LaTeX math rendering as HTML, and force it to render as an image, even if people have set their preferences to render as HTML) < 1268147786 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : AnMaster: because sometimes, it's faster not to use an IDE < 1268147786 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : whether for programming, or for typesetting < 1268147786 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : ais523, he said texmacs, not emacs < 1268147787 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : and texmacs has the same idea as lyx basically < 1268147804 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, the line above that was where I asked "why not lyx" < 1268147810 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(and you answered that) < 1268147823 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The interface is not really sluggish for me, your display sucks, I don't care about LaTeX import, and LyX is a pain to use < 1268147823 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, I never found LyX hard to use once you learnt it < 1268147834 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It looks exactly like .ps TeX output to me < 1268147836 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :further, I found it well worth the time it took to learn LyX < 1268147861 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : The interface is not really sluggish for me, your display sucks, I don't care about LaTeX import, and LyX is a pain to use <-- I said last I tried it, which might have been a year or two ago < 1268147881 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :in LyX: click click click click click click click click < 1268147895 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, no? there are keyboard shortcuts for everything in LyX reallyt < 1268147897 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :really* < 1268147907 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and it shows them in the status bar when you select a command < 1268147909 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :right/center/left aligned eqnarray in the middle of the doc in texmacs: M-& < 1268147920 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268147931 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Go on then, what is the shortcut? < 1268147954 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, Ctrl-M, Alt-M T E < 1268147967 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, I had to look up the latter, because I very rarely use it < 1268147975 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :the former, "insert math formula" is ctrl-m < 1268147976 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: the leading control-M isn't needed for alt-M shortcuts < 1268147978 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and I know that < 1268147990 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's harmless to give it, but you can omit it as an abbreviation < 1268147991 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, oh? well, since I so rarely use eqnarray < 1268148002 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I haven't bothered learning that one < 1268148007 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :whoa, flood < 1268148009 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :everything after what-is-the-shortcut took ages < 1268148009 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, ? < 1268148016 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1268148019 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: : he's lagging < 1268148023 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :right < 1268148039 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and that second : was a tab-complete fail, assume it's a stray newt or something < 1268148041 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and I'm not going to be like ehird and complain about other people lagging :P < 1268148041 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Alt-M T E. Well, may be acceptable. < 1268148042 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :LyX has a windows binary, right? < 1268148059 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, XD < 1268148065 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, iirc yes < 1268148104 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, lyx tends to have somewhat emacs-y key bindings for some things, but you can configure that somewhere iirc < 1268148143 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :of course, if you haven't yet gotten used to lyx, keyboard shortcuts won't help you, it *does* take a while to learn < 1268148191 0 :alise!~d4b78c25@gateway/web/freenode/x-xqbaislcgzqjcbwk JOIN :#esoteric < 1268148198 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Maybe I'll try LyX next time, then. < 1268148212 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I really ought to name my language someyear. < 1268148214 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, but yes you can always look at the status bar after clicking almost any button to see what the command is to insert that. And you can type \LaTeX commands directly in math mode (lyx will try to display it WYSIWYW style if it knows the latex command in question) < 1268148257 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :interestingly opening preferences in lyx shows (dialog-show prefs) < 1268148273 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I wasn't aware lyx used anything lispish internally < 1268148286 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: you mean WYSIWYM? < 1268148296 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, ah yeah, thought it was "want" < 1268148297 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: it uses sexp notation for commands, I think < 1268148299 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :right "meant" < 1268148302 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*WYSIWYG. WYSIWY[WM] is a lie. < 1268148316 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268148329 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: it's not pure WYSIWYG; for instance it shows nonstandard-width spaces with blue underscores with ticks on the end, rather than as blank space < 1268148330 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, well, lyx is not WYSIWYG, because it shows it in a screen friendly font rather than exactly what it will look like < 1268148336 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(for example) < 1268148347 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and what ais523 said < 1268148358 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, it typesets relatively terribly, about as well as Word < 1268148359 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :What you see is not even what you get. < 1268148363 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :plus floats are shown as boxes with a thingy saying it is a float at the top < 1268148365 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :(although TeX typesets the finished product) < 1268148368 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, what does? lyx? < 1268148372 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :well maybe < 1268148374 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: yes, I mean onscreen < 1268148377 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Oh snap. < 1268148400 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, it can be set to instant preview math formulas though < 1268148415 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :when you leave the equation it will render it, takes a split second < 1268148425 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :not on by default iirc < 1268148428 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: so can auctex for emacs (that mode is a work of art, btw) < 1268148433 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(possibly the nicest typesetting environment ever created) < 1268148437 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1268148442 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, why aren't you using that then? < 1268148462 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because i can't be arsed to set up latex. and i don't really want to write a document template every time I want to ogle at how pretty my language is < 1268148472 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :speaking of can't be arsed to set things up on windows, < 1268148477 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :How should I install Ubuntu given that all I have is a costly 3G stick connection? < 1268148484 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Ship-It is not an option. < 1268148490 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, well, lyx would need latex installed somewhere it can run it < 1268148501 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Oh. TeXmacs is self-contained. < 1268148515 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(It isn't actualy TeX. Or Emacs.) < 1268148516 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, perhaps the lyx windows installer includes latex? < 1268148517 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*actually < 1268148580 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: put it this way: alise has tools that work, why would you force him onto different tools even if those also work? < 1268148582 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://www.gnu.org/software/auctex/img/preview-screenshot.png ;; yum < 1268148582 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, I always use pdftex, it renders nicely and you can add a command to the document preamble so it does fancy microtyping with visually straight margins and what not < 1268148587 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, I didn't < 1268148595 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :he is free to choose < 1268148607 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Well, I'll certainly try LyX now. < 1268148628 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I've used it; it seems to be decent enough for what it does, but has a few annoyances < 1268148635 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, such as? < 1268148637 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :such as no easy way to type the prime character, as in a' < 1268148647 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, eh? in math mode? < 1268148652 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: yes < 1268148654 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :pressing ' doesn't work < 1268148673 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, it renders as a primelooking one in the instant preview for me < 1268148674 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you have to do M-m e M-m ' < 1268148685 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: oh, but as a plain quote in the ordinary window? < 1268148689 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :how... ridiculous < 1268148694 0 :alise_!~d4b78c25@gateway/web/freenode/x-jkkymkgoynwcctyq JOIN :#esoteric < 1268148699 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Last 30 lines or so? < 1268148701 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :because there is a way to do a superscripted prime that renders as one in LyX < 1268148703 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, seems so < 1268148705 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: I'll pastebin < 1268148708 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Not just since my last utterance; I probably missed things. < 1268148725 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :is clog broken? < 1268148749 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ugh, sorry, this internet's being insanely slow today for some reason < 1268148756 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, this connection < 1268148757 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, well, they *could* be different, but to me they look pixel identical. But yes when editing they look different < 1268148769 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :http://pastebin.ca/1830126 < 1268148774 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: No, but that's /two/ page loads, and this connection is... well... < 1268148782 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, this mouse is doing so badly I even just used control-C control-V to paste < 1268148789 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, you could also type \prime < 1268148793 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :which might be faster < 1268148795 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :umm, http://pastebin.ca/raw/1830126 for convenience < 1268148803 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: wouldn't you have to unescape the \ < 1268148812 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I thought \ means \ (as in, $backslash$) in LyX < 1268148817 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and it only did formatting if you told it to < 1268148817 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, ? In math mode it doesn't < 1268148825 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ok, that's just silly < 1268148830 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, it shows auto completion for \commands in math mode even < 1268148832 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :very nice < 1268148841 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :especially as there's a perfectly sensible shortcut for command-introducer \ < 1268148846 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :although I forget what it is, offhand < 1268148849 0 :alise__!~d4b78c25@gateway/web/freenode/x-xzwbxfcqbiswepdx JOIN :#esoteric < 1268148856 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, you mean insert a tex box? < 1268148861 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, but looking at the view source I see: $ $$p^{\prime}'$ < 1268148866 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268148868 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :So, 22.[15:27] How should I install Ubuntu given that all I have is a costly 3G stick connection? < 1268148869 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but yes, that renders as two prime symbols < 1268148871 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :as far as I can tell < 1268148891 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise__: I'm not sure that you easily can < 1268148912 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :do you live near enough to someone with a stock of them to just ask them for one? < 1268148918 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :um, stock of CDs < 1268148919 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: does lyx let me write Aa(a->a) and get {forall} {greek a} ({greek a} {right arrow} {greek a})? < 1268148920 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :alise__: :( < 1268148921 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, anyway typing ^\prime was faster than the key combo you suggested < 1268148932 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, *tries* < 1268148946 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, what would the A do? < 1268148951 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :alise__: No. I could get to Birmingham in some hours, though, and stalk you! < 1268148953 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :err < 1268148953 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: you're turning me more and more off LyX as time goes on here < 1268148954 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, ^ < 1268148959 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Presumably you have at least one Ubuntu cD. < 1268148962 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise__: nickping fail < 1268148967 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :A gives forall symbol < 1268148970 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise__: two, but they're both rather old versions < 1268148974 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :a gives alpha < 1268148975 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, \for completed the forall symbol here < 1268148984 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: A is faster < 1268148993 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Does a give greek alpha? < 1268148998 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Wow, this is the most confusing maze of nickpings ever. < 1268149009 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, why would it auto complete plain letters? < 1268149009 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Does -> give right-arrow? < 1268149011 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise__: it's alt-M G a in LyX < 1268149017 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :for the greek a < 1268149019 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :tab isn't autocomplete < 1268149022 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Does -> give right arrow? < 1268149042 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268149047 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, in math mode? No, but AltGr-i seems to insert the latex one < 1268149062 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Then LyX is useless to me. < 1268149074 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :I use TeXmacs because it lets me mainly type ASCII-ish stuff and get what I want. < 1268149086 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, well sure, if you don't like the exact key bindings < 1268149087 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :*shrug* < 1268149091 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :NN->NN^+{right arrow key}->a < 1268149094 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :gives < 1268149105 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :{blackboard N} {right arrow} {blackboard n with superscript +} {right arrow} {greek alpha} < 1268149106 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, does alpha give you a single alphpa? < 1268149108 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alpha* < 1268149116 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :no, a does. < 1268149119 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :tab is not autocomplete. < 1268149122 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :tab is "variations" < 1268149128 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, on what? last letter? < 1268149132 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :for instance, | gives \vee < 1268149140 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: yes. < 1268149143 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :also, what if I want aleph instead? < 1268149148 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, how would one type that? < 1268149156 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :in TeXmacs < 1268149158 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :\aleph. it probably has some shortcut < 1268149166 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :also, @ is for circle stuff, so @@ = infinity, @+ = circled +, etc < 1268149167 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, not a? < 1268149170 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :it's actually very, very handy < 1268149174 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: maybe it is. maybe it's something else < 1268149179 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :aleph doesn't look like a < 1268149184 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :so it's probably not a < 1268149185 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :true < 1268149198 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :perhaps N < 1268149202 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :perhaps < 1268149210 0 :cpressey!~CPressey@173-9-215-173-Illinois.hfc.comcastbusiness.net JOIN :#esoteric < 1268149217 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, what about an actual @? < 1268149251 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Well, \text{@} works. < 1268149260 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, how verbose! < 1268149260 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Which is actually \text@ < 1268149268 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :yes, very very verbose < 1268149269 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :A-$ also works for text. < 1268149272 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :A-$ @ right < 1268149277 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I can just type a single @ < 1268149286 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Now write infinity. @@ < 1268149290 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Blackboard bold N. NN < 1268149294 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :+ in circle. @+ < 1268149298 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Right arrow. -> < 1268149315 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Yeah, A-$ @ right is soooo horrible. < 1268149325 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, I wouldn't write @@, since it is on altgr here, that is not so easy as \infty < 1268149326 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Especially as @ is /so/ /common/ in mathematics. < 1268149331 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Of course, @ outside of an equation still produces @. < 1268149388 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, anyway, I find lyx have no major issues. A few small quirks sure. But then LaTeX itself has plenty of those too. And LyX does a reasonable job of producing a good result without a lot of fine tuning < 1268149401 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: the issue's mostly with the interface < 1268149408 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I have no issues with the general concept, just the details < 1268149448 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, I would hate to edit in Computer Modern on a "normal" dpi desktop monitor < 1268149457 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :But you're okay with reading it? < 1268149463 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Also, TeXmacs allows you to choose among fonts < 1268149464 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Obviously. < 1268149471 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, well I wouldn't use CM unless I aim to print it < 1268149481 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :So choose another font. You are boring. < 1268149488 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :if it is primarily intended for on screen reading, I would use another font < 1268149534 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, my point was that I don't want WYSIWYG. I want to concentrate on the actual text and such first, and only at the end care about small formatting details < 1268149569 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :I don't feel like talking to you about this any more. < 1268149578 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :well, I have other things to do as well < 1268149605 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :I don't, but (nothing) is better than this. < 1268149611 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :[15:46] == #ω Illegal channel name < 1268149617 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Fuck you, Freenode. < 1268149656 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1268149689 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, if doing direct latex editing I found kile quite nice < 1268149703 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :auctex. No competition at all. < 1268149786 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Microsoft Works is preinstalled on this computer. < 1268149787 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Wow. < 1268149815 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :now you must use that instead! < 1268149818 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Apparently Ctrl - = delete and Ctrl + is increase font size, but it's also its own inverse. < 1268149844 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, what? in TeXmacs? < 1268149850 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :how weird < 1268149852 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :No. < 1268149858 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oh works? < 1268149860 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :In Microsoft Works Word Processor. < 1268149867 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :still weird < 1268149918 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Works is awful < 1268149923 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :ais523: indeed < 1268149927 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I know, I used to use it to some extent < 1268149929 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Also, I implemented the Lambda Calculus of Continuations. < 1268149944 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :apart from the word processor; the computer came preinstalled with Works - word processor, and Word < 1268149971 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Not interested? < 1268150005 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise__: vaguely < 1268150015 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I was busy argumenting in two other channels, so was distracted even from a nickping < 1268150019 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Hey, it's for Feather. < 1268150024 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yay < 1268150033 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :what did you implement it in? Haskell? < 1268150039 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1268150041 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :I'll pastie. < 1268150043 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, how well does bibtex integrate with TeXmacs? < 1268150070 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: TeXmacs is not tex at all. < 1268150089 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise__, well, what does it use for a replacement of bibtex then? < 1268150097 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Dunno < 1268150146 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :ais523: http://pastie.org/861515.txt?key=n5pnirguwnncksdk7homzq. So, we have two main structures: < 1268150157 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :f(x,k) and (\x,k.E) < 1268150173 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :There are constraints: f must be a lambda expression, not another application. < 1268150176 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1268150185 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise__: that's nice and short < 1268150188 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :There are constraints: in f(x,k), f, x and k must be lambda expressions, not applications. < 1268150215 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :In (\x,k.E), E must be an application. (I neglected to include this in my implementation) < 1268150223 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :(LCC t should be LCC App). < 1268150243 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :So, we have: no nested applications, and forced continuation "arguments". < 1268150259 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :It has the interesting property of making application a triadic operation (since k isn't "really" an argument) < 1268150281 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Anyway, it's basicaly just the lambda calculus, except continuation-passing style is enforced. < 1268150296 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :I'll probably write a CPS-converter for it. < 1268150320 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :ais523: A disadvantage of my representation is that I can't pretty-print it without a lot of fuss. < 1268150362 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, yes < 1268150378 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :so what you've implemented is LC+continuations, but restricted such that CPS is enforced? < 1268150382 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :ais523: But that's no issue with the actual calculus. < 1268150386 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Not +continuations. < 1268150390 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :Continuations are done with CPS. < 1268150414 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :It's basically a variant of the lambda calculus that replaces nested application with continuation-passing style. (But CPS isn't inherent in the model; you don't /have/ to "normally" pass things to k.) < 1268150419 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :My god, Works is still around? < 1268150425 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: apparently so < 1268150427 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :(As in, you don't have to write "normal" functions that don't do stupid shit with k.) < 1268150431 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :IIRC, Microsoft are trying to get rid of it though < 1268150463 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :The first hit on Google is under microsoft.com/uk/ < 1268150476 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Maybe it's a British thing. < 1268150724 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268150835 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : Hypothesis: It is impossible to be comfortable. <-- it is possible for short moments, although only by accident, and if you try to prolong it it backfires horribly. at least that's my experience. < 1268150848 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :HTH < 1268150874 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :cps (LApp f x) k = cps f $ Lam $ \k' f' -> App k' $ cps x $ Lam $ \k'' x' -> App f' x' (Lam (\k''' r -> App k r k''')) < 1268150875 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :I made an error. Dammit. < 1268150878 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise__: I haven't had the time to encode the theory of rationals in it, but I do have in my proof-checking language a proof of a statement in Peano arithmetic: http://dpaste.com/169965/ < 1268150886 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :You may commence talkin' smack about it. < 1268150889 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: I mean physical comfort, not mental-anguish-comfort. :P < 1268150912 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise__: i mean both < 1268150918 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Well look at that, you have specification of theorems now :P < 1268150947 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise__: It's just for clarity; itrepeated in the body of < 1268150952 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :the proof anyway < 1268150975 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Or rather, its the first step of the proof < 1268150984 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: that doesn't look like the Peano axioms that you've assumed at the start, but rather something else < 1268150994 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and those feed on each other. for example my mental comfort is now helped by chatting on the pc. but eventually i'll tense up physically from doing so. < 1268151005 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, I love that qed is a keyword < 1268151008 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :ais523: I'm kind of leaving out the ones I don't need. Actually I don't need the zero? < 1268151011 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :I /very/ much like proof/qed as structures, though. :-) < 1268151021 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm yes, looks like you don't < 1268151065 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Kind of disturbing that it only relies on a fragment of Peano arithmetic, but it is very simple I guess < 1268151112 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm working on another one which is more practical: prove that find(x,tree) always returns true or false if tree is a proper tree. That'll probably require extending this syntax with cases < 1268151129 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :like, case tree -> branch A B ... case tree -> leaf X ... < 1268151135 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :it's actually Qed. < 1268151136 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: i think you have depression :P < 1268151136 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :well < 1268151137 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :or are just /the/ /most/ cynical person there is < 1268151143 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Which means non-deterministic rewrite rules :/ < 1268151158 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: what do you think of ultrafinitism? :D < 1268151158 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: no, not really < 1268151165 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :find x (branch A B) -> ... < 1268151170 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :find x (leaf X) -> ... < 1268151172 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :same rewriting thing < 1268151181 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well, not "non deterministic" so much as "ambiguous outside the presence of cases" < 1268151195 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I mean, to describe what is a tree < 1268151209 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :tree -> (leaf X); tree -> (branch A B) < 1268151253 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :if you rewrite App [Expr] | Symbol String | Free String < 1268151253 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: easy < 1268151254 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :have it be a predicate < 1268151254 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :App [Symbol "find", Free "X", App [Symbol "leaf", Free "X"]] < 1268151254 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :vs < 1268151254 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :tree (branch A B) -> true < 1268151254 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :tree (leaf X) -> true < 1268151255 0 :alise__!unknown@unknown.invalid PRIVMSG #esoteric :tree X -> false < 1268151257 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise__: (1) quite possibly. (2) don't really know what it is. < 1268151284 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1268151342 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise__: Not so easy; to have predicates would require building a theory of booleans < 1268151366 0 :alise!~d4b78c25@gateway/web/freenode/x-qdvrzmvpdqmkpngz JOIN :#esoteric < 1268151389 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Which clearly could be done, and might be done first to make this easier < 1268151392 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: a crazy, crazy mathematical position: http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/real.pdf < 1268151403 0 :MigoMipo!~migomipo@84-217-0-13.tn.glocalnet.net JOIN :#esoteric < 1268151404 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that everything that cannot exist in this universe - like sufficiently big integers - does not exist < 1268151408 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But then, I wonder if I would have to use predicates to prove theorems about my theory of booleans :P < 1268151413 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yay < 1268151426 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :correspondingly, that "real" analysis is completely bunk < 1268151443 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Or at least, that it does not "exist" < 1268151445 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and that godel was wrong because all the impossible proveys are in fact merely meaningless < 1268151460 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well not "wrong" but < 1268151488 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(ii) the traditional real line is a meaningless concept. Instead the real REAL `line', is neither real, < 1268151490 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(ii) the traditional real line is a meaningless concept. Instead the real REAL `line', is neither real, < 1268151491 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oops < 1268151493 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(ii) the traditional real line is a meaningless concept. Instead the real REAL `line', is neither real, < 1268151496 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :When a mathematican says "exist" they mean something quite specific < 1268151499 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :nor a line. It is a discrete necklace! In other words R = hZp, where p is a huge and unknowable < 1268151501 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Oh "real" too :) < 1268151510 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(but xed!) prime number, and h is a tiny, but not innitesimal , `mesh size'. < 1268151517 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: the worst thing is /this guy is a professor/ < 1268151528 0 :alise__!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268151546 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise: That's bad, but there are worse, much worse, out there. This guy, being a mathematician, is relatively harmless. < 1268151552 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Since mathematics is irrelevant. < 1268151556 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :(Sorry, I couldn't resist) < 1268151577 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::-) < 1268151579 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION beats cpressey with the saucepan of doom ===\__/
< 1268151623 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION 's skull goes "BLONG"
< 1268151631 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise: planck length anyone? < 1268151632 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: bleh, /you/ implement CPS for that calculus :P < 1268151640 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: Planck length... OF THE REALS < 1268151689 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :For all reals R1 and R2 there exists a real R3 where R1 < R2 < R3. And by "exists" I mean "I CAN TOUCH IT" < 1268151701 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Damn, scambled the order of those. < 1268151708 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :*R1 < R3 < R2 < 1268151748 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: so, do you know what the bootstrap progam will look like for feather? < 1268151767 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: not yet; I tried to write it in Scheme, but went mad < 1268151768 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Also, Kronecker was wrong. God invented the *primes*. The integers I blame on the devil. < 1268151770 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well R3 can be taken rational. although you still get problems with the sufficiently big integers. < 1268151785 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: well clearly it must be written in the lambda calculus of continuations! < 1268151785 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: clearly then addition is demonic < 1268151796 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Ooh, a number system based entirely on primes? Tell me more < 1268151810 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: that's the thing though, ultrafinitism means that not even infinite rationals exist < 1268151818 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because you run out of integers to put on either side < 1268151822 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: the problem was an infinite loop in trying to define "atoms", which is the next stage in the bootstrapping < 1268151837 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise: Well they have this remarkable property that, when you multiply them together, you can get any integer you want, so long as it's black. < 1268151841 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: hmm... atoms as in symbols, I presume < 1268151845 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: yes < 1268151853 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :they're basically objects that can be compared to other atoms < 1268151855 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :atoms aren't the same thing as symbols :) < 1268151859 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: clearly you need renormalization :D < 1268151862 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: easy: < 1268151863 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: atom as in Prolog < 1268151874 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: the issue is making them forward-compatible with actual Feather atoms < 1268151886 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you can use a fake-object at the start of the bootstrapping, but not later < 1268151898 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :symbol : a = (() -> ((b = (b -> bool)), a)) < 1268151902 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, the next bit is basically impossible to explain because a) I don't know how it works myself, and b) it's complicated anyway < 1268151912 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: doesn't work < 1268151921 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and the reason it doesn't work is, there's no implementation for the symbol you could use < 1268151935 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :That is, symbol is a function taking any old object (), and returning a pair of (a function whose type is (a function taking an object of the type of this function, and returning a boolean)), and another function of the same type as symbol. < 1268151944 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: well, symbols are identified by their name, right? < 1268151949 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :no two symbols have the same name < 1268151959 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :then make them lists of church numerals < 1268151978 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep, you can do that; but how do you return it using that typing? < 1268152004 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Return it? What do you think this is, a library book? < 1268152015 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION detonates an atomic symbol
< 1268152017 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: well, you don't < 1268152024 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :you just implement: < 1268152029 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :'foo -> foo < 1268152035 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because, presumably, your input is a string of characters < 1268152037 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i.e. list of church numerals < 1268152039 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so you have it right ther < 1268152041 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :implementing < 1268152046 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :sym= : symbol -> symbol -> bool < 1268152077 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION runs into seeming issue with his LCC definition: typed magic means that, I think, I can't write a parser for LCC a :(
< 1268152123 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise: typeclass restriction on a maybe? < 1268152146 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(just a wild guess) < 1268152154 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: hmm? < 1268152207 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise: say when deriving Read instances of things of the form T a, you frequently get the requirement that a also is a Read instance < 1268152221 0 :alise_!~d4b78c25@gateway/web/freenode/x-jacunqshzmmjhego JOIN :#esoteric < 1268152225 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :s/things/types/ < 1268152227 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :everything said after (just a wild guess)? < 1268152235 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise: say when deriving Read instances of things of the form T a, you frequently get the requirement that a also is a Read instance < 1268152261 0 :fax!~none@unaffiliated/fax JOIN :#esoteric < 1268152309 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ah. < 1268152337 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: I'm writing a syntax for the Lambda Calculus of Continuations < 1268152343 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: this doesn't actually work, but http://pastebin.ca/1830205 < 1268152349 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that's the start of an attempt to implement Feather < 1268152364 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :if you run it, you get an infinite loop, due to the failed attempt to implement everything in terms of everything else < 1268152369 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it'll provide sugar for the most common case of application < 1268152373 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so e.g. this is what S will look like: < 1268152391 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :erm, never mind S < 1268152395 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(haven't written sugar for that yet :D) < 1268152402 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but, say you want to make a list < 1268152408 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268152418 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cons1 := cons 1; < 1268152425 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1268152431 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cons1 := cons 1 nil; < 1268152434 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I can't even remember the difference between a fakeobject and an object offhand < 1268152435 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cons2 := cons 2 cons1; < 1268152438 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: argh < 1268152439 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :shaddup < 1268152441 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cons1 := cons 1 nil; < 1268152443 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cons2 := cons 2 cons1; < 1268152449 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cons3 := cons 3 cons2; < 1268152455 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :k cons3 < 1268152466 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that's k (cons 3 (cons 2 (cons 1 nil))) < 1268152520 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I think K will be: < 1268152545 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :\x. <- (\y. <- x) < 1268152567 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :<- is bound to the most recent explicit lambda-abstraction's return argument if a name wasn't provided < 1268152569 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so I think S would be < 1268152598 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :\x. <- \y. <- \z. xz := x z; yz := y z; r := xz yz; <- r < 1268152636 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: does that seem like a reasonable syntax to you? < 1268152637 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm, I just realised my definition is incorrect, in that continuations shouldn't get continuation arguments themselves < 1268152638 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ideally, it'd be possible to implement feather in it < 1268152639 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hello! < 1268152651 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: it lets you do naming quite nicely < 1268152658 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: vaguely reasonable, yes < 1268152659 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :foo := id (\x. ...); < 1268152659 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hi fax < 1268152761 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cwcc := id (\f. r := f <-; <- r) < 1268152766 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric : have a problem < 1268152775 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that is the same thing as just (\f. f <-) lol :P < 1268152783 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I need to (today and tommorow) solve some problems < 1268152814 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: you'd do IO by making the final continuation not in the lambda calculus of continuations, instead in the host, and returning a lazy stream of church numerals < 1268152815 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but what will probably happen is I just sit on the computer doing nothing < 1268152849 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: akrasia! or, well, the case more commonly known as procrastination < 1268152899 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I need to solve lots of ODEs so that I am able to do it quicky and accurately (REALLY USEFUL SKILL!!) < 1268152933 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :my foot < 1268153206 0 :alise!~d4b78c25@gateway/web/freenode/x-umwfbbnfkppivwsd JOIN :#esoteric < 1268153208 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://us.metamath.org/mmsolitaire/mms.html < 1268153210 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :metamath solitaire < 1268153244 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268153270 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise have you see sokoban in coq? < 1268153280 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :playing the game <=> proving a level has a solution < 1268153282 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that one you wrote? < 1268153287 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I didn't write it < 1268153290 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(i stalked all your blog :P) < 1268153291 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1268153292 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :then no < 1268153318 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :04:39:47 I'm not convinced that (\x. f x) is the same function < 1268153318 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :04:40:04 it certainly isn't in a strict lang if determining the value of f has side effects < 1268153328 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's not even true in haskell < 1268153337 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :haskell isn't pure though < 1268153339 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cf seq < 1268153351 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and it has the most evil thing of all < 1268153358 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :unsafe < 1268153359 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :RECURSION! < 1268153361 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Perform < 1268153364 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :IO! < 1268153364 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and < 1268153364 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :undefined! < 1268153367 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: *GENERAL recursion < 1268153370 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :seq (\x -> undefined x) is different from seq undefined < 1268153407 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: recursion is not the problem for eta reduction though < 1268153417 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hm? < 1268153435 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :eta reduction : identifying \x -> f x with f < 1268153471 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh right I understand < 1268153471 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's consistent with pure lambda calculus, which can do recursion using the y combinator < 1268153481 0 :kar8nga!~kar8nga@jol13-1-82-66-176-74.fbx.proxad.net JOIN :#esoteric < 1268153515 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: i have a real live copy of word 2007 here, let's see who was right about it < 1268153531 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: metacontext? < 1268153543 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :as in, who said what to be right or wrong? < 1268153558 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I said it probably isn't so bad, you said it's horrible < 1268153571 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION needs help
< 1268153586 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :btw there is an evaluation order called superstrict or something, which solves the problem of \x -> f x being f by actually evaluating f inside the lambda :) < 1268153597 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that's sounds scary < 1268153798 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: I used that (where legal under the as-if principle) in at least one of my Underload interps < 1268153809 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :for optimisation purposes < 1268153813 0 :zeotrope!~zeotrope@bas3-kitchener06-1096649314.dsl.bell.ca JOIN :#esoteric < 1268153815 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, or was it an Underlambda interp? < 1268153862 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :flit < 1268153876 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :flit? < 1268153890 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :`define flit < 1268153901 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I know what it normally means, but it doesn't seem to make sense in this context < 1268153902 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :* a sudden quick movement \ * move along rapidly and lightly; skim or dart; "The hummingbird flitted among the branches" \ * a secret move (to avoid paying debts); "they did a moonlight flit" < 1268153940 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I like Word 2007's equation editor < 1268153944 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :;_; < 1268153947 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :clearly the second meaning is intended < 1268153964 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Like flip but less upside-down; like blit but more fly. < 1268153993 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :flit would be a god name for an esolang < 1268154008 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*good < 1268154223 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1268154551 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: constructivist metamath! < 1268154559 0 :tombom!tombom@86.25.49.176 JOIN :#esoteric < 1268154561 0 :tombom!unknown@unknown.invalid QUIT :Changing host < 1268154561 0 :tombom!tombom@wikipedia/Tombomp JOIN :#esoteric < 1268154643 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :?? < 1268154681 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :my proposal is more modest < 1268154683 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: imagine metamath, but constructivist < 1268154693 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it would be sweet < 1268154704 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, do you want to do this? < 1268154709 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and I mean literally do this < 1268154715 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i think i do < 1268154723 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it would certainly be cool. < 1268154747 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I think so too < 1268154757 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :define this though < 1268154952 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :"filt" would be language with no explicit looping, but data being passed between components? < 1268154975 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :flit, not filt :P < 1268154998 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :Ah. < 1268155041 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :`define filt < 1268155042 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :* La Federazione italiana lavoratori trasporti � il sindacato dei lavoratori iscritti alla Cgil che operano nel campo dei trasporti e della viabilit�. \ [13]it.wikipedia.org/wiki/Filt \ < 1268155065 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Molto relevante < 1268155367 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :there is also sv:flit < 1268155378 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :which I'm not completely sure of how to translate to English < 1268155381 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :`translate < 1268155388 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :var sl_select, tl_select, web_sl_select, web_tl_select;var ctr, web_ctr, h;var tld = ".com";var sug_lab = "Contribute a better translation";var sug_thk = "Thank you for contributing your translation suggestion to Google Translate.";var sug_exp = "Contribute a better translation:";var dhead = "Dictionary";var dmore = "View < 1268155390 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :err < 1268155394 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :how does one use it? < 1268155413 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :`translate sv en flit < 1268155415 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :En flit < 1268155418 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :err no < 1268155429 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :`translate en flit < 1268155432 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :A prolific < 1268155436 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :no! < 1268155475 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :well google translate gives: < 1268155477 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :"noun < 1268155477 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : 1. DILIGENCE < 1268155477 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : 2. INDUSTRY < 1268155477 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : 3. ASSIDUITY < 1268155477 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : 4. APPLICATION" < 1268155486 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :the second one seems completely wrong < 1268155492 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :the third one I have no clue what it means < 1268155500 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :the last one also seems suspect < 1268155538 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh, I know the concept you mean < 1268155546 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :"industry" has two meanings in English < 1268155550 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oh? < 1268155560 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :`translate no en flid < 1268155561 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :so all 4 words give much the same meaning < 1268155562 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :no one industry < 1268155570 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, I think I used it wrong < 1268155575 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :`translatefromto no en flid < 1268155577 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :diligence < 1268155585 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: in multiple words, think "tendency to work hard" for the second meaning < 1268155595 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, isn't that the meaning for the first one? < 1268155615 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :hey guyses :D < 1268155621 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, and that would be sv:flitig, flit is as google said a noun < 1268155628 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the more common meaning is a collective noun for all the companies/factories that manufacture things < 1268155638 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, indeed < 1268155650 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and "tendency to work hard" is a noun, as tendencies are nouns < 1268155669 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: yeah i think constructivist metamath would be really awesome < 1268155677 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :especially if the proofs were actually in executable form < 1268155686 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: i think the second one uses a more original meaning of industry < 1268155808 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Heh < 1268155819 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I thought that was some kind of government slogan < 1268155833 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :DILIGENCE! INDUSTRY! ASSIDUITY! APPLICATION! < 1268155835 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :No One Industry, or Tendency To Work Hard? < 1268155840 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oh :D < 1268155872 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Adherence to these principles makes our society strong! < 1268155877 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :anyway, I think I know what sv:flit means < 1268155882 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :first word of Swedish I know! < 1268155935 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: from now on, you can choose from a veritable smörgåsbord of them < 1268156043 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: it seems to me that for simple constructivist proofs, a list of the theorems/axioms (given standard proofs/values) you use along with their types is the best way of presenting a proof < 1268156058 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :And will help us solve a large number of ODEs in a short amount of time! < 1268156069 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: wait, what? < 1268156083 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :assuming ODE = ordinary differential equation, that makes no sense < 1268156087 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :unless it's some sort of pun I don't getg < 1268156088 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :*get < 1268156104 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: i think it's a hint to fax < 1268156109 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :along with the type of the resulting composition < 1268156128 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: fax said e had to do a bunch of them a while ago < 1268156135 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1268156152 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :ais523: I was riffing on what fax was saying earlier < 1268156153 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, whats with the Agoranese? < 1268156166 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: + nested proofs, perhaps that's tc < 1268156167 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :the nose of agora < 1268156397 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Thank you ais523, I am now exactly as confused about feather as I was before. < 1268156408 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: so am I < 1268156415 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :There are fake things in it. I can tell that much. < 1268156421 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Feather is ALL FAKE < 1268156422 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :For some meaning of "fake" < 1268156426 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :actually, that's an implementation technique < 1268156428 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: _clearly_ you need renormalization < 1268156439 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Drat, so even the fake stuff is... fake < 1268156442 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1268156457 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, no, because the details of the implementation are relevant to the actual lang < 1268156460 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fake(fake(X)) -> fake(X) < 1268156463 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, I may have to leave again, my head's hurting < 1268156481 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :exists P. Component(Feather,P) & Fake(Fake(X)) < 1268156487 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :-> exists P. Component(Feather,P) & Fake(X) < 1268156495 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So yes, there are fake things in Feather. < 1268156500 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Even if they're not actually in it. < 1268156502 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Q.E.D. < 1268156514 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :OK, so "relevant, but somewhat arbitrary" =/= fake, true < 1268156548 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Fake(Fake(X)) -> Fake(X) is justified because a fake thing is fake. The fact that the thing was already presumed to be fake is irrelevant. < 1268156549 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :If a fake fake thing isn't fake, then what? < 1268156568 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and how is something fake, true? < 1268156569 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :basically, a fakeobject is something that obeys a subset of the restrictions necessary to be considered an object < 1268156579 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Fakeobjects, although fake, are actually real? So they're legitimate objects? No. < 1268156581 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Feather, to me, sounds like a way to fold nondeterminism. For some ill-defined notion of "fold" < 1268156581 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Nothing fake is true, obviously. < 1268156585 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Now go make a logical system where ~~p -> ~p. < 1268156587 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fakeobject != object < 1268156606 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I must now goify for... 15 minutes? Do that logical system. Nao. < 1268156611 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: that's an interesting analogy; and about as close to the truth as anything else about Feather that I've managed to put into words < 1268156647 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: the poker sense < 1268156792 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :feather is folding nondeterminism because instead of giving a variable its multiple possible values at once, you give it them later on < 1268156799 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so all previous continuations in some way account for this < 1268156804 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :potential nondeterminism < 1268156805 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :bye now < 1268156973 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :bye < 1268157387 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm still trying to wrap my head around the plain ol' logical system. Namely, how to state proofs about the properties of the booleans, without invoking boolean logic. < 1268157452 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Like, assume A and B are finite. Then rewriting (and A B) always terminates in one of these normal forms: {true, false}. < 1268157471 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :*finite and boolean expressions. < 1268157491 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268157523 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I need to prove that I've implemented "and" correctly! Clearly, such complex functions are not to be trusted without proofs < 1268157532 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1268157548 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :(I'm not serious) < 1268157582 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But figuring this out might give me insight on how to approach more practical proofs < 1268157619 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, I don't understand.... < 1268157649 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you want to prove that a term with type bool is a boolean? < 1268157694 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: Ah, see there is where I am in different waters from you and alise. My terms don't have types. < 1268157754 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :maybe this is the problem :P < 1268158047 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Lack of types shouldn't be a huge barrier. < 1268158065 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :http://www4.informatik.tu-muenchen.de/~schulz/WORK/e-examples.html < 1268158094 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION thinks if you don't have a type system you will implement it
< 1268158118 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :which leaves the type system you choose to implement, up to you < 1268158123 0 :jcp!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268158128 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh well < 1268158131 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"type" just means "set of values", anyway. < 1268158199 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm having more trouble with variables < 1268158223 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1268158277 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, what about variables? < 1268158732 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :http://dpaste.com/170053/ <-- have cases now, but still need to tackle induction < 1268158768 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: Well, I'm not sure. If I have variables, types look like predicates. If I don't, they look like nondeterministic/ambiguous rewrite rules. < 1268158830 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :It probably works out saner with the variables. But I'm finding it easier to do the other way. < 1268158941 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :The nice thing about this is, if you prove that terms of some form always reduce to some other form, you haven't just proved their type, you've also proved that they're total. < 1268158979 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :really?? < 1268158999 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :if you have a diverging term, can't you just prove it's anything? like a bool or a frog or whatever < 1268159012 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(by baseless induction) < 1268159046 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well, if evaluating (and X Y) always results in a bool when X and Y are finite boolean expressions, then you know (and X Y) always results in *something*, therefore (and X Y) is total < 1268159059 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If you have a diverging term, yes. < 1268159076 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Hard to prove the type of a diverging term... < 1268159080 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :At least in this < 1268159607 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :grr, now i keep reading the word as "boo-lean" < 1268159612 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Boo! < 1268159616 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION tilts to the right
< 1268159636 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :frightfullean < 1268159664 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :So, induction. Yeah. Fun stuff, teaching a computer how to do mathematical induction. < 1268159688 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :In MI one of your cases relies on the other. < 1268159694 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Is it fair to call the base case a lemma? < 1268159703 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :of course < 1268159713 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: an example of how better deptypes are < 1268159713 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :induction = recursion < 1268159723 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :you prove induction and the function it results in does recursion < 1268159732 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :induction is not recursion :P < 1268159757 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Types are a crutch < 1268159759 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :the elaboration you did is good but "induction = recursion" is nonsense < 1268159817 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Awkward to state it as a lemma because it only proves certain cases < 1268159819 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yes i know < 1268159830 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Awkward to have cases depend on previous cases too, though < 1268159840 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, types are not a crutch, types are my wheelchair! I couldn't even move without them! < 1268159861 0 :alise_!~d4b78c25@gateway/web/freenode/x-ocwuwrvlyygkwogj JOIN :#esoteric < 1268159867 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: I was going to say, dependent types are an ambulance :) < 1268159868 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :induction ~ recursion < 1268159869 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :is what i meant < 1268159891 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :now that's vauge enough for me not to be able to attack :P < 1268159924 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: yes, they take suffering programmers and, after a while, where they undergo a change in their entire philosophy due to a near-death experience, they are converted into happy progammers < 1268159928 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*programmers < 1268159949 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :too much dependent types and you'll need an ambulance < 1268159969 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :better dependent than delinquent < 1268159973 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION bans oerjan from life
< 1268159999 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :also it took me a while to realise that (exists (x:T). a) is a dependent tuple... < 1268159999 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :FWIW hardly anyone can actual program with dependent types < 1268160007 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: MY LANGUAGE WILL FIX THAT < 1268160014 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :including alise :p < 1268160022 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I don't think I can do the base case as a lemma in my system. A case isn't complete. So I think I have to go with cases being able to depend on previous cases < 1268160026 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :That's not SO bad, is it? < 1268160038 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: why did you use sum rather than exists for the exists symbol btw? < 1268160063 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :convention < 1268160068 0 :ais523!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268160073 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :also 'exists' is a proof thing, Sigma is the data version < 1268160074 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: forall P:Nat->*, P 0 -> (forall n:Nat, P n -> P (succ n)) -> forall n:Nat, P n < 1268160078 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Prop vs Type < 1268160084 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: why not have it polymorphic on both < 1268160086 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268160101 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i guess i'm still seeing proof elimination as an optimisation < 1268160142 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: also is \sum or \sigma more correct? I think \sum since you have \prod for forall < 1268160150 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :although wait, doesn't that mean that \prod is the data version of forall? < 1268160153 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Sigma < 1268160157 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :uppercase < 1268160162 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :er right < 1268160168 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so \Pi is functions and \forall is just for profs < 1268160171 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*proofs < 1268160187 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :which I think is taking it too far. which is why I think I disagree with separating \Sigma and \exists < 1268160253 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :feel free to tell me i'm stupid tho :P < 1268160270 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: so \Sigma or \exists? < 1268160280 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1268160280 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I mean < 1268160283 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: so \Sigma or \sum? < 1268160294 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :since we also have \Pi or \prod i bet sum < 1268160306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :as the coincidence is a bit too much to accept < 1268160323 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I don't know what \Sigma or \sum is < 1268160340 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uh basically \sum is a big \Sigma like you use for sums.. < 1268160344 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :same with Pi vs prod < 1268160345 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :http://dpaste.com/170070/ <-- there's my stab at MI. < 1268160347 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :different unicode chars < 1268160379 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Not confluent! Waah! < 1268160385 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION thinks "mathematical" induction should be primitive, and the other sort should be called "idiotic wrong induction"
< 1268160412 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :wait, what /other/ induction does cpressey have? < 1268160416 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: What makes you think it's not confluent? Or are you complaining I haven't proved it such? < 1268160430 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it... looks sorta nonconfluent :P < 1268160461 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It pisses me off that I can't do (Foo (x:T). a) syntax myself < 1268160468 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :just (Foo T (\x. a)) < 1268160472 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well < 1268160475 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I guess < 1268160480 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Foo_._ would work if you have (x:T) < 1268160481 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :   | < 1268160481 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :   |\ < 1268160482 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :presumably \exists and \forall are sums and products in a suitable category... < 1268160485 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but (x:T) isn't anything coherent by itself < 1268160488 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh wait < 1268160489 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I have no idea if "expand at least once on the LHS" and "expand to anything you want that's legal on the RHS" actually works, it only seems to, to me, right now. < 1268160493 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Foo_(_:_)._ < 1268160502 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: yes < 1268160503 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :duh < 1268160504 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I have to prove properties about my proof system :/ < 1268160513 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and then define Foo_._ ... but that's ambiguous I think < 1268160513 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                   | < 1268160514 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                  /< < 1268160524 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :myndzi: oh god not again < 1268160559 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Any mathematicians here know anything about Galois connections? < 1268160560 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Off by one too < 1268160562 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: so data ∃(_:_)._ : (a : Set) → (P : a → Prop) → Set where right? < 1268160568 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :not -> Prop < 1268160570 0 :hiato!~fdulu@dsl-245-63-253.telkomadsl.co.za JOIN :#esoteric < 1268160573 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :because you use exists to do the computable reals < 1268160576 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :oh no, off by one error \o/ < 1268160576 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                         | < 1268160576 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                        /`\ < 1268160606 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh wait Foo(_:_)._ isn't acceptable because i need to bind the var and stuff < 1268160652 0 :hiato!unknown@unknown.invalid PRIVMSG #esoteric :myndzi: plus ten for that < 1268160653 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :No wait, case 2 doesn't rely on case 1 < 1268160655 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :confused < 1268160662 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :galois connections rings a bell... < 1268160664 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :that can't be good < 1268160714 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: just come to the dark side. < 1268160733 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Uh, I need to prove boolexpr ~> boolean, that implies (not boolexpr) ~> boolean < 1268160758 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :obvious : ∀(P:Prop). Obvious P → P < 1268160770 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Give me a proof that a certain proof is obvious, and I'll give you the proof! < 1268160774 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Simple! < 1268160786 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Obvious "P" -> P < 1268160801 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: oh, good point < 1268160806 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :wait, no < 1268160809 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it'd be more like < 1268160817 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Obvious (x === x) < 1268160821 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well forall x that is < 1268160832 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm maybe you're right < 1268161023 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :It's not confluent in the sense that if you just used these rules in a rewriting system, and rewrote the term "boolexpr", you would generate infinite boolean expressions < 1268161094 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But that is what "boolexpr" means (to me) (right now) (and this is loosely connected to Galois connections) and it certainly seems possible to ignore "runaway" cases when you give an explicit derivation. < 1268161165 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Maybe those rules should be backwards, though. < 1268161173 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :true -> boolean, false -> boolean < 1268161197 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :That means true and false are indistinguishable < 1268161213 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I would use guillemets, though: < 1268161214 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :In a type system, they are. They're both booleans. I wanted a boolean result, great I have one. < 1268161215 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :obvious : ∀(P:Prop). Obvious «P» → P < 1268161264 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :The problem comes in that you don't want to rewrite them too early. Oh wait, I control that with the explciit derivation! < 1268161276 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i'm not sure infinitely growing expressions is a problem for confluence, provided that at any step you can start reducing back down instead < 1268161282 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*are < 1268161306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: a -> b doesn't mean that when you choose to rewrite a it results in b < 1268161310 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it means that a is /just an alias/ for b < 1268161329 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Not what it means to me < 1268161332 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I've been thinking about the interaction axiom < 1268161338 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Not even sure what "just an alias" is supposed to mean in this context < 1268161399 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :axiom interact : Interaction pre final transform result → (ω:Worldish) → pre ω → (result → transform ω → Φ Worldish (λω₁ → final ω₁)) < 1268161404 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(where capital phi was my dependent tuple) < 1268161405 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :or < 1268161406 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :axiom interact : Interaction pre final transform result → (c:Conditions) → pre c → (result → transform c → Φ Conditions (λc₁ → final c₁)) → (ω:World) → (conditions ω ≡ c) → World < 1268161410 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :both are unacceptable for the same reason < 1268161418 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i.e., that the previous world/conditions don't become unacceptable < 1268161420 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :to use < 1268161424 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so I need to eliminate them, somehow < 1268161774 0 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1268161779 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :"a little-known feature of the C standard: it explicitly states that pointer arithmetic is defined only for pointers belonging to the same memory block (i.e. statically or dynamically allocated array or structure). So when you write (char*)malloc(1) - (char*)malloc(1) you get undefined behavior" < 1268161781 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: verify? < 1268161789 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apparently that's how the memory-safe C compiler works < 1268161801 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: yes, that's correct < 1268161808 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ha < 1268161829 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :in fact, even comparing with < can cause a crash in some compilers < 1268161875 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :anyway, someone posted something in another channel that made Konversation segfault, apparently < 1268161882 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I'm not sure whether to shout at them or congratulate them < 1268161906 0 :hiato!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION chuckles to himself (c2h?)
< 1268161955 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: hmm... this is making me want to write a pure c compiler < 1268162131 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :That's not such a little-known feature; it was mentioned on this very channel not many days ago. Though coincidentally only. < 1268162193 0 :alise!~d4b78c25@gateway/web/freenode/x-obpqymwsuluxbknc JOIN :#esoteric < 1268162202 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Why does -4^4 = -256 instead of 256? I'm only a high school student, but I know for a fact that -4^4 = 256 and not negative 256. < 1268162203 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Is the typed ski + fix turing-complete? < 1268162215 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :http://community.wolframalpha.com/viewtopic.php?f=32&t=6774 < 1268162220 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fax: precedence < 1268162225 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's being parsed as -(4^4) < 1268162316 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it was a quote < 1268162352 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268162431 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise: it can do everything you need with church numerals can it not < 1268162444 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so all recursive functions < 1268162455 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: The point is that typed SK isn't turing-complete, presumably (because typed LC is not). < 1268162463 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'm talking idiotically typed, here < 1268162467 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :as in arrow and Base < 1268162479 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric : The world’s best browser. Free download for Mac + PC. < 1268162484 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So is idiotically-typed SKF complete? < 1268162486 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :they don't have a Linux version, though < 1268162492 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Correct. < 1268162495 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And? < 1268162498 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the download page is specifically a Windows one, and they directed me to it < 1268162506 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1268162515 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I was messing about with browserchoice.eu < 1268162530 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :all their advertising doesn't say "os x and windows", but "mac and PC" < 1268162541 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise: hm iirc everything that can be typed in ML can be typed in simply typed lambda calculus with fix, just by duplicating things used with more than one type < 1268162559 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :vague recall as usual < 1268162608 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :anyone have that nice ~> symbol? < 1268162614 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :http://dpaste.com/170084/ <-- last cleanup for now. < 1268162640 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :⇝ < 1268162643 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :is not so nice in my font < 1268162648 0 :kar8nga!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268162654 0 :alise_!~d4b78c25@gateway/web/freenode/x-wflgyeulqcnltwrq JOIN :#esoteric < 1268162657 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :no, it's just like --> < 1268162661 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but the -- is wavy < 1268162678 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :⇝ is the closest I can find < 1268162681 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :ais523: It is in the interest of both Apple and Microsoft to confuse people into thinking that the computer and OS are intrinsically bonded. < 1268162681 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I can barely see the squiggling at this font size, but it's there < 1268162683 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :"rightwards squiggle arrow2 < 1268162684 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :*" < 1268162702 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: I suppose so < 1268162712 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :except then, why do Apple advertise Parallels? < 1268162716 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Maybe it's just a latex thing < 1268162718 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: More so Apple than Microsoft. < 1268162728 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :nah < 1268162732 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: I would say about equal. < 1268162737 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apple even have parallels on their apple store computers < 1268162742 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Since Microsoft doesn't care *too* much so long as their OS is running on it. < 1268162746 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you think microsoft would advertise mac compatibility? < 1268162755 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apple are a hardware company, microsoft not < 1268162764 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :ais523: They don't advertize Parallels as something to run Linux on, they advertize it as if Windows is just as magically bonded to it as to a PC. < 1268162764 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ok then, what about the => char? < 1268162767 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that is also acceptable < 1268162770 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Apple is first and foremost a hardware manufacturer, and sells their hardware based on OS features. < 1268162776 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: ah, maybe < 1268162812 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Although their reasons for wanting people to think there's a magical bond are different, they both have the same want, and probably about to the same degree. < 1268162812 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :As long as Apple are not a grammar company. < 1268162836 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :For Apple it's about getting money for something that has little to no benefit in and of itself, for Microsoft it's about squashing all competition. < 1268162880 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268162921 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :What Microsoft wants is to confuse people into thinking that "Microsoft" == "program". < 1268162975 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Dude, I downloaded this Microsoft, but I think it was spyware, it installed like eight other Microsofts on my Microsoft! < 1268162992 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yes, exactly. < 1268163013 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :static discharge against a car *through thick gloves* < 1268163013 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :wth < 1268163016 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: what has little to no benefit? < 1268163018 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :anyone can explain that? < 1268163045 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: woolen, or leather? < 1268163061 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :alise_: The hardware, without the software. It's pretty good as hardware goes, but it's not so good to be worth its rather high price :P < 1268163075 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, wool/acrylic mix I think < 1268163087 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: I actually investigated that a while ago. It turns out that actually it's pretty reasonably priced for the components and the boutiqueness of Apple. < 1268163089 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :possibly some cotton as well < 1268163099 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The markup is something like 30% on the lower-end models, typical of boutique products. On the higher end models? Less. < 1268163100 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :"Boutiqueness" < 1268163105 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Yes :P < 1268163110 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :WTF is "boutiqueness" < 1268163117 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: well, there are probably air gaps inside the gloves; pushing against the car (say to pull a handle) would have compressed it to the extent that you could get a spark between your skin and the metal of the car through them < 1268163123 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The image of it being a high quality product because of its social/fashion status. < 1268163127 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Cachet. < 1268163137 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Uhh, isn't that exactly my point? < 1268163147 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Yes, but it's not a hugely unreasonable margin. But. < 1268163160 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :For instance the 27" iMac is pretty good value, actually. Just the 27" IPS display would cost about as much as the lowest-end model of it. It's a very expensive component. < 1268163162 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, actually by that point I had just laid my finger against it, hadn't yet had time to push the door closed < 1268163178 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :so it must have been a huge charge < 1268163179 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The higher-end model of it comes with a Core i7 - at that point the profit margins just keep diminishing. < 1268163183 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the issue is not that Macs are overly expensive for a high-end model, IIRC, but that they don't offer low-end models < 1268163186 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :still feels somewhat from it in my thumb < 1268163193 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It's something like $3k for the whole lot. Add in the huge cost of the the-whole-fucking-thing-is-one-gigantic-bit-of-aluminium... < 1268163208 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And the top-of-the-range 27" iMac is probably the cheapest way to get all those components. < 1268163210 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I don't think we fully understand static electricity < 1268163211 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: pretty much < 1268163217 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and its low range has a higher-than-average profit margin < 1268163241 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, oh? < 1268163242 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I have seen it be very bad in humid environments and very mild in dry environments in the winter < 1268163252 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Which is not how I was told it was supposed to work < 1268163261 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, I usually see the reverse of that < 1268163268 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :a *lot* when try < 1268163269 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :dry* < 1268163275 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and not very much when humid < 1268163285 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I don't doubt it, but maybe there is some other correlate < 1268163306 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, perhaps something specific to that environment? Or was the observation made in different places? < 1268163309 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: static electricity discharges through the air faster when it's humid, but that isn't to say you can't charge it up < 1268163337 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the way static electricity discharges from humans work is, you normally build it up over time walking on carpets, etc, and when you touch metal it discharges through that < 1268163343 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and if it had charged up far enough, you can feel it < 1268163350 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Different geographical locations, yes, I would guess it might vary on something else that was different between them < 1268163369 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: what about ↝ < 1268163406 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ais my cats ears < 1268163440 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Ohhey, looks like we traded out Miss Piggy. < 1268163468 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It's now a fax. < 1268163617 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yup < 1268163637 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Gregorification. < 1268163652 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :GreGLORIFICATION < 1268163656 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268163677 0 :olsner!unknown@unknown.invalid PRIVMSG #esoteric :GregLOLification < 1268163697 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :How Gregarious it is to Greglorify. < 1268163721 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :dulce et gregorum < 1268163773 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Definition DiscreteDerivative (f : Z -> Z) (x : Z) := f (x + 1) - f x. < 1268163814 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Notation "∆" := DiscreteDerivative. < 1268163819 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise paying attention?? < 1268163905 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :huh what now i am < 1268163916 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: what about it < 1268164161 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/861902.txt?key=71fbadzjph5ovvw9xvbkxa this is pretty but not valid < 1268164182 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :because `⟪∗⟫ = ∀a. SKF a` means that ⟦_⟧ is too fancy for its own type :( < 1268164184 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :re. your earlier question: YES < 1268164202 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I've forgotten the earlier question. I ask so many... < 1268164231 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :SKI is equivalent to STLC, but STLC + fix is recursive < 1268164253 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :by SKI I assume you mean STSKI there < 1268164256 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1268164296 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so cool < 1268164306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :if my interpreter wasn't broken i'd have done sum tc'ing < 1268164310 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :mind it is particularly pretty broken code < 1268164525 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: so why did you define discrete derivative there? < 1268164543 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :making sure coq is ready for the new age of ultrafinitism? :D < 1268164880 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION tries to devise a logic in which !!x = !x
< 1268164901 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'm implementing the finite calculus! < 1268164976 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: cool < 1268164977 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :how does Notation work btw? < 1268165022 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :|||||||||||||\\\\\\\\ < 1268165091 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :finitists can't have limits either? How do you do calculus at all? < 1268165107 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :just numerically, with some estimate of the error? < 1268165125 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lament, finite calculus is about finite sums :D < 1268165129 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lament: i'm talking ultrafinitists here < 1268165132 0 :Azstal!~asztal@host86-156-98-112.range86-156.btcentralplus.com JOIN :#esoteric < 1268165140 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :like Sum[i=1..n] i^2 < 1268165146 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :if IE wasn't being a bitch I'd link you < 1268165163 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :what specifically's the problem with IE? < 1268165174 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :thanks, i don't really wanna know < 1268165177 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lament: http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/real.pdf < 1268165181 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lament: oh you do, it's hilarious < 1268165189 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :no i really don't trust me < 1268165195 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :YES YOU DO :| < 1268165202 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: all keyboard shortcuts and commands are being ignored < 1268165211 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :err, wow < 1268165217 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lament: basically there's some defined mesh size of the reals < 1268165218 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I'm pretty sure that isn't intentional behaviour < 1268165223 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and you treat it as an infinitesimal < 1268165235 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(actual, real mesh size, as a "universal constant") < 1268165259 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :let's say it's 1 < 1268165278 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :since it's gotta be scale-invariant anyway < 1268165291 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :nice. Reals = Integers. < 1268165296 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lament: in real.pdf he does it paramaterisabled < 1268165299 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ified < 1268165301 0 :Asztal!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1268165305 0 :Azstal!unknown@unknown.invalid NICK :Asztal < 1268165307 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: and the integers are finite < 1268165311 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :or more precisely the integers don't exist < 1268165312 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :probably easier to prove it's scale-invariant and then set it to 1 < 1268165320 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: vacuous : ∀a, (P : ⊥ → ⋆), (x:⊥). P x! < 1268165335 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"exist" is more precise than "finite" now is it < 1268165345 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :⋆? < 1268165346 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: :D < 1268165354 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: supertype of set and prop < 1268165383 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :but what's the ultrafinitist perspective on nullity?? < 1268165395 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lament: it's totally yeah man < 1268165425 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :needs more skolemization < 1268165431 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: is that pdf meant to be serious? < 1268165437 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: yes < 1268165441 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :zeilberg is a fucking nutcase :) < 1268165442 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I can't tell whether it's a parody, or just deluded people < 1268165456 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :btw this guy is a professor < 1268165476 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :vacuous {_} {_} {x} = explosion x < 1268165479 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hooray for ex falso quodlibet < 1268165503 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"truer" < 1268165507 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the best thing is though you can say that < 1268165510 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I totally agree. < 1268165517 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :∀(x:⊥). x ≠ x < 1268165534 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and all sorts of fun stuff besides < 1268165546 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :"Analogously, my own best ideas, far surpassing anything in my ‘serious’ papers, are contained in my annual April Fool’s jokes, sent to my E-correspondents and posted on my website. This way I can express my ‘off the wall’ ideas without being considered a crackpot." < 1268165580 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :isn't a similar principle used for distributing INTERCAL? < 1268165585 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise_: if you define !x = x then you get !!x = !x for free ;D < 1268165596 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: hahaha no. < 1268165631 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :another option is the modal necessity operator < 1268165637 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: it's unprovable that all that is wrong; no matter how small a number you suggest, it's always possible that the mesh size is smaller < 1268165642 0 :alise!~d4b78c25@gateway/web/freenode/x-vqbzejjiawebdyhc JOIN :#esoteric < 1268165657 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric : alise_: it's unprovable that all that is wrong; no matter how small a number you suggest, it's always possible that the mesh size is smaller < 1268165666 0 :oklokok!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268165686 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: yep, except not quite < 1268165690 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it can't be smaller than the planck length < 1268165702 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well unless you pack multiple bits of info into one tiny particle < 1268165707 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well < 1268165709 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :who says that maths and physics have the same fundamental measurements? < 1268165712 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i guess not in zeilberger's ultrafinitism < 1268165723 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but most ultrafinitists are such because of physical limits < 1268165735 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i.e. you can't have an infinite set of natural numbers because you can never compute it all < 1268165754 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :you can't have a really tiny rational because there isn't the space to show its tininess < 1268165776 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I love the talk about sqrt(2) not actually existing after all, because distances don't exist, just areas < 1268165799 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Math is a consistent fiction. < 1268165807 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Guess what? It's the consistent part that's important. < 1268165815 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :*"consistent" < 1268165824 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :"consistent" fiction < 1268165826 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :LIKE ZFC < 1268165842 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :ZFC is too powerful for my taste. < 1268165850 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268165852 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I like simple theories. < 1268165856 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Like !x = x. < 1268165873 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I thought you liked consistency :P < 1268165895 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: I like how he says that Goedel is "irrelevant" because the things it applies to have no meaning < 1268165896 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well, I ilke !x -> x better. < 1268165900 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but that isn't even implied by rejecting all infinites < 1268165906 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :goedel numbers are huge but not infinite... < 1268165914 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and certainly not so huge that we can't represent them < 1268165971 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'm restarting IE. < 1268165985 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION wonders how to write (x+1)x(x-1)...(x-m+2)-x(x-1)...(x-m+2)(x-m+1) in a proof assistant
< 1268165993 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: just write it :P < 1268165995 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :"..." means induction I guess < 1268166014 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: zeilberger will love you < 1268166019 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :are you defining R := his definition too? :D < 1268166020 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :mesh size! < 1268166101 0 :alise_!~d4b78c25@gateway/web/freenode/x-mxzepjiuxgtamxed JOIN :#esoteric < 1268166122 0 :whtspc!~whtspc@j92195.upc-j.chello.nl JOIN :#esoteric < 1268166123 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what I missed I desire elaboration upon < 1268166194 0 :whtspc!unknown@unknown.invalid QUIT :Client Quit < 1268166219 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Wow, what insane garbage. It's not that I inherently object to his premise, either. It's far more that he tries to buttress it with crap. < 1268166243 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :His writing style is putrid. I'd much prefer my own whiny. < 1268166290 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268166292 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Also, I have an unstoppable urge now to define his paramaterisable finite universe. < 1268166294 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"Suppose x is even." "Well suppose it's not!" < 1268166352 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hehe < 1268166522 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Presumably the mesh size h is an ultrafinitist-rational. < 1268166524 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And p is an ultrafinitist-natural. < 1268166529 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I imagine he'd just freak out at concepts like "Turing-complete". I mean, you *can't* have infinite memory. You just *can't*. < 1268166553 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The problem is that the Ultrafinitism module is paramaterised over h and p, so how do you do it? < 1268166569 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I didn't read it as being parameterized. < 1268166576 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I read it as h is a constant. < 1268166587 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :A very small, unidentified constant. But not variable. < 1268166592 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Oh, yes. < 1268166601 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :But he parameterises it later in his analysis. < 1268166606 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Oh nice. < 1268166615 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(Because you don't know what it is.) < 1268166622 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And, of course, we don't know their True Universal Values, so for now we must specify it < 1268166631 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Trying very very hard not to LOL, natch. < 1268166634 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :(me) < 1268166646 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Until the Ultrafinitist Physicist Association of America completes its experiments. < 1268166700 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :With their grant from NAO2^{80}PSA, the National Aeronautics and Observable 2^80 Particles of Space Administration. < 1268166803 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: are you sure you don't have the link to that site < 1268166808 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what site? < 1268166821 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it says it was a book that claimed to be from the future, with a bunch of formalised mathematical proofs in it < 1268166830 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :saying that oh in the past they did this all by hand ha ha ha < 1268166830 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I told you I don't know what you're talking about < 1268166833 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and it defined a bunch of maths in it < 1268166836 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ugghh yes you do you linked to it < 1268167055 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :just explain it so that I understand what you meanl < 1268167058 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: it was either in maple or ... i think coq < 1268167068 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :its name was an acronym, i think a deliberately-amusing one < 1268167071 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Ah Zeilbergers book! < 1268167082 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :haha same guy? < 1268167084 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :http://www.math.rutgers.edu/~zeilberg/GT.html < 1268167089 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :how come it wasn't ultrafinitist < 1268167100 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Zeilberger is one of my idols < 1268167103 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well < 1268167113 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you /idolise/ this insane man? < 1268167118 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I don't really have idols but I really enjoy his work < 1268167120 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :he doesn't believe there are any infinite sets... < 1268167130 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :have you ever seen an infinite set? < 1268167159 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(and don't say, yeah in my ZFC textbook: I can write "magic rainbow unicorn" on a bit of paper too) < 1268167167 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :no, i mean exist as in mathematically < 1268167176 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :he thinks the definition of the reals is R = hZ_p < 1268167204 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :No, he thinks it should be < 1268167206 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yes, but he's /talking/ about abstract systems < 1268167219 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that's radical < 1268167233 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and talks about the REAL real line < 1268167233 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :as if anything abstract is "real" < 1268167237 0 :Gracenotes!~person@wikipedia/Gracenotes JOIN :#esoteric < 1268167238 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I think if you gave me an infinite amount of time and an infinite lifetime and an infinite supply of paper I could show you an infinite set < 1268167249 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :*lifespan < 1268167251 0 :alise!~d4b78c25@gateway/web/freenode/x-mldhfxbfgprqjpqv JOIN :#esoteric < 1268167258 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: it's a word starting with r < 1268167258 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but not radical < 1268167260 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i'd go for retarded < 1268167283 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :no you couldn't, {a^n | n \in N} doesn't contain an infinite word < 1268167345 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :That's true, it doesn't even, at that. < 1268167373 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :All the more reason to go ultrafinitish! < 1268167377 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: seriously the fact that you don't see real.pdf and immediately realise that this guy is completely idiotic shakes my faith in things you say < 1268167409 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But wait, it's still an infinite *set*, right? < 1268167438 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1268167448 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :N = {0, 1, 2, 3, ..., p} < 1268167451 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hmm, actually < 1268167458 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :he never says p is the biggest natural < 1268167459 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you are young alise, sometimes you say things which rembind me of that < 1268167460 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :or indeed the biggest prime < 1268167470 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :obviously it must be the biggest prime or the definition of R would make no sense < 1268167485 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so |N| = p and a bit :P < 1268167494 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: yeah, but at any point you'll have an element of {{a^n | n = 0, ..., k} | k \in N} < 1268167500 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268167511 0 :alise_!~d4b78c25@gateway/web/freenode/x-utszxvbodjfohytv JOIN :#esoteric < 1268167533 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :"oh you don't understand the subtle adultness of considering ultrafinitism... you have to be older to know these things... one day... one day" bullshit < 1268167550 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268167640 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I would probably describe myself as a mathematical generativist, or something. < 1268167656 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :constructivism, hells yeah < 1268167669 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Not exactly constructivist. < 1268167704 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i was just asserting my own position < 1268167719 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I was just clarifying my own :) < 1268167742 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268167803 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :alise_: why wouldn't the definition of R make sense if p wasn't prime? < 1268167824 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :needs a prime p to be a field ? < 1268167826 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :i don't really even believe in finite numbers, actually i often wonder whether i exist < 1268167860 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :It's a matter of whether you regard computations to "halt" or not, I think. < 1268167861 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :it's not a field, p is so big you can't actually do division < 1268167863 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :now THAT is radical < 1268167891 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :CA's never "halt" unless I have some way to recognize what I want "halt" to look like < 1268167893 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklokok: nonono, he asserts that it is prime < 1268167893 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but it makes no sense to arbitrarily restrict R's size when the whole point is "there is a limit to these things" < 1268167893 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: it's not a field, big + n is undefined < 1268167893 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh wait it's modulo < 1268167902 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :TMs are assumed to "halt" because recognizing it is trivial < 1268167918 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION loves the alisedumps
< 1268167926 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :at least that's how i see ultrafinitism, p sets the bound on anything we do, so if we wanna divide, we run out of Z_p when we try to find the number near p that's the inverse < 1268167965 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :there is an inverse but it's incredibly big so it's irrelevant < 1268167986 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: alisedumps? < 1268167988 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :i'd say inverses come from assuming we have such big numbers that when dividing them by each other the rounding errors don't matter :o < 1268167992 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :no coppro is the poo-lovin' guy < 1268168057 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: what's a matter of whether to regard computations to halt or not? < 1268168066 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :the constructing an infinite set thing? < 1268168083 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Every so often 4 or 5 lines from you show up at the same time, presumably due to your web->irc gateway thing < 1268168106 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: just 3g stick lag < 1268168108 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :oklokok: Whether there are finite numbers, or not, or infinite numbers, or not < 1268168117 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :1 = 1.0000000000.... < 1268168124 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :i don't see a connection < 1268168142 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :1 has halted < 1268168144 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :is 1.0000... an infinite number? < 1268168149 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :1.0000000.... never halts < 1268168156 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Why wouldn't it be? < 1268168178 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :well it's impossible for 1 to be finite and 1.000... to be infinite, because they are the exact same object < 1268168194 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :so in fact we're working in some sort of universe of representations here? < 1268168217 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION shrugs
< 1268168228 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION too
< 1268168284 0 :oklokok!unknown@unknown.invalid NICK :o|{|_o9o|_ < 1268168289 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :i'm not very leet < 1268168304 0 :alise_!unknown@unknown.invalid TOPIC #esoteric :arys < 1268168308 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oops < 1268168312 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :i should go clean up random parts of the apartment < 1268168313 0 :alise_!unknown@unknown.invalid NICK :arys < 1268168322 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :~~> < 1268168327 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Of course, the ultrafinitist, along with their unacceptance of the concept of Turing-complete, will find the Halting problem trivial. All machines always halt, due to entropy. < 1268168336 0 :arys!unknown@unknown.invalid TOPIC #esoteric :q < 1268168381 0 :ais523!unknown@unknown.invalid TOPIC #esoteric :"Gwandocu (n): Extremely strong evidence, far beyond a reasonable doubt." | alise sighting counter currently out of sequence | http://tunes.org/~nef/logs/esoteric/?C=M;O=D < 1268168479 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :due to entropy? < 1268168481 0 :arys!unknown@unknown.invalid PRIVMSG #esoteric :DFEHGJIKGMLINGPOQIKG$L5RS&TUMVGJI@WJX)YZE)[\R?G^]NEHGJIKGLINGMSR?'aOcbML5R?d5GJVI@L5[\eS&TUMVGJI@WJf - zeilberger < 1268168481 0 :arys!unknown@unknown.invalid PRIVMSG #esoteric :oops < 1268168482 0 :arys!unknown@unknown.invalid PRIVMSG #esoteric :fucking copy from pdf < 1268168493 0 :arys!unknown@unknown.invalid PRIVMSG #esoteric :http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/goodwin.pdf < 1268168501 0 :arys!unknown@unknown.invalid PRIVMSG #esoteric :he isn't even consistent about ultrafinitism < 1268168504 0 :arys!unknown@unknown.invalid PRIVMSG #esoteric :see first paragraph < 1268168527 0 :arys!unknown@unknown.invalid PRIVMSG #esoteric :joke paper, but < 1268168566 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Perhaps he believes Aleph is a finite value. < 1268168582 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :p+1? < 1268168685 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1268168685 0 :arys!unknown@unknown.invalid PRIVMSG #esoteric :now now he never said that x in N -> x < p < 1268168686 0 :arys!unknown@unknown.invalid PRIVMSG #esoteric :he just /strongly implied/ that there is no bigger prime than p < 1268168699 0 :alise!~d4b78c25@gateway/web/freenode/x-ibrcbaswxkckeirz JOIN :#esoteric < 1268168811 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1268168813 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: should i learn coq? < 1268168865 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :how i stopped worrying and learned to love the coq < 1268168952 0 :arys!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268168989 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Eval compute in Discrete_Definite_Integral 1 5 (fun x => x). < 1268168995 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric : = 10 < 1268168995 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric : : Z < 1268169120 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :paste the code somewhere < 1268169136 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric := 1 + 2 + 3 + 4 + 5 < 1268169167 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :10 =/= 1 + 2 + 3 + 4 + 5 < 1268169169 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION is about to prove Fundamental_Theorem_Of_Finite_Calculus
< 1268169172 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: err... < 1268169173 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yeah :P < 1268169178 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, it's correct within experimental error < 1268169181 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Unless it does < 1268169186 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :OK, I'll buy that < 1268169189 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: experimental error my arse :P < 1268169794 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :So, my woes are all because a mock object is not sufficiently mocking the the thing it set out to mock, huh? < 1268169802 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Nice. < 1268170368 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :the discrete definite integral from 1 to 5 is the sum from 1 to 4 < 1268170379 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric := 10 < 1268170467 0 :hiato!unknown@unknown.invalid QUIT :Quit: leaving < 1268170524 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: show yer koed < 1268170546 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :it's because given f we're computing a function g such that g(x+1) - g(x) = f(x), so the sum of f(x), where x goes from a to b is g(b+1) - g(a) < 1268170581 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :The code sounds like it would be trivial to me. < 1268170588 0 :FireFly!unknown@unknown.invalid PRIVMSG #esoteric :Who's the o guy...ah, should've guessed < 1268170595 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :should be pretty trivial < 1268170624 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: yeah but proving fundamental theorem of finite calculus will be fun < 1268170645 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :what i just said is basically the proof < 1268170658 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :although i skipped it completely because it's obvious < 1268170674 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :i mean the "it's because given f ..." thing < 1268170725 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :no wait actually what's the fundamental theorem < 1268170738 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, I will when it's done < 1268170752 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'm still working on proving Fundamental_Theorem_Of_Finite_Calculus < 1268170763 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :can you link the paper? < 1268170767 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :o|{|_o9o|_: inversitude < 1268170774 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :presummyby < 1268170783 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :woah you guys are talking about finite calculus too! what a coincidence < 1268170788 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION reads about the Trojan Horse found in the drivers for a battery charger
< 1268170798 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: because of you :P < 1268170802 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :aren't we talking about finite calculus because you brought it up? < 1268170823 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's funny seeing the arguments "well, if a battery charger connects to the Internet there's probably something wrong with it" vs. "why on earth would a battery charger company check to see if it connects to the Internet anyway?" < 1268170946 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :so what's the fundamental theorem? < 1268170955 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :or alternatively can someone link the paper? < 1268170977 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :the finite calculus paper? http://www.stanford.edu/~dgleich/publications/finite-calculus.pdf ? < 1268170982 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :thanks < 1268170992 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I thought you already had it < 1268171098 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :okay yeah then i proved it by saying it's obvious < 1268171110 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :well i did, i didn't know i did < 1268171141 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I don't know how to correct that impression < 1268171192 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :the theorem doesn't actually have any mathematical content, it's just stated for convenience, so you don't have to think about what happens on the boundaries of the sum and the integral every time < 1268171211 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :not so! < 1268171232 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric : I'm not some open source hater by any means, but I think the chances that someone who gave a shit about the source of a freaking battery charger driver would be exactly the type of person who would never be dumb enough to buy a battery charger that needs a windows driver install. < 1268171238 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :this is one of the best flamewars I've seen for a while < 1268171315 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :It makes me sad < 1268171366 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION proved the fundamental theorem :D
< 1268171389 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Right on. < 1268171395 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :#esoteric is full of proofs today < 1268171400 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Maybe we'll open up the bonus level < 1268171403 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :i really don't see what there is to prove < 1268171418 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :o|{|_o9o|_, I mean formal proof < 1268171438 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :if you sum adjacent values of f(x+1)-f(x)'s, obviously all but the left and rightmost ones cancel out < 1268171441 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :oh in coq? < 1268171462 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :then i obviously have no idea how hard it is < 1268171464 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :o|{|_o9o|_, oh and, I used "The Fundamental Theorem" as my definition, which means MY fundamental theorem is their definition < 1268171493 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :not very hard because Z has already a fair bit of theory in the standard library, without that -- this would not be possible < 1268171514 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :i believe you < 1268171515 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :clearly you need to use coq's "obvious" tactic < 1268171592 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268171613 0 :Daexpos!~unknown@212-166-128-139.red-acceso.airtel.net JOIN :#esoteric < 1268171640 0 :Daexpos!unknown@unknown.invalid PRIVMSG #esoteric :Who is the exoterisc? < 1268171678 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Him! < 1268171679 0 :Daexpos!unknown@unknown.invalid PRIVMSG #esoteric :Pene < 1268171680 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION points
< 1268171684 0 :Daexpos!unknown@unknown.invalid PART #esoteric :? < 1268171707 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :And all present were enlightened, I'm sure. < 1268171715 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Pene. < 1268171735 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that's the ablative of penis, right? < 1268171756 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Fax intends to ablate your penis. < 1268171774 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :fricative < 1268171776 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I don't know what ablate means, but it sounds painful. < 1268171776 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ouch < 1268171783 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :`define ablate < 1268171786 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :* wear away through erosion or vaporization \ * remove an organ or bodily structure \ [14]wordnetweb.princeton.edu/perl/webwn < 1268171797 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It is in fact quite painful. < 1268171807 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :`define fricative < 1268171809 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :* fricative consonant: a continuant consonant produced by breath moving against a narrowing of the vocal tract \ * of speech sounds produced by forcing air through a constricted passage (as `f', `s', `z', or `th' in both `thin' and `then') \ [18]wordnetweb.princeton.edu/perl/webwn < 1268171811 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Or at best, very shocking. < 1268171821 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :`define fricate < 1268171823 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :* Frication - Fricatives are consonants produced by forcing air through a narrow channel made by placing two articulators close together. ... \ [13]en.wikipedia.org/wiki/Frication \ * frication - friction; turbulent and noisy airflow < 1268171828 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Darn. < 1268171832 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :;) < 1268171839 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :force air through narrow channel < 1268171947 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :i forced.... ughr < 1268171957 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :oh, fricate. not fornicate. < 1268172117 0 :werdan7!unknown@unknown.invalid QUIT :Ping timeout: 619 seconds < 1268172130 0 :Gracenotes!unknown@unknown.invalid QUIT :Quit: Leaving < 1268172436 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hey alis < 1268172437 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hey alise < 1268172494 0 :werdan7!~w7@freenode/staff/wikimedia.werdan7 JOIN :#esoteric < 1268172629 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :lament: can you believe I was banned??? :( < 1268172731 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: from where? < 1268172738 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :#nm < 1268172761 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :and after all this time I thought I was an asset to the channel :((((((((((((((((((((((((((((((((((((((((((((( < 1268172838 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :what holy shit < 1268172867 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :lament: |Steve| did because I banned him from ~m < 1268172901 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :[otherwise no other reason] < 1268172947 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :wow, what a jerk! < 1268172960 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :such tit-for-tat brinkmanship < 1268172998 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :he should have turned the other cheek and made you an op so you can ban him in #nm < 1268173071 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION seems to be having troubles with his sarcasm meter
< 1268173109 0 :MigoMipo_Zwei!~migomipo@84-217-4-83.tn.glocalnet.net JOIN :#esoteric < 1268173121 0 :MigoMipo!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268173142 0 :MigoMipo_Zwei!unknown@unknown.invalid NICK :MigoMipo < 1268173214 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: i'm using all my diplomatic finesse to get you unbanned < 1268173220 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :so expect a permaban, probably in #math too < 1268173236 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268173241 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :lament: awww < 1268173255 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :OK, that was funny. < 1268173257 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Noooo don't get yourself in trouble < 1268173284 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :nono i'm not getting *myself* in trouble :D < 1268173297 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Hahaha okay good < 1268173309 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :- famous last words < 1268173422 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :"oerjan: lol" <<< is it just me or is this really out of character < 1268173446 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :or was that just the first thing ever you found funny here < 1268173454 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :I found this quite funny: [16:17.27] * oerjan seems to be having troubles with his sarcasm meter < 1268173460 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :also god i hate this nick < 1268173490 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan leaks this constant flow of hilarious humor < 1268173499 0 :cpressey!unknown@unknown.invalid NICK :cpressez < 1268173541 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: i found lament's comment hard to measure < 1268173551 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :I know < 1268173553 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :it was funny < 1268173558 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :the way you said it < 1268173563 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :at the time you said it < 1268173610 0 :muni_!~opera@metroeth-nat91.217.146.194.generacja.pl JOIN :#esoteric < 1268173638 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :"I love you." "LOL!" < 1268173672 0 :cpressez!unknown@unknown.invalid PRIVMSG #esoteric :I suppose that's better than "I love you." "ROTFL" < 1268173694 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268173715 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(yeah i'm just messing with o|{|_o9o|_ now) < 1268173730 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(ok, and laughing) < 1268173744 0 :cpressez!unknown@unknown.invalid PRIVMSG #esoteric :limh < 1268173748 0 :cpressez!unknown@unknown.invalid PRIVMSG #esoteric :(laughing in my head) < 1268173772 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why did alise just disappear like that? < 1268173772 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :sounds painful < 1268173786 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: THEY found him < 1268173796 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yeah not funny < 1268173914 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :it's an unfunny in-joke in bad taste < 1268173927 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :the best kind < 1268173932 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :maybe i should ban myself < 1268173945 0 :o|{|_o9o|_!unknown@unknown.invalid PRIVMSG #esoteric :can you? < 1268173952 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :okklopkuabp < 1268173952 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :presumably < 1268173957 0 :tombom!unknown@unknown.invalid QUIT :Quit: Leaving < 1268173959 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep, he has ops nowadays < 1268173960 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you didn't respond < 1268173964 0 :o|{|_o9o|_!unknown@unknown.invalid NICK :oklopol < 1268173998 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :didn't respond to what? if it was in pm, i had a different nick for a while, not sure if you noticed because there were only typographical differences < 1268174005 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :8:/ < 1268174030 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :you asked me whether 8, or what? < 1268174042 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :_clearly_ 8 < 1268174053 0 :cpressez!unknown@unknown.invalid PRIVMSG #esoteric :The ratio between 8 and / < 1268174055 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that much is obvious < 1268174070 0 :MigoMipo!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268174082 0 :muni_!unknown@unknown.invalid PART #esoteric :? < 1268174103 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressez: you zuddenlee look very french < 1268174143 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :this is really frustrating < 1268174221 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :fax are you hot < 1268174265 0 :cpressez!unknown@unknown.invalid PRIVMSG #esoteric :Si pressez-vous la bouton < 1268174290 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION presse la bouton.
< 1268174301 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Le monde explode! < 1268174326 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Que galère!!! < 1268174351 0 :cpressez!unknown@unknown.invalid NICK :cpressey < 1268174353 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well enough of that. < 1268174373 0 :alise!~d4b78c25@gateway/web/freenode/x-gragdkscfdmocvqg JOIN :#esoteric < 1268174386 0 :jcp!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1268174397 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*explose < 1268174400 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :darn french < 1268174404 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :depose* < 1268174468 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1268174631 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :bzflag < 1268174634 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :i remember that game < 1268174647 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :13:46:32 the theorem doesn't actually have any mathematical content, it's just stated for convenience, so you don't have to think about what happens on the boundaries of the sum and the integral every time < 1268174647 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :         | < 1268174647 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :        /�\ < 1268174653 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :everything that is true is an obvious tautology :P < 1268174665 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*facepalm* < 1268174678 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :*kneeear* < 1268174685 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :etc. < 1268174689 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION snickers
< 1268174697 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :lawl < 1268174697 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :There are no trivial mathematics, only trivial mathematicians! < 1268174724 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :myndzi: was that supposed to look dirty? < 1268174728 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: you're quite limber, i take < 1268174748 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: I am on IRC, at least. < 1268174756 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1268174775 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :argh < 1268174780 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268174787 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric : \o/ \o/ \o/ \o/ < 1268174787 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :   |   |   |     | < 1268174788 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :  /|   |\ /|    /| < 1268174799 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric : \o/\o/\o/\o/ < 1268174799 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :   |  |  |  | < 1268174799 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :   |\ |\ >\/�\ < 1268174810 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :/´\ < 1268174821 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric : \o/ < 1268174822 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :    | < 1268174822 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :   /| < 1268174824 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :\o/\o/\o/ < 1268174825 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric : |  |  | < 1268174825 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric : >\ >\ >\ < 1268174846 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/ < 1268174846 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric : |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  | < 1268174846 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric : >\/| /| /< /< /'\/�\/< /< /<  |\ |\/`\ |\/<  |\/| < 1268174850 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric : \o/ < 1268174850 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                                                                 | < 1268174851 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                                                                /| < 1268174854 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :wow awesome < 1268174857 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :very few of them have dicks. < 1268174858 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :that is the coolest thing ever < 1268174868 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :i know \o/ < 1268174868 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :        | < 1268174868 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :        |\ < 1268174877 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :_o/ < 1268174878 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :       | < 1268174878 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :      /'\ < 1268174881 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :HAHA < 1268174882 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :are there actually spaces before? if so, my client strips them >_< < 1268174893 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :there used to be iirc < 1268174895 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :get a client that doesn't suck < 1268174904 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : \m/ \m/ < 1268174905 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :   `\o/� < 1268174905 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :     | < 1268174905 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric : (_|�'\ < 1268174905 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :      |_) < 1268174915 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :LOL WUT < 1268174927 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :\m/ < 1268174933 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric : \m/ < 1268174935 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :\m/ \m/ < 1268174943 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :14:27:52 I suppose that's better than "I love you." "ROTFL" < 1268174944 0 :cheater2!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268174946 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric : \m/ \m/ < 1268174946 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                           `\o/� < 1268174946 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                             | < 1268174946 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                            /'\ < 1268174946 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                          (_| |_) < 1268174947 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*ROTFUL < 1268174967 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric : o < 1268174970 0 :cheater2!~cheater@ip-80-226-44-25.vodafone-net.de JOIN :#esoteric < 1268174974 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric : _o_ < 1268174975 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                          | < 1268174975 0 :myndzi!unknown@unknown.invalid PRIVMSG #esoteric :                         /| < 1268174981 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :wowowowow < 1268174984 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :that is so cool < 1268174993 0 :alise!unknown@unknown.invalid PART #esoteric :? < 1268174999 0 :alise!~d4b78c25@gateway/web/freenode/x-gragdkscfdmocvqg JOIN :#esoteric < 1268175040 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :that script is the only reason i go to #esoteric < 1268175047 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :"alise: are there actually spaces before? if so, my client strips them >_<" <<< first whitespace i've ever seen that nnscript *doesn't* strip < 1268175075 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in the logs it's spaces /and/ some other char < 1268175127 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :lament: ur the only reason I go to #esoteric~ < 1268175158 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: ur the only reason fax goes to #esoteric < 1268175166 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :FU*K < 1268175170 0 :cpressey!unknown@unknown.invalid PART #esoteric :? < 1268175177 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :fax has acne and boils < 1268175202 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :#~esoteric is either the most interesting channel I can think of, or the least, depending on what #esoteric is at the time, < 1268175233 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well, I guess it's #(~esoteric), not ~(#esoteric) < 1268175234 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so most boring < 1268175250 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :oh shut up < 1268175285 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :(I was talking to EgoBot not you alise) < 1268175287 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :it's transitive < 1268175293 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :EgoBot is talking? < 1268175305 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :yeh < 1268175423 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :!echo I'm human! < 1268175427 0 :EgoBot!unknown@unknown.invalid PRIVMSG #esoteric :I'm human! < 1268175456 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :he's just using facilitated communication < 1268175513 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: <3 < 1268175531 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :lament: http://i.imgur.com/ZFlbv.jpg < 1268175549 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :i'm not opening anything at work < 1268175554 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION wonders if that's the same image Quadrescence linked to me before
< 1268175558 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :if so, lament made the right choice :p < 1268175562 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268175577 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :"However, under Japanese rules, the game is already considered to have ended. The players attempt to ascertain which groups of stones would remain if both players played perfectly from that point on. (These groups are said to be alive.) In addition, this play is done under rules in which kos are treated differently from ordinary play. If the players reach an incorrect conclusion, then they both lose." < 1268175590 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: the situation for a disputed endgame in Go is even funnier than I thought < 1268175598 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268175598 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :coppro: if you ever need latex help, you're welcome to ask me instead of going to #latex where people treat you like you're 8.5 years old < 1268175614 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You get nothing! You LOSE! Good DAY sir. < 1268175614 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I love the way that the double loss is given for getting it wrong, rather than for disagreement < 1268175657 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i wonder how many famous games of go are actually platonically a double loss < 1268175662 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but nobody's realised < 1268175672 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise: except with more honorifics < 1268175701 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i wonder how many chess games actually ended with the white winning, but the players thought black won. < 1268175702 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: probably not that many in famous games, you'd expect the players to get it right < 1268175724 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :for draws, there probably are such instances < 1268175736 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: a few famous ones (if you allow vice versa); there was one where one of the players lost on time, and the referee accidentally turned the clock round and gave the win to the wrong player < 1268175738 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: None :P < 1268175740 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :in a relatively publicised tournament < 1268175751 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: that's cheating < 1268175755 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1268175770 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: by the referee? < 1268175773 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it was a mistake, rather than deliberate < 1268175778 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I wonder how many chess games actually ended with the X winning, but the players thought Y won, and the game ended by the taking of a king, where X =/= Y. < 1268175783 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: i mean as an example < 1268175783 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it's cheating as an answer to my wonderingment < 1268175786 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1268175820 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Note that X or Y can be "draw" < 1268175821 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well, xor < 1268175825 0 :FireFly!unknown@unknown.invalid QUIT :Quit: Leaving < 1268175860 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1268175901 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :there was a case (again in a serious tournament) where a player offered a draw, his opponent said "make a move first", the player moved, then the opponent resigned < 1268175907 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :legally, you can still take the draw in that situation < 1268175926 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :(it's a rule against draw offer spam; if someone offers a draw, you can accept until the end of your next move) < 1268175938 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :(so there's no point in offering more than once in the same move) < 1268175949 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but anyway i think it's technically possible that black moves a piece so that the king can't move anymore, and neither player realizes there's a distant piece making it a checkmate instead of a stalemate < 1268175989 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep, I suppose so vaguely < 1268175993 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://sci.tech-archive.net/Archive/sci.logic/2006-10/msg00751.html < 1268175994 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i keep < 1268175994 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1268175995 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :reading this < 1268175996 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :as a < 1268175997 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :poem < 1268175999 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and it < 1268176000 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :is really < 1268176001 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :annoying < 1268176001 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :actually, there are probably loads of draws on time which were claimed as wins on time by mistake < 1268176019 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :(draw on time: if your opponent runs out of time, but it's theoretically impossible to win given the material on the board) < 1268176035 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise "Yessenin-Volpin"? wow a THIRD ultra-finitist?? < 1268176048 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: they don't even include what'shisname in that list < 1268176052 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :the guy we've been talking about < 1268176055 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :japanese rules allow draws on time??? < 1268176056 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so there are FOUR??? < 1268176059 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :fax: oh crap < 1268176067 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :no wait, three < 1268176073 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :fax: the number of ultrafinitists is getting dangerously big < 1268176076 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :lament: Chess, not Go < 1268176082 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :this movement has gained its maximum possible mass (I don't believe in 4) < 1268176085 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :fax: what if it overflows??? < 1268176086 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lament, lol < 1268176095 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's always theoretically possible to play Go so badly that your opponent wins < 1268176098 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :lament: damn you made the same joke as me but beter < 1268176098 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :lament: dammit stealing my joke < 1268176105 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hahaha < 1268176199 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, you know Freek Wiedijk < 1268176200 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268176261 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i do now < 1268176261 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: resend your latest /msg, i closed the tab by mistake < 1268176271 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :ais523: that can't possibly be true, do you see why?? < 1268176279 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :DUCY??? < 1268176294 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :lament: the game lasts an infinite length of time if both people try it < 1268176305 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm sure everyone thought of the joke < 1268176310 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, unless you enforce superko, in which case my statement is indeed incorrect < 1268176334 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :It depends on the form of superko < 1268176340 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :ais523: why would either of them capture at all? They would pass. < 1268176365 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh, good point < 1268176366 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :they ought to pass when there's one empty point remaining < 1268176374 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I somehow assumed that you'd capture with only one point left < 1268176377 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :if the game ends < 1268176382 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :too much exposure to the stupid stupid Yahoo auto-go thing < 1268176391 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :which has a bug where you can run an opponent out of time by repeated passing < 1268176402 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :i'm not sure what's the status if the game ends but i guess it's seki < 1268176413 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :either seki or "both players lose" < 1268176533 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :SEKSI < 1268176555 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :what would be funny would be if you somehow got half a stone onto the board < 1268176559 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and then claimed a draw despite komi < 1268176639 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :very easy with cheap chinese stones, they break all the time < 1268176670 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Here's a thought: hybridize Go and Chess by simply having a chess board, where the intersections are the points on a Go board, every turn you do either a Chess or a Go move, and the Go game works as usual, including taking out Chess pieces :P < 1268176725 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :who wins? < 1268176740 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Whoever either checkmates or takes out the opponent's king. < 1268176763 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Which, I suppose, is problematic for the Go component ... < 1268176767 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :do you need to surround a piece on four sides to capture is? < 1268176770 0 :ais523!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268176770 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Needs some rough edges smoothed out. < 1268176771 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :*it < 1268176777 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :lament: That was the idea? < 1268176779 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :lament: you could take it with a chess piece < 1268176783 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :or surround it < 1268176784 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Well, yes. < 1268176788 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :does go have a winning condition? < 1268176790 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I don't actually know < 1268176790 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: well it's not quite how Go works < 1268176795 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :alise: no, people just fuck around. < 1268176820 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1268176820 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i mean < 1268176821 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :an endgame condition < 1268176821 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :apart from like... running out of pieces < 1268176821 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :or time < 1268176861 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1268176870 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :both players pass < 1268176885 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :note that sometimes you're forced to pass due to not having any valid moves < 1268176892 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :but in principle a game could go on forever < 1268176904 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Checkmate/taking out/both passing = game ends. < 1268176907 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :there's an optional rule, which nobody uses, that disallows repetition < 1268176918 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Then you can invent a hybrid chess/Go winning condition to be applied at endgame. < 1268176940 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Well, that makes sense since both passing is an endgame condition for Chess anyway, stalemate :P < 1268176956 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :From what little I know about Common Lisp, I despise it < 1268176966 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The problem is that in chess, endgame almost always is because of someone winning. < 1268176969 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :funcall? Really? < 1268176974 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :alise: Yuh < 1268176975 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :In Go that appears to be calculated after the fact. < 1268176980 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: So you can name a variable "list". < 1268177007 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: You could redefine instead Go's endgame condition to be because of someone winning somehow. < 1268177021 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :The Go pieces would be controlling areas of the board ... you couldn't move there because you'd be instantly surrounded by opposing pieces. Maybe that's bad :P < 1268177043 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Maybe that's AWESOME. < 1268177050 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Maybe! < 1268177056 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So how does a Chess piece take a Go piece? Maybe jumping over it. < 1268177065 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I wasn't considering that possibility ... < 1268177073 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Say you have a Go piece to the top-left of a pawn. If the pawn moves one space top-left, the Go piece is taken < 1268177074 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :etc. < 1268177097 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :So, Bishops have free take-out powers :P < 1268177121 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :For knights... No fucking clue. < 1268177123 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: They do anyway :P < 1268177125 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I don't think you would use typical Go notions of control < 1268177138 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Probably not quite. < 1268177145 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It's not a hybrid if you significantly modify G1+G2 < 1268177152 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :control really just means an area that if you put a piece in, it will die eventually < 1268177153 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It's your own game inspired by G1, G2. < 1268177164 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :alise: Oh nooooooooes < 1268177168 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :G0? < 1268177175 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The only modifications should be to resolve contradictions. < 1268177219 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :so if you add the ability to leave the area or take one of the controlling pieces, there's no sense in preventing a piece from entering a controlled area < 1268177255 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: You made Chesskers. < 1268177262 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yes, I did :P < 1268177267 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You're making Gochess. < 1268177273 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So, Gochesskers. < 1268177275 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yes, I am :P < 1268177279 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You should add Othello to that mix. < 1268177291 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gothellochesskers. < 1268177296 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yes, I ... wait, whaaaa? < 1268177300 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Go, Othello, Chess and Checkers. Living in perfect disharmony. < 1268177300 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION would never have discovered FICS if XP had "Internet Chess"
< 1268177320 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Wait, what? :D < 1268177329 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Haha, imagine Chess pieces flipping colour because you connect a line. < 1268177361 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Then subsequently taking Go pieces, which then surround a Checker piece, eliminating it. < 1268177380 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Combine ALL board games into one! < 1268177384 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Throw some Risk in there! < 1268177389 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I think we need some 18xx! < 1268177392 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :And where's Clue?! < 1268177392 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :No :P < 1268177402 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But Go, Othello, Chess and Checkers are all fundamentally similar. < 1268177427 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Abstract pieces on a uniform board, with uniform rules throughout, involving pieces "getting rid" of other pieces, with complex strategy underlying simple rules. < 1268177443 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And any two are quite easily hybridised. So.. < 1268177486 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION wishes FICS had a way of defining your own game that used a chessboard and chess pieces
< 1268177500 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :With some simple not-necessarily-TC scripting language < 1268177509 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: fork the source < 1268177524 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :coppro: it's closed < 1268177527 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :the latest version of the server at least < 1268177529 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :it is? < 1268177543 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well wikipedia says an old version was open and is mum about the current, so.. < 1268177548 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*so... < 1268177557 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(directly next to each other) < 1268177559 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Easy enough to ask < 1268177582 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :"MAd(1): no" < 1268177732 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :And now ... < 1268177734 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :FINLANDIA! < 1268177785 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Also, LaTeX's default title font is disturbingly similar to the "font" used for the title of the original publication of Finlandia. < 1268177801 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :COMPUTER MODERN: Disturbing < 1268177840 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :not so modern after all < 1268177859 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :somewhere, on a forgotten sumerian clay tablet... < 1268177898 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :the first ug was typeset by knuth < 1268177922 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :definition: a game A totally wins the game B if there's a winning strategy in the mixed game A|B that uses only moves of A < 1268178009 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm is this related to surreal number ordering? < 1268178058 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Totally wins; terminology first used by Euclid in his Elements. < 1268178061 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Specifically: < 1268178083 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :"Let there be the games A, B. I say that A totally wins B. < 1268178101 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :First, let there be a strategy of A. < 1268178124 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Let it be that when this strategy is used in AB, it is winning. < 1268178125 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i can confirm this because strategy is a greek word. < 1268178140 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :If this is not so, then instead I say B totally wins A." < 1268178155 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that's my piss-poor attempt at emulating the style of Elements... < 1268178159 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh but totally winning is a proper partial order! < 1268178177 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so in fact it's not necessarily true that B totally wins A if A does not totally win B < 1268178216 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :right but that's a modern development of Winning theory < 1268178227 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Euclidean winning theory doesn't have that < 1268178249 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :definition: if A does not totally win B, and B does not totally win A, then we say A|B is not ridiculous < 1268178267 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1268178284 0 :oerjan!unknown@unknown.invalid QUIT :Quit: Good night < 1268178294 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :now the obvious question is, is go|chess a ridiculous idea? < 1268178294 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(Euclid considered "That all entities must be ordered. Take entities A and B and A is not more than B, and B is not more than A. Then A appears before B, and B appears before A. This is an absurdity. So all entities must be ordered.") < 1268178322 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268178361 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: you're abusing notation, A|B is the common parts of the games A and B < 1268178373 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :go|chess would be a board with things that move around and remove other pieces, but past that undefined < 1268178377 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :you mean AB < 1268178401 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(euclid wrote A|B as superscript A, subscript B.) < 1268178418 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :winning theory is like game theory but more indie < 1268178454 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(In complex expressions the notation A above B is often used to save space, but for more complex expressions the super/subscript format is used.) < 1268178463 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Erm, that is, as a component of complex expressions. < 1268178574 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :| is an OR-like character, AB is multiplication which is an AND-like operation < 1268178595 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :exactly < 1268178613 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :remember that euclid thought of games as primitives < 1268178615 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so A|B is the mix of the games, and AB is the common parts. < 1268178635 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :as such, (go chess) was go & chess, i.e. both go and chess. < 1268178650 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's what AND and OR mean in the philosophy of fuzziness. < 1268178655 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :eh fine :P < 1268178668 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :go fish < 1268178808 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the common parts operation probably actually makes sense in some cases, because either you get the empty game or you get some basic moves or something. i guess stuff like winning might be completely removed though < 1268178828 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :is there a good definition for board games somewhere? < 1268178870 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :clearly winning theory is our chance to invent it. < 1268178877 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :game theory is to board games sort of what category theory is to algebras, imo < 1268178889 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :also, euclid didn't even consider common parts by itself to be a valid formula. < 1268178897 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :he always built it up from there to a full game < 1268178903 0 :MizardX!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1268178913 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :maybe, maybe < 1268178973 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :in algebra, the common parts of two algebras are usually directly an algebra, but the mix of two algebras needs to be extended to be a full algebra < 1268179071 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :game theory doesn't talk about board games at all. < 1268179093 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and the second rule of game theory: Do not talk about board games