00:00:31 -!- oklopol has joined.
00:05:15 * Sgeo wonders what Ilari thinks about energy drinks and caffeine pills
00:05:47 -!- Oranjer has joined.
00:07:30 <fax> *Diophant> mathematica ((U "x" :\=: U "y") :/\: (U "x" :>: I 13) :/\: (U "y" :>=: I 7))
00:07:34 <fax> "FindInstance[(((((((x + (-1 * y)) ^ 2) + (-1 * (x1 + 1))) ^ 2) + ((((13 + x2) + 1) + (-1 * x)) ^ 2)) ^ 2) + (((7 + x3) + (-1 * y)) ^ 2))==0 &&x>=0&&y>=0&&x1>=0&&x2>=0&&x3>=0,{x, y, x1, x2, x3},Integers]"
00:07:48 <fax> mathematica takes about 10 seconds then it finds: x -> 16, y -> 11
00:12:58 <Sgeo> "I understand and accept that my choice of cryopreservation may affect the type and extend of medical care I receive. Some physicians and medical facilities may refuse to treat or admit me because of my cryopreservation arrangements or may require that I be transferred to another, perhaps less suitable medical facility for treatment and care."
00:13:05 -!- Phantom_Hoover has quit (Ping timeout: 240 seconds).
00:13:10 <Sgeo> That's kind of.. unacceptable, really
00:14:31 -!- MigoMipo has quit (Remote host closed the connection).
00:14:37 * fax is running '(I 2 :|: U "x") :/\: (I 3 :|: U "x") :/\: (I 5 :|: U "x") :/\: (U "x" :>: I 1)'
00:14:42 <fax> and it is taking a long long time
00:14:57 <Sgeo> J?
00:15:37 <fax> Sgeo, it means that x is divisible by 2 3 and 5, and it's greater than 1
00:18:01 -!- Phantom_Hoover has joined.
00:20:49 -!- FireFly has quit (Quit: Leaving).
00:21:20 <Phantom_Hoover> I lie!
00:21:23 <Phantom_Hoover> Oops.
00:21:30 <Phantom_Hoover> Freudian slit.
00:22:00 <fax> I have asked mathematica to find me a number which is divisible by 2, 3 and 5. and is greater than 1...
00:22:03 <fax> it says "The methods available to FindInstance are insufficient to find the \
00:22:06 <fax> requested instances or prove they do not exist."
00:22:18 <Phantom_Hoover> :O
00:23:36 <Sgeo> fax, J is slow, o.O
00:23:46 <Sgeo> even _I_ know an answer
00:23:48 <oklopol> DID YOU TRY 2*3*5??
00:24:09 <Sgeo> Or wait, that code's Mathematica?
00:24:15 <Sgeo> I've never seen Mathematica code before
00:24:33 <fax> um it's not J
00:24:57 <AnMaster> night
00:24:57 <fax> exists x1, x2, x3, x4, (((x - 2 x1)^2 + (x - 3 x2)^2)^2 + (x - 5 x3)^2)^2 + (2 - x + x4)^2 <--- this expresses that x is divisible by 2, 3, 5 & is greater than 1
00:25:08 <fax> but mathematica gave up on it
00:25:32 <fax> stupid thing
00:26:25 <AnMaster> fax, try reduce?
00:26:34 <AnMaster> Reduce that is
00:26:39 <Sgeo> How would you do it in J?
00:28:24 <Phantom_Hoover> Hmm... I sent a fax to my secretary.
00:28:46 <AnMaster> huh, having your own secretary
00:29:31 <Phantom_Hoover> That was just to test the IRC thing.
00:29:43 <AnMaster> what irc thing?
00:29:55 -!- BeholdMyGlory has quit (Remote host closed the connection).
00:30:25 -!- oklopol has quit (Ping timeout: 264 seconds).
00:31:39 -!- jcp has joined.
00:33:54 <Phantom_Hoover> At least in my client, it highlights stuff.
00:36:26 <AnMaster> what stuff?
00:36:34 <AnMaster> your own nick?
00:36:38 <AnMaster> you were just annoying fax?
00:37:30 <Phantom_Hoover> ...Not particularly.
00:38:28 <Phantom_Hoover> How did everyone else find out about esolangs?
00:39:28 <AnMaster> night really →
00:41:40 <Phantom_Hoover> Anyway, bye.
00:41:42 -!- Phantom_Hoover has quit (Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838]).
00:46:22 <Slereah> I found about it when seeing a humorous drawing involving INTERCAL
01:02:41 -!- zzo38 has joined.
01:04:58 -!- adam_d has quit (Ping timeout: 264 seconds).
01:12:43 -!- zzo38 has quit (Remote host closed the connection).
01:17:55 -!- wareya has joined.
02:30:03 -!- jcp has quit (Ping timeout: 276 seconds).
02:54:34 -!- jcp has joined.
03:05:20 -!- adu has joined.
03:07:37 -!- Oranjer has left (?).
03:12:10 -!- fax has quit (Quit: Lost terminal).
03:48:25 -!- Asztal has quit (Ping timeout: 245 seconds).
03:53:08 -!- augur has joined.
04:53:41 -!- adu has quit (Quit: adu).
05:22:39 -!- pikhq has quit (Read error: Connection reset by peer).
05:23:59 -!- pikhq has joined.
05:24:20 <pikhq> GAH INTERNET HATES ME
05:25:37 <pikhq> Lag: 31.91
05:25:54 <pikhq> GAAAAH
05:28:28 <pikhq> WHO HIT THE INTERNET-SUCKS BUTTON
05:29:49 -!- augur has quit (Ping timeout: 264 seconds).
05:29:56 <Quadrescence> oh that is what that button does ._.
05:37:20 -!- pikhq has quit (Read error: Connection reset by peer).
05:42:59 -!- pikhq has joined.
05:43:40 * Sgeo blames Pez.. err, Quadrescence 
05:44:03 <dixon> It only started happening since people started using Haskell.
05:44:21 <dixon> I know correlation doesn't imply causation--except when it does.
06:02:04 -!- augur has joined.
06:35:42 -!- Gracenotes has joined.
06:45:28 -!- coppro has joined.
06:51:10 * pikhq sees a lack of alise. OH NOES
06:53:34 <coppro> I hope he's made it to Sweden
07:37:40 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:32:49 -!- oerjan has joined.
09:15:54 -!- oerjan has quit (Quit: leaving).
09:36:57 -!- adam_d has joined.
09:42:52 -!- kar8nga has joined.
10:16:28 -!- tombom has joined.
10:28:04 -!- MigoMipo has joined.
10:30:06 -!- adam_d has quit (Ping timeout: 260 seconds).
11:22:23 -!- alise has joined.
11:22:45 <alise> This is a dispatch / it numbers five. / Every weekend / the #esoteric jive. Also: worst poem ever.
11:26:54 <alise> 18:02:33 * alise gets in TARDIS; destination: Friday.
11:26:58 <alise> Oh snap, I caused a pime taradox.
11:28:14 <alise> 20:29:53 <zzo38> I have my own story about teleportation: One guy makes up a new kind of teleporter but something goes wrong. Now we lost the harp. But that's OK, because it caused other things too which are beneficial to the situation anyways. The End
11:28:22 <alise> /speechless
11:28:36 <alise> 21:12:00 * Sgeo fails to see "Cryonics" on WhatsTheHarm
11:28:42 <alise> Most people see cryonics as a harmless scam...
11:29:07 <alise> Most people, of course, usually taking the most mediocrely dumb opinion they can.
11:30:38 <alise> 09:54:11 <ais523_> the quote's from <http://www.geocities.com/tablizer/science.htm>, which somehow still exists, and which is interesting (although I don't know if I agree with it or not yet)
11:30:42 <alise> oh no, not the OOP guy!
11:30:46 <alise> well, anti-oop
11:33:26 <alise> so what's everyone's favourite binary lambda calculus encoding
11:34:10 <alise> I thought I liked John Tromp's especially because it has a 210 bit self-interpreter, but it doesn't seem to be very pure LC to me
11:34:27 <alise> 'cause it isn't directly lambdas and stuff
11:34:51 <alise> no wait it is
11:34:54 <alise> i just read the io section
11:35:29 <alise> hey tromp invented exactly my notation
11:35:38 <alise> well more or less
11:35:47 <alise> 00e = \e
11:35:51 <alise> 01fx = f x
11:36:13 <alise> 1^i0 = i
11:36:22 <alise> although hmm
11:36:33 <alise> don't you need an extra 1 with i?
11:36:45 <alise> because otherwise, 000 ... well actually it is unambiguous
11:36:58 <alise> it kind of irks me that we have 0s at the start though, I don't like that
11:37:06 <alise> because 0 and 000 are distinct programs...
11:37:11 <alise> adding 1 at the start solves that but that's ugly
11:38:12 <alise> then again numbers outside of a lambda aren't allowed
11:38:16 <alise> so we don't need them to be valid on their own
11:38:20 -!- kar8nga has quit (Remote host closed the connection).
11:38:51 <alise> we can do
11:38:52 <alise> 100e = \e
11:38:52 <alise> 101fx = f x
11:38:52 <alise> 11(n 1s)0 = n
11:39:05 <alise> but that's verbose...
11:48:34 <alise> ;
11:48:35 <alise> oops
11:51:32 <alise> 16:52:58 <Tritonio_GR> but a way to implement arrays ovcer brainfuck
11:51:58 <alise> x_0, 1, x_1, 1, x_2, 1, ..., x_(n-1), 1, x_n, 0
11:52:34 <alise> 22:23:01 <pikhq> I IS NOW 10
11:52:34 <alise> 22:23:03 <pikhq> 20
11:52:35 <alise> 22:23:08 <pikhq> NOT 10, 20.
11:52:36 <alise> :|
11:52:39 <alise> stop making me feel inferior
11:52:43 <alise> 23:00:05 <Sgeo> Why are all these younger people smarter than I am?
11:52:45 <alise> CAUSE YOU SUCK
11:53:50 <alise> 23:16:12 <Quadrescence> Yes but reading a book on paper > reading a book on screen
11:53:51 <alise> ebook
11:55:25 -!- BeholdMyGlory has joined.
11:57:04 <alise> http://web.tiscali.it/magazzinocartoniani/ Hey look, old computer ROMs.
11:57:28 -!- oklopol has joined.
11:57:36 <alise> hi oklopol
11:59:50 -!- fax has joined.
12:01:57 <oklopol> hi alise
12:02:00 <oklopol> hi fax
12:02:12 <alise> i has a ti 83 emulator
12:02:22 <alise> i note that it cannot handle me pressing + on the keboard
12:03:59 <fax> hello!
12:05:01 <alise> this thing is a bitch to use
12:06:42 <alise> srsly
12:07:07 <fax> alise what category do you know
12:07:19 <alise> i don't even think ti calculators can do symbolic stuff
12:07:23 <alise> fax: category theory?
12:07:27 <fax> 1
12:07:35 <alise> not a lot at all. and what i do know is mostly how it works in CS
12:08:03 <fax> I got this book called Computational Category Theory, and it implements all the stuff it talks about in SML
12:08:16 <fax> it's realy cool
12:08:22 <alise> sounds nice, apart from SML :P
12:08:35 <fizzie> alise: The TI-89 can do some; that's why it wasn't allowed for exam-use at school.
12:08:40 <alise> pah i'm gonna make my own calculators
12:08:43 <alise> with blackjack, and hookers
12:08:49 <alise> fizzie: downloading a rom as we speak
12:09:13 <alise> if it isn't as good as a cas i don't wnat it :P
12:09:26 <fizzie> It probably won't be.
12:09:30 <fax> wtf
12:09:30 <alise> meh archive is invalid
12:09:38 <fax> alise do you catually know what SML is...
12:09:54 <alise> fax: yes
12:10:02 <alise> i just don't like it much as a language, personal taste
12:10:07 <fax> it like one of the most important functional languages in CS historyr...
12:10:12 <alise> yes, I know
12:10:17 <alise> and i respect it for its innovation
12:10:19 <fax> -_-
12:10:20 <alise> as I do Lisp 1.5
12:10:23 <alise> but I don't like Lisp 1.5, either
12:10:24 <fax> hehe
12:10:38 <oklopol> basic is pretty historically relevant too
12:10:40 <alise> I'd certainly choose it over the abomination that is OCaml.
12:10:50 <oklopol> maybe for slightly different reasons
12:10:55 <fax> whaaaaaaat
12:10:59 <fax> OCAML IS EVEN BETER
12:11:13 <alise> You are of course joking.
12:11:44 <fax> alise: let me explain why ocaml is awesome in one word: categorical abstact machine
12:11:52 <oklopol> "fax: alise do you catually know what SML is..." <<< thought "catually" was some sort of category theory pun at first
12:11:54 <alise> Granted, that is sweet.
12:11:58 <alise> But the actual language I do not like.
12:12:12 <fax> who carse about 'actual language' that's for employees :P
12:12:27 <alise> Yeaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaahhhhhhhhhhh :P
12:12:41 <fax> alise I've been trying to do cats in coq but I failed a lot
12:12:49 <alise> cat = lol cat
12:12:56 <alise> a catamorphism over the lol functor
12:13:15 <oklopol> OMG MY COQ IS FULL OF CATS
12:13:21 <fax> lol
12:13:30 <alise> oklopol: hawt
12:13:32 <alise> AAAANYWAY
12:13:32 <fax> succ it
12:13:49 <oklopol> i like how i made a penis joke after alise's sophisticated category theory one
12:13:54 <alise> I was thinking about representing infinity as (\h -> h) but I'm pretty sure the basic ordinal type you do in functoinal langs is that isn't it
12:14:09 <oklopol> oh good fax made one too
12:14:20 <alise> well, basically representing (lim k->inf e) as (\k -> e)
12:14:35 <alise> and (lim k->n e) as some sort of scaling so that infinity = n
12:15:18 <alise> 11:30:14 <AnMaster> also I assume it was in the kitchen? As you (or I at least) never take any fluids near a computer for safety reason
12:15:20 <alise> oh come on
12:15:26 <oklopol> zorn's lemma is a pretty magical tool
12:15:28 <oklopol> i love it
12:15:29 <alise> your thinkpad has a sophisticated drainage system
12:15:38 <alise> oklopol: is zorn's lemma implied by intensional choice or just extensional?
12:15:42 <alise> I know well-ordering is extensional
12:15:49 <oklopol> i don't know what those terms mean
12:15:53 <oklopol> enlighten me
12:16:09 <fax> zorns LEMMON LOL
12:16:14 <oklopol> :DDDDDDDDDDDDDDDDDDDDDDDDDDD
12:16:16 <alise> http://r6.ca/blog/20050604T143800Z.html intensional choice lets you have ∀ a:A. ∃ b:B. R a b then ∃ f:A ⇒ B. ∀ a:A. R a (f a).
12:16:19 <alise> without well-ordering
12:16:35 <alise> (intensional choice is provable in type theory, extensional isn't)
12:16:38 <oklopol> which ones of those are exists'
12:16:49 <oklopol> i'm still blind
12:17:14 <alise> Intensional choice:
12:17:25 <alise> If FORALL a:A. EXISTS b:B. R a b
12:17:37 <alise> Then EXISTS f:(A->B). FORALL a:A. R a (f a)
12:17:53 <alise> It is provable in type theory.
12:17:56 <oklopol> oh right i guess it's kinda obvious what the quantifiers are based on what choice is
12:18:07 <oklopol> okay what's extensional
12:18:30 <fax> this makes sense because a proof of forall is a function, and exists is a pair b & proof of R a b
12:18:32 <oklopol> i'll still not be able to answer because i haven't seen zorn's lemma derived from choice
12:18:46 <fax> so you are just doing an eta switch thingy, then rewiggling the proof
12:18:56 <alise> What is stated above is the intensional axiom of choice. It is equivalent to saying that every surjective function has a right inverse. The extensional axiom of choice states that if (A, ~A) and (B, ~B) are setiods (a type and equivalence relation on that type), and R is a relation on A and B respecting the equivalence relations, then if FORALL a:A. EXISTS b:B. R a b then EXIST f:(A -> B). FORALL a:A. R a (f a). Further more f will respect the equivalen
12:18:57 <alise> ce relations. The extensional axiom of choice is equivalent to saying that for every surjective extensional function there exists a right inverse that is also extensional.
12:18:58 <alise> "Hope this helps"
12:19:18 <fax> I wonder what zorns lemon woudl be in type theory?
12:19:49 <fax> 99% of the words are things that we DO NOT SPEAK OF in type theory
12:19:56 <alise> Zorn's lemma is equivalent to the well-ordering theorem and the axiom of choice, in the sense that any one of them, together with the Zermelo�Fraenkel axioms of set theory, is sufficient to prove the others
12:20:02 <alise> so zorn's lemma is extensional choice
12:20:10 <alise> so type theory doesn't have zorn's lemma
12:20:19 <fax> in set theory it is.. but in type theory thery may be stratified more preciesly
12:20:33 <alise> also oklopol: http://en.wikipedia.org/wiki/Zorn%27s_lemma#Sketch_of_the_proof_of_Zorn.27s_lemma_.28from_the_axiom_of_choice.29
12:21:22 <fax> alise I'm having universe inconsisency problems but the bitch aint one
12:21:49 <alise> fax: true
12:21:49 <alise> but "probably"
12:21:49 <alise> oh fuck i ran out of mobile broadband
12:21:49 <alise> can anyone hear me?
12:21:50 <alise> 15:26:03 <coppro> do you program Haskell a lot?
12:21:50 <alise> 15:26:09 <fax> never heard of it
12:21:51 <alise> trollaxin'
12:21:59 <fax> ;(
12:22:43 <alise> 15:30:40 <fax> coppro, that's not possible in haskell
12:22:43 <alise> double trollaxin'
12:22:43 <alise> 15:31:02 <coppro> fax: yes, it can. There's a particularly elegant solution to this problem
12:22:43 <alise> 15:31:07 <fax> it says 'purely functional'
12:22:43 <alise> 15:31:16 <coppro> yes. You work on IO objects
12:22:44 <alise> 15:31:24 <fax> oh it's object oriented?
12:22:44 <alise> 15:31:25 <fax> I can do that
12:22:45 <alise> haha you fucking asshole
12:23:12 <fax> alise I thought he was playing along with me but he was actually oblivious :/
12:23:24 <Sgeo> >.>
12:23:28 <fax> it was a disastair on so many levels
12:23:43 <fax> infact I would go so far as to call it a disastaircase
12:24:54 <alise> 15:31:30 <adu> fax: you obviously know nothing about Haskell, so stop making these kinds of assertions
12:24:54 <alise> xDD
12:24:54 <alise> 15:39:26 <fax> coppro [] is nondeterministic search
12:24:54 <alise> 15:39:43 <coppro> hey, thanks, fax, you helped me make up my mind! /ignore it is!
12:24:54 <alise> It is, actually.
12:24:55 <alise> So you're an idiot.
12:24:55 <alise> Admittedly I wouldn't have much confidence in fax's ability to Haskell afte rthe above.
12:24:59 <oklopol> kay so basically you just take bigger and bigger elements and have the sequence be longer than the set's size
12:25:12 <oklopol> i think i can fill in the AoC details
12:26:13 <alise> my opinion on http://tunes.org/~nef/logs/esoteric/10.03.23: you're all whiny cunts, STFU
12:26:19 <fax> lol
12:26:49 <Sgeo> alise, I _still_ don't get the "search" part of []
12:27:03 <fax> Sgeo, uh .. you could have asked me
12:27:27 <alise> 16:37:14 <ais523> oklopol: then it's no different from any other form of government, just with more paperwork
12:27:27 <alise> apart from anarchy
12:27:40 <Sgeo> s/alise/fax/
12:27:55 <oklopol> when you take a cartesian product, you try out all the combinations. the monad lets you do with nice syntax
12:28:02 <oklopol> *do this
12:28:35 <alise> 17:14:59 <ais523> basically, you return an infinitely big lookup table listing what outputs should go with all possible inputs, allowing for interspersings of them
12:28:35 <alise> so you mean Input -> Output.
12:28:35 <alise> fax: Well, to be honest, trolling so convincingly that you don't know Haskell and /then/ making authoritative statements about Haskell Doesn't Really Work.
12:29:27 <fax> Sgeo: do a <- [a1,a2,a3] ; b <- [b1,b2] ; p a b <=> a(a1). a(a2). a(a3). b(b1). b(b2). ?- a(A), b(B), p(A,B).
12:30:16 <oklopol> is it okay that i still find big numbers scary... there was this proof about varieties that starts with us finding a sub*set* of this class that can still be arbitrarily infinite... and then we define m to be a cardinal upper bound for all those infinities, which is possible because there's only a set of them and not a class
12:30:21 <oklopol> and i was like woooooah
12:30:29 <oklopol> well big numbrs
12:30:31 <oklopol> *numbers
12:30:33 <oklopol> more like big sets
12:30:36 <fax> infinity is not a number!!
12:30:37 <Sgeo> oklopol, too much of the math here makes me go wooosh
12:30:42 <Sgeo> I wish less did
12:30:54 <oklopol> but there are infinite cardinals
12:30:59 <fax> Sgeo did you read the finite calculus stuff?
12:31:00 <alise> But Sgeo jumped to conclusions and coppro did the most annoying thing ever (rubbing in /ignores)
12:31:00 <alise> stuff is coming in spurts i think i need to top up mah broadband
12:31:00 <alise> stupid costly POS
12:31:15 <oklopol> stuff coming in spurts for me too
12:31:19 <Sgeo> fax, finite calculus stuff?
12:31:22 <oklopol> oh wait maybe fax was joking again
12:31:24 <fax> -_-
12:32:07 <oklopol> Sgeo: finite calculus is when your integrals only take a finite amount of time to calculate
12:32:30 <alise> Sgeo could have asked you and you could also have explained rather than saying how stupid he is :P
12:32:30 <alise> Neutrality achieved by blaming everyone in equal amounts!
12:32:35 <alise> whoa huge flood
12:32:59 -!- alise has quit (Quit: Leaving).
12:33:13 <fax> 11:32 <fax> wanna se my depedend type
12:33:14 <fax> 11:32 <alise> sure
12:33:14 <fax> 11:32 -!- alise [~alise___@212.183.140.51] has quit [Quit: Leaving]
12:33:15 <fax> ;_;
12:33:19 -!- alise has joined.
12:33:29 <alise> a thing i don't like about binary LC
12:33:34 <alise> false is more complex than true
12:33:36 <alise> because of de bruijn
12:33:38 <oklopol> i wanna see your dependent type too
12:33:46 <oklopol> i didn't know humans had types
12:33:49 <oklopol> that's kinda racist
12:33:58 <Sgeo> Can there be integrals that take an infinite time to calculate but don't have infinitity or neg infinity as the.. bounds [not sure of the terminology]
12:34:00 <fax> come to #morphism
12:34:27 <oklopol> i think yes, for any sensible definition of that
12:34:56 <oklopol> say the integral from zero to zero
12:35:23 <Sgeo> How is that not simply 0?
12:37:23 <oklopol> we'd really have to define all this
12:37:41 <oklopol> i was assuming we'd use some sort of rules to find the expression to be integrated
12:38:54 <fax> Sgeo -- this is where I learned about finite calculus www.stanford.edu/~dgleich/publications/finite-calculus.pdf
12:39:28 <oklopol> you might misunderstand it as talking about something completely different from what i said, i suggest you read harder in that case
12:41:15 * Sgeo wishes we could easily use notation in here
12:41:33 <oklopol> you can use those \ thingies
12:41:37 <fax> yeah I wish we have proper math in IRC :(
12:41:50 <fax> it would be so nice to be abel to type with \mathbb and \mathcal
12:42:18 <oklopol> i don't really like most of math syntax, but what i hate even more is that most of math is in plain english
12:42:30 <alise> fax: you could do that more easiersy
12:42:46 <alise> fax: just have an irc client plugggin
12:42:50 <alise> that looks out for $...$
12:42:55 <alise> or maybe $$...$$ to reduce clashes
12:43:03 <alise> then the rest of the nerds who know latex could just read that
12:49:48 <fax> nerds don't exist
12:52:40 -!- FireFly has joined.
12:56:33 <alise> how come unicode doesn't have ~>
12:56:33 <alise> :(
12:56:34 * Sgeo is trying Elfen Lied
12:56:34 <Sgeo> It's a bit.. gory for my tastes
12:56:41 <alise> it would be a perfect function arrow over setoids
12:58:38 <fizzie> So ↝ doesn't quite cut it? (Admittedly it points a bit to the wrong direction.)
12:59:17 <fax> ~↝
12:59:28 <fizzie> Use the "I don't know where I'm going" arrow, ↬
12:59:36 <fax> dangerous curve :P
13:00:15 <fizzie> What about ⟿ ?
13:00:25 <fizzie> The "LONG RIGHTWARDS SQUIGGLE ARROW".
13:00:33 <fax> loks like a maggot
13:01:52 <fizzie> Or the WAVE ARROW POINTING DIRECTLY RIGHT, ⤳
13:02:09 <fizzie> It doesn't have that much of a wave there, at least in this font, just a hump.
13:02:22 <fizzie> Maybe they just felt that the "HUMP ARROW" didn't sound quite as good.
13:02:38 <alise> Ah, ↝ would work, I suppose.
13:02:58 <alise> ⤳ could do with a bit more of a wave, yeah.
13:05:42 -!- adam_d has joined.
13:07:34 <fax> alise
13:07:57 <alise> what
13:08:26 <fax> http://i.imgur.com/VKAiL.png
13:14:39 -!- augur has quit (Ping timeout: 252 seconds).
13:20:05 -!- kar8nga has joined.
13:21:12 <alise> 11:33:47 <Phantom_Hoover> No, the notion that medical technology will be able to revive you.
13:21:21 <alise> the whole premise is that non-information-theoretic death is not really death, which is true
13:21:33 <alise> it's all about tradeoffs
13:22:31 <Sgeo> The thing is, there are some non-monetary costs too. No autopsies, organ donation is questionable [I'm going to contact Alcor or something and ask], and worst: Do Not Resscussitate once the standby team's there
13:22:40 <oklopol> i ask ya, who'd want to be revived without a soul
13:22:43 <oklopol> ??
13:22:50 <alise> Autopsies -- who cares?
13:23:08 <alise> Organ donation -- Well, cryonics is selfish in the first place: I value /my/ life
13:23:09 <fax> oklopol uh.. hate to break this to ya...
13:23:16 <fax> "soul" doesn't exist
13:23:18 <alise> fax: o, the troller is trolled
13:23:21 -!- oklopol has quit (Read error: Connection reset by peer).
13:23:27 <fax> ^ alise
13:23:32 <fax> or so you thought
13:23:41 <alise> sgeo: and so what about DNR?? you're only gonna be frozen if there's nothing that can be done
13:23:44 <fax> -!- oklopol [~oklopol@a91-153-117-208.elisa-laajakaista.fi] has quit [Read error: Connection reset by getting trolled so hard]
13:25:27 -!- tombom has quit (Quit: Leaving).
13:26:51 -!- oklopol has joined.
13:28:33 <oklopol> fax: people who don't have souls don't have free will because free will comes from souls by deffinition i have free will because if i want i can do whatever i want therefore i have a soul
13:29:00 <oklopol> the logic is irrefutable
13:29:50 <fax> free will is a stupid concept from the dark ages
13:30:18 <fax> I'm so fucking sick of 'atheists' who believe in stupid shit like determinism or free will
13:30:35 <oklopol> no it's not see if i didn't have free will then i couldn't lift this cup unless there was DETERMINISTIC PROCESS in my brain who does it but i can do it if i want or not do it so i must have a free will
13:31:05 <fax> oklopol have I showed you my conscious program?
13:31:22 <fax> int main(void) { puts("I am conscious!"); return EXIT_SUCCESS; }
13:31:26 <oklopol> i mean maybe you don't have free will because you're a ignorance person but i do i'm a thinker logician
13:31:33 <alise> fax: you are such a fucking idiot
13:31:38 <alise> oklopol is trolling you so obviously
13:31:44 <fax> alise your the idiot
13:31:50 <fax> alise.... TWICE
13:31:53 <oklopol> :D
13:31:54 <alise> *you're/
13:31:56 <alise> *you're.
13:32:01 <fax> *you're
13:32:06 <oklopol> fax: no in fact she's trolling *you*
13:32:10 <oklopol> wait
13:32:14 <oklopol> maybe you were both trolling me
13:32:22 <oklopol> this is getting too complicated
13:32:26 <fax> maybe nobody is trolling anyone
13:32:34 <oklopol> my soul can't take this complicatedness
13:32:35 <fax> and we're all secretly serious but wont admit it
13:33:29 <oklopol> i find most of the crazy theories sensible, i think i could seriously believe any of them, but belief is pretty irrelevant
13:33:39 <fax> what crazy theories??
13:33:55 <oklopol> soul, finitism, infinite sets, that reality exists, etc
13:34:46 <oklopol> i prefer to go with the flow and believe what others seem to
13:35:19 <fax> another thing is people who hide behind the guise of 'formalism' to attack REAL philosophies
13:35:47 <fax> I guess I know how people who thing being bisexual is 'cheating' feel
13:36:03 <oklopol> hmm
13:36:17 <oklopol> can you elaborate on the analogy, i'm sort of slow
13:36:20 <alise> i love people who criticise bisexuality in that way, it's hilarious
13:36:25 <alise> this is sex. there are _RULES!_
13:37:06 <oklopol> bisexuality makes you twice more sexable, wanking makes you infinitely sexable
13:37:14 <alise> whoa
13:38:45 <fax> oklopol, people who pretend to be formalists.. but then they attack platonism or whatever. It's like "way to be a formalist" ..
13:41:44 <fax> kind of like people who think they can program in every language but in honesty what they do is pretend they're using the IO monad in haskell or whatever
13:42:09 <alise> fizzie: is there a ≈> arrow, maybe?
13:42:10 <fax> and they think of state as being some "object" that is implicitly passed around
13:42:10 <alise> that would work too
13:42:54 <oklopol> yeah those people probably don't have souls
13:45:27 <alise> fax: btw shouldn't there be another setoid arrow
13:45:36 <fax> what do you eman
13:45:37 <fax> mean
13:45:38 <alise> from one setoid to a different one so that if a~b then f(a)~f(b)
13:45:46 <alise> as opposed to from a setoid to some random type so that if a~b then f(a)=f(b)
13:45:57 <oklopol> that's what the original was
13:46:01 <oklopol> with <->
13:46:04 <fax> I wrote a ~ b ==> f(a) <-> f(b)  earlier, to show that you could use different equivalences
13:46:04 <oklopol> on the right
13:46:05 <alise> the former is more general since you can have ~ be =
13:46:10 <alise> fax: ah.
13:46:27 <fax> but alise if you use quotients then you can just use = everywhere
13:46:34 <fax> a ~ b <=> [a] = [b]
13:46:47 <fax> where [a] is the equivalence class of a
13:47:00 -!- kar8nga has quit (Remote host closed the connection).
13:47:26 <alise> fax: quotients imply extensional choice
13:47:35 <alise> so i don't want them
13:47:53 <fax> alise but say you had some development that used quotients
13:48:06 * alise wonders what to call the constructor A -> A/~
13:48:13 <fax> there could be an automatic elaboration that turns it all into the equivalent setoid development no?
13:48:25 <alise> fax: sure
13:48:34 <fax> so where does choice come into it?
13:48:36 <alise> I think it's the bending = that makes choice happen
13:48:43 <alise> because = is a very strong statement...
13:48:53 <alise> if we elaborate it out we no longer use =
13:48:54 <fax> [a] = [b] just means a ~ b
13:49:04 <alise> fax: all I know is that it has been proved
13:49:09 <fax> llol
13:49:17 <fax> I proved that 4 = 2
13:49:40 <alise> fax:
13:49:40 <alise> The key difference between set theory and type theory is that in set theory one can form quotient sets for arbitrary equivalence relations. In intensional type theory, one cannot form quotient types. If one could form quotient types, then one could reduce an extensional relation to an intensional relation on quotient types. Then one could use the intensional axiom of choice to get the extensional choice function.
13:50:03 <fax> I don't get your point
13:50:05 <alise> i can't bring myself to argue with roconnor he's too cool
13:50:17 <fax> link?
13:50:32 <alise> http://r6.ca/blog/20050604T143800Z.html
13:50:37 <alise> plus
13:50:38 <alise> For more information see EM + EXT- + ACint is Equivalent to ACext by Jesper Carlstr�m.
13:53:25 -!- MizardX has joined.
14:34:51 <alise> http://pastie.org/889672.txt?key=yr84tq66b2gw65xcuq2o3a
14:35:05 <alise> Setoids, fuck yeah.
14:37:41 <alise> pikhq: Bow to my superiority! You only know Haskell! (Now pikhq will learn dependent type theory in three days.)
14:47:58 <fizzie> alise: I don't seem to see any squiggliness in the double-line arrows. :/
14:48:13 <alise> fizzie: Aww.
14:48:16 <alise> Oh well; what I have now is aceptable.
14:49:08 <fizzie> alise: But when you *really* want to point right, there's the three-arrow ⇶, and the triple-arrow ⇛. And if you don't mind pointing up; the quadruple-arrow, ⟰. (There's also a rightwards quadruple arrow, ⭆, but my fonts don't have that one.)
14:49:34 <alise> ⟰ - the penis hut arrow.
14:58:40 -!- adam_d has quit (Ping timeout: 258 seconds).
15:07:21 -!- Sgeo_ has joined.
15:10:12 -!- Sgeo has quit (Ping timeout: 265 seconds).
15:15:04 <AnMaster> <alise> your thinkpad has a sophisticated drainage system <-- it does. a) That does not mean my desktop keyboard has one as well. b) It is meant for when things go wrong, there is no reason to increase the risk of having to put it to use.
15:15:29 <alise> drinking near a computer is completely harmless.
15:16:07 <alise> and I'm fairly sure the design for the drainage system started with "I hate it when I spill drinks on my laptop and it gets fucked up, we should make it safe to drink"
15:16:25 <alise> maybe you just have really wobbly hands
15:26:44 -!- ais523 has joined.
15:31:29 <alise> hi ais523
15:31:39 <ais523> hi alise
15:53:02 -!- Asztal has joined.
16:02:16 -!- coppro has quit (Quit: I am leaving. You are about to explode.).
16:12:33 -!- AnMaster has quit (Ping timeout: 265 seconds).
16:14:40 <alise> so now fax has dragged me into using coq :(
17:01:05 <fax> success!
17:16:45 -!- Asztal has quit (Ping timeout: 245 seconds).
17:16:56 <Gregor> Haw haw
17:16:59 <Gregor> alise loves the coq.
17:17:43 <alise> That I do.
17:26:01 <olsner> ...
17:30:15 <alise> #esoteric: home of ...
18:02:11 <pikhq> alise: THOU
18:05:31 <fax> aliζe
18:06:47 <pikhq> alise: BOW TO MY SUPERIORITY YOU KNOW ONLY ENGLISH! でも、何も日本語で言うつもり！悪人ね！
18:07:51 <fax> wow 言 is nice
18:08:17 <fax> 言 -- japanese for beehive
18:09:52 <pikhq> Japanese for "say", actually.
18:10:12 <fax> wrong
18:10:13 <pikhq> Also Chinese.
18:10:26 <fax> you can't redefine it
18:10:39 <pikhq> -_-'
18:10:48 <fax> ^ζ^
18:10:49 <fax>  -
18:22:50 -!- mibygl has joined.
18:23:29 <mibygl> So, I'm pondering making a Unix MOO. No surprise there.
18:24:52 <mibygl> And I'm thinking it might be a good idea to set processes' UIDs to random junk, and then set files' owners to the same random junk so that the processes can access the files.
18:25:15 <ais523> hmm, interesting...
18:25:22 <mibygl> Is there anything wrong with doing such a thing?
18:26:45 <mibygl> What makes a user, anyway? Just an entry in /etc/passwd?
18:29:09 <alise> yes
18:29:14 <alise> plus /etc/shadow nowadays
18:30:03 <mibygl> So does anything bad happen if the /etc/passwd entry is missing?
18:31:51 -!- jcp has joined.
18:37:42 <alise> Well... if things try and look up things like username, yes
18:39:43 <pikhq> Actually, /etc/passwd doesn't make a user on most NIXen. PAM just uses /etc/passwd to check users.
18:39:54 <pikhq> PAM can do other things for that.
18:42:06 -!- jcp has quit (Read error: Connection reset by peer).
18:42:56 -!- AnMaster has joined.
18:43:15 -!- jcp has joined.
18:53:15 -!- oerjan has joined.
18:56:51 <fax> hehehe
18:57:28 <fax> infinity! = sqrt(2pi)
18:57:43 <fax> just like how 1+1+1+1... = -1/2
19:01:43 <ais523> there is something wrong with the reasoning here...
19:01:56 <ais523> (there is a decent argument that 9 recurring = -1, though)
19:10:41 -!- Slereah has quit (Ping timeout: 276 seconds).
19:16:34 -!- Slereah has joined.
19:34:43 <Sgeo_> ais523, there's a reddit comment I wanted to link you to
19:34:58 <ais523> Sgeo_: why don't you link me to it then?
19:35:12 <Sgeo_> Because I don't remember it offhand
19:35:14 <Sgeo_> It's in the logs
19:35:46 <ais523> on which day?
19:35:54 <Sgeo_> Today/yesterday
19:37:46 <ais523> http://www.reddit.com/r/programming/comments/bioxv/while_thinking_about_turing_machines_i_found_that/c0mypya ?
19:38:37 <ais523> I think I prefer alise's concept; create a device with an extensible tape, that asks a human to give it more tape if it runs out
19:38:38 <Sgeo_> Yes
19:38:54 <alise> Wait, when did I say that?
19:39:06 <ais523> ages ago
19:39:10 <alise> ais523: I just want you to know that Coq is the bes tthing ever
19:39:14 <ais523> at least, I think it was you
19:39:16 <ais523> what is Coq anyway?
19:39:16 <alise> *thing
19:39:22 <alise> A programming language / proof assistant.
19:39:27 <alise> Practical: the four-colour theorem has been formalised in it.
19:39:36 <ais523> that was a weird theorem
19:39:39 <alise> It's French, so they don't mean no harm with that slightly iffy name.
19:39:39 <ais523> or at least, a weird proof
19:39:59 <alise> ais523: My first project in it has been - with fax's help - making an stdlib from scratch for it.
19:40:09 <alise> It's been smooth sailing.
19:40:35 <ais523> I've been having more thoughts about "splint done right"
19:40:40 <alise> It has the typical proof assistant conveniences: tactic-based proving but also tactic-based definitions, so you basically choose a bunch of different ways to mangle data/existing proofs/etc and it applies it to the right stuff and constructs the huge lambda-expression for you.
19:40:46 <alise> Which has helped me define quite a few functions.
19:40:51 <alise> Dependent up the wazoo, naturally.
19:41:00 <ais523> lambdas are one thing that tends to need sugar
19:41:05 <ais523> (or in the case of esolangs, antisugar)
19:41:12 <ais523> hmm... syntactic salt?
19:41:32 <alise> well, proofs are lambda-expressions
19:41:39 <alise> (and propositions are types; curry-howard)
19:41:44 <alise> tactics let you write it a lot nicer
19:42:02 <alise>   Theorem Identity_leibniz {x y : T} {P : T -> Prop} : Identity x y -> P x -> P y.
19:42:04 <alise>     intros x y P H H′.
19:42:04 <alise>     destruct H.
19:42:04 <alise>     assumption.
19:42:04 <alise>   Qed.
19:42:22 <ais523> I should logread more often
19:42:29 <alise> intros binds all your assumptions to variables; x and y are the Ts, P is the T -> Prop, H is the identity proof, H' is the P x proof
19:43:22 <fax> 18:39 < alise> It's French, so they don't mean no harm with that slightly iffy name.
19:43:27 * ais523 catches oerjan in a butterfly net -----\XXX/
19:43:37 <fax> It's French so they do everything they possibly can to mock our stupid language :P
19:43:58 <ais523> I've wanted to do that unexpectedly for months, but never found an opportunity at which simultaneously I was thinking about it, and it would be sufficiently unexpected
19:44:04 <ais523> I would make an awful Spanish Inquisition
19:46:33 <alise> Coq is totally unwashed
19:46:40 <ais523> <AnMaster> I have seen the *same* multimeter display, without me touching anything on it displaying:  1.010 V, 1.01 V, 1010 mV
19:47:01 <ais523> that's easy to explain, it was an autoranging multimeter with substantial hysteresis involved (so that you could actually read the number)
19:47:02 * oerjan buzzes frantically around in the net
19:47:02 <AnMaster> ais523, and why did you mention this?
19:47:08 <ais523> AnMaster: to explain it
19:47:12 <AnMaster> err
19:47:14 <AnMaster> ah
19:47:18 <AnMaster> ais523, well tell me then
19:47:23 <ais523> I just did
19:47:26 <ais523> <ais523> that's easy to explain, it was an autoranging multimeter with substantial hysteresis involved (so that you could actually read the number)
19:47:26 <AnMaster> ah there
19:47:48 <AnMaster> ais523, that explains two of it
19:47:53 <AnMaster> ais523, but not why there are three?
19:47:55 <ais523> all three, actually
19:48:06 <AnMaster> ais523, really? I could see the V/mV thingy but...
19:48:11 <ais523> those are three different ranges
19:48:18 <ais523> because autoranging works in multiples of 10
19:48:30 <ais523> internally, the second one is 0101 units of .01 V
19:48:31 <AnMaster> ais523, it seems strange that three ranges overlaps for a single value
19:49:00 <ais523> but a decimal point's added to make it less weird-looking
19:49:07 <AnMaster> hah
19:49:13 <ais523> in theory, a single value could be in loads of ranges
19:49:27 <AnMaster> ais523, that seems poor design though to me?
19:49:28 <ais523> 0.001µV is probably in every range on the multimeter
19:49:32 <ais523> but they'd probably all treat it as 0
19:49:45 <AnMaster> heh
19:49:47 <ais523> it's not poor design; no range has trouble reading numbers /below/ the ideal region
19:50:09 <ais523> and if the signal was, say, a square wave changing relatively slowly
19:50:20 <ais523> you wouldn't want it to keep re-ranging every time it went past 0
19:50:28 <AnMaster> ais523, but why is the hysteresis so large that the value may be displayed in 3 different way?
19:50:36 <ais523> because you'd end up overloading the multimeter and/or blowing the fuse
19:50:45 <AnMaster> aha
19:51:01 <ais523> AnMaster: because, the size of the hysteresis is measured in time, and the ranges are measured in volts
19:51:02 <AnMaster> ais523, it was stable at all three values
19:51:08 <AnMaster> so there wasn't any such time delay
19:51:15 <ais523> now, it likely also doesn't change if the voltage isn't changing
19:51:32 <ais523> there'll probably be a processor in there somewhere, and that would be a plausible way to program it
19:51:47 <AnMaster> ais523, well the voltage was jittering up and down a tiny bit. it was for AC. so RMS value
19:51:51 <ais523> (processors are cheap nowadays, trying to do autoranging "by hand" is entirely possible but would be expensive)
19:52:26 <ais523> ooh, theory: there were two hystereses involved
19:52:34 <AnMaster> ais523, and considering it has a digital display and lots and lots of buttons I assume it has a processor
19:52:40 <ais523> one for the actual range selected (millivolts, or tens of millivolts)
19:52:47 <ais523> and one for the units to display in (millivolts, or volts)
19:52:53 <AnMaster> ais523, well, the selector was on voltage (AC)
19:52:55 <ais523> that would explain how you got all three possibilities stably
19:52:56 <AnMaster> if that helps
19:53:17 <AnMaster> ais523, heh, quite insane :D
19:53:33 <ais523> AnMaster: not at all, as the display and the measurement would be entirely different circuits
19:53:34 <oerjan> so this is all quite hysterical?
19:53:45 <ais523> oerjan: quite
19:53:48 <AnMaster> hah
19:54:49 <AnMaster> ais523, I'm not sure if the fact that it was measuring RMS and not peak voltage complicates it further or not
19:55:02 <alise> Measure what aspect of Stallman?
19:55:06 <ais523> AnMaster: it depends on /how/ it was trying to measure RMS
19:55:19 <AnMaster> ais523, well it was marked "true RMS" whatever that means.
19:55:23 <pikhq> alise: Clearly it was trying to measure the proximity of RMS.
19:55:23 <ais523> it shouldn't make any difference if it's by the standard method of rectifying then putting a capacitor in there
19:55:26 <AnMaster> oh and input was a sinusoidal, from a function generator
19:55:32 <ais523> oh, it wasn't using the standard method then
19:55:36 <pikhq> But only the true RMS, not the impersonators.
19:55:37 <alise> pikhq: a warning meter then
19:55:47 <AnMaster> ais523, how does it measure "true rms" then?
19:55:50 <ais523> if you rectify then add a capacitor, the result depends on the shape of the wave
19:56:09 <ais523> as in, there's a correction factor (1/sqrt(2) for a sine wave, 1 for a square wave) to get RMS
19:56:18 <AnMaster> alise, RMS is, uh, Root Mean <something>
19:56:29 * AnMaster know what it means, just not what it stands for
19:56:32 <AnMaster> knows*
19:56:41 <ais523> true RMS means that it's using some form of measurement that can deduce the actual RMS without knowing the shape, but I'm not sure how to measure that
19:56:44 <ais523> AnMaster: root mean square
19:56:51 <AnMaster> right duh
19:57:27 <AnMaster> ais523, measuring peak-to-peak would be a lot simpler sometimes. :/
19:57:40 <AnMaster> well I guess that is what you have oscilloscopes for
19:57:53 <ais523> I can't think of an obvious way to do peak-to-peak either
19:58:04 <AnMaster> ais523, well, using a oscilloscope
19:58:08 <AnMaster> that seems obvious to me
19:58:10 <ais523> I mean, on a multimeter
19:58:24 <AnMaster> (the oscilloscope I used even has a measure button with an option for peak-to-peak)
19:58:24 <ais523> analog oscilloscopes rely on a human to see which bits of phosphorous are getting marked
19:58:27 <ais523> and to set trigger levels
19:58:30 <AnMaster> ais523, it was a digital one
19:58:36 <AnMaster> the oscilloscope
19:58:44 <ais523> yep, modern oscilloscopes are a lot more sophisticated and can actually pick up the signal themselves
19:58:52 <ais523> rather than relying on physics to amplify the signal
20:01:22 <oerjan> metaphysical oscilloscopes
20:02:45 <AnMaster> ais523, yes indeed it did
20:02:55 <AnMaster> you just pressed autoset or something like that iirc
20:03:02 <AnMaster> and possibly adjusted some settings afterwards
20:03:15 <AnMaster> like changed from peak-detect to sample or to average-sample
20:03:39 <AnMaster> (I don't know why it always preferred the noisy peak detect mode)
20:04:48 <ais523> peak detection is inherently noisy, because it relies on a very short length of time to grab the peak
20:04:57 <ais523> and any noise will have a full effect at that moment, rather than averaging over time
20:15:11 -!- Quadrescence has quit (Ping timeout: 265 seconds).
20:16:23 <AnMaster> ais523, indeed
20:16:34 <AnMaster> ais523, sample mode was rather noisy too iirc
20:16:43 <AnMaster> while averaging sample was quite nice
20:16:59 <lament> there was a technician named Pope
20:17:10 <lament> who plugged into an oscilloscope
20:17:16 <lament> the cyclical trace
20:17:20 <lament> of their carnal embrace
20:17:35 <lament> had a damn near infinite slope
20:17:49 <ais523> so in other words, it was a square wave?
20:19:20 <ais523> or arguably sawtooth, but that would have implied two slopes, one near-infinite, the other definitely finite
20:20:09 <oerjan> well it said _a_ damn near infinite slope
20:20:25 <ais523> yep, that's why I thought square wave was more likely
20:20:33 <ais523> we know it's some sort of wave, as it's cyclical
20:20:39 <oerjan> a square wave has two infinite slopes
20:20:44 <oerjan> up, and down
20:20:46 <ais523> yes
20:20:53 <ais523> and two zero slopes, for the horizontal bits
20:21:06 <ais523> btw, "rising edge" and "falling edge" are more common names for them
20:21:22 -!- FireFly has quit (Remote host closed the connection).
20:22:35 <ais523> <AnMaster> intercal needs to be... more self-modifying
20:22:42 <ais523> AnMaster: you've obviously never really looked into CLC-INTERCAL
20:22:49 <ais523> you can redefine syntax on the fly
20:24:44 -!- mibygl has quit (Ping timeout: 252 seconds).
20:25:10 <fax> I ROTE A HASKEL PROGAM sqrt . sqrt . (120 *) . sum $ do [ 1/(m*m*n*n) | n <- [1..150], m <- [1..n-1] ]
20:25:30 <AnMaster> ais523, heh
20:25:33 <fax> it uses a nondeterministic search for pie
20:25:39 <AnMaster> ais523, can you modify the program code at runtime too?
20:25:43 <AnMaster> or just the syntax?
20:25:58 <ais523> AnMaster: just the syntax, but that makes the code mean something else
20:26:06 <AnMaster> btw, is earth hour at the same time over there as here?
20:26:12 <AnMaster> here it starts in a few minutes
20:26:20 <ais523> it's a much better form of self-mod than limited little code modification
20:26:38 <ais523> action at a distance is INTERCAL's niche, I think
20:27:23 <ais523> things like DO ABSTAIN FROM CALCULATING have been around for ages
20:27:31 <ais523> although that's /so/ global it's not that useful
20:27:38 <ais523> CLC-INTERCAL has scoped abstentions
20:27:48 <ais523> as in, DO ABSTAIN #1 FROM CALCULATING followed by DO REINSTATE CALCULATING
20:27:59 <AnMaster> also why do I get statically charged whenever I rise up out of this chair
20:28:03 <AnMaster> very strange
20:28:13 <ais523> which will abstain/reinstate without clobbering any existing abstentions, like the -72 version does
20:28:35 <ais523> I love INTERCAL's scoping mechanism so much
20:31:51 * AnMaster loads a 133 MB large pcap dump into wireshark
20:31:55 <AnMaster> lets see what happens
20:32:22 <AnMaster> ouch bad idea
20:32:27 <AnMaster> swap trashing on laptop
20:34:25 * AnMaster tries to split it into several dumps
20:34:45 <alise> http://pastie.org/889997.txt?key=xph638b5e1j3ea7zdtfga ;; this stuff /half/ works!
20:35:35 -!- Oranjer has joined.
20:41:58 <Sgeo_> alise, are you IRCing in OCaml or something?
20:42:54 <alise> ircing howso?
20:42:56 <alise> and that is Coq, not OCaml
20:44:25 * Sgeo_ was trying to make a reference to the ;;
20:44:49 <Sgeo_> I glanced at an OCaml tutorial, and ;; at the end of statements is the only thing I remember
20:46:09 <fax> hehe
20:48:38 <alise> ah.
20:48:41 <alise> those are lisp comments
20:50:25 <alise> defining setoid arrows is hard
21:27:38 <dixon> alise: I see the problem. The definition of an equivalence relation is taking up half your code.
21:27:45 <dixon> I kid.
21:27:56 -!- adam_d has joined.
21:27:56 <alise> Hey, it's the very complicated relation A = A!
21:27:58 <alise> Just ask Ayn Rand!
21:28:07 <alise> Also, technically only Inductive Identity (T : Type) (x : T) : T -> Prop := refl : Identity x x.
21:28:09 <alise> is the actual definition :P
21:28:15 <alise> The rest are really trivial theorems.
21:28:59 <dixon> I would ask Ayn Rand, but she's dead, and most of her proponents are stupid or batshit insane.
21:29:22 <dixon> And considering she's the butt of most modern philosophers' jokes, I dare not ask them either.
21:30:40 <alise> Ayn Rand is of course an idiot.
21:31:03 <alise> She thought A = A was the most profound statement ever and based her entire self-aggrandising, psychopathic philosophy on it.
21:31:07 <alise> Well, was, not is.
21:32:10 <dixon> I read A = A! as "A equals A factorial"
21:32:15 <dixon> <_<
21:32:36 <Sgeo_> {0, 1} E A
21:32:57 <Sgeo_> A bit backwards, but the best I could do
21:33:05 <alise> A is a value, not a set.
21:33:05 <Sgeo_> Wait
21:33:09 <alise> Perhaps you meant:
21:33:14 <alise> E = 0 \/ E = 1
21:33:15 <Sgeo_> I got it wrong, it's 1,2
21:33:21 <alise> That also
21:33:39 <fax> 20:30 < alise> She thought A = A was the most profound statement ever and based her entire self-aggrandising, psychopathic philosophy on it.
21:33:40 <alise> Or A in {1,2}.
21:33:41 * Sgeo_ meant the E to be a backwards.. membership thing
21:33:43 <fax> alise: where can I read this?
21:34:19 <dixon> Sgeo_: The backwards E is "there exists"
21:34:37 <Sgeo_> Not literally backwards E. More like a curved backwards E
21:34:39 <alise> faxObjectivism states that "Existence exists" and "Existence is Identity." To be is to be "an entity of a specific nature made of specific attributes." That which has no attributes does not and cannot exist. Hence, the axiom of identity: a thing is what it is. Whereas "existence exists" pertains to existence itself (whether something exists or not), the law of identity pertains to the nature of an object as being necessarily distinct from other objects
21:34:39 <alise> (whether something exists as this or that). As Rand wrote, "A leaf ... cannot be all red and green at the same time, it cannot freeze and burn at the same time. A is A."[9]
21:35:00 <dixon> Sgeo_: A \in {0, 1} or {0, 1} \in A?
21:35:00 <fax> alise I mean a book or what?
21:35:01 <Sgeo_> But it can be green and have cells at the same time.
21:35:11 <alise> fax: what ayn rand?
21:35:14 <alise> you want to read ayn rand?
21:35:23 <alise> do you have the /patience/ for that many thousands of pages of nonsense?
21:35:24 <fax> alise, yes about A = A
21:35:35 <ais523> ooh, TVTropes has a really clever CAPTCHA
21:35:36 <alise> do you really want to sit through the rape-is-awesome scenes?
21:35:45 * Sgeo_ had to read, um, Anthem I think, for school
21:35:57 <ais523> it's http auth, which states the password in the login dialog
21:36:01 <alise> Sgeo_: Suicide is the only option.
21:36:07 <Sgeo_> The one where the boy discovers a light-bulb-box thing, and the scientist people of the time threaten to destroy it
21:36:22 <pikhq> Such a poorly written book.
21:36:36 * Sgeo_ may be describing it poorly
21:36:38 <pikhq> alise: It was at least a short work of hers. A mere few hundred pages.
21:36:54 <pikhq> Sgeo_: I, too, had to read that book. It sucked ass.
21:37:08 <alise> "This is my favourite Ayn Rand novel. It blows."
21:37:13 * Sgeo_ doesn't remember having an opinion in particular
21:37:38 <Sgeo_> Other than that yes, the society that Ayn Rand describes is dystopian
21:37:47 <dixon> I would've made them opt for some good-ole Huxley.
21:38:14 <Sgeo_> Having people be able to take credit for things is not a bad thing.
21:38:37 <pikhq> Sgeo_: She considers that dystopian society the result of having government.
21:38:44 <pikhq> Just... *Having* government.
21:39:00 -!- adam_d has quit (Ping timeout: 252 seconds).
21:39:01 * Sgeo_ blinks
21:39:05 <pikhq> Yes.
21:39:22 <pikhq> Your government just forced you to read an anarchist screed.
21:39:36 <alise> I have anarchistic tendencies but make no mistake: anarcho-capitalism is not anarchism.
21:39:38 <ais523> of course, editing TV Tropes is a sign of a deliberate choice to have your life sucked in, I suspect
21:39:53 <pikhq> alise: Well... Yeah...
21:41:19 <Gregor> I thought we were an anarcho-syndicalist commune.
21:41:29 <pikhq> Gregor: XD
21:41:33 -!- FireFly has joined.
21:41:37 * Sgeo_ would tend to prefer something that didn't need various patches
21:41:48 <alise> No, we're mutalist.
21:41:48 <alise> Just so we can be more obscure and esoteric.
21:41:58 <Gregor> Oh, you're talking about Ayn Rand.
21:42:02 <Sgeo_> And will only ever support something that has a non-violent transition plan.
21:42:04 <Gregor> No wonder so much retardation has invaded the channel.
21:42:10 <alise> I'd say we're actually more like anarcho-anarchism, by which I mean that everyone does what the fuck they want because they can't hurt anybody else.
21:42:21 <Sgeo_> CAN'T?
21:42:27 <Sgeo_> Sounds like the world of Prime Intellect
21:42:47 <alise> Sgeo_: Anarchism will probably never have a non-violent transition plan, as the whole point is that capitalism will use violent measures to maintain it.
21:42:48 <alise> *itself
21:42:52 <Sgeo_> I don't know why the author made it seem dystopian. To me, it would be Heaven.
21:43:00 <alise> I wouldn't say that's anarchism's fault...
21:43:19 -!- tombom has joined.
21:43:58 <Sgeo_> Aren't anarchism and capitalism orthogonal?
21:44:45 <Gregor> When you start talking about such things you have to start distinguishing "government" from any other form of social structure, but that distinction becomes meaningless very fast.
21:45:09 <Gregor> In lack of a formal government, any form of social structure will soon become an effective government.
21:45:36 <tombom> but MONEY IS NATURAL
21:45:38 <tombom> or something
21:46:04 <pikhq> In particular, the corporations that will form to provide basic services will soon function as a form of government.
21:46:21 <Gregor> GOVERNMENT IS INEVITABLE
21:46:21 <tombom> but it's capitalist, it's all ok
21:46:23 <Gregor> MUAHAHAHAAHAH
21:46:56 <pikhq> More than likely a form of feudalism, but it's a complete and utter crapshoot what would actually happen.
21:46:58 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
21:48:06 <AnMaster> how comes all the wlan channels except channel 13 are overcrowded around here...
21:48:08 <AnMaster> strange
21:48:25 * AnMaster uses channel 13 for his router, and so does one other AP
21:50:15 <pikhq> Beats me.
21:50:23 <pikhq> Hmm. Which country are you in?\
21:50:42 <alise> sweden
21:50:44 <alise> <Sgeo_> Aren't anarchism and capitalism orthogonal?
21:50:45 <alise> no
21:50:49 <AnMaster> alise beat me to it
21:51:00 <alise> they are mutually exclusive
21:51:12 <pikhq> Beats me.
21:51:14 <AnMaster> alise, are they?
21:51:15 <alise> Gregor: Indeed but anarchism is more the opposition to government than the belief that it can be completely eliminated for all time.
21:51:18 <alise> yes
21:51:34 <AnMaster> channel 6 and 11 btw seems to be the most over populated
21:51:43 <alise> "anarcho-capitalism" is just a silly lie invented by proponents of laissez-faire
21:51:51 <AnMaster> in total there are 43 networks visible from walking around this floor
21:51:59 <pikhq> In the US, channel 13 is more regulated than the rest (requires lower power gain, because it buts up against licensed spectrum)
21:51:59 <AnMaster> (not all are visible from any given point)
21:52:25 <AnMaster> pikhq, not so in EU afaik
21:52:38 <pikhq> alise: Anarcho-capitalism, AKA "Lalala capitalism is god, hail Adam Smith"
21:53:27 <alise> Ripple is possibly the closest thing to anarcho-capitalism that could work.
21:53:37 <pikhq> As an aside, I find the "hail Adam Smith" stuff pretty funny.
21:53:40 <AnMaster> also, compared to my last scan a few months ago there are fewer WEP and fewer open, a lot more WPA, but the same number of WPA2
21:53:56 <pikhq> ... He was a proponent of various forms of welfare, in addition to a market economy.
21:54:47 <AnMaster> oh also some people seem to shut off their wireless in the evening
21:55:03 <AnMaster> did a number of scans today, and it went down by half in the last hour
21:55:42 * Sgeo_ misread that as "scams"
21:56:48 <AnMaster> har
21:57:42 <AnMaster> also I'm really curious about that hidden ssid that I have never seen any clients connected to. Could be that the client's have too weak signals for it to reach me I guess
22:03:59 <ais523> hmm... my rule 34 test case seems to be holding up
22:04:06 <AnMaster> ais523, oh?
22:04:13 <ais523> the standard "proof" of rule 34 is that there is porn of every Pokémon in existence
22:04:20 <AnMaster> ais523, there is+
22:04:21 -!- lament has quit (Ping timeout: 240 seconds).
22:04:24 <AnMaster> s/+/?/
22:04:31 <ais523> and apparently the Pokémon that was recently announced as being in the next games has already been involved in this
22:04:40 <ais523> to the extent that it's being marked as a prime example in TV Tropes
22:04:54 <ais523> (I check there to verify existence, rather than searching myself; it seems someone else is doing the same measurements)
22:04:54 <AnMaster> -_-
22:05:08 <AnMaster> ais523, I thought you never visited tv troupes?
22:05:12 <AnMaster> you told me so before
22:05:16 <ais523> AnMaster: I visit it in bursts
22:05:19 <ais523> and I'm on one at the moment
22:05:25 <AnMaster> tropes*
22:05:27 <ais523> I decide that this is a moment where I don't mind spending hours on it
22:05:41 -!- lament has joined.
22:05:43 <AnMaster> ais523, you told me before that you had *never visited* it though
22:05:45 <AnMaster> was quite recently
22:05:47 <ais523> and then I just decide to stop looking after a while, bookmarking all the pages I'm on so I can find them again
22:05:52 <ais523> AnMaster: at that point, I had never visited it
22:05:57 <ais523> I've only been on three bursts altogether
22:06:16 <AnMaster> ais523, did you get stuck in those cases? XD
22:06:24 <ais523> no
22:06:27 <AnMaster> huh
22:06:34 <ais523> at least, yes but I planned to in advance
22:06:36 <ais523> so that isn't really getting stuck
22:06:41 <AnMaster> har
22:07:34 <lament> nice topic
22:08:54 -!- almya has joined.
22:10:04 <alise> according to fax, pi = 2*((inf!!^4)/(inf!^2))
22:10:22 <alise> http://pastebin.tlhiv.org/MBFEx5L2 (send to latex previewer then click preview, popup)
22:10:25 <AnMaster> alise, inf!!?
22:10:33 <alise> The factorial of the factorial of infinity
22:10:37 <alise> *infinity.
22:10:47 <AnMaster> what does the factorial of infinity even mean?
22:10:53 <alise> Precisely!
22:10:56 <alise> What is it again fax?
22:11:53 <fax> double factorial of infinity = 2*4*6*8*10*...
22:11:55 <AnMaster> I know that there are series that goes on forever that makes up pi
22:11:58 <Sgeo_> Surely we can figure it out based on the equation
22:12:10 <AnMaster> fax, is that a common definition of it?
22:12:28 <AnMaster> I would have expected some product or sum sign or such for it
22:12:36 <AnMaster> to write it out I mean
22:13:06 <AnMaster> alise, what is that 2^inf though?
22:13:24 <AnMaster> 2*2*... forever?
22:13:35 <alise> ask fax
22:13:40 <AnMaster> and isn't that just infinity then
22:13:44 <alise> I don't pretend to understand his infinitarian musings
22:13:51 <AnMaster> (though common sense seldom works for infinity)
22:14:05 <fax> I am NOT an infinitarian!!!
22:14:22 * AnMaster googles "infinitarian"
22:14:29 <dixon> Which infinity?
22:14:50 <fax> infinity = 1+1+1+1+... = -1/2
22:14:50 <AnMaster> dixon, it just used to 90° rotated 8
22:14:53 <AnMaster> so hard to tell
22:14:59 <AnMaster> if it was aleph_0 or some other
22:15:57 <dixon> Mebbe he was talking about the cardinality of the continuum
22:16:52 <alise> <fax> infinity = 1+1+1+1+... = -1/2
22:17:02 <alise> so the infinite chain of successors
22:17:12 <alise> which is the only infinite natural - presuming we allow infinite nestings of constructors
22:17:18 <alise> which we must to have infinity
22:17:53 <almya> omg! a math chan!
22:18:01 <fax> almya where??
22:18:05 <alise> almya: programming actually... but
22:18:09 <almya> here
22:18:12 <almya> ok
22:18:14 <almya> lol
22:18:16 <alise> well esoteric programming
22:18:22 <alise> which is close enough to mathematics... when it's good, that is
22:19:01 <almya> there are esoteric programming theories ?
22:19:14 <oerjan> probably >_>
22:19:44 <pikhq> The theory of Brainfuck: every esolanger has developed at least one Brainfuck derivative.
22:19:44 <pikhq> :P
22:20:03 <oerjan> hm, _have_ i done that now
22:20:07 <almya> lol
22:20:16 * fax hasn't
22:20:21 * oerjan cannot recall, but it's so easy to do that he may have forgotten it
22:20:25 <fax> i have implemented barinfuck
22:20:51 <fax> I should make a brainfuck
22:20:52 <fax> now
22:21:58 <almya> is all that language agnostic ?
22:22:13 <lament> i have developed two :(
22:22:32 <pikhq> Indeed, we are language agnostic. We are in doubt but apathetic about the existence of languages.
22:22:58 * oerjan swats pikhq for stealing his joke -----###
22:22:58 -!- rapido has joined.
22:24:14 <rapido> is my language is esoteric?: http://www.enchiladacode.nl ... you decide
22:24:47 <fax> oerjan
22:25:18 <oerjan> rapido: looks far too well-developed to be esoteric :D
22:26:11 <pikhq> Far too usable.
22:26:14 <rapido> i think to most interesting esoteric languages are extremely well-developed to be different
22:26:17 * oerjan had this strange impression there was an enchilada language on the wiki
22:26:49 <rapido> pikhq: you insult me! - usable? - nah
22:27:02 <oerjan> but no
22:27:06 * pikhq shoves Befunge at you
22:27:06 <fax> rapido -- it doesn't look esoteric but I just glanced
22:28:27 <rapido> the esoteric bit is that it would be very difficult to compile enchilada to efficient machine code
22:28:48 <rapido> but i guess most esoteric languages have that property
22:29:11 <fax> aaahh!! so the product of all the prime numbers = 4pi^2
22:29:12 <rapido> may be not
22:29:31 <pikhq> rapido: Many languages are difficult to compile efficiently.
22:29:58 <oerjan> rapido: befunge has that as a design feature
22:30:02 <pikhq> Many commonly used languages cannot readily be compiled to machine code, for that matter.
22:30:10 <pikhq> ... Without including an eval function, that is.
22:30:45 <rapido> pikhq: enchilada's eval is always there - always
22:30:49 <AnMaster> <pikhq> The theory of Brainfuck: every esolanger has developed at least one Brainfuck derivative. <-- err actually I'm a counter example too
22:30:57 <oerjan> hm wait cpressey has burrito, maybe he has an enchilada too
22:31:10 <AnMaster> I have of course implemented brainfuck though
22:31:15 <oerjan> um burro not burrito
22:31:18 <alise> rapido: you're the enchilada creator?
22:31:26 <pikhq> rapido: BTW, what makes it difficult to compile efficiently?
22:31:27 <alise> huh
22:31:31 <alise> great to meet you rapido
22:31:38 <alise> your language is interesting and it sucks. :)
22:31:44 <alise> (The highest compliment I ever give to a language.)
22:31:46 <rapido> alise: thanks!
22:32:10 <rapido> pikhq: every unwritten term carries a hash
22:32:25 <rapido> code = data = hashed
22:32:30 <alise> rapido: May I comment? Making the correctness of your language depend on the infallibility of SHA-1 is unwise.
22:32:42 <alise> Especially as SHA-1, by definition, cannot satisfy what you ask of it: a distinct output for every distinct input.
22:32:47 <AnMaster> <alise> (The highest compliment I ever give to a language.) <-- really?
22:32:53 <alise> AnMaster: Yes.
22:32:54 <AnMaster> I think you praised your own ones more
22:32:55 <rapido> alise: SHA-1 is just one choice of hash
22:33:01 <alise> AnMaster: That's because I am infallible.
22:33:05 <alise> rapido: But it is true of every hash.
22:33:07 <AnMaster> alise, also feather
22:33:13 <AnMaster> (but ssh! ais523 is near)
22:33:15 <rapido> alise: is it?
22:33:20 <pikhq> rapido: Hashes, by definition, cannot satisfy what you ask of it.
22:33:27 <alise> If F is a hash function, then there exists (x,y) such that F(x) = F(y), /because/ the output domain of F is smaller than the input domain.
22:33:32 <alise> That is, after all, the purpose of a hash function.
22:33:35 <ais523> AnMaster: I love the way you can try to avoid attracting someone's opinion by nickpinging them
22:33:36 <rapido> what is the chance of your memory to fail or have a hash collision?
22:33:46 <rapido> not your memory of course ;)
22:34:00 <AnMaster> ais523, haha
22:34:28 <pikhq> rapido: Hashes are not unique.
22:34:36 <AnMaster> ais523, it was only a theatrical "avoid attraction"
22:34:39 <AnMaster> if you see what I mean
22:34:47 <pikhq> Relying on hashes being not unique is stupidity.
22:34:50 <alise> rapido: Well there's all sorts of "chance"; many hash functions have been broken.
22:34:53 <alise> It is only a matter of time.
22:35:08 <pikhq> (exception: perfect hash, where you know the input domain perfectly.)
22:35:10 <alise> rapido: Correctness doesn't care about the practical reality, though, because it is about mathematical properties.
22:35:36 <AnMaster> pikhq, indeed
22:35:48 <AnMaster> I used perfect hashes somewhere, forgot for what it was
22:35:54 <alise> AnMaster: cfunge i think.
22:36:01 <AnMaster> oh indeed you are right
22:36:03 <pikhq> Probably hash map of some sort.
22:36:08 <AnMaster> alise, but pretty sure I used it elsewhere too
22:36:17 <AnMaster> pikhq, gperf, to check if a keyword was in a list
22:36:25 <AnMaster> (in the cfunge case)
22:36:31 <pikhq> They're fairly common things to use when you can. ;)
22:36:46 <alise> rapido: I think Enchilada is certainly one of the most unique extant languages.
22:36:47 <AnMaster> the other case wasn't gperf iirc
22:36:49 <rapido> alise: i believe the reality is not correct - at least my computer fails me many more times than hash collisions which have probability  10 ^ -30 - depending on the hash function
22:37:04 <alise> rapido: Me and cpressey discussed one aspect of it recently, actually.
22:37:15 <alise> rapido: Go and look up how many hash functions have been broken.
22:37:25 <fax> I have some cat buiscuts
22:37:31 <alise> SHA-1 is not infallible, and the difficulty of generating collisions reduces every year.
22:37:38 <pikhq> Doesn't SHA1 have some known weaknesses?
22:37:46 <rapido> alise: forget about SHA1 - think about hashes
22:37:49 <alise> pikhq: Yes.
22:37:58 <alise> rapido: If we're being abstract we have to be formal too.
22:38:04 <pikhq> rapido: This is a problem with all hashes.
22:38:07 <ais523> I think it has no known /exploitable/ weaknesses, but the fact that weaknesses exist is making people suspicious
22:38:27 <alise> rapido: forall f:A->B, (card B < card A) -> exists x:A,y:A. f x = f y
22:38:30 <rapido> pikhq: i don't see it as a problem - i see it as a opportunity
22:38:32 <alise> This is a fact.
22:38:44 <pikhq> rapido: An opportunity... For security flaws.
22:38:48 <rapido> if you give a little you gain a lot
22:38:49 <pikhq> Or incorrect execution.
22:38:57 <pikhq> Your choice.
22:39:07 <rapido> pikhq: memory failure is also a possibility
22:39:15 <alise> rapido: pikhq is actually right about security: consider an Enchilada program comparing for equality to some secret value.
22:39:22 <alise> If you can create SHA-1 collisions, you can break this system.
22:39:25 <rapido> you need a physical platform - which is faulty
22:40:00 <alise> rapido: IMO that is an error similar to the one that claims that Turing-completeness of a language is impossible because no universal Turing machine can be constructed.
22:40:09 <pikhq> Yes, this is why things like hashes are useful to secure against this. However, relying on hashes causes greater issues.
22:41:00 <alise> rapido: Actually if we are considering physical things, why do you use hashes? Comparison is not slow.
22:41:18 <alise> Especially if you memoise the results so only the section of the tree not previously compared must be analysed.
22:41:30 <rapido> alise: try comparing two sets which are different in only one element
22:41:34 <alise> Well, I guess that involves comparison in itself.
22:41:42 <alise> rapido: How big are these sets?
22:41:46 <rapido> big
22:42:00 <rapido> let's do some O complexity
22:42:14 <rapido> two sets with size n and m
22:42:18 <pikhq> rapido: Depends heavily on the representation of the set, the location of the difference, and the comparison algorithm in use.
22:42:34 <alise> rapido: you are appealing to practical reasons
22:42:44 <alise> so specify n and m for the actual speed matters...
22:42:58 <rapido> sure it does - but what's the most efficient algorithm?
22:43:04 <alise> Does it matter?
22:43:05 <pikhq> It depends.
22:43:23 <alise> Oh, another criticism - and I'm not trying to sound whiny, just offering my opinions because the positive ones are boring - having every object have a sign is weird-ass.
22:43:32 <pikhq> Efficiency of an algorithm depends a lot on the input.
22:43:53 <rapido> alise: hey, i'm just being esoteric ;)
22:44:10 <pikhq> For instance: if your input is going to always be mostly-sorted, insertion sort is a pretty dang nice algorithm.
22:44:15 <alise> Well, you appear to have practical aims with your language to an extent; perhaps I am wrong.
22:44:30 <fax> why cant an esolang be practical too?
22:44:49 <oerjan> alise: now you are just being negative
22:44:56 <alise> oerjan: Oh ho ho ho
22:45:14 <fax> heh
22:45:19 <rapido> fax: Heresy!
22:45:20 <alise> rapido: Anyway, add dependent types and termination checking and I'll love it.
22:45:37 <alise> This rule is the only exception to the rule that the highest praise I give to any language is that it's interesting and it sucks.
22:45:42 <AnMaster> alise, would you love INTERCAL with dependant types?
22:46:01 * AnMaster prods ais523 about that idea
22:46:08 <alise> AnMaster: As I said, there are no other exceptions to the rule; so since I have stated the single exception, you can assume it applies in all cases the exception enumerates.
22:46:24 <alise> (I hear Enchilada doesn't have exceptions.)
22:46:37 <AnMaster> alise, you lost me there
22:46:39 <fax> Enchiladas don't have souls
22:46:45 <rapido> alise: no exceptions, yes baby!
22:46:56 <alise> rapido: But it has _|_, I presume?
22:47:02 <alise> There are computations that do not terminate?
22:47:23 <alise> Mathematically, this is equivalent to errors: It is the addition of an element _|_ to every type that you cannot check for.
22:47:26 <alise> It is just as insidious.
22:47:44 <rapido> no, it doesn't have bottom - everything terminates eventually
22:47:46 <oerjan> fax: lies! if they're filled with beans they do!
22:47:50 <fax> poor rapido having to listen to this :P
22:48:15 <alise> rapido: Well, that is good. I do hope you realise that this means it cannot be turing-complete.
22:48:21 <alise> So, wait, it is impossible to write cat(1)?
22:49:42 <AnMaster> try to be somewhat nicer to rapido
22:49:43 <rapido> alise: i have thought of this. what about doing something 10^100000 times?
22:49:47 <Sgeo_> It's impossible to surf the web in BF?
22:49:52 <alise> AnMaster: I am not being unkind.
22:49:56 <Sgeo_> [Note: It isn't impossible, given PSOX]
22:50:04 <Sgeo_> So analogy fail
22:50:04 <AnMaster> I agree that depending on hash is bad
22:50:10 <alise> Are you misinterpreting neutrality and my not offering trivial praises of its novelty (which I have already done) as hostility?
22:50:14 <AnMaster> Sgeo_, it is not relevant to TCness though
22:50:18 <alise> rapido: So, you are an ultrafinitist, then?
22:50:34 <alise> rapido: If something could never be computed it is not computable.
22:50:39 <alise> So sufficiently large numbers do not exist...
22:50:40 * Sgeo_ just likes mentioning PSOX around alise 
22:50:53 <AnMaster> Sgeo_, while non-terminating is related to TC
22:51:19 <rapido> alise: i like brouwer - the dutch mathematician
22:51:24 <pikhq> TC implies non-termination...
22:51:53 <alise> rapido: You are at least a constructivist then.
22:51:57 <Sgeo_> Would a language in which no program terminates be TC? I'd assume so, since it's easy to make a terminating program not terminate
22:52:30 <alise> But if you respond to a question about non-terminating programs with a question about programs that run for too long to be computed in this universe, then you are at least some form of finitist; I would say the ultra variety.
22:52:34 <alise> Sgeo_: Yes.
22:53:29 * AnMaster accepts non-constructive proofs btw
22:53:32 <fax> Sgeo I guess that you could maybe define 'termination' as something else
22:53:38 <rapido> let me try to explain my case
22:53:46 <fax> like when a particular switch is flicked.. even if other stuff is still happening
22:53:48 <rapido> let's say you have a long winding proof
22:54:00 <rapido> the proof will hold references to other proofs
22:54:27 <rapido> and those proofs will hold references to yet other proofs
22:54:49 <rapido> what is the chance of any reference to be faulty?
22:55:00 <Sgeo_> We should make a system in which cyclical proof references can exist.
22:55:06 <rapido> what can we do to lower that chance?
22:55:07 <pikhq> Sgeo_: Yes, you can implement "termination" as going into a busy-loop or some such.
22:55:30 <rapido> can we make a reference absolutely non-faulty - always?
22:55:34 <rapido> i don't believe so
22:55:41 <rapido> we can lower it
22:55:44 <alise> rapido: Eh?
22:55:48 <alise> You mean it references an incorrect proof?
22:55:57 <alise> Formal proof verification systems mean that the only point of infallibility is the axioms.
22:56:04 <Sgeo_> rapido, that's a problem of mathematicians being wrong, not a property of mathematics itself
22:56:06 <fax> or definitions :P
22:56:06 <alise> See metamath(.org), Coq, Mizar, ...
22:56:15 <rapido> alise: think of the reference itself
22:56:20 <fax> you could defined say 'prime' wrong.. so that every number is prime
22:56:24 <fax> and not realize
22:56:27 <alise> rapido: Define what a reference to a proof IS, as an actual object.
22:56:35 <alise> You seem to be positing some sort of mathematical universe of pointers to proofs.
22:57:10 <rapido> alise: i'm saying that you need pointers
22:57:16 <Sgeo_> Why?
22:57:20 <alise> rapido: This is false.
22:57:25 <rapido> alise: to scala
22:57:29 <rapido> scala <- scale
22:57:40 <alise> Define scale, and what has scaling got to do with abstract mathematics?
22:58:10 <rapido> doesn't abstract mathematics need pointers?
22:58:16 <alise> Nope?
22:58:24 <alise> At least I haven't found any in the axioms I've looked at recently.
22:58:27 <rapido> to refer to something? a word is a pointer
22:59:07 <Sgeo_> rapido, a reference to a proof is just um.. kind of included, I guess? More like a #define than an import?
22:59:12 * Sgeo_ is not sure if he's making sense
22:59:17 <alise> rapido: No, a name is just a placeholder.
22:59:25 <alise> You can replace it directly, rather than assigning it to anything.
22:59:56 <alise> (forall p, p -> (forall q, q -> p)) doesn't have any pointers; it has placeholders. By itself, it means nothing: not unless you know how to fill in the foralls.
23:00:02 <rapido> alise: but the name must be unique, not?
23:00:05 <alise> When you do, you replace them directly. There are no pointers, only symbol manipulation.
23:00:21 <rapido> otherwise the statement will be ambigious
23:00:31 <rapido> ambiguous
23:01:08 <alise> yes, and?
23:01:13 <rapido> come on - names refer to bigger things
23:01:23 <rapido> they compress the bigger things
23:01:40 <rapido> they are a poor-mans hash of the things they refer to
23:02:11 <rapido> the bigger things have names in them
23:02:19 -!- alise has left (?).
23:02:21 <rapido> they refer to other objects
23:02:24 -!- alise has joined.
23:02:32 <alise> rapido: I think that's rubbish.
23:02:37 <rapido> alise: ok
23:02:40 <alise> Symbolic notation is not compression.
23:02:55 <rapido> i think it's exactly that
23:03:03 <rapido> that's abstraction
23:03:07 <rapido> to compress
23:03:10 <oerjan> rapido: a name would only be a hash if it was derived entirely from the thing it named
23:03:11 <fax> heh you could hard code in something that ensures that every variable name you use, names some term which is larger
23:03:25 <alise> oerjan: precisely!
23:03:29 <alise> It's a placeholder, not a smaller form.
23:03:34 <rapido> oerjan: yes, that's why i like hashes better than names
23:03:35 <fax> ilke you couldn't define  sum = +/
23:03:40 <fax> it would be an error
23:03:40 <alise> In (p -> (q -> p)), we're really just defining a template for truths.
23:04:02 <oerjan> rapido: and it is also why hashes must have the possibility of collisions, but names need not
23:04:03 <alise> We're saying that: If we have a thing, and another thing, then the first thing implies that the second thing implies the first thing.
23:04:08 <alise> There is no compression.
23:04:12 <alise> brb.
23:05:22 <rapido> oerjan: names may not - but who will make sure the names don't clash?
23:05:35 <oerjan> rapido: the compiler/verifier
23:06:11 <rapido> oerjan: don't you agree that names compress the complex objects hat they refer to?
23:06:21 <rapido> hat <- that
23:06:54 <oerjan> rapido: now you are just shifting the meaning of a term, it won't help your actual argument any
23:06:59 <rapido> otherwise you would end up with pure value passing semantics - which is very inefficient
23:07:24 <rapido> oerjan: and what's my actual argument?
23:07:40 <oerjan> _whatever_ it is :D
23:07:55 <fax> hello
23:08:35 <oerjan> as in, whether the term "compression" includes names is uninteresting if it's just defined to do so
23:08:39 <rapido> fax: 'heh you could hard code in something that ensures that every variable name you use, names some term which is larger'
23:09:03 <rapido> fax: this would end up with names as big as the objects themselves
23:09:33 <Sgeo_> inefficient? When dealing with _shifting math around_?
23:09:34 <rapido> fax: just would rather have the objects - thank you very much
23:09:41 -!- cheater2 has changed nick to cheater.
23:10:06 <oerjan> rapido: i think you are reading fax backwards
23:10:25 * fax doesn't havea problem with that
23:11:03 <rapido> oerjan: that's right
23:11:16 <rapido> fax: it is an interesting thought - thanks!
23:12:14 -!- chromakode has joined.
23:12:28 <rapido> but i do still think names/pointers/links are meant to compress information - think of exact repetitions
23:12:50 -!- almya has left (?).
23:13:11 <rapido> you just say: hey i've got this object and a name it x
23:13:14 -!- rbradfor has joined.
23:13:20 -!- rbradfor has left (?).
23:13:29 <rapido> now i have this other object y, and it holds 4 x's
23:13:50 <rapido> and so forth
23:14:27 <rapido> but how are you going to name the 10^10000 object that holds other object names?
23:15:09 <rapido> names are important especially in a distributed setup where you can't have a central naming service
23:15:24 <rapido> who is giving out the names?
23:17:07 -!- MigoMipo has quit (Read error: Connection reset by peer).
23:19:37 <rapido> i will give myself a name, and a won't be a hash
23:20:31 <Sgeo_> rapido, to be clear, you're talking about computers, and not math, right?
23:20:56 <fax> I am a name not a number!
23:21:30 <rapido> Sgeo_: math is riddled with references and names that refer to complex abstractions
23:21:34 <lament> be quiet, 38
23:22:26 <rapido> Sgeo_: of course, you can always create the full proof down the axioms, without references
23:22:50 -!- chromakode has left (?).
23:23:40 <rapido> Sgeo_: 'math' doesn't difference from 'computers' - whatever that means
23:24:55 <rapido> you can never be certain
23:25:01 <alise> back
23:25:03 <rapido> even mathematical proofs aren't certain
23:25:06 <alise> rapido: sigh
23:25:07 <alise> yes they are
23:25:14 <alise> see proof verifiers
23:25:15 <rapido> you need faulty humans to falsify mathematical proofs
23:25:19 <alise> nope
23:25:22 <alise> you need computers
23:25:37 <alise> fax: correct him plz
23:25:44 <fax> who?
23:25:52 <Oranjer> me!
23:25:56 * Sgeo_ wonders if rapido might be pulling a fax.
23:25:59 <alise> rapido, saying that proofs aren't certain because you need humans to falsify them or something
23:26:09 <rapido> alise: but computers are faulty - the change of computers to faulty is much higher than hash collisions
23:26:26 <fax> Oranjer, you are so damn wrong it makes my head hurt. I have never haerd someone be so wrong, I can't beleive you are sreious forgoodness sake -- you gotta be kidding? The sad thing is I know you arent..
23:26:31 <rapido> change <-chance
23:26:35 <alise> rapido: except when computers go wrong - they don't say "Yes this is valid omg!"
23:26:38 <Sgeo_> fax, wrong person
23:26:43 <alise> they say "Segmentation fault"
23:26:51 <fax> Sgeo, you are so damn wrong it makes my head hurt. I have never haerd someone be so wrong, I can't beleive you are sreious forgoodness sake -- you gotta be kidding? The sad thing is I know you arent..
23:26:54 <rapido> fax: thanks for correcting me - thank you very much
23:26:59 <pikhq> alise: Or just say nothing, if you've got very bad luck.
23:27:03 <alise> he pinged Oranjer, rapido
23:27:05 <alise> not you!
23:27:09 <Oranjer> yeah!
23:27:13 <pikhq> But, it tends to be pretty clear when that happens.
23:27:16 <fax> rapido, what?
23:27:42 <pikhq> "This is putting out 5 instead of 6. WTF? Oh, it works in the debugger. Mmkay, Heisenbug."
23:28:02 <rapido> heisenbug! now you are talking my way!
23:28:22 <rapido> i like heisenbugs!
23:28:25 <rapido> they are great!
23:28:43 <pikhq> Hash collisions are not heisenbugs in your language. They are just *inexplicable* ones. ;)
23:28:57 <rapido> we should create a esoteric language called heisenbug!
23:29:40 <rapido> the default would be an heisenbug statement - with the remote exception of a correct statement
23:30:55 <rapido> if the heisenbug language proves to be turing complete - i'm done!
23:31:06 * oerjan notices no one seems to have named any actual insect after heisenberg
23:32:23 <fax> what is my role in all this?
23:33:00 <rapido> pikhq: just to make you shiver: 'corporate' storage depends on hashes (that may have collisions)
23:33:10 <oerjan> fax: you write this all down and send it as beeps over a phone line
23:33:55 <pikhq> rapido: Yes, hash tables are common.
23:33:56 <alise> rapido: You are mixing the practical and the theoretical, seemingly repeatedly.
23:33:59 <alise> Why?
23:34:00 <pikhq> They allow for collisions.
23:34:07 <alise> Some people believe them to be equal. Do yu
23:34:09 <alise> *you?
23:34:16 <alise> I'm merely curious as to how your justifications work...
23:34:47 <pikhq> (You hash the index, look in the table, and then compare against the proper index to find the proper item.)
23:34:47 <fax> alise hey
23:34:51 <fax> what was that earlier
23:34:59 <rapido> alise: i think theoretical abstractions need reality to be expressed.
23:35:03 <alise> What was what, fax?
23:35:08 <rapido> i do see the difference
23:35:11 <alise> pikhq: precisely, hash tables don't require collisions to break things :)
23:35:30 <pikhq> alise: Heheheh.
23:35:48 <alise> rapido: Then it is a philosophical disagreement we have, and having reached the bottom layer of where rationality works, we should abandon the discussion immediately. :)
23:36:25 <rapido> alise: i see that - no prob :)
23:36:41 <fax> alise you told me to correct something -- what?
23:36:44 <Ilari> Hmm... Esolang where programs consist of prime - 1 operations and next operation is selected by g(1+x) - 1 mod p (x + 1 mod p for branches).
23:36:53 <alise> fax: rapido :P
23:37:07 <alise> rapido: Well, I applaud your work on Enchilada and hope you'll visit here often.
23:37:21 <fax> yes butwhat did he say?
23:37:28 <rapido> fax: lol!
23:37:48 <rapido> fax: hey - at least i've made something runnable!
23:38:43 <alise> fax: that mathematical proofs were fallible
23:38:48 <alise> because "you need fallible humans to falsify them"
23:39:14 <fax> sounds like a word definition problem
23:39:15 <Sgeo_> Ilari, that sounds very familiar
23:39:53 <Ilari> "Nice" properties of that include that program flow totally changes if program space is enlarged.
23:40:00 <rapido> sound like the scientific approach - repeat and measure
23:40:07 <alise> Science is not mathematics.
23:40:18 <rapido> alise: again we disagree
23:40:21 <alise> Mathematics is the domain of the certain. Science is the domain of the uncertain, that which we must experiment on to determine.
23:40:39 <alise> Science is the art of building mathematical theories based on experiment.
23:41:10 <fax> alise I dont think I agree with that
23:41:15 <alise> rapido: Well, I think I have the evidence on my side. There are many mechanical proof checkers upon which a large part of mathematics has been formulated.
23:41:26 <alise> Saying that mathematics is uncertain is a bit silly in light of that.
23:41:29 <pikhq> Mathematics is the art of producing absolute certainties based upon other absolute certainties or absolute declarations.
23:41:39 <alise> You must be sure that your axioms are consistent.
23:41:43 <alise> Beyond that, you can be sure.
23:42:05 <fax> i don't really agree with you guys
23:42:21 <rapido> alise: your romance with math is before 1935
23:42:32 <alise> Ha!
23:42:43 <alise> What are you trying to say?
23:42:56 <Ilari> In space of size 6, the execution order goes: 1,3,2,6,4,5,1... In space of size 10 it goes: 1,2,4,8,5,10,9,7,3,6,1...
23:42:58 <Sgeo_> When was Godel doing his stuff?
23:43:13 <rapido> alise: that math is much to great and complex and interesting to be certain
23:43:15 <oerjan> Ilari: what's your g?
23:43:18 <alise> Sgeo_: '31
23:43:45 <Ilari> oerjan: First g with maximal order. 3 in first example, 2 in second.
23:43:56 <alise> rapido: I really do invite you to go up to any of the many people who have worked on proof checkers, proof assistants, and laboriously defined and proved things in these systems - and say that to them.
23:44:01 <rapido> alise: and that axioms are not enough - godel has proved that
23:44:06 <alise> You could start with the people who used a computer to prove the four-colour theorem.
23:44:17 <alise> "Axioms are not enough"? Godel says nothing of the sort.
23:44:18 <pikhq> No, he showed that axioms could not be shown to be consistent.
23:44:25 <alise> No he didn't.
23:44:34 <fax> rapido: btw I think most people here are post-godel
23:44:40 <pikhq> Erm. Could not within the axiomatic system, wasn't it?
23:44:53 <alise> He showed that a theory of at least the strength of Peano Arithmetic can be either two things:
23:45:03 <fax> rapido: of course it is a big factor
23:45:03 <rapido> sure - i'm more into popper <- an oldie also
23:45:10 <alise> Consistent, or have a proof of its own consistency inside itself.
23:45:17 <pikhq> Ah, right. That was it.
23:45:30 <alise> i.e. no consistent theory of sufficient strength contains a proof of its own consistency
23:45:38 <rapido> alise: that's one way of putting it
23:45:41 <alise> That's the second theorem.
23:45:51 <pikhq> ... That's what he... Said...
23:45:54 <alise> The first is that a theory at least as strong as PA can either be consistent or complete.
23:46:13 <oerjan> Ilari: i think you left out the +1 -1 bits in your examples.  although that may be a good thing.
23:46:28 <lament> your definition is inconsistent with the ones that are usually given
23:46:32 <rapido> alise: what i don't understand is that you allow proof checkers
23:46:47 <pikhq> rapido: What's to not understand?
23:46:49 <alise> rapido: Perhaps you do not understand what a proof checker is.
23:46:54 <rapido> why do you rely on faulty memory
23:47:04 <Ilari> oerjan: Of course branch jumps are pretty incompatible with general flow (but that's a "feature").
23:47:05 <rapido> alise: i perfectly understand.
23:47:06 <oerjan> Ilari: so, first primitive root
23:47:11 <alise> rapido: Your appeal to errors in memory to demonstrate that mathematics is uncertain is really poor.
23:47:15 <rapido> do you trust the compiler
23:47:16 <Ilari> oerjan: Yes.
23:47:27 <rapido> has the compiler been proved correctly?
23:47:32 <rapido> what about the processor?
23:47:34 <rapido> etc, etc
23:47:39 <pikhq> Your appeal to human fallibility to demonstrate that mathematics is uncertain is also very poor.
23:47:39 <alise> For one,  you can have RAM with so much error checking that it is physically impossible for it not to detect an error for the computation you are doing...
23:47:47 <alise> rapido: There is an article about this.
23:47:49 <pikhq> They are either correct or incorrect. This is certain.
23:47:50 <alise> Let me find it.
23:47:56 <alise> http://r6.ca/homework.html
23:47:58 <alise> There.
23:48:38 <fax> rapido - of course the main thing people are forgetting is there's so much more to mathematics than formal proof
23:48:51 <rapido> fax: very true
23:48:54 <dixon> (no there's not)
23:49:18 <rapido> alise: http://r6.ca/homework.html <- this i don't like
23:49:58 <alise> Specify this.
23:50:12 <fax> alise, he doesn't like URLs
23:50:16 <Sgeo_> It doesn't have www., therefore it's nonsensical
23:50:25 <Sgeo_> Darn it, fax is funnier
23:50:32 <Ilari> Hmm... Is there point where one couldn't branch. That would correspond to  gx = x + 1 mod p => (g-1)x = 1 mod p => x = (g-1)^-1 mod p. Since g > 1, g-1 > 0 and thus inverse exists...
23:50:39 * Sgeo_ goes back to feeling useless
23:50:50 <fax> Ilari, I couldn't understand the first sentence of that :(
23:53:20 <dixon> See, his first mistake is thinking he could be novel.
23:53:23 <oerjan> Ilari: x = g^(p-2) (mod p)
23:53:29 <oerjan> er wait
23:53:39 <oerjan> (g-1)^(p-2)
23:54:27 * Sgeo_ is a novel.
23:54:43 <rapido> alise: 'For one,  you can have RAM with so much error checking that it is physically impossible for it not to detect an error for the computation you are doing...'
23:55:27 <rapido> alise: for one, you can have hashes with so many bits that it is physically impossible not to detect an error for the computation you are doing...
23:55:43 -!- tombom has quit (Quit: Leaving).
23:55:55 <rapido> now i will stop moaning about hashes
23:56:04 <alise> rapido: no that's false
23:56:11 <alise> because if the output domain is smaller than the input - the definition of a hash
23:56:21 <alise> it is MATHEMATICALLY IMPOSSIBLE for it to do what you want...
23:56:29 <Sgeo_> alise, I think rapido is trying to make an analogy?
23:56:29 * oerjan has his laptop spontaneously quantum tunnel into a state where it thinks 2+2=5
23:56:40 <rapido> the checking bits of faulty ram is smaller than the ram
23:57:28 <rapido> you can't have absolutely perfect ram
23:57:45 <fax> MATHEMATICALLY IMPOSSIBLE -- the most kind of impossible there is
23:58:11 <fax> oerjan, I was reading this algebra book right
23:58:14 * Sgeo_ lossessly compresses everyone into a bit.
23:58:18 <fax> and they were saying: Lets solve some equation: ...
23:58:20 <rapido> fax: no, the most kind of impossible there is - is god
23:58:28 <dixon> Actually, you can have infinitely outputting hash functions.
23:58:33 <fax> and to 'solve it' they just invent a NEW number system... which has a new element in it... which solves the equation
23:58:35 <dixon> e.g., sponge constructions
23:58:37 <fax> it's cheating!
23:59:11 <fax> rapido oh you're another of the atheist people I guess -_-
23:59:12 <rapido> dixon: a sponge bob - another hero if mine!
23:59:24 <rapido> if <- of
23:59:29 <dixon> haha
23:59:36 <oerjan> fax: hm that's a bit rough.  it can be useful for some things, though.  (witness complex numbers.)
23:59:46 <Sgeo_> alise, what were your dictatorship plans? I think it's safe to discuss them now