00:02:53 <oklopol> but isn't the way board game players interact, taking turns to manipulate some state, game theoretical stuff
00:05:04 <alise> A|(B C) = (A|B) (A|C), obviously
00:05:15 <alise> but does A (B|C) = (A B)|(A C)?
00:05:23 <alise> where A B is common parts and A|B is combination
00:06:16 <oklopol> isn't the study of general properties of game trees an important part of game theory? at least the one book i've read talks about it a lot.
00:08:09 <alise> oklopol: winning theory could be your chance to include all the ridiculous ideas you've ever thought of into mathematics
00:08:23 <alise> so what's the symbol for A totally winning B?
00:08:31 <oklopol> i'm not sure how that maps to what category theory is to algebra though
00:08:42 <alise> Tw(A,B)? TW(A,B)? TwAB? A op B?
00:09:02 <oklopol> as always, A | B = A <==> A > B
00:10:43 <alise> but totally winning is about strategy
00:11:17 <alise> I think op is the best route as you know, operators are awesome and you can invent symbols for them
00:11:24 <oklopol> doesn't mean we should get too creative when defining the algebra of games
00:11:55 <alise> Circled > would be nice.
00:12:02 <oklopol> i'm not really following any of these conversations
00:12:03 <alise> Might confuse with just >, but isn't that a good thing?
00:16:34 -!- alise has quit (Ping timeout: 252 seconds).
00:19:16 -!- Oranjer has joined.
00:30:42 -!- alise has joined.
00:30:55 <alise> what did i miss since what i last said?
00:34:15 <Ilari> alise: < oklopol> yeah!
00:35:25 <oklopol> well also "02:17… Oranjer has joined #esoteric"
00:35:26 <oklopol> that's sort of relevant to what Oranjer said
00:36:16 <alise> what is it with chess ais, you give them a huge amount of time because you don't wanna feel pressure and they just sit about doing nothing
00:36:27 <alise> you're a computer. you don't panic. stop wasting my time
00:37:50 <lament> chess is too hard anyway
00:38:37 <alise> lament: i don't care, it's entertaining
00:38:47 -!- Ilari has quit (Ping timeout: 268 seconds).
00:38:58 <alise> oh I think i may just have set up the ai wrongly
00:39:01 <alise> it just sat there and ran out of time
00:39:06 <coppro> alise: AIs do use up time
00:39:22 <alise> coppro: yes but this one played fine with little time. also, as i said, it ended up not moving at all.
00:39:58 <Oranjer> how does it end up not moving
00:40:19 <oklopol> lament: yeah i never learned how knights move
00:40:31 * alise tries a different type of clock
00:40:33 <alise> Oranjer: by not moving in the allocated time
00:40:42 <Oranjer> I think they do the Kansas City Shuffle, oklopol
00:41:22 <oklopol> two steps this way and then one step this way oh and by the way YOU CAN FLY OVER OTHER PIECES, that's just insane
00:41:59 <lament> it's just a game after all
00:42:25 -!- cal153 has quit.
00:42:47 <Oranjer> Chess: the only playable Allegory of Islam
00:43:31 <oklopol> lament: your responses are really boring today, are you drunk on life?
00:44:00 <alise> Oranjer: you are way too postmodern
00:44:22 -!- Ilari has joined.
00:44:25 <Oranjer> Muhammed flys somewhere on a flying ass
00:49:24 -!- cal153 has joined.
00:57:20 -!- adu has joined.
01:00:10 -!- coppro has quit (Ping timeout: 245 seconds).
01:11:51 <alise> In which I play Chess extremely shittily:
01:11:52 <alise> 1. b4 c6 {+0.17/8} 2. Nc3 Nf6 {+0.31/9} 3. Na4 d6 {+0.21/9} 4. c4 g6 {+0.06/8} 5. d4 Be6 {+0.14/8} 6. c5 Na6 {+0.06/9} 7. d5 Nxd5 {+0.79/8} 8. b5 cxb5 {+1.70/10} 9. e4 Qa5+ {+1.61/10} 10. Bd2 Qxa4 {+1.71/11} 11. Qxa4 bxa4 {+1.98/10} 12. exd5 Bxd5 {+2.00/10} 13. a3 Nxc5 {+3.09/9} 14. Ba5 Nb3 {+3.00/9} 15. Rb1 Bg7 {+3.82/10} 16. Bc7 Rc8 {+5.19/10} 17. Ba5 Nxa5 {+5.87/10} 18. g4 Bxh1 {+10.37/10} 19. Nf3 Bxf3 {+13.43/11} 20. Be2 Bxe2
01:12:06 <alise> 23. Rb4 Rxa3 {+14.69/9} 24. Rb5 Rh3 {+14.96/8} 25. g5 a3 {+17.63/9} 26. f4 a2 {+22.11/9} 27. Rc5 bxc5 {+26.91/9} 28. f5 gxf5 {+27.85/9} 29. Ke1 Rxh2 {+79.98/28} 30. Kd1 a1=Q# {+79.99/28}
01:12:11 <alise> Admittedly a few mistakes were due to the mouse slipping.
01:12:27 <alise> That probably made the already ridiculous difference in skill vs the computer vastly worse
01:12:38 <alise> But hey, it was entertaining. I am awfully bad though.
01:13:48 <Oranjer> how does one read this notation
01:13:48 <lament> can the computer give an estimate of how much you sucked?
01:16:16 <alise> Oranjer: ignore the bits in {}s
01:16:23 <alise> and then just google chess move notation
01:16:38 <alise> lament: probably, but i don't feel like hating myself that badly
01:18:18 <fax> I love finite calculus
01:18:47 <alise> it isn't really very calculusy tbh :p
01:19:04 <fax> it blows my mind that the are so many stiking similarities with the real calculus
01:20:05 <lament> it blows my mind that this blows your mind
01:20:23 <lament> given that calculus is obviously the limit of finite calculus
01:20:31 <alise> well 1 is basically the infinitesimal of the integers :P
01:20:47 <oklopol> finite calculus isn't calculus on integers
01:21:09 <oklopol> i know you know, i just like saying it
01:21:22 <fax> it's not calculus on integers?
01:21:28 <fax> are you reading the same paper as me? :P
01:21:49 <oklopol> oh well it's calculus from integers
01:22:02 <oklopol> but the functions still go to R
01:22:11 <alise> fax: why not on booleans
01:22:12 <fax> mine are Z -> Z
01:22:17 <alise> boolean calculus, do it now
01:22:24 <fax> alise, I am actually reading George Booles paper on this right now
01:22:39 <alise> haha man I'm laughing too much at the idea of boolean calculus
01:23:00 <alise> fax: no you /must/ do it on Bool -> Bool where true : Bool, false : Bool and nothing else
01:23:03 <oklopol> well the reason the paper doesn't talk about Z -> R, i think, is that integers always sum to integers, so you can restrict it that way, unlike normal calculus
01:23:11 <alise> I guess I'm basically asking for calculus from naturals mod 2
01:23:34 -!- augur has quit (Ping timeout: 264 seconds).
01:24:01 <fax> well it could be Q -> Q also
01:24:03 <fax> but that's not as elegant
01:24:12 <alise> why are you talking
01:24:28 <fax> alise, it's your idea, you do it!
01:24:41 <alise> i don't have a cock compiler
01:24:50 <alise> just s/Z/Bool/ in your code, job done
01:24:56 <fax> um :P that wont do it
01:25:02 <oklopol> i think it's very elegant from Z to R
01:25:06 <fax> hey I just realized Bool is a field
01:25:27 <fax> oklopol, why is Z -> R better than Z -> Z?
01:26:11 <alise> true/false = undefined
01:26:17 <alise> that's one fucking awesome field xD
01:26:19 <fax> "= undefined" *barf*
01:26:26 <alise> as in "is undefined"
01:26:27 <oklopol> because if we consider Z a measure space with cardinality as the measure, then sums are just integrals
01:26:29 <alise> false/true = false
01:26:32 <alise> false/false is undefined
01:26:41 <oklopol> and with integration we usually have functions from our measure space to R.
01:26:42 <alise> so basically X/true = X anything else is undefined
01:27:04 <fax> oklopol, wait what
01:27:07 <alise> so the multiplicative inverse is
01:27:31 <fax> oklopol, ooh I wonder if there's a Z[i] calculus with all the nice harmonic, holomorphic stuff
01:27:31 <alise> then again multiplication is boring on booleans anyway
01:27:38 <alise> multiplication is division on booleans
01:27:49 <alise> except for half of it (/false) >_<
01:27:53 <fax> alise, unitary calculus!!
01:28:02 <oklopol> fax: the crazy dude's paper talked about discrete analytic functions
01:28:06 <alise> for all the cases where / is defined on bools it is identical to *
01:28:15 <fax> 01:27 < alise> for all the cases where / is defined on bools it is identical to *
01:28:24 <alise> oklopol: if you're using his notation you say R but you mean hZ_p
01:28:29 <alise> (where Z is a finite set)
01:28:37 <alise> do not pervert /our/ discourse :P
01:28:52 <alise> tbh addition on booleans is pretty nice, being xor
01:29:18 <alise> true - true = false; true - false = true; false - true = true; false - false = false;
01:29:23 <fax> this is the best discovery I have made :))))))
01:29:28 <fax> finding this finite calculus
01:29:36 <alise> dude it's just some addition and subtraction
01:30:48 <alise> hey fax DID YOU KNOW you also have exponentiation on booleans
01:30:54 <alise> x^true = x; otherwise undefined
01:31:04 <alise> in fact, you can even use the ackermann function on them.
01:31:07 <oklopol> it's clear sums are integrals because every function is simple
01:31:07 <oklopol> from Z, with the usual measure
01:31:07 <oklopol> that's bullshit, let me gather myself.
01:31:09 <oklopol> okay maybe it's not completely obvious
01:31:11 <fax> "Vladimir Arnold forcefully stated in one of his books that it is wrong to think about finite difference equations as approximations of differential equations. It is the differential equation which approximates finite difference laws of physics"
01:31:12 <alise> now you have INFINITE OPERATORS!!!!!!!!!
01:31:39 <alise> so fax is now the fifth ultrafinitist i gather
01:35:20 <fax> this pleases me
01:35:30 <alise> fax: I'll love you if you make a Coq module with ultrafinitist definitions of the following, paramaterised on the rational h and the prime p: Naturals, so that there is no prime greater than p; Integers, presumably with each half of the integers dedicated to a sign; Rationals, divided once more (h must fit into one of these); and Reals, defined as hZ_p.
01:35:48 <alise> Along with associated operations, the calculus he defines, and properties.
01:35:51 <fax> alise, I will help you do it :)
01:35:54 <alise> And by love you, I mean hate you love you.
01:36:06 <alise> fax: Well... I started writing it in my language but couldn't be bothered.
01:36:10 <fax> alise, I should implement (normal) construtive reals though
01:36:30 <fax> following the sketch in my constructie functional analysis text
01:37:07 <alise> Sigma (f:Q+->Q), Forall (e1,e2:Q+), abs (f e1 - f e2) <= e1 + e2
01:37:19 <alise> fax: now do it, ultrafinitistic peon
01:39:53 <alise> fax: Actually I suppose that all those sets don't neccessarily have to have the same size because they all coexist.
01:40:19 <alise> So having the integers be twice the size of the naturals (minus 1, because there's only one 0...) and having rationals be the size of the naturals plus the integers would be OK.
01:40:31 <alise> The reals have to be hZ_p by Order of Zeilberger.
01:42:30 <alise> The nice thing is that we don't need any pesky functions or anything to define these because there's a simple, finite number of cases.
01:46:53 <fax> p would be what? The largest known* mersenne prime (* known by http://coqprime.gforge.inria.fr/ )
01:47:10 <alise> p and h are parameters to the module
01:47:43 <alise> they are universal constants like physical ones but we don't know what they are (zeilberger says that the True Value either p or h - i forget which - is unknowable so uh whatever)
01:47:50 <alise> so we just plug in values we like.
01:48:10 -!- augur has joined.
01:48:22 <uorygl> Time for a nick change.
01:48:39 -!- uorygl has changed nick to uorygl[hireMe].
01:48:45 <alise> fax: if you have an awful lot of cpu time on your hands the largest mersenne prime would be a good choice for p, yes.
01:49:03 <alise> h would be the result of pressing 0., holding down 0 for a long while, then pressing 1, probably.
01:49:23 <fax> shouldn't h come from a physical/science experiment
01:49:28 <fax> like the fine structure constant or something
01:49:43 <alise> Zeilberger claims they are separate to physical constraints and that he is a platonist.
01:50:01 <alise> Since we are following his school of ultrafinitism, not the usual physical-constraints one, that is not required.
01:50:14 <alise> 1/p is a good value for h if you have that in your system.
01:50:30 <alise> p is a natural and rationals = size of naturals + size of integers, so
01:50:36 <alise> 1/p should always be acceptable
01:50:42 <alise> uorygl[hireMe]: Z is the integers
01:50:57 <alise> Zeilberger, an ultrafinitist that believes no infinite sets exist, defines the reals as hZ_p
01:51:06 <alise> where h is a very, very small number
01:51:09 <alise> and p is a very, very large prime
01:51:24 <fax> 01:50 < uorygl[hireMe]> That explains so much.
01:51:50 <alise> It means hZ_p. :-P
01:52:23 <uorygl[hireMe]> Or, if it is a definition, then your mom is a perfectly good model of hZ_p.
01:53:37 <fax> Z_p = Z/Zp I guess?
01:53:49 <fax> Galois field
01:54:13 <fax> F_p = Z/pZ
01:54:27 <fax> h is the fundamental mesh constant, it's smaller than 1
01:54:42 <fax> so hZ_p = {...-h,0,h,2h,3h,...}
01:54:56 <alise> h: It's Smaller Than One.
01:56:20 <fax> alise you should make slogans
01:56:22 <alise> so if h is the fundamental mesh constant, what's the cool name for p
01:56:39 <fax> uorygl this is my interpretation, but I am by no mean an expert on this
01:57:41 <oklopol> it doesn't actually do anything
01:57:42 <alise> Hmm, ultrafinitists don't even let you have a type of types.
01:57:54 <alise> After all, it's infinite.
01:58:00 <alise> Unless you have a finite number of sets, which would be cool.
01:58:03 <alise> oklopol: what doesn't?
02:00:01 <alise> I guess the best thing is to have the integers be of size p.
02:00:43 <alise> Which means that the naturals are of size (p+1)/2.
02:01:05 <alise> So the rationals are of size p+((p+1)/2).
02:01:11 <uorygl[hireMe]> I know of... not many systems under which that's possible.
02:01:12 <alise> uorygl[hireMe]: Anything?
02:01:43 <alise> But Set is still infinite.
02:02:08 <alise> So, the reals have the same size as the integers.
02:02:16 <alise> Which means that the reals are smaller than the rationals.
02:02:23 <alise> This Makes No Sense (not that ultrafinitism does); start over.
02:02:41 <alise> The naturals are of size (p+1)/2.
02:02:44 <alise> The integers are of size p.
02:02:52 <alise> The rationals are of size p.
02:03:06 <alise> Half negative, half positive.
02:03:26 <uorygl[hireMe]> Here's some ultrafinitism for you: take ZFC, remove the axiom of infinity, add an axiom of non-infinity.
02:03:52 <alise> fax: i don't know coq man I can't do this :(
02:06:34 <fax> alise, (p-1)/2 is valid Coq
02:09:13 <alise> the size of the integers must be prime
02:09:41 <fax> that would make integers a field - weird
02:10:01 <alise> isn't that awesome not weird :)
02:10:14 <alise> see these are the possibilities ultrafinitism gives you dude
02:10:28 <fax> lol I will ttyl
02:10:37 <fax> I have to go
02:10:52 * Sgeo should have gotten an F on his history exam. Instead, I got a B+
02:11:27 <fax> 1234567890123456789012353 is a prime number
02:19:01 <alise> Things about the rationals: 1/p is a rational.
02:19:14 <alise> So, for every integer, there are p elements in the rationals for it.
02:19:26 <alise> p is the maximum size of a set. So, the rationals suck.
02:19:30 <alise> So, I must sacrifice something.
02:19:34 -!- Asztal has quit (Ping timeout: 265 seconds).
02:21:23 -!- fax has quit (Quit: 1234567890123456789012353).
02:38:14 -!- coppro has joined.
02:42:44 <alise> It would be interesting to see how varied an ultrafinitist system is.
02:42:45 <alise> My bet: Not at all.
02:47:07 -!- oklopol has quit (Ping timeout: 265 seconds).
03:15:37 -!- uorygl[hireMe] has changed nick to uorygl.
03:16:01 <adu> what language lends itself to reflection the most?
03:16:56 -!- alise has quit (Quit: Page closed).
03:16:58 <adu> not that kind of reflectiong
03:26:01 -!- werdan7 has quit (*.net *.split).
03:26:02 -!- rodgort has quit (*.net *.split).
03:26:02 -!- ttm has quit (*.net *.split).
03:28:24 -!- ttm has joined.
03:28:35 <uorygl> Or whatever that's called.
03:29:03 -!- rodgort has joined.
03:40:39 -!- werdan7 has joined.
03:50:57 -!- Gracenotes has joined.
04:13:45 <Sgeo> Gah, I'm so unclear sometimes.
04:17:52 <uorygl> I'm tempted to throw neutrons at you.
04:18:02 <uorygl> But that wouldn't really help.
04:18:29 -!- jcp has quit (Ping timeout: 260 seconds).
04:43:28 -!- coppro has quit (Read error: Operation timed out).
04:59:52 -!- coppro has joined.
05:08:13 -!- coppro has quit (Ping timeout: 276 seconds).
05:24:30 <Gregor> Hm, smeta.na is available for the low low price of $4,000/yr
05:25:38 -!- coppro has joined.
05:34:19 -!- Oranjer has left (?).
05:39:42 * Sgeo is half tempted to use PSOX with Scheme
05:40:41 * Gregor three-quarters tempted to mock Sgeo's use of fractional temptation.
06:09:36 -!- skeeto has joined.
06:10:55 <skeeto> is it possible to write the identity function in Fractran? I don't think it's possible.
06:23:05 -!- skeeto has left (?).
06:33:24 <uorygl> So, what does PSOX look like?
06:33:50 <Gregor> One can only ... /experience/ PSOX.
06:33:56 * Sgeo decides that uorygl has been living in a bubble since the end of 2007
06:33:59 <uorygl> Does it provide the Unix standard library?
06:34:11 <uorygl> I don't think PSOX is famous.
06:34:33 <Sgeo> It is infamous in these parts
06:35:11 <Sgeo> It gives alise aneurysms
06:35:35 <uorygl> If it gives alise aneurysms, I'm almost bound to probably be slightly irritated by it.
06:45:05 -!- FireFly has joined.
06:49:15 -!- oerjan has joined.
06:56:10 <pikhq> Sgeo: Isn't PSOX about as well-maintained as PEBBLE these days?
06:56:27 <Sgeo> pikhq, if PEBBLE was abandoned, yes
06:56:45 <pikhq> I've not touched it since, oh, 2007.
06:56:49 <Sgeo> If people start showing interest, I may regain interest in maintaining PSOX
07:00:06 -!- kar8nga has joined.
07:06:43 -!- tombom has joined.
07:29:32 -!- oerjan has quit (Quit: leaving).
07:39:42 * Sgeo goes to try Smalltalk
07:51:44 -!- tombom has quit (Quit: Leaving).
07:52:53 -!- cheater2 has quit (Ping timeout: 246 seconds).
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:02:50 -!- cheater2 has joined.
08:13:19 -!- FireFly has quit (Quit: Leaving).
08:15:54 -!- cheater3 has joined.
08:17:55 -!- coppro has quit (Quit: I am leaving. You are about to explode.).
08:19:53 -!- cheater2 has quit (Ping timeout: 256 seconds).
08:20:29 -!- zeotrope has quit (Ping timeout: 256 seconds).
08:21:04 -!- zeotrope has joined.
08:32:21 -!- OxE6 has quit (Ping timeout: 260 seconds).
08:33:24 -!- adu has quit (Quit: adu).
08:36:59 -!- adu has joined.
08:38:20 -!- MU has joined.
08:38:29 -!- MU has left (?).
08:52:01 -!- MizardX has joined.
09:15:03 -!- lament has quit (Ping timeout: 240 seconds).
09:15:10 -!- lament has joined.
10:16:32 -!- kar8nga has quit (Remote host closed the connection).
10:23:36 -!- oklopol has joined.
10:44:28 <oklopol> do the types by any chance form a quasigroup in your a/b b\a type thingie?
10:46:21 <augur> no no, dont take it as anything
10:46:26 <augur> i dont know what you're asking
10:46:48 <oklopol> linguistics thing you tried to teach me and someone else and he was like whaaaaaa
10:47:08 <oklopol> and you were like okay this is going nowhere i'm gonna go do something otherthing.
10:47:32 <augur> lecomte and retore's minimalism
10:47:34 <oklopol> it was about semiconflabulent grammars
10:48:00 <augur> i dont know if the types for a well defined structure. i doubt it
10:49:31 <oklopol> hmm minimalism has (a/b)*b = a, but does it have (a*b)/b? i guess that makes no sense
10:50:07 <augur> well, * is an operation on lexical items that bear types
10:50:17 <oklopol> i just noticed a similarity when reading about quasigroups, but i haven't actually given it any thought
10:50:21 <augur> not a type constructor
10:50:33 <oklopol> so a*b isn't even defined in general
10:50:44 <oklopol> therefore it can't form an algebra
10:50:47 <augur> its just not a type constructor
10:50:57 <augur> look at it like this
10:50:58 <oklopol> but is it defined no matter what the types of a and b are
10:51:12 <augur> but / is a type constructor
10:51:29 <augur> so you cant do (a*b)/c
10:51:33 <augur> why? because a*b is not a type
10:51:43 <augur> so you cant use / on it
10:51:58 <augur> think of it like haskell
10:52:04 <augur> a -> b is a type in haskell
10:52:11 <augur> a + b is not a type
10:52:17 <augur> so you cant have some type
10:52:51 <oklopol> so i can't really say (A/B)*B = A either, i can say c*d : B if c : (A/B) and d : B?
10:53:33 <augur> pretty but. i mean, (A/B)*B would be seen as just an operation over the type objects
10:53:42 <augur> its just not a type constructor
10:53:52 <augur> its an operation on types.
10:54:11 <oklopol> but as an operation over type objects, isn't it partial?
10:55:01 <oklopol> say we just have the types A and B, how can A*B be defined if * isn't a type constructor
10:55:37 <oklopol> also how can it be defined on the objects or whatever, if a : A, b : B, what's the type of a*b?
10:56:53 <augur> it is indeed partial
10:57:31 <augur> A*B is undefined. only A/B * B and B * A\B are defined
10:57:43 <augur> for all types A and B
10:57:47 <oklopol> okay, so they do form an algebra, but it's partial
10:57:54 <oklopol> therefore it clearly can't be a quasigroup
10:57:55 <augur> its just function application dude
10:58:11 <augur> its literally beta reduction
10:58:17 <augur> on types instead of functions
10:58:27 <augur> and the types are directional
10:59:02 <oklopol> what's the difference between type constructors and type operators? both are operators that take types to other types
10:59:15 <oklopol> constructors are used to define the universe of types, yes, but i don't see how that's relevant
10:59:34 <oklopol> i probably shouldn't be looking at this quite this algebraically.
10:59:38 <augur> sure but a type constructor is, at least in this case, and i think in all cases, total
11:00:07 <augur> * : (T x T) x T -> T
11:01:14 <augur> theres also the tensor product thing that they had tho fight
11:01:27 <augur> they had a second type constructor, x
11:01:30 <oklopol> so (T, /, \) forms an algebra, but it doesn't really have any structure... so i guess you should just think of those as type constructors instead of an algebra
11:01:41 <augur> well, it DOES have structure
11:01:45 <augur> its just not a well known one
11:02:08 <augur> or rather, its not an interesting one
11:02:43 <augur> if you did math, for instance, + or * over the integers has all sorts of fun properties
11:02:49 <oklopol> well right, that's what i meant, it's the free algebra on two binary operations, sort of
11:02:51 <augur> like, sometimes you can get back what you gave it
11:02:58 <augur> or you can go in circles
11:03:13 <augur> / and \ are not like that
11:03:47 <augur> which is to say, there are finite subsets of Z which are closed under + or *
11:04:03 <augur> there is no subset of T that is closed under / or \
11:04:13 <augur> T as a whole is closed, but no subset of it is
11:04:35 <oklopol> the subalgebra generated by A/B is a subset
11:04:59 <augur> sorry, no finite subset
11:05:33 <oklopol> but it's freeness that's the point
11:05:39 <augur> but there ARE finite subsets of Z which are closed under *, lets say
11:06:06 <oklopol> why are you telling me this?
11:06:21 <oklopol> oh well i guess that's allowed
11:06:25 <augur> the structure of Z under + or * is more interesting than \ and /
11:06:40 <augur> simply because you can get substructures that are interesting like this
11:08:11 <augur> you can do all sorts of fun stuff with * and + that you cant do with / and \ simply because / and \ are, you might say, information preserving
11:08:26 <oklopol> yeah, you might even say it's free.
11:08:45 <augur> the result of addition is not something that has a uniquely identifiable origin
11:08:56 <augur> 1 + 1 = 0 + 2 = -1 + 3 = ...
11:09:19 <augur> but A/B is just A/B. theres only one way to get A/B.
11:10:15 -!- Slereah has quit (Ping timeout: 240 seconds).
11:10:27 -!- comex has quit (Ping timeout: 276 seconds).
11:10:35 <oklopol> i don't really know the exact definition of freeness, but that's exactly what i mean by free in the case of an algebra that doesn't have any sort of identities.
11:11:43 <oklopol> there's a base and there's only one way to get everything from it. in the case of no identities, we have the stronger thing that every individual operation is completely reversible
11:12:57 <augur> if you let * be a type operator (which it technically isnt; it operators on things _with_ types, but we can pretend it can operate on just types for convenience)
11:13:15 <augur> then you get \ / and * forming some sort of "non-free" object, as you might say
11:13:18 <oklopol> identities being where the structure comes from, in the free monoid we can still have ab*c = a*bc even though it's free, where {a,b,c} is the base, because we have an identity that makes them the same, but if the operation satisfies no identities, then it's fully information preserving
11:13:52 <oklopol> they form a partial algebra, if that's the term
11:14:06 <augur> e.g. (A/B * B)/B, ((A/B)/B)*B, etc.
11:14:32 <oklopol> might still be free though
11:14:49 <augur> maybe. im just saying that there you now get the non-uniqueness of histories.
11:15:50 <oklopol> i'm actually literally atm reading a book that would completely explain the role of identities in universal algebra, if i just read like 20 pages ahead
11:16:13 -!- Slereah has joined.
11:20:40 -!- cal153 has quit (Ping timeout: 276 seconds).
11:22:02 <oklopol> (which also might be why i'm obsessing about the algebraic side of these things)
11:27:07 -!- cal153 has joined.
11:50:50 -!- cal153 has quit (Ping timeout: 248 seconds).
11:54:39 -!- cal153 has joined.
12:32:09 -!- fax has joined.
12:36:12 -!- alise has joined.
12:43:23 -!- oklopol has quit (Ping timeout: 245 seconds).
12:50:24 <alise> Gregor: I finished sibeli.us
12:50:43 <alise> Your score: 175822 / Points possible: 660500 / Grade: 26% (F)
12:50:50 <alise> I couldn't go any swbps because of my kb matrix
12:52:40 <alise> augur: + /is/ an operation on types tyvm
12:52:40 <alise> it's (Either a b) in haskell syntax
12:53:14 <alise> a*b (same thing as cartesian product) = (a,b)
13:02:13 <augur> alise: oh, well ok. :P
13:02:30 <augur> i meant + as integer addition tho
13:04:22 -!- alise has quit (Ping timeout: 252 seconds).
13:04:36 -!- alise has joined.
13:04:42 <fizzie> Your score: 480612; Points possible: 660500; Grade: 72% (C-); this could do swbp (1234) most of the time, though I got some key-jammery there somewhere. I have to wonder if it would've been easier with the music, though.
13:05:20 <Deewiant> Your score: 380183 Points possible: 660500 Grade: 57% (F)
13:05:33 <Deewiant> 1234 would have worked too? That'd have made it easier
13:05:47 <fizzie> "Use the keys '1', '2', '3' and '4' (or 's', 'w', 'b' and 'p') for strings, woodwinds, brass and percussion."
13:05:52 <fizzie> That's what it says on the front page.
13:06:04 <Deewiant> I just pressed "play" without reading the instructions.
13:06:14 <fizzie> Sounds exactly like the sort of thing you'd do!
13:06:53 <Deewiant> swbp is highly inconvenient on Colemak; all left hand and in 2143 order
13:06:54 <alise> Deewiant loses at something!
13:07:41 <alise> But yeah, I started thinking ohh this is easy
13:07:41 <alise> And then it was all, like, SSSWSWSWISBWndhFoiDSJpKAFPAJDOIHWDSOIWJD
13:08:04 <Deewiant> I dreaded the fast bits from the start :-P
13:08:05 <alise> fizzie: It's worse with the music, trust me
13:08:22 <fizzie> With a 100+-key keyboard, though, shouldn't you be controlling just about every instrument?
13:09:24 <alise> Deewiant: I've heard the whole thing like... once before
13:09:54 <alise> So a couple of times I thought "thank god, it's over" and then more shit popped up
13:10:44 <fizzie> Being .fi, it's sort-of required reading, I think.
13:11:34 <alise> You Finlanders suck :P
13:12:21 <fizzie> Deewiant: More automatic tweetery, though this is a bit Finnish-only: [2010-03-10 14:53:19] Tweeted: verikissanhiekka valtaa kanavia internetissä / akuutti rautaneito kuin laiteristiriita / laiminlyöty ja kukertava (runogen)
13:13:40 <fizzie> It's automagical poetry-generation; a rather old (10 years?) bit of code that I was suggested to make auto-tweet too.
13:15:57 <Deewiant> 1234 was a lot more comfortable if not easier: Your score: 418757 Points possible: 660500 Grade: 63% (D)
13:16:12 <fizzie> alise: I don't think my poetic skills are up to a faithful translation, but if you want a mostly literal one... "blood-cat-litter takes over channels on the Internet / the acute iron maiden like a device conflict / neglected and colorful".
13:16:25 <fizzie> Though "colorful" is a crappy word for "kukertava"; I don't really know what it should be.
13:16:48 <fizzie> Wiktionary's entry -- http://en.wiktionary.org/wiki/kukertaa#Finnish -- lacks a definition.
13:18:29 <fizzie> I'm not sure. Perhaps, though the connection to actual flowers is (at least to me) less there.
13:18:39 <fizzie> 1. flowery -- (of or relating to or suggestive of flowers; "a flowery hat"; "flowery wine")
13:18:39 <fizzie> 2. flowery, ornate -- (marked by elaborate rhetoric and elaborated with decorative details; "a flowery speech"; "ornate rhetoric taught out of the rule of Plato"-John Milton)
13:19:07 <fizzie> It's not sense #2, but it's maybe not exactly sense #1 either.
13:19:45 <fizzie> Interwebs say: "It's a Finnish word for a colour that isn't of any particular colour, I think."
13:20:21 <Deewiant> Weird-ass word; to me it suggests flowers
13:20:50 <fizzie> Deewiant: Here's one poem I created earlier: "saatanan aarre ei ole valopuu / humanistien aurinko ymmärtää antaa kuin ruoska / kaipaus ei ole käytävä eikä brainfuck"
13:20:51 <Deewiant> But evidently that's not what it means
13:21:21 -!- kar8nga has joined.
13:22:10 <fizzie> alise: "The treasure of Satan is not a light-tree / the sun of humanists knows to put out like a whip / longing is not a corridor, nor brainfuck".
13:22:31 <fizzie> "ymmärtää antaa" is another a bit difficult one.
13:22:34 <Deewiant> fizzie: I'd've said "insinuates"
13:23:07 <fizzie> Deewiant: But that's "antaa ymmärtää", isn't it?
13:23:23 <Deewiant> Yes, but with poetic license you can write it the other way around.
13:23:39 <fizzie> Oh, but it's not that, in fact; that thing there in the poem is the other half from the saying "antaa ymmärtää, muttei ymmärrä antaa".
13:23:39 <Deewiant> I don't know, that just made more sense to me.
13:24:10 <fizzie> The translation used the "6. put out -- (be sexually active; "She is supposed to put out")" sense of "put out".
13:24:10 <Deewiant> Then I'd just say "understands to give"
13:24:25 <Deewiant> And to me, that wasn't implied :-P
13:25:13 <fizzie> Well, you'd have to know the guy whose irc behaviour was used as a model when constructing that particular wordlist. :p
13:25:14 <alise> those would make goodterrible lyrics
13:25:14 <alise> for a goodterribleterrible song
13:26:19 <fizzie> Deewiant: "ymmärtää antaa" is only in the "naula" wordset, c.f. http://www.pelulamu.net/naula/
13:26:45 <Deewiant> I learned long ago not to visit pelulamu.net
13:27:40 <fizzie> Anyway, that generator is a handcrafted CFG, mostly not by me; there's four wordsets ("poetic", "gothy", "funny" and "naula") you can tell it to use.
13:28:01 <fizzie> If you do "-w goth", you get out stuff like: "sinä olet pääkallo / risti kylpee veressä / pikkutyttö kylpee veressä tulvillaan kipua sydänyöllä"
13:28:50 <Deewiant> Do you have this available? I could put this in /etc/profile.d
13:29:43 <fizzie> Deewiant: Sowwy, but there's only a binary-only version available; I'm supposed to clean up the code before release; have been for the last ten years.
13:29:49 <fizzie> Deewiant: http://maija.irtie.org/runogen/ anyway.
13:30:23 <alise> specially as i'm going in ... 20 seconds?
13:30:23 <alise> but srsly what's pelulamu.net
13:30:23 <alise> like finnish rotten.com or sth?
13:30:28 <fizzie> alise: Well, the gothy one is approximately "you are a skull / a cross bathes in blood / a little girl bathes in blood full of pain at midnight".
13:30:45 <Deewiant> fizzie: Can you hook me up with a 64-bit binary?
13:30:54 <fizzie> Deewiant: Um, sure, I guess.
13:31:15 <fizzie> Deewiant: Don't you have any 32-bit compatibility libs, though?-)
13:31:26 -!- alise_ has joined.
13:31:28 <Deewiant> I have a 32-bit chroot, which I'd rather avoid when possible
13:31:32 <alise_> what was said since um sure i guess
13:31:48 <Deewiant> Three lines that are available in the tunes.org clog log
13:32:05 <alise_> well as i'm leaving right now
13:32:16 <fizzie> Deewiant: It also generates the output in iso-8859-1; is that a problem, or can you pipe it through iconv or something manually?
13:32:48 <Deewiant> Presumably something iconv-like is no problem
13:33:40 <fizzie> http://zem.fi/~fis/runogen in that case -- the server will send it as text/plain, unfortunately.
13:34:45 <Deewiant> It seems something between the program and my screen even automatically understands the 8-bittiness
13:35:10 -!- alise has quit (Ping timeout: 252 seconds).
13:37:00 -!- alise_ has quit (Ping timeout: 252 seconds).
13:37:10 <fizzie> Yes, it's a bit strange; the output looked just fine in rxvt-unicode when I ran it directly, but when I had the Python script print it out, it came up as the missing-character ? signs. I guess Python might do something there, though I was under the impression that if I just used os.popen and read() to get a 'str'-type 8-bit string and then print that, it shouldn't go and alter the bytes.
13:37:32 <fizzie> Though I had to manually utf-8ify it anyway for Twitter posting.
13:38:52 <fizzie> Unless I'm mistaken, there was also one undocumented (by -h) command line option, though I can't remember what it did.
13:39:32 <fizzie> Using "-v -v -v" will give you some printouts of the rule-parsing at least. :p
13:41:13 <fizzie> Written in very ugly C.
13:41:20 <fizzie> That's the main reason there's only binaries.
13:41:35 <fizzie> Gah, that thing's written in 2002; I'm ashamed of myself.
13:42:55 <fizzie> Deewiant: Here's a representative snippet of code quality: http://pastebin.com/XvpEJHVv
13:43:25 <fizzie> Maybe I'm overly critical.
13:46:09 <fizzie> Deewiant: Well... the win32 gui code at least is a mess. :p
13:48:10 <fizzie> Deewiant: http://pastebin.com/KMqHn2e6
13:48:20 <fizzie> Deewiant: There's even a manually implemented checkbox-listbox thing.
13:49:41 <fizzie> Heh. I don't quite know what they mean.
13:49:42 <Deewiant> And I wonder what's going on with the number 20000 in get_opts
13:50:02 <Deewiant> Also, the loop: for (i = 20002; i < 20013; ++i) { if (i == 20012) break; ... } is nice
13:52:17 <Deewiant> At least the messages are cheerful
13:53:28 <fizzie> I think the mapping there is that 20000+N (for N = 2 .. 10) means to generate a poem of N lines; and 20011 means that the length is taken from some textfield.
13:56:18 <fizzie> Deewiant: Nnngh. Look at this nonsense: mii.dwTypeData = strdup("&Muu pituus... (xxxxxxxxxxxxxx)"); sprintf(mii.dwTypeData, "&Muu pituus... (%d)", dw);
13:57:34 <Deewiant> Makes sense to me; strdup is just a not very efficient way of doing it
13:58:40 <Deewiant> (And of course it assumes a 32-bit DWORD but I guess everybody does)
13:59:41 <fizzie> I could've just used snprintf to calculate the length. Except that I guess MSVC calls that _snprintf and it doesn't actually return the number of bytes that were needed, so maybe not.
14:01:12 <Deewiant> You should use the safer _snprintf_s!
14:01:54 -!- adu has quit (Quit: adu).
14:02:42 <fizzie> I don't think MSVC6 had the _s functions yet, in fact.
14:39:36 -!- cpressey has joined.
15:07:18 -!- ais523 has joined.
15:27:22 <cpressey> http://dpaste.com/hold/170444/
15:29:33 <fax> cpressey its very long :|
15:29:56 <cpressey> Yeah and it doesn't tell you much you didn't already know, either :)
15:30:08 <fax> I don't really get why don't you just use types to do this proof..
15:30:37 <cpressey> But it helped me work out the system (so the comment is really the most valuable)
15:30:51 <cpressey> In short, because I don't want to be tied to any particular type system.
15:31:10 <cpressey> This method of (basically) pure rewriting lets you roll your own.
15:31:53 <cpressey> Hm, I guess I could have just done 'nand' to make it shorter.
15:32:20 -!- oerjan has joined.
15:34:07 <oerjan> <oklopol> oerjan come quick <-- er..
15:37:45 * Sgeo should not have stayed up until 4 last night
15:38:20 <oerjan> Sgeo: now you'll _never_ catch up
15:43:44 <fax> cpressey what does tied to a particular type system mean? what I am suggesting is that a type system could be on you side, rather than against you
15:44:32 <Sgeo> I guess there's no way to make a smalltalk system look like it's native?
15:53:44 <fax> wow alise is gonna love this http://www.paulkabay.com/#trivialism
15:57:23 -!- FireFly has joined.
15:57:34 -!- augur has quit (Ping timeout: 276 seconds).
16:02:53 <cpressey> fax: Well, people make up new type systems all the time, as research. I'd like to have something that supports that effort, rather than picking one type system and saying "That's all I got".
16:03:08 <cpressey> I gotta say, I love trivialism already.
16:03:13 -!- cpressey has left (?).
16:05:33 -!- cpressey has joined.
16:07:40 <cpressey> fax: To me, type systems are just a special case of abstract interpretation.
16:07:53 <fax> isn't that true in general?
16:08:20 <cpressey> Uh... yes? Not sure what you're referring to.
16:08:27 <fax> well you don't need to say "to me"
16:09:04 <fax> why don't you have an abstract interpretation module and use it to prove this boolean stuff in a much more effecient way?
16:09:53 <cpressey> That was kind of the plan, but I think it turned out that this proof construct thing *is* my abstract interpretation module...
16:10:19 <cpressey> Abstract interpretations can be mathematically modelled as Galois connections.
16:10:43 <cpressey> And these rewrite rules, with types going one way and evaluations going the other way, seem to be... close to that idea.
16:12:11 <cpressey> (I guess read my first statement as "Type systems are just a special case of abstract interpretation. Most people seem content to work inside the special case. But I want to design very general things.")
16:14:20 <fax> Galois connections??
16:15:07 <cpressey> Oh, I barely understand it myself :/
16:16:22 <cpressey> http://en.wikipedia.org/wiki/Galois_connection vs my shitty explanation http://catseye.tc/about/galois-connections.html
16:17:12 <cpressey> Also, my examples are wrong, and I think I say "element" where I mean "subset" in one place.
16:17:13 <fax> abstract values (such as {int, even, odd, power-of-two, prime, ... }).
16:17:20 <fax> ^ THIS AER TYPES!@!
16:20:09 <cpressey> And "turing-machines-that-always-halt" is a type, too...
16:21:04 <cpressey> Just, good luck proving that your function always evaluates to one.
16:23:58 <oerjan> aerotypes, just so much hot air?
16:26:28 -!- augur has joined.
16:27:16 <cpressey> Is !x -> x just as inconsistent as !x = x ? In the former, every statement has the same normal form, but there's only one normal form. In the latter, there are no normal forms.
16:28:59 -!- Gracenotes has quit (Quit: Leaving).
16:29:52 <oerjan> with intuitionistic logic otherwise, it is.
16:30:06 <oerjan> !false -> false, for example
16:31:04 <oerjan> or hm, x -> !!x is a theorem, so
16:31:17 <oerjan> x -> !!x -> !x follows
16:34:33 <augur> guess who's 24 today :D
16:34:53 <cpressey> oerjan: I agree it's ... on the same level, I just don't know if there is terminology to distinguish between the two.
16:35:21 <cpressey> Hey, augur shares Chuck Norris's birthday.
16:35:31 <oerjan> cpressey: they're equivalent by my argument, in intuitionistic logic
16:36:48 <cpressey> oerjan: Well, maybe replace ! with @ to drop the connotation of "not" ... I'm just thinking symbolically. In both systems, you can pick any two arbitrary statements, like @@@@@x and @@x, and show they are equal.
16:37:19 <oerjan> without the connotation of "not" neither is inconsistent
16:37:25 <cpressey> Only diff is the first says they're equal because they're both equal to x. The second doesn't have to pass through x.
16:37:58 <cpressey> er, by "pass through" I mean "refer to x directly"
16:38:20 <oerjan> um neither has to pass through x
16:39:08 <cpressey> I still think they're inconsistent.
16:39:15 <oerjan> when you say !x -> x do you mean that there _exists_ an x for which this is true? in which case !x -> x is not inconsistent, just take x = true
16:39:55 <cpressey> oerjan: I mean, for all x, this is true.
16:40:28 <oerjan> cpressey: @x = x is not inconsistent if @ has nothing to do with "not"
16:40:32 <cpressey> x is a valid evaluation of !x.
16:40:54 <cpressey> oerjan: OK, then I totally don't understand formal logic.
16:41:39 <oerjan> cpressey: and by nothing to do with "not", i mean that you throw away all the other axioms of !
16:41:46 <fax> what's !x?
16:41:57 <fax> in a particular system?
16:42:02 <fax> (if so, which one)
16:42:18 <oerjan> fax: i don't think cpressey knows yet :D
16:42:22 <cpressey> maybe the problem is that the term "inconsistent" refers to logical systems and by discarding the "logical" meaning of the system, you can no longer use that term?
16:42:50 <oerjan> cpressey: if you have just @x = x, you cannot prove x = y for all x and y
16:43:10 <oerjan> one of them has to be a number of @'s applied to the other
16:43:44 <oerjan> (or to something common, but that happens to be the same thing in this case)
16:44:33 <cpressey> I think we need to clarify the universe, like what x and y can be
16:44:58 <fax> clarify the universe by melting it down and seiving it
16:45:11 <oerjan> cpressey: for example say that @x has the meaning !!x
16:45:36 <oerjan> then it is definitely consistent for @x = x to be true, because it's true in classical logic
16:46:05 <oerjan> although not necessary, since it is not always true in intuitionistic logic
16:46:16 <cpressey> If x and y elem {0, @0, @@0, ...} then we can prove x = y for any choice.
16:46:53 <cpressey> If you start picking them from {0, 1} or something, yeah, I see how you can't prove arbitrary things.
16:50:56 -!- BeholdMyGlory has joined.
16:53:41 * augur uses email instead
16:58:51 <cpressey> OK, let me restate. In a system where there is only one value (call it 0), is @x -> x considered just as "inconsistent" as @x = x (which is just shorthand for {@x -> x, x -> @x}), or are there two different terms for "everything reduces to the same normal form, so we can prove any statement" vs. "there are no normal forms, so we can prove any statement"?
17:00:24 <oerjan> cpressey: if there is only one value, then @x = x is obviously true
17:02:11 <cpressey> I might need to rethink again.
17:04:00 <cpressey> Like, what is a value. If we add another axiom #x = #x, then there are a bunch of irreducible terms #0, ##0, ###0, which are all distinct from 0, at least syntactically -- are they values? Is @@@0 not a value (well, it can't be distinguished from 0 or @0 or any other expression involving @, so maybe not?)
17:05:25 <cpressey> (Logic always was my least favourite esolang...)
17:06:08 -!- tombom has joined.
17:07:04 <oerjan> cpressey: also it is not a requirement of logics to be defined by reductions or have normal forms...
17:07:48 <fax> cpressey, oh I see what you mean, like adding a new 'function' as an axiom, without giving it reduction rules
17:07:48 <cpressey> oerjan: Yeah, I realize that. Kind of.
17:08:59 <cpressey> Kind of like saying it is not a requirement of graphs to be directed :D
17:11:04 -!- oklopol has joined.
17:11:17 <oklopol> i just turned either 21 or 20 a few weeks ago
17:11:39 <fax> http://en.wikipedia.org/wiki/Anus_language
17:12:21 <oklopol> didn't i talk about this here?
17:12:29 <oklopol> i'm sure i've mentioned my age
17:12:38 <oerjan> fax: you'd think that page should have been protected...
17:13:01 <fax> oklopol: why donto you figure it out based on your date of birth
17:13:03 <oerjan> oklopol: well i recall you turning 20 i think, and it was more than a few weeks ago
17:13:17 <oklopol> fax: sounds like a lot of work
17:13:29 <oerjan> as in, quite possibly a year and a few weeks ago
17:13:49 <oklopol> also i think my memory problems are funny, which is also a reason to ask
17:14:35 <oklopol> okay so this year i turn 2010-1989 = 21
17:14:40 <oklopol> so in fact i just had to turn that.
17:15:14 <oklopol> oh right i had to be 20 and not 19 because of something alise said about 19 last year
17:15:27 <oklopol> i would remember if it'd applied to me
17:15:39 <oerjan> clearly oklopol is a being outside time and space
17:15:49 <oerjan> with troubles adapting
17:15:53 <FireFly> oklopol, quick, fetch a GPS!
17:16:17 <FireFly> except that it depends on the location being on earth
17:16:23 <FireFly> which is a small subset of space
17:16:42 <oerjan> FireFly: you'd think it should be usable in low earth orbit too
17:17:00 <FireFly> I guess, but still just a small subset
17:21:54 <oklopol> lol my compositions from ~6 years ago are craaaazy
17:31:24 <ais523> in theory, you could use GPS to determine your location anywhere in space
17:31:31 <ais523> but it would be rather inaccurate far from the Earth
17:33:26 <Gregor> When you're far enough away that the Earth is basically a point, triangulating is hard :P
18:34:21 -!- augur has quit (Ping timeout: 260 seconds).
18:41:24 <lament> but you're unbanned in #Nm
18:42:57 <lament> you should take a stand
18:54:26 <Deewiant> fizzie: I just got one starting with "lohikäärme on lohikäärme ja lohikäärme on lohikäärme"... maybe you should've enforced a bit of variety ;-)
18:54:57 <Deewiant> Although I guess that's arguably validly poetic
19:00:14 -!- MizardX has quit (Ping timeout: 256 seconds).
19:02:00 -!- MizardX has joined.
19:06:23 <fizzie> Deewiant: I think there's supposed to be some sort of enforcement like that.
19:07:06 <fizzie> Deewiant: Apparently not for that rule, though.
19:23:05 -!- MizardX has quit (Read error: Connection reset by peer).
19:23:19 -!- MizardX has joined.
19:33:21 -!- oklopol has quit (Read error: No route to host).
19:33:44 -!- oklopol has joined.
19:42:11 -!- augur has joined.
19:47:21 <cpressey> fax: Actually I have other motivations for doing it this way, but they're... of questionable value
19:56:09 -!- kar8nga has quit (Remote host closed the connection).
20:12:48 -!- jcp has joined.
20:27:08 -!- Phantom_Hoover has joined.
20:27:30 <Phantom_Hoover> Is there any need for a modern-day version of INTERCAL?
20:27:46 <ais523> I don't think there's been any need for INTERCAL all along
20:27:51 <ais523> it's still fun to work with, though
20:28:08 <ais523> there isn't a whole lot of point to much of what we do here
20:28:16 <ais523> although, there's always the chance we might learn something about programming
20:28:25 <ais523> Phantom_Hoover: have you seen C-INTERCAL and CLC-INTERCAL?
20:28:34 <ais523> quite a lot of work has gone into modernising INTERCAL already
20:29:28 -!- Phantom_Hoover has quit (Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838]).
20:33:53 -!- augur has quit (Ping timeout: 240 seconds).
20:38:35 <oerjan> Practical INTERCAL for the modern enterprise programmer
20:38:55 <oerjan> ais523: you just _know_ you need to write that book
20:43:29 <cpressey> there's always the chance we might learn something about the deepest fantasies of wombats, as well.
20:46:47 <oerjan> hey we'll need to do _some_ animal testing of our telepathic sensors before using them on humans, wombats should be excellent.
20:48:58 <AnMaster> "<cpressey> there's always the chance we might learn something about the deepest fantasies of wombats, as well."
20:49:01 -!- augur has joined.
20:49:25 <oerjan> i'm not entirely sure there was any
20:49:44 <AnMaster> oerjan, that is rather worrying
20:49:54 <ais523> AnMaster: yep, it was completely out of context
20:49:56 <oerjan> <ais523> although, there's always the chance we might learn something about programming
20:49:57 <ais523> which is why it was so strange
20:50:08 <AnMaster> oerjan, and "INTERCAL for dummies"?
20:51:18 <oerjan> well, sufficiently hyperintelligent dummies
20:51:48 <oerjan> or possibly crash test dummies. that might fit even better, actually.
20:52:45 <oerjan> ...wherein AnMaster reveals himself as really being cthulhu.
20:53:05 <AnMaster> oerjan, or that I'm using qwerty
20:53:24 <oerjan> well i have no idea if they're close in dvorak or not
20:53:36 <AnMaster> but that would be too simple of course
20:55:11 <oerjan> do crash test dummies dream of roadkill sheep?
20:58:10 <Gregor> Do people in #esoteric dream of inflatable sheep?
20:58:35 <fax> mystery of the cube?
20:58:44 <oerjan> i cannot honestly say i'm sure i've ever done so
20:58:56 <AnMaster> I haven't dreamt about that either
20:59:25 <AnMaster> flying and cardinal sheeps possibly. But if so I must have forgot about them
20:59:38 <oerjan> what's a cardinal sheep?
20:59:53 <AnMaster> oerjan, I believe that pun only works in Swedish
21:00:17 <AnMaster> "karda" is a part of the process for making thread out of wool
21:00:25 <AnMaster> I'm somewhat fuzzy on what exactly it involves
21:00:43 <AnMaster> and the bits "kard" and "card" are produced the same in Swedish
21:00:53 <AnMaster> we don't have the latter in any word afaik
21:02:37 <oerjan> inflatable sheep my be a cardinal sin
21:03:30 <Gregor> (A sin often practiced by cardinals)
21:06:49 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
21:10:58 -!- jcp has joined.
21:20:09 -!- alise has joined.
21:24:30 -!- alise has quit (Ping timeout: 252 seconds).
21:26:55 -!- alise has joined.
21:26:58 <alise> 05:41:13 <fizzie> Written in very ugly C.
21:27:01 <alise> the standard dialect of C
21:27:47 <alise> 05:43:53 <Quadrescence> alise is a girl
21:30:45 -!- ais523 has quit (Remote host closed the connection).
21:32:06 <alise> 07:53:44 <fax> wow alise is gonna love this http://www.paulkabay.com/#trivialism
21:32:07 <fax> alise http://www.paulkabay.com/#trivialism
21:32:20 * cpressey applauds the psychic connection
21:32:20 <alise> Sorry, I'm already a preëventualist (http://viewsourcecode.org/why/preeventualist/; some links broken)
21:35:47 -!- pikhq has quit (Read error: Connection reset by peer).
21:36:03 <alise> /Philosophically/ I guess I cannot reject the proposition that all things are true.
21:36:15 -!- pikhq has joined.
21:36:16 <alise> But only because the question is a bit meaningless: from what frame of reference?
21:36:30 <alise> Even if you supply one, you must define the terms you use - and you cannot do that precisely.
21:36:39 <alise> So perhaps I actually believe that truth doesn't really exist, rather.
21:38:21 <cpressey> Something exists, else why am I doing this?
21:38:31 <cpressey> And if it exists, might it not be true? It might.
21:39:03 <fax> alise philosophically
21:39:05 <fax> alise #philosophically
21:39:28 -!- alise_ has joined.
21:41:00 -!- alise has quit (Ping timeout: 252 seconds).
21:41:31 <alise_> 13:38:21 <cpressey> Something exists, else why am I doing this?
21:41:33 <alise_> I don't know why you're doing this.
21:41:38 <cpressey> I gave (ack 4 1) half an hour, and it still didn't finish evaluating. It must hate me.
21:41:50 <alise_> Also, the things that exist for you might differ from the things that exist for me.
21:42:04 <alise_> Solipsism, while a ludicrously unlikely premise from inside our frame of reference, is still possible.
21:42:13 <alise_> And philosophy is all about the possible yet unlikely.
21:42:27 <cpressey> But it's a sucky basis for action.
21:42:32 <alise_> If I assumed cogito-ergo-sum, that wouldn't really be valid in philosophy, since it'd only be valid for me.
21:42:48 <alise_> And philosophy shouldn't really only work for the author, otherwise it's ... not philosophy.
21:42:55 <alise_> So objectively, nothing can be said to exist for certain;
21:43:11 <alise_> Truth is still ill-defined either way, though.
21:43:18 <alise_> We have a rigorous definition of provability, but not truth.
21:43:27 <alise_> We call things true if they seem to be true to us.
21:43:45 <alise_> Oh, the Axiom of Choice is probably true. But that doesn't really mean anything, it's just human folly.
21:43:53 <alise_> So, really, I guess I technically don't believe in anything.
21:44:11 <alise_> In practice though, from this frame of reference, solipsism is bullshit, philosophical zombies don't exist, the universe is objective, and truth is a useful notion.
21:44:11 <fax> cpressey make ack doesn't terminated
21:44:59 <alise_> A must confusing jumble of tenses, fax.
21:45:16 <cpressey> fax: ... I think I wrote it correctly, (ack 3 2) and such gave a result which corresponded with what I thought I saw when I had the impression I was looking at the Wikipedia page on the Ackermann function
21:48:30 <cpressey> or, what they *claim* is the Ackermann function
21:48:55 -!- Asztal has joined.
21:59:22 <cpressey> I should probably disappear from IRC for a while.
22:00:34 -!- cpressey has left (?).
22:02:33 <oerjan> alise_: muphry's law in action
22:03:12 <alise_> I just caused a stack overflow of the meta tower.
22:04:48 <fax> bufuhukfbawf
22:05:00 -!- lament has quit (Ping timeout: 276 seconds).
22:05:26 <oerjan> fax: that's a very naughty word
22:05:35 <fax> my style is strictly ruude
22:05:38 <fax> aramakayhe
22:05:59 * alise_ wonders what's a better name for "data" that more strongly suggests induction and not just boring... data
22:06:06 <alise_> "Inductive" is a bit too long.
22:06:14 -!- lament has joined.
22:17:59 -!- cheater2 has joined.
22:21:05 -!- cheater3 has quit (Ping timeout: 260 seconds).
22:30:29 -!- tombom has quit (Quit: Leaving).
22:46:12 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
23:02:45 <alise_> doing classical logic in constructivist logic is fun
23:03:38 <Slereah> Try doing the non-contradiction theorem!
23:05:57 -!- oklopol has quit (Ping timeout: 260 seconds).
23:07:48 -!- oklopol has joined.
23:08:20 <alise_> Slereah: What, not (p and not p)?
23:08:35 <alise_> That's in constructivist logic too :P
23:08:54 <Slereah> Or am I thinking of p or not p
23:09:05 -!- coppro has joined.
23:09:07 <alise_> We get rid of (p \/ ~p), not ~(p /\ ~p)
23:09:21 <alise_> The way to do classical logic in constructivist logic is to write everything as (p \/ ~p) -> ...
23:09:39 <fax> you can define classical P OR Q :<=> ~~(P \/ Q)
23:09:39 <alise_> Law of the excluded middle.
23:09:42 <fax> and so on,
23:09:52 <fax> then you can prove classical tautologies
23:10:10 <alise_> http://pastie.org/864149.txt?key=efscdf3wmdhlbyfpnxqfdw
23:10:41 <alise_> proof of (p->q) -> (~p->~q) -> q -> p classically
23:10:56 <alise_> I love the beauty of just letting LEM hand us a contradiction, at which point we simply take its word and prove the thing we want to prove, whatever it is, from it.
23:11:00 <Slereah> I can tell from your taut pants
23:11:25 -!- oklopol has quit (Read error: Connection reset by peer).
23:11:56 -!- oklopol has joined.
23:12:34 <fax> There are no trivial mathematics, just trivial mathematicians
23:12:56 -!- FireFly has quit (Quit: Leaving).
23:13:15 -!- BeholdMyGlory has quit (Read error: Connection reset by peer).
23:13:16 <oerjan> lament feels singled out there
23:13:51 -!- alise__ has joined.
23:14:10 * alise__ realises he redefined modus tollendo ponens in that proof
23:15:14 -!- alise_ has quit (Ping timeout: 252 seconds).
23:18:38 <coppro> alise__: are the implications left-associative or right-associative?
23:19:15 <alise__> right-associative. Obviously. As they're also the function arrows.
23:19:55 <alise__> Curry-Howard isomorphism. Types = statements in constructivist logic.
23:20:03 <alise__> (In a dependently-typed language.)
23:20:08 <alise__> It's the future, mon. See: Agda, Coq, Epigram.
23:20:37 <coppro> I'll believe you when I see it in .NET :P
23:20:47 <oerjan> non-dependently typed too. just you only get propositional logic then, or thereabouts.
23:21:03 <coppro> .NET is looking to be the future, regrettably
23:21:32 <alise__> oerjan: propositional logic is for butts
23:22:13 <oerjan> i see an obvious pun but i'll leave it for Slereah
23:23:48 <fax> nice of you to throw him some scraps of meat that you can't be bothered to pick from the bones
23:24:59 <oerjan> it's more like it seems more his style
23:28:10 <alise__> metastruct will be so cool :|
23:28:49 <coppro> does anyone know a program that will simply ask X to clean up any temporary resources it has hanging around?
23:29:00 <oerjan> i n *hit by falling anvil*
23:29:01 <coppro> so that I don't have to write one myself
23:29:38 <alise__> foo : (ProgDescription -> Prog) -> Prog
23:29:53 <alise__> foo p = englishDescr "ask X to clean up any temporary resources it has hanging around"
23:30:01 <alise__> foo p = p (englishDescr "ask X to clean up any temporary resources it has hanging around")
23:33:21 -!- augur has quit (Ping timeout: 252 seconds).
23:38:13 -!- oklopol has quit (Ping timeout: 240 seconds).
23:56:33 -!- oerjan has quit (Quit: Good night).
23:57:05 -!- oklopol has joined.
23:57:36 <pikhq> (note: all resources considered temporary)
23:58:39 <alise__> Resources should totally include their extents.