00:00:02 But your proofs aren't proofs and if they were they'd be nothing in particular. If I'm reading your snippet right. 00:00:07 fundamental theorem was solutions of XY = YX? 00:00:15 oklokok, okay but can you give me one hint on OR? 00:00:25 because right now I am just sort of lost 00:00:43 oklokok but this finite calculus is so cool! 00:00:44 alise_: How would you prove that pop(push(X,Stack)) == Stack ? 00:00:53 cpressey: Also, I assume that your proofs are first-class values. So how do you create a function taking a function from a positive rational to a rational, and also a proof that for all positive rationals e1 and e2, |f e1 - f e2| < e1 + e2? 00:01:14 Or could you give me an example of something more interesting that could be proved (but still under a page of derivation)? 00:01:17 i.e., a function taking (f, |f e1 - f e2| < e1 + e2), also known as a computable real 00:01:20 yeah fundamental theorem was your pet name for the commutation thing 00:01:21 cpressey, in dependent type theory this would be a trivial proof, because pop(push(X,Stack)) would compute down to Stack, so all you really need to prove is Stack == Stack 00:01:23 cpressey: depends 00:01:23 -!- bsmntbombdood_ has joined. 00:01:48 fax: A better example to prove would be most welcome, then 00:01:52 cpressey (if P reduces to P' then a proof of P is a proof of P') 00:02:00 cpressey: I gave you one. 00:02:10 alise_: I don't have functions in my language 00:02:16 okay for OR, the first thing is to reduce it to a=b OR a=c. 00:02:17 or reals, for that matter 00:02:24 cpressey: You don't need reals. 00:02:25 oklokok, I think it has something to do with sequence of lydon words.. (because you told me that) 00:02:25 I just defined the reals. 00:02:33 -!- bsmntbombdood has quit (Ping timeout: 245 seconds). 00:02:39 oklokok, okay byebye! 00:02:41 at least i think that's the easiest way 00:02:42 alise_: You're too quick for me. 00:02:54 cpressey: The tuple (f : Q+ -> Q, forall e1, e2 : Q+, |f e1 - f e2| < e1 + e2) is a computable real. 00:03:03 (Which is just like the reals, except without things like chaitin's constant) 00:03:07 fax: nope, lyndon's aren't useful at all, i just like them. 00:03:15 oklokok, oh :p 00:03:19 cpressey: The second element is a property of the first, a function. 00:03:22 I thought they were integral to this 00:03:34 ah, sorry if i gave you that impression 00:03:44 cpressey: (Basically pi 0.1 = 3.1, pi 0.01 = 3.14, etc) 00:03:45 -!- coppro has joined. 00:04:00 cpressey: So, substitute whatever is the best analogue for a function. 00:04:07 How do you construct the proof? 00:04:15 alise_: I'm not going to be able to prove that without defining some axioms for ordering and stuff. 00:04:30 cpressey: You don't need any axioms above the standard for this 00:04:45 i've basically lectured you parts of the "introduction" chapter of our combinatorics on words course, so things don't necessarily progress that linearly yet! 00:05:09 alise_: Basically, we have term rewriting. We say, "X rewrites into Y"! The proof is simply to list the derivation. Maybe this isn't very impressive to *you*, but remember what world *I'm* living in. 00:05:16 oh well actually chapters 1 and 2 00:05:25 cpressey: So construct the computable reals. 00:05:41 where "lectured" == "listed theorems as exercises" ;) 00:05:43 alise_: No. What am I proving about them? Their existence? 00:05:43 anyway I better go to bed 00:05:49 me too 00:05:59 cpressey: No. 00:06:09 Okay, let me express this in Haskell-ish things for you. 00:06:15 "for all positive rationals e1 and e2, |f e1 - f e2| < e1 + e2" is closer, but requires, like, numbers and shit. 00:06:21 Symbolic. 00:06:36 data Real = Real (Q+ -> Q) (forall (e1:Q+), (e2:Q+). abs (f e1 - f e2) < e1 + e2) 00:06:40 The latter bit is the dependent part. 00:06:45 So, to construct a computable real, we do 00:06:50 Real f (proof of that property of f) 00:07:02 So a Real is a function that satisfies a certain property; you must prove it does. 00:07:15 -!- fax has quit (Quit: Lost terminal). 00:07:18 So if we have p : (forall (e1:Q+), (e2:Q+). abs (f e1 - f e2) < e1 + e2), p is a proof of that. 00:07:33 If A is a rational, and B is a rational, and f is a function(?), the absolute value of the difference between f(A) and f(B) is less than the sum of A and B. ? 00:07:36 Since all your proofs are just simply proving that x evaluates to x', it's pointless. 00:07:44 The proof is nonexistent; x equiv-to x' by virtue of evaluating to it. 00:07:47 So the proof is that x = x. 00:07:57 cpressey: *positive rational, not rational. 00:07:58 -!- lament has quit (Ping timeout: 264 seconds). 00:07:59 Also, no. 00:08:05 Sigh. 00:08:20 It is only true for some functions. Obviously. 00:08:32 Our constructor takes a function f, and a proof that that holds /for only the single function f that we give/. 00:08:52 That's a proof *schema* in my book. 00:08:52 Any function that satisfies that property is a /computable real/, so to create a computable real we must /supply a proof that the function we give obeys the property/. 00:09:04 So, how would you structure such a thing? 00:09:13 I bet you can't, because your proof construct is uber-limited. 00:09:25 -!- lament has joined. 00:09:58 alise_: Nowhere did I say I was writing a *prover*, only a *proof checker* 00:10:12 What is the problem with specifying f in my proof? 00:10:13 Irrelevant. 00:10:25 You cannot even /express the proof/ in your language, because you can only prove things of the form x = eval x 00:10:37 And you cannot check a proof you can't express. 00:10:51 If there are some values for f where it holds, and others where it doesn't, then it's not a proof! 00:11:37 You prove it for some given function f. 00:11:46 Right, so give me some function f. 00:11:52 And I'll write the proof. 00:11:57 If you don't, I can't. 00:12:18 i : Q -> R; i q = (\_. q, ...proof...) 00:12:21 Like I said, what you gave sounds like a proof schema to me. 00:12:24 Really simple there. 00:12:27 Write the proof in your language. 00:12:37 \x. e being lambda, of course. 00:13:45 How am I supposed to read that? 00:14:10 i takes the rationals to the reals; i is some function... 00:14:24 ... which contains a proof... 00:14:48 i : Q -> R -- i is a function from rationals to reals. 00:14:52 Digression: 00:15:23 type R = (f : Q+ -> Q, forall (e1,e2 : Q+). abs (f e1 - f e2) < e1 + e2) 00:15:24 so 00:15:33 i q = (\_. q, ...) 00:15:42 \_.q is a function taking one argument, ignoring it, and returning q 00:16:00 you must now prove that for all positive rationals e1 and e2, |(\_. q) e1 - (\_. q) e2| < e1 + e2 00:16:01 i.e. 00:16:10 you must now prove that for all positive rationals e1 and e2, |e1 - e2| < e1 + e2 00:16:13 but you can't just assume that 00:16:18 do it methodically with your proof construct 00:16:20 (I don't believe you can) 00:17:01 "you must now prove that for all positive rationals e1 and e2, |e1 - e2| < e1 + e2" - that sounds at least closer to a sane request, but it still will require me defining rationals, to do it completely symbolically. 00:17:25 Well, no. I mean, |a - b| = a + b 00:17:31 I assume you meant <= 00:17:39 Well, no. 00:17:48 I mean, could = a + b 00:17:55 Oh wait, positive. 00:18:02 cpressey: also, no 00:18:04 you must now prove that for all positive rationals e1 and e2, |(\_. q) e1 - (\_. q) e2| < e1 + e2 00:18:10 I did it wrong :D 00:18:19 What is q in that statement? 00:18:29 the argument to the function i. pay attention 00:18:32 => for all positive rationals e1 and e2, |q - q| < e1 + e2 00:18:36 => for all positive rationals e1 and e2, |0| < e1 + e2 00:18:40 => for all positive rationals e1 and e2, 0 < e1 + e2 00:18:51 (prove so) 00:18:53 => for all positive rationals e1 and e2, true 00:18:55 => true 00:19:02 but you must prove it /with your proof construct/ 00:19:04 => QED 00:19:07 that's the whole point; it's verified 00:19:46 OK, if a > 0, and b > 0, then a + b > 0, I can do. I *still* do not know what you are talking about with your function i. Do you want this quantified over all possible functions i? 00:20:16 * alise_ sigh 00:20:23 You know Haskell. Correct? 00:20:32 Assume that I do not. 00:21:03 Look, actually forget it. Thanks for your feedback. If I'm making a huge error I'm sure I'll figure it out myself. 00:21:08 Later, folks. 00:21:10 Seems to be more functions of the type (i :: a -> R) 00:21:10 -!- cpressey has left (?). 00:21:49 No, wait, more specific, :: Q -> R. Anyways. 00:22:21 -!- alise has joined. 00:22:29 If you didn't know Haskell I couldn't explain it in a million years. 00:23:04 Sounds like a personal problem. 00:23:10 Sure you could. You could give a Haskell tutorial. 00:24:15 Gregor: Do you have any idea what dependent type theory is? 00:24:20 Haskell is utter peanuts in comparison. I have to assume some baseline. 00:24:44 -!- alise_ has quit (Ping timeout: 252 seconds). 00:25:08 I have no formal experience with dependent type theory, only indirect. 00:25:16 Erm, indirect isn't the right word. 00:25:19 Informal, I suppose. 00:25:21 i don't remember what peanuts taste like, but i'm sure i love them 00:26:33 What a tragic statement :P 00:27:10 thank you about me. 00:29:26 I keep looking down, not seeing a tie, and thinking "?!" 00:29:28 Silly bowtie. 00:30:10 -!- werdan7 has quit (Ping timeout: 624 seconds). 00:32:58 -!- BeholdMyGlory has quit (Read error: Connection reset by peer). 00:33:15 do you like clothes? 00:34:02 Clothes are for the weak. 00:34:18 sooooo... you don't? 00:34:37 he wears a barrel 00:34:40 and a bear skin 00:34:44 i mean you wear all sorts of different clothes, which is weird if you, like normal humans, hate wearing clothes 00:34:56 And a necktie. 00:35:03 -!- werdan7 has joined. 00:35:14 Just a barrel, a bear skin and a necktie. 00:35:15 That's me. 00:35:26 Well, on a dressier day. 00:35:32 I lose the barrel on average days. 00:35:43 which days are the average days? 00:35:47 somehow i feel i'm the only one being serious 00:35:50 how does one calculate that 00:35:55 Pretty much anything other than going to a wedding or whatnot. 00:36:06 weddings are the outliers of my life! 00:36:19 Hence why they're not the normal days. 00:44:00 http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/real.pdf 00:44:04 The ramblings of a crazy man. 00:46:18 I learned something great from Ruby: Fibers! 00:46:33 "Andrew Wiles's alleged `proof' of FLT, while a crowning human achievement, is not rigorous, since" 00:46:34 I think Fibers would be very useful in the C# project I'm working on 00:46:42 "it uses continuous analysis, which is meaningless." 00:46:44 Sgeo: fibers are shit 00:47:04 yeah looking at this pdf... it's crazy 00:47:05 Howso? And is there ANYTHING that isn't? 00:50:02 -!- FireFly has quit (Quit: Leaving). 00:50:05 Well, for instance, he's telling us stuff like "sqrt(2) doesn't exist" 00:50:13 -!- jcp has joined. 00:50:16 he is talking to me 00:50:21 Sgeo: because fibers are like continuations and coroutines but shittier 00:50:52 ph 00:50:54 oh 00:51:18 Well, I want something that lets me resume the current .. thing later 00:51:33 I'm willing to work with whatever exists the most in .NET 00:51:38 Sgeo: continuations. coroutines. 00:55:30 Continuations exist in .NET? 00:55:50 no, but .net is almost useless for programming. 00:56:15 .net is the best 00:56:24 if you hate yourself. 00:56:31 Continuations can be done in .Net. 00:56:42 By which I of course mean CPS. 00:56:50 Only via... yeah. 00:56:59 I understand call/cc better than CPS 00:57:31 Sgeo: CPS is simply the act of transforming the usage of return values to a function that takes a value. 00:57:57 Instead of "x = function_call(bar);", you do "function_call(bar, \x -> ...);" 00:58:14 And that was a delicously odd hybrid of C and Haskell syntax. 01:03:21 So, Chrome maps the numpad keys, with numlock on, to the keyCodes 97 etc. 01:03:31 97, for the non-ASCII-inclined, is lower-case 'a'. 01:03:41 (The key 'A' sends a capital A, 65) 01:03:58 That's ... confusing. 01:05:26 Oh look, Firefox does it too. 01:05:27 Weird. 01:06:22 ? 01:06:31 grop 01:13:08 -!- alise has quit (Ping timeout: 252 seconds). 01:28:25 -!- Asztal has quit (Ping timeout: 265 seconds). 01:29:11 weird html5 keyboard handling? 01:35:05 -!- oklokok has quit (Read error: Connection reset by peer). 01:52:40 Weird blaming of HTML5 for totally irrelevant things? :P 01:53:39 ah 02:04:58 -!- adu has joined. 02:07:24 -!- Oranjer has quit (Quit: Leaving.). 03:01:01 -!- Oranjer has joined. 03:08:12 -!- OxE6 has joined. 03:20:06 -!- Oranjer has quit (Quit: Leaving.). 03:35:51 -!- Oranjer has joined. 03:42:24 ugh, people in #latex treating me like I've never used a text editor before; much less LaTeX 03:43:37 I've never used LaTeX 03:49:51 -!- myndzi\ has joined. 03:50:18 -!- myndzi\ has changed nick to myndzi. 03:53:26 anyone know a LaTeX equivalent of OO.o Math's csub? 03:54:07 -!- coppro has quit (Remote host closed the connection). 03:57:00 -!- coppro has joined. 03:57:46 a "tnx you badass" would have been appreciated... 03:58:57 Sgeo: firefox crashed 03:59:37 Ah 04:21:16 -!- GreaseMonkey has joined. 05:12:44 -!- oerjan has joined. 05:33:31 -!- adu has quit (Read error: Connection reset by peer). 05:38:52 -!- pikhq has quit (Read error: Connection reset by peer). 05:42:36 -!- adu has joined. 05:43:45 -!- Oranjer has left (?). 05:43:57 -!- pikhq has joined. 05:44:26 -!- bsmntbombdood_ has changed nick to bsmntbombdood. 05:49:30 -!- Gracenotes has quit (Read error: Connection reset by peer). 05:57:10 I discovered http://www.periodicvideos.com/ today :( 06:01:15 now I'll never get to sleep 06:08:05 the one guy looks like your stereotypical professor 06:08:07 and he is 06:15:24 -!- coppro has quit (Read error: Connection reset by peer). 06:15:26 -!- Halph has joined. 06:15:34 -!- Halph has changed nick to coppro. 06:15:35 -!- werdan7 has quit (Ping timeout: 619 seconds). 06:16:29 -!- yetifoot has joined. 06:16:53 -!- yetifoot has left (?). 06:21:21 -!- werdan7 has joined. 06:25:44 -!- jcp has quit (Quit: I will do anything (almost) for a new router.). 06:42:17 -!- oerjan has quit (Quit: leaving). 06:48:49 -!- MizardX has quit (Ping timeout: 268 seconds). 07:02:59 -!- tombom has joined. 07:08:57 anyone know a LaTeX equivalent of OO.o Math's csub? <--- what does csub do? 07:09:11 nevermind, found it 07:09:29 coppro, but I'm genuinely interested! 07:09:32 busy watching videos that tell me things I already know in humourous manner 07:09:43 AnMaster: positions a subscript directly below the principal 07:09:50 done with \underset 07:09:55 * Sgeo will attempt to learn E tomorrow 07:09:55 right 07:09:58 E? 07:10:10 D done correctly :P 07:10:19 http://www.erights.org/elang/ 07:10:36 Supposed to be secure distrubuted language thingy 07:10:56 sure that isn't Erlang? 07:11:02 (that you're thinking of; not the site) 07:12:01 I'm pretty sure 07:13:53 G'night 07:16:49 Morning. 07:17:09 I discovered http://www.periodicvideos.com/ today :( <--- looks interesting 07:17:24 it is 07:18:06 Supposed to be secure distrubuted language thingy sure that isn't Erlang? <-- "secure" isn't a way I would describe erlang. Not insecure either though. 07:18:24 I mean, it isn't specifically geared towards security 07:18:28 bbl 07:18:31 that's true 07:18:50 I mentioned it specifically because it's 'elang' 07:19:22 Bot-tweets are getting a bit suspicious: "About IRC: for sex.. assembly language reminds you at very instruction. at http://paste.lisp.org/display/UNK" 07:20:25 sulphur is a really good video 07:20:38 -!- fungot has joined. 07:53:48 -!- tombom has quit (Quit: Leaving). 07:55:17 you must watch iron 07:55:22 the story is hilarious 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:06:13 -!- lament has quit (Ping timeout: 264 seconds). 08:07:18 -!- lament has joined. 08:21:13 -!- madbr has quit (Quit: Radiateur). 08:28:10 -!- oklokok has joined. 08:37:28 -!- Asztal has joined. 08:52:08 -!- coppro has quit (Ping timeout: 245 seconds). 09:07:33 -!- adu has quit (Quit: adu). 09:15:28 -!- GreaseMonkey has quit (Quit: HydraIRC -> http://www.hydrairc.org <- Nobody cares enough to cybersquat it). 09:22:58 -!- oklokok has quit (Ping timeout: 245 seconds). 09:40:22 -!- MizardX has joined. 10:04:37 -!- Asztal has quit (Ping timeout: 260 seconds). 10:09:59 -!- amca has joined. 10:12:11 -!- oerjan has joined. 10:50:51 -!- oerjan has quit (Quit: leaving). 10:51:53 -!- amca has quit (Quit: Farewell). 12:24:08 -!- alise has joined. 12:24:33 Hypothesis: It is impossible to be comfortable. 12:26:00 19:42:24 ugh, people in #latex treating me like I've never used a text editor before; much less LaTeX 12:26:12 Most users of LaTeX are near computer-illiterate, I think. 12:26:19 Mostly mathy people. 12:27:03 Sgeo: E is interesting but not nearly as magical as you think. 12:27:17 And it requires a good understanding of its principles to use. 12:27:32 wow 12:27:36 thanks asshole alise 12:27:51 What? 12:28:10 I am in #LATEX 12:28:23 and too bad coppro isn't here; I could help him 12:28:24 You mean my LaTeX remark? "Most users of LaTeX are near computer-illiterate" = >50% of LaTeX users are computer-illiterate. 12:28:26 I love latekz 12:28:36 LaTeX is fine. 12:28:43 alise: thank you, you're saying there's a >50% chance I'm computer illiterate 12:29:00 Quadrescence: No, because there is a large deluge of other evidence to suggest you are not. 12:29:04 -!- ais523 has joined. 12:29:08 okay I am happy then :))) 12:29:09 For instance, anyone in #esoteric is almost certainly highly computer literate. 12:29:20 Hi ais523. 12:30:03 hi 12:30:24 I have a seminar in half an hour, but am happy to talk until then 12:30:40 ais523: about Feather. 12:31:00 well, if you have questions... 12:31:07 I haven't thought much further on it, though 12:31:12 ais523: What is Feather, in detail? 12:31:14 >:) 12:31:34 god dammit, you asshole! 12:31:38 well, I'm not sure myself 12:31:41 We were sane for a while there! 12:32:09 let's see... you start with a very small TC language 12:32:16 I'm planning to use lambda calculus + continuations 12:32:30 and a very small bootstrap program, written in that language 12:33:18 originally, the bootstrap is just an implementation of that language; simplicity is more important here than correctness or features or anything, so long as it remains TC 12:33:29 wait, it has to be correct 12:33:37 but it doesn't matter if it has no error handling or something like that 12:33:57 now, the bootstrap program has to be written in a vaguely object-oriented style 12:34:17 it doesn't need to be actual OO or even a C++ level of OO, but it needs to have parts which are vaguely identifiable as objects 12:34:33 lambda calculus + continuations; interesting 12:34:38 and the property, that each of those parts can be retroactively replaced 12:34:39 I'm going to implement that 12:35:18 the easiest way to do this seems to be to make each part the return from a call/cc, or somehow otherwise have a continuation that goes back in time to when it was created and replaces it 12:35:30 ais523: are you sure you absolutely need lambda if you have continuations? 12:35:33 calculus of continuations! 12:35:52 alise: I'm not, but it's likely to make the self-interp shorter and easier to write 12:35:59 ais523: also, LC sucks, make it combinator calculus 12:36:13 LC has syntactic stupidities like (\f x.f x) vs f 12:36:14 and Subtle Cough was proved non-TC, so you need /something/ other than call/cc, at least 12:36:20 and (\x. x) vs (\y. y) 12:36:28 de bruijn indexes solve the latter but you still need n-conversion 12:36:43 alise: planned Feather syntax is [ x | f x ] 12:36:48 for \x.(f x) 12:36:53 So what? 12:37:02 semantics (\f x. f x) = semantics f 12:37:03 but 12:37:03 alise: because if I didn't say, AnMaster would ask 12:37:08 (\f x. f x) =/= f 12:37:20 hmm, semantics (\x. f x) = semantics f 12:37:27 semantics (\x. x) = semantics (\y. y) 12:37:29 but etc 12:37:32 De Bruijn indexes solve that one: 12:37:37 semantics (\0) = semantics (\0) 12:37:39 \0 = \0 12:37:43 but not n-conversion: 12:37:52 the same problem happens even with combinators 12:37:58 n conversion? 12:38:01 ETA CONVERSION? 12:38:04 erm oops I wrote it wrong 12:38:12 semantics (\x. f x) 12:38:13 and, well, in general because you can't compare functions in general in a TC language 12:38:25 ais523: you compare syntactic structure 12:38:37 anyway n-conversion + de bruijn indexes make it work 12:38:39 well, ``skk is semantically equal to i, for instance 12:38:40 but n-conversion is ugly 12:38:46 converting (\{f} 0) to {f} 12:38:52 where {f} is f's current identifier number 12:39:09 ais523: that's irrelevant though 12:39:21 (\x. f x) is literally /the same function/ as f 12:39:24 just written a different way 12:39:30 skk is more like a different implementation of the same thing as i 12:39:47 I'm not convinced that (\x. f x) is the same function 12:40:04 it certainly isn't in a strict lang if determining the value of f has side effects 12:40:15 then f isn't a value :P 12:41:01 yep; this argument only works if f is a function constant 12:41:06 this is such a weird discussion 12:41:14 perhaps the issue here is, that constant folding on functions is a fool's errand 12:41:28 because you end up evaluating the whole program at compile time, and if it contains an infinite loop you're in trouble 12:41:33 Quadrescence: it's the sort of discussion we have here 12:42:23 ais523: I know 12:42:28 But this needs to be more interesting 12:42:38 ais523: let's put it this way - eta-conversion + n-reduction and then comparing syntactic structure is the kind of thing we do in our fancy functional langs :P 12:42:42 although I credit alise and him talking about de bruijn seqs 12:42:42 anyway, anything remotely related to Feather is inherently weird 12:42:53 Quadrescence: de bruijn indexes 12:42:56 different thing 12:42:58 alise: as an optimisation? 12:42:59 idxs, yeah 12:43:01 that's what I meant 12:43:11 ais523: no 12:43:26 why, then? 12:43:34 hmm... the type of continuations is really strange 12:43:55 well, of callCC, specifically 12:44:14 continuations have a relatively simple type (function from some type to bottom) 12:44:21 ((a -> X) -> a) -> a 12:44:25 where X is forall b. b 12:44:28 call/cc, yes, that's weird 12:44:35 which is actually exists b. b 12:44:44 which is actually isomorphic to () :-) 12:44:53 but we have it as forall for convenience... 12:45:19 alise: the isomorphism there is misleading, I think 12:45:31 it's true, though 12:45:34 type-theoretically 12:45:40 yes, but rather vacuous 12:45:49 no, actually 12:45:59 T (except the opposite of _|_) really is the supertype of all types, theoretically 12:46:04 in practice, you implement it like data T = T 12:46:11 because they're the same thing 12:46:13 (it also represents truth) 12:46:22 (where false is the empty type, _|_) 12:46:48 App :: LC (a -> b) -> LC a -> LC b -- it annoys me that you can't do this 12:47:00 because it stops you writing `semantics :: LC a -> a` 12:47:51 top bot 12:48:11 modal logic is weird; it has _|_, T, 0, and 1 as logic values 12:48:27 where 0 and 1 vaguely correspond to false and true, T to both, and _|_ to neither 12:48:33 The fundamental theorem of type theory: all types are sandwiched between an act of gay sex, top to bottom. 12:48:44 alise: hahahahaha 12:48:48 that is great 12:49:08 also, "bottom" is a stupid name for it 12:49:13 it's not 12:49:22 it's at the bottom of the type hierarchy 12:49:24 I've seen "eet" used for the same symbol ("tee" spelt backwards), for instance 12:49:42 alise: I know why it has that name; but it's too many syllables and looks nothing like the symbol 12:50:09 I just like to call them top and bot 12:50:13 literally "bot" 12:50:20 like bot fly :( 12:51:18 alise: Maybe I should recruit you for helping me design my language 12:51:37 since you seem more competent about type theory and stuff than I originally imagined 12:51:47 Quadrescence: alise is an expert on that sort of stuff 12:51:51 App :: LCC (a -> b) -> LCC a -> LCC (b -> c) -> LCC c -- I wonder how to modify this type to (apart from making it possible to compile) enforce CPS-style. 12:51:54 I tend to care more about the practice than the theory 12:52:08 Hey, I'm no expert. 12:52:09 I like practice too. 12:52:16 Practice is very, very important. 12:52:32 Hmm. I could fold App's type into Lam. 12:52:41 So we have LamApp and LamVar. 12:52:48 But then we can't have a top-level application. 12:52:54 But I can model that to applying the main function to, say, id. 12:53:35 LamApp :: LCC (a -> b) -> LCC (b -> c) -> LCC (a -> c) -- Hey, look. It's compose. 12:57:18 Yeah, this model isn't workable. 13:00:00 oh well, time for my seminar 13:00:10 Seminyarrrrrrrr 13:07:14 Aw man, my HOAS broke cwcc 13:07:25 * Sgeo is probably going to have potato chips for breakfast 13:14:08 -!- Asztal has joined. 13:18:34 -!- augur has quit (Ping timeout: 268 seconds). 13:18:47 I now have an interpreter for the Lambda Calculus of Continuations, but no pretty-printer, so I can't test it. 13:24:18 So, put differently, you have nothing. 13:24:57 Well, I'm going to write a type-inferrer so that I can see the sort of results. 13:25:03 Any hey, I can make it loop forever. 13:25:26 Wait, all LC expressions have the type a = a -> a. 13:25:30 Um. 13:25:45 The AST isn't terribly conducive to pretty-printing: 13:25:50 data LCC t where 13:25:52 App :: LCC Lam -> LCC Lam -> LCC Lam -> LCC App 13:25:54 Lam :: (LCC Lam -> LCC Lam -> LCC t) -> LCC Lam 13:26:50 alise, should I learn Common Lisp or Scheme [I think I may have asked you this before]. Although Scheme seems attractive, there's pretty much no large standard library 13:27:02 Don't know if CL has one, but from what I gathered.. 13:28:07 I'm not even going to answer because you seem to value a language based on how many BSD socket libraries it has, and this is poisonous. 13:28:43 Scheme (R5RS, not R6RS) is clearly the superior language. Common Lisp doesn't have standard sockets either. It does have Roman Numeral support, though. 13:29:20 ...who said anything about sockets? 13:30:23 The prototypical example of a "practical" "standard" "library"> 13:30:23 *. 13:32:39 Quadrescence: So, uh, tell me about your language. 13:34:30 alise, Quadrescence and Gregor seem to hate PLT Scheme, I'm still not sure why. Do you have any comments on PLT Scheme? 13:34:43 It is a language that is intended to be practical for general programming, but will be particularly designed for building a computer algebra system with it. I want it strictly statically typed, however, if a certain type can't be proven/shown, that should NOT error, but be left for run-time resolution 13:34:50 PLT Scheme [...] is rubbish. 13:35:06 Use SISC, or Scheme48, or Chicken, or ... 13:35:24 Quadrescence: Computer algebra system: You want a term rewriting language. (Trust me.) 13:35:40 A typed one is an endeavour I've looked into before, and one that is very interesting. 13:35:47 alise: Yes definitely 13:35:57 I've read my fair share of TRS junk 13:36:04 Quadrescence: But as for the untyped-leave-to-runtime... Why not just have a more powerful type system? 13:36:39 In what way is PLT rubbish? 13:36:52 -!- ztirf4 has joined. 13:37:17 Sgeo: To understand the reasons why you'd have to understand Scheme. 13:37:17 Catch-22. 13:37:22 Trust ze sexperts. 13:37:40 Every single implemented dependent type system is annoying as ! to use, at least in my opinion. I don't want the programmer to fight with the compiler; I want him/her to work with it. This is NOT to say the type system can't be powerful! I am just saying things should be optional in a sense. 13:38:03 alise, how well do I have to understand Scheme? I think I understand the basics at this point 13:38:14 Quadrescence: Well, I agree that most dependently-typed languages aren't too nice to use. 13:38:17 Sgeo: almost entirely. 13:38:26 Sgeo: Knowing some functions and stuff won't make you "know" scheme 13:38:30 Quadrescence: But, I mean, my main project is to make dependently-typed languages nice. 13:38:33 You really have to "see the light" to know scheme 13:38:37 Quadrescence: So you must understand that I'll push for that. :-) 13:38:51 alise: Of course. I *want* dependent types. 13:38:56 Also, even something like Haskell's type system can be extended a little bit to make it lenient for anything you'd want. 13:38:58 So, what Scheme is most recommended for newbies? 13:39:09 Quadrescence: Right. My opinion is that you can make them nice /and/ mandatory. 13:39:25 Sgeo: Well, not SISC, too barebones... Scheme48 or Chicken. Chicken has more librarooz. 13:39:28 alise: That might be possible, and if so, I'd probably enforce that 13:39:49 alise: You might agree that less libraries = better for a new schemer 13:39:56 Quadrescence: But dependent types for term rewriting is in fact a project I had! (I gave up on it because it was really hard >_>) 13:40:11 Quadrescence: Yes, but Sgeo's obsessed with libraries. And really most eggs are fine. 13:40:15 Besides, SISC is Java. :-P 13:40:22 Nothing is wrong with libraries 13:40:29 but I think the "point" of Scheme will be missed 13:40:34 True. 13:40:42 Just at the start. 13:40:49 Is "SRFI" what is meant by libraries? 13:40:53 I'd use Scheme48 or so 13:40:59 Sgeo: They are "standard" libraries 13:41:07 Quadrescence: The problems with typing a term rewriting language are basically: One, identifying what you're typing (There's no nameable function, since we simply put little holes of free variables into an expression and rewrite it), and two, dealing with the extensibility (you can add to a "function" at any time just by creating a rule). 13:41:22 I think I know how to solve the second one (with an entirely new type system). The first may just be a syntactic fluff. 13:41:25 *a bit of 13:41:35 Quadrescence: Oh, I forgot S48. 13:41:38 Sgeo: Use Scheme48. 13:42:12 The Windows distribution is "experimental" 13:42:15 alise: Right. My rule was going to be this: you can't create a new function/constructor unless it can be typed 13:42:39 Sgeo: Oh, you're on windows, no wonder why you are attached to dr scheme 13:42:44 Sgeo: Oh. 13:42:46 Windows. 13:42:50 Is Notepad++ any good with Scheme? 13:42:57 Emacs. Only. 13:42:59 emacs is good for scheme 13:42:59 Or Edwin, even, lol. 13:42:59 ;) 13:43:05 with Quack, I suggest. 13:43:10 Anything else will fail. Horribly. Do not even bother. 13:43:15 Sgeo: Bla just use dr scheme 13:43:24 Set to R5RS at least 13:43:26 Since you're on windows, there's little you can really do 13:43:29 Think of the /children/ 13:43:32 and yes, set it to R5RS 13:43:47 Notepad++ seems to have Scheme support 13:43:58 Quadrescence: Should we move discussion of this language elsewhere so I can blab a lot about the type system for term rewriting I half-thought up? 13:44:01 Sgeo: It has rudimentary highlighting, probably. 13:44:02 Scheme highlighting isn't the important part 13:44:05 And no nice indentation thingy 13:44:14 If you are not going to trust the opinions of people who /know/ what they're talking about, why ask? 13:44:15 I typed (let ((a 5) and hit enter 13:44:16 alise: Sure 13:44:19 It didn't autoindent 13:44:33 Sgeo: Same with Emacs. Technically. (Ctrl-J :P) 13:44:38 Sgeo: Just use PLT/whatever 13:44:42 Quadrescence: Name it 13:44:57 yeah dr scheme at least has a workable editor for newbz 13:44:59 Quadrescence: (the channel) 13:45:03 ummmmmmm 13:45:47 Does PLT in r5rs mode support the SRFIs that PLT is supposed to support? 13:46:10 Quadrescence: Well I wouldn't want to usurp your holy rights as a Platonic-space-excavator. :P 13:46:18 Sgeo: Yes. 13:46:19 alise: #~math 13:46:24 * Sgeo is happy now 13:46:41 Quadrescence: No, Libster and base3 will just start attempting to troll me again. 13:46:42 Keyword "attempting". 13:47:06 alise: No. 13:47:09 Libster is banned 13:47:17 Hah, really? 13:47:19 base3 is gone 13:47:21 yes really 13:47:34 Anyway, let's just do #rewritetypes so there's no flood. 13:47:40 Unless someone /else/ has that channel... 13:47:51 No one is talking 13:48:05 but we can make a new channel if you so desire 13:48:10 -!- augur has joined. 13:48:22 The holy institution of making a new channel, a.k.a. /j #foo :-P 13:51:01 Um... >.> 13:51:14 Are there any socket thingies in any SRFIs? 13:52:13 I shouldn't have even bothered. 13:52:48 I'll take that as a "No, and you're completely missing the point" 13:53:00 Not no. 13:53:15 But not yes. Actually not even mu, I meant exactly what I said. But yes, you are missing the point. 13:55:36 .. 13:57:24 What is the point, exactly? 13:57:37 Maybe I should just stick with Haskell >.> 13:58:27 I doubt you get Haskell's point either. 13:58:33 woo 13:58:35 xv 13:58:37 tomorrow i turn 2^3 * 3 years old. :D 14:01:42 You'll be 512! 14:02:35 That spacing is misleading, since the exclusive-or binds less tightly than multiplication there. 14:02:55 :-D 14:03:21 He'll be 11. 14:03:49 Or 3, if you interpret it like he said. 14:03:57 hmm... INTERCAL can do Roman Numerals, at least for output 14:04:12 maybe Common Lisp was just making implementing it easier? 14:04:30 :-) 14:04:43 ais523: Have you any opinions on how to best represent an Othello board? 14:04:46 (Functional language.) 14:05:10 I'm thinking of some sort of function-based representation, something that reifies the concept of the continuous line into the way you access the board. 14:05:32 alise: I don't think I can come up with correct opinions 14:05:42 alise: not exclusive or. 14:05:44 exponentiation. 14:05:45 :| 14:05:46 based on what I'm doing at work atm, I'd come up with a functional translation of the OO way to represent it 14:05:47 Incorrect ones are fine too, ais523. 14:05:51 augur: Ohh you don't say 14:05:54 #boring, that way 14:05:58 no matter what the correct representation actually was 14:06:03 true 14:06:10 i could've done something more interesting 14:06:28 Wilful misinterpretation is the norm here, isn't it? 14:06:33 so basically, you'd have a function with arguments (method of accessing the board, argument to that method) 14:06:37 * Sgeo fails to see PLT on http://people.csail.mit.edu/jaffer/SLIB.html 14:06:40 wow, that is terrible 14:06:57 nicely abstracted and extensible, but otherwise terrible 14:07:40 Sgeo: slib sucks 14:07:51 Quadrescence will back me up on this... i hope 14:08:16 Ok, so what doesn't suck? 14:08:30 Nothing! 14:08:55 Me! It'd be illegal. 14:09:44 Speaking of which, where does the "put a sock on it" expression come from? (And don't reply with a line number.) 14:10:47 Condoms. 14:11:01 OBVIOUSLY. 14:11:18 Oh, that "it". 14:11:19 alise: hahahahaha 14:11:20 slib 14:11:22 slib blows 14:11:41 slib blows... anuses 14:12:37 So... does this mean for networking stuff, I'd be using the implementation's stuff? 14:12:46 Or is there anything else? 14:15:40 Just learn scheme 14:15:42 then do cool stuff 14:18:02 -!- MizardX has quit (Ping timeout: 248 seconds). 14:18:08 -!- ztirf4 has quit (Quit: Nettalk6 - www.ntalk.de). 14:19:01 * Sgeo gibbers a bit 14:29:53 axiom interact : Interaction pre final transform result → (ω:Worldish) → pre ω → (result → transform ω → Φ Worldish (λω₁ → final ω₁)) 14:29:55 "Or something." 14:30:04 I think Worldish has to be an opaque type. 14:30:21 That still lets us use the old world, though... 14:30:23 Oh, perhaps: 14:31:55 axiom interact : Interaction pre final transform result → (c:Conditions) → pre c → (result → transform c → Φ Conditions (λc₁ → final c₁)) → (ω:World) → (conditions ω ≡ c) → World 14:31:58 Except with all the bits involving World omitted. 14:32:09 Except then you just move the problem of worlds to the conditions. 14:32:27 I think I'm going to try learning Common Lisp 14:35:24 Hah. 14:36:41 Although I already know for a fact that I hate the names of some of the functions [saw a chart contrasting Scheme and CL] 14:37:34 AFK 14:51:19 -!- MizardX has joined. 14:54:07 -!- ais523 has quit (Ping timeout: 265 seconds). 14:54:45 -!- ais523 has joined. 14:55:15 ouch 14:55:28 my entire system was being really slow, for some reason 14:55:42 the DNS server in particular; I'm not sure if that's deliberate or not, but I changed the DNS to level3's 14:58:39 fop 14:59:14 fop? 15:00:03 alise: planned Feather syntax is [ x | f x ] <-- yay Feather! 15:00:25 AnMaster: I thought you only had one line of scrollback? or did alise invent that? 15:00:45 ais523, it's from the esoteric false rumours file 15:00:49 didn't you know? 15:01:00 haha, #esoteric so needs a rumors.tru and rumors.fal 15:01:01 ais523: he read the logs 15:01:06 not scrollback 15:01:19 I read highlights and their context in logs 15:01:19 rumors.tru: alise is a girl pretending to be a man pretending to be a girl. 15:01:26 latex genii: how do i make an invisible char the same width as another given char? 15:01:28 rumors.fal: #esoteric's logs come from sustainable forest 15:01:38 oh, I'll look it up 15:01:46 I know it's possible, and where to find out how, but not the actual command 15:01:58 ais523, \hphantom? 15:02:03 rumors.mu: This rumour is false. 15:02:08 alise: that sounds right, yes 15:02:14 ais523, what? 15:02:16 hphantom, I think ,yes 15:02:19 *think, yes 15:02:21 well 15:02:22 even works in TeXmacs 15:02:26 it is horizontal 15:02:32 there is a vertical version too iirc 15:02:41 AnMaster: gah, but it seems to treat it as not italic 15:02:43 or just \phantom generally 15:02:44 and possible one that does both vertical and horizontal (not sure about that) 15:02:47 alise, what? 15:02:54 very, very subtle spacing issues 15:03:03 alise: you could italicise inside the \phantom, or doesn't that work? 15:03:15 ais523, did I mention I put a -6 em vertical spacer at the top of a minipage yesteday? 15:03:21 yes a negative one 15:03:26 AnMaster: no, or at least not to me 15:04:00 nope, it's still too long 15:04:10 ais523, needed two mini pages side by side, one contained a display style formula, which some tests showed was responsible for causing it to be put below the other mini box 15:04:11 I'm trying to make _! look the same as the n! in the definition 15:04:12 _! : ... 15:04:13 n! = ... 15:04:24 so I'm doing \underline{\phantom{n}}, but the first line is too long 15:04:26 so I had to move it up using negative spacer 15:04:41 alise: oh, try \phantom{$n$} 15:04:46 that's a math n, not an italic n, presumably 15:05:20 ais523, err? does phantom inside math mode exit math mode? 15:05:46 AnMaster: I don't actually know; is it a math mode command, though? 15:06:16 ais523, I think it works in either 15:07:03 ais523, and since I normally use LyX, and LyX has support for phantoms without needing "insert tex code" it may abstract such things away 15:07:05 hmm, apparently so 15:07:48 alise: maybe it's a kerning issue? I can sort-of imagine that \phantom would block kerning, and some typefaces will attempt to kern together any two italic characters 15:09:34 what exactly is alise trying to do? 15:10:04 I mean, I saw what he said, but he didn't say what part of it should align 15:10:07 ais523: ! isn't italic 15:10:11 _! : ... 15:10:11 n! = ... 15:10:13 AnMaster: 15:10:14 hmm 15:10:15 _! : ... 15:10:17 n! = ... 15:10:22 _ and n should have same width 15:10:22 alise, if you want those to align on the : and = ? 15:10:25 i.e., ! and ! should align 15:10:26 hm 15:10:30 AnMaster: no, I already handle that 15:10:49 alise, I was about to suggest eqnarray environment or something 15:10:57 yeah, doing that 15:11:08 alise, also since n and _ are not in monospace there I assume? 15:11:21 then it might be hard to make them equal width 15:11:46 they're not 15:11:49 they're italicy variably thingy 15:11:59 AnMaster: why are you even suggesting monospace for a TeX-typeset document? 15:12:02 it's not an actual _ character 15:12:06 in the tex 15:12:07 ais523, I'm not 15:12:08 i'm trying 15:12:12 \underline{\phantom{n}} 15:12:17 but that's wider than n, somehow 15:12:20 perhaps the underline has padding 15:12:22 heh 15:12:38 alise, perhaps, why not add a negative spacer in there to compensate! 15:12:47 AnMaster: because that is missing the point of TeX 15:13:05 hmm, LyX goes out of its way to make it hard to make semantically incorrect documents, but it seems that people still manage somehow 15:13:17 AnMaster: because i'd have to get it totally exact 15:13:30 ais523, I would quote fizzie from yesterday on that, but I'm too lazy to grep the log file 15:13:34 -!- FireFly has joined. 15:13:39 ais523, wrt. negative spacers and latex that is 15:13:59 even positive spacers are normally semantically incorrect 15:14:03 ais523, also I have used mono space in a LaTeX document, for a code listing 15:14:11 also, this is texmacs; so almost identical but slightly different typesetting algo 15:14:16 but that is the only case I can think of 15:14:17 i imagine it's the same in tex thogh 15:14:19 *though 15:14:33 alise, why not LyX btw? 15:14:46 (/me remembers the Wikipedia advice to use positive space and negative space that cancel each other out to prevent LaTeX math rendering as HTML, and force it to render as an image, even if people have set their preferences to render as HTML) 15:15:05 AnMaster: because sometimes, it's faster not to use an IDE 15:15:10 whether for programming, or for typesetting 15:15:18 ais523, he said texmacs, not emacs 15:15:33 and texmacs has the same idea as lyx basically 15:16:05 -!- alise_ has joined. 15:16:11 AnMaster: because lyx is harder to use 15:16:16 however, my impressions of TeXmacs last I tried it were: sluggish user interface, blurry font rendering when editing (this might have been a fontconfig issue, I don't know), buggy import from LaTeX (this might not matter so much), much fewer features than LyX or similar 15:16:17 Someone paste the last few lines to me 15:16:17 got disconnected 15:16:26 (/me remembers the Wikipedia advice to use positive space and negative space that cancel each other out to prevent LaTeX math rendering as HTML, and force it to render as an image, even if people have set their preferences to render as HTML) 15:16:26 AnMaster: because sometimes, it's faster not to use an IDE 15:16:26 whether for programming, or for typesetting 15:16:26 ais523, he said texmacs, not emacs 15:16:27 and texmacs has the same idea as lyx basically 15:16:44 alise_, the line above that was where I asked "why not lyx" 15:16:50 (and you answered that) 15:17:03 The interface is not really sluggish for me, your display sucks, I don't care about LaTeX import, and LyX is a pain to use 15:17:03 alise_, I never found LyX hard to use once you learnt it 15:17:14 It looks exactly like .ps TeX output to me 15:17:16 further, I found it well worth the time it took to learn LyX 15:17:41 The interface is not really sluggish for me, your display sucks, I don't care about LaTeX import, and LyX is a pain to use <-- I said last I tried it, which might have been a year or two ago 15:18:01 in LyX: click click click click click click click click 15:18:15 alise_, no? there are keyboard shortcuts for everything in LyX reallyt 15:18:17 really* 15:18:27 and it shows them in the status bar when you select a command 15:18:29 right/center/left aligned eqnarray in the middle of the doc in texmacs: M-& 15:18:40 -!- alise has quit (Ping timeout: 252 seconds). 15:18:51 Go on then, what is the shortcut? 15:19:14 alise_, Ctrl-M, Alt-M T E 15:19:27 alise_, I had to look up the latter, because I very rarely use it 15:19:35 the former, "insert math formula" is ctrl-m 15:19:36 AnMaster: the leading control-M isn't needed for alt-M shortcuts 15:19:38 and I know that 15:19:50 it's harmless to give it, but you can omit it as an abbreviation 15:19:51 ais523, oh? well, since I so rarely use eqnarray 15:20:02 I haven't bothered learning that one 15:20:07 whoa, flood 15:20:09 everything after what-is-the-shortcut took ages 15:20:09 alise_, ? 15:20:16 ah 15:20:19 AnMaster: : he's lagging 15:20:23 right 15:20:39 and that second : was a tab-complete fail, assume it's a stray newt or something 15:20:41 and I'm not going to be like ehird and complain about other people lagging :P 15:20:41 Alt-M T E. Well, may be acceptable. 15:20:42 LyX has a windows binary, right? 15:20:59 ais523, XD 15:21:05 alise_, iirc yes 15:21:44 alise_, lyx tends to have somewhat emacs-y key bindings for some things, but you can configure that somewhere iirc 15:22:23 of course, if you haven't yet gotten used to lyx, keyboard shortcuts won't help you, it *does* take a while to learn 15:23:11 -!- alise has joined. 15:23:18 Maybe I'll try LyX next time, then. 15:23:32 I really ought to name my language someyear. 15:23:34 alise_, but yes you can always look at the status bar after clicking almost any button to see what the command is to insert that. And you can type \LaTeX commands directly in math mode (lyx will try to display it WYSIWYW style if it knows the latex command in question) 15:24:17 interestingly opening preferences in lyx shows (dialog-show prefs) 15:24:33 I wasn't aware lyx used anything lispish internally 15:24:46 AnMaster: you mean WYSIWYM? 15:24:56 ais523, ah yeah, thought it was "want" 15:24:57 AnMaster: it uses sexp notation for commands, I think 15:24:59 right "meant" 15:25:02 *WYSIWYG. WYSIWY[WM] is a lie. 15:25:16 -!- alise_ has quit (Ping timeout: 252 seconds). 15:25:29 alise: it's not pure WYSIWYG; for instance it shows nonstandard-width spaces with blue underscores with ticks on the end, rather than as blank space 15:25:30 alise, well, lyx is not WYSIWYG, because it shows it in a screen friendly font rather than exactly what it will look like 15:25:36 (for example) 15:25:47 and what ais523 said 15:25:58 also, it typesets relatively terribly, about as well as Word 15:25:59 What you see is not even what you get. 15:26:03 plus floats are shown as boxes with a thingy saying it is a float at the top 15:26:05 (although TeX typesets the finished product) 15:26:08 ais523, what does? lyx? 15:26:12 well maybe 15:26:14 AnMaster: yes, I mean onscreen 15:26:17 ais523: Oh snap. 15:26:40 alise, it can be set to instant preview math formulas though 15:26:55 when you leave the equation it will render it, takes a split second 15:27:05 not on by default iirc 15:27:08 AnMaster: so can auctex for emacs (that mode is a work of art, btw) 15:27:13 (possibly the nicest typesetting environment ever created) 15:27:17 hm 15:27:22 alise, why aren't you using that then? 15:27:42 because i can't be arsed to set up latex. and i don't really want to write a document template every time I want to ogle at how pretty my language is 15:27:52 speaking of can't be arsed to set things up on windows, 15:27:57 How should I install Ubuntu given that all I have is a costly 3G stick connection? 15:28:04 Ship-It is not an option. 15:28:10 alise, well, lyx would need latex installed somewhere it can run it 15:28:21 AnMaster: Oh. TeXmacs is self-contained. 15:28:35 (It isn't actualy TeX. Or Emacs.) 15:28:36 alise, perhaps the lyx windows installer includes latex? 15:28:37 *actually 15:29:40 AnMaster: put it this way: alise has tools that work, why would you force him onto different tools even if those also work? 15:29:42 http://www.gnu.org/software/auctex/img/preview-screenshot.png ;; yum 15:29:42 alise, I always use pdftex, it renders nicely and you can add a command to the document preamble so it does fancy microtyping with visually straight margins and what not 15:29:47 ais523, I didn't 15:29:55 he is free to choose 15:30:07 ais523: Well, I'll certainly try LyX now. 15:30:28 I've used it; it seems to be decent enough for what it does, but has a few annoyances 15:30:35 ais523, such as? 15:30:37 such as no easy way to type the prime character, as in a' 15:30:47 ais523, eh? in math mode? 15:30:52 AnMaster: yes 15:30:54 pressing ' doesn't work 15:31:13 ais523, it renders as a primelooking one in the instant preview for me 15:31:14 you have to do M-m e M-m ' 15:31:25 AnMaster: oh, but as a plain quote in the ordinary window? 15:31:29 how... ridiculous 15:31:34 -!- alise_ has joined. 15:31:39 Last 30 lines or so? 15:31:41 because there is a way to do a superscripted prime that renders as one in LyX 15:31:43 ais523, seems so 15:31:45 alise_: I'll pastebin 15:31:48 Not just since my last utterance; I probably missed things. 15:32:05 is clog broken? 15:32:29 ugh, sorry, this internet's being insanely slow today for some reason 15:32:36 well, this connection 15:32:37 ais523, well, they *could* be different, but to me they look pixel identical. But yes when editing they look different 15:32:49 http://pastebin.ca/1830126 15:32:54 AnMaster: No, but that's /two/ page loads, and this connection is... well... 15:33:02 also, this mouse is doing so badly I even just used control-C control-V to paste 15:33:09 ais523, you could also type \prime 15:33:13 which might be faster 15:33:15 umm, http://pastebin.ca/raw/1830126 for convenience 15:33:23 AnMaster: wouldn't you have to unescape the \ 15:33:32 I thought \ means \ (as in, $backslash$) in LyX 15:33:37 and it only did formatting if you told it to 15:33:37 ais523, ? In math mode it doesn't 15:33:45 ok, that's just silly 15:33:50 ais523, it shows auto completion for \commands in math mode even 15:33:52 very nice 15:34:01 especially as there's a perfectly sensible shortcut for command-introducer \ 15:34:06 although I forget what it is, offhand 15:34:09 -!- alise__ has joined. 15:34:16 ais523, you mean insert a tex box? 15:34:21 ais523, but looking at the view source I see: $ $$p^{\prime}'$ 15:34:26 -!- alise has quit (Ping timeout: 252 seconds). 15:34:28 So, 22.[15:27] How should I install Ubuntu given that all I have is a costly 3G stick connection? 15:34:29 but yes, that renders as two prime symbols 15:34:31 as far as I can tell 15:34:51 alise__: I'm not sure that you easily can 15:35:12 do you live near enough to someone with a stock of them to just ask them for one? 15:35:18 um, stock of CDs 15:35:19 AnMaster: does lyx let me write Aa(a->a) and get {forall} {greek a} ({greek a} {right arrow} {greek a})? 15:35:20 alise__: :( 15:35:21 ais523, anyway typing ^\prime was faster than the key combo you suggested 15:35:32 alise__, *tries* 15:35:46 ais523, what would the A do? 15:35:51 alise__: No. I could get to Birmingham in some hours, though, and stalk you! 15:35:53 err 15:35:53 AnMaster: you're turning me more and more off LyX as time goes on here 15:35:54 alise__, ^ 15:35:59 Presumably you have at least one Ubuntu cD. 15:36:02 alise__: nickping fail 15:36:07 A gives forall symbol 15:36:10 alise__: two, but they're both rather old versions 15:36:14 a gives alpha 15:36:15 alise__, \for completed the forall symbol here 15:36:24 AnMaster: A is faster 15:36:33 Does a give greek alpha? 15:36:38 Wow, this is the most confusing maze of nickpings ever. 15:36:49 alise__, why would it auto complete plain letters? 15:36:49 AnMaster: Does -> give right-arrow? 15:36:51 alise__: it's alt-M G a in LyX 15:36:57 for the greek a 15:36:59 tab isn't autocomplete 15:37:02 AnMaster: Does -> give right arrow? 15:37:22 -!- alise_ has quit (Ping timeout: 252 seconds). 15:37:27 alise__, in math mode? No, but AltGr-i seems to insert the latex one 15:37:42 Then LyX is useless to me. 15:37:54 I use TeXmacs because it lets me mainly type ASCII-ish stuff and get what I want. 15:38:06 alise__, well sure, if you don't like the exact key bindings 15:38:07 *shrug* 15:38:11 NN->NN^+{right arrow key}->a 15:38:14 gives 15:38:25 {blackboard N} {right arrow} {blackboard n with superscript +} {right arrow} {greek alpha} 15:38:26 alise__, does alpha give you a single alphpa? 15:38:28 alpha* 15:38:36 no, a does. 15:38:39 tab is not autocomplete. 15:38:42 tab is "variations" 15:38:48 alise__, on what? last letter? 15:38:52 for instance, | gives \vee 15:39:00 AnMaster: yes. 15:39:03 also, what if I want aleph instead? 15:39:08 alise__, how would one type that? 15:39:16 in TeXmacs 15:39:18 \aleph. it probably has some shortcut 15:39:26 also, @ is for circle stuff, so @@ = infinity, @+ = circled +, etc 15:39:27 alise__, not a? 15:39:30 it's actually very, very handy 15:39:34 AnMaster: maybe it is. maybe it's something else 15:39:39 aleph doesn't look like a 15:39:44 so it's probably not a 15:39:45 true 15:39:58 perhaps N 15:40:02 perhaps 15:40:10 -!- cpressey has joined. 15:40:17 alise__, what about an actual @? 15:40:51 Well, \text{@} works. 15:41:00 alise__, how verbose! 15:41:00 Which is actually \text@ 15:41:08 yes, very very verbose 15:41:09 A-$ also works for text. 15:41:12 A-$ @ right 15:41:17 I can just type a single @ 15:41:26 Now write infinity. @@ 15:41:30 Blackboard bold N. NN 15:41:34 + in circle. @+ 15:41:38 Right arrow. -> 15:41:55 Yeah, A-$ @ right is soooo horrible. 15:42:05 alise__, I wouldn't write @@, since it is on altgr here, that is not so easy as \infty 15:42:06 Especially as @ is /so/ /common/ in mathematics. 15:42:11 Of course, @ outside of an equation still produces @. 15:43:08 ais523, anyway, I find lyx have no major issues. A few small quirks sure. But then LaTeX itself has plenty of those too. And LyX does a reasonable job of producing a good result without a lot of fine tuning 15:43:21 AnMaster: the issue's mostly with the interface 15:43:28 I have no issues with the general concept, just the details 15:44:08 ais523, I would hate to edit in Computer Modern on a "normal" dpi desktop monitor 15:44:17 But you're okay with reading it? 15:44:23 Also, TeXmacs allows you to choose among fonts 15:44:24 Obviously. 15:44:31 alise__, well I wouldn't use CM unless I aim to print it 15:44:41 So choose another font. You are boring. 15:44:48 if it is primarily intended for on screen reading, I would use another font 15:45:34 alise__, my point was that I don't want WYSIWYG. I want to concentrate on the actual text and such first, and only at the end care about small formatting details 15:46:09 I don't feel like talking to you about this any more. 15:46:18 well, I have other things to do as well 15:46:45 I don't, but (nothing) is better than this. 15:46:51 [15:46] == #ω Illegal channel name 15:46:57 Fuck you, Freenode. 15:47:36 :P 15:48:09 ais523, if doing direct latex editing I found kile quite nice 15:48:23 auctex. No competition at all. 15:49:46 Microsoft Works is preinstalled on this computer. 15:49:47 Wow. 15:50:15 now you must use that instead! 15:50:18 Apparently Ctrl - = delete and Ctrl + is increase font size, but it's also its own inverse. 15:50:44 alise__, what? in TeXmacs? 15:50:50 how weird 15:50:52 No. 15:50:58 oh works? 15:51:00 In Microsoft Works Word Processor. 15:51:07 still weird 15:51:58 Works is awful 15:52:03 ais523: indeed 15:52:07 I know, I used to use it to some extent 15:52:09 ais523: Also, I implemented the Lambda Calculus of Continuations. 15:52:24 apart from the word processor; the computer came preinstalled with Works - word processor, and Word 15:52:51 ais523: Not interested? 15:53:25 alise__: vaguely 15:53:35 I was busy argumenting in two other channels, so was distracted even from a nickping 15:53:39 ais523: Hey, it's for Feather. 15:53:44 yay 15:53:53 what did you implement it in? Haskell? 15:53:59 Yes. 15:54:01 I'll pastie. 15:54:03 alise__, how well does bibtex integrate with TeXmacs? 15:54:30 AnMaster: TeXmacs is not tex at all. 15:54:49 alise__, well, what does it use for a replacement of bibtex then? 15:54:57 AnMaster: Dunno 15:55:46 ais523: http://pastie.org/861515.txt?key=n5pnirguwnncksdk7homzq. So, we have two main structures: 15:55:57 f(x,k) and (\x,k.E) 15:56:13 There are constraints: f must be a lambda expression, not another application. 15:56:16 erm 15:56:25 alise__: that's nice and short 15:56:28 There are constraints: in f(x,k), f, x and k must be lambda expressions, not applications. 15:56:55 In (\x,k.E), E must be an application. (I neglected to include this in my implementation) 15:57:03 (LCC t should be LCC App). 15:57:23 So, we have: no nested applications, and forced continuation "arguments". 15:57:39 It has the interesting property of making application a triadic operation (since k isn't "really" an argument) 15:58:01 Anyway, it's basicaly just the lambda calculus, except continuation-passing style is enforced. 15:58:16 I'll probably write a CPS-converter for it. 15:58:40 ais523: A disadvantage of my representation is that I can't pretty-print it without a lot of fuss. 15:59:22 hmm, yes 15:59:38 so what you've implemented is LC+continuations, but restricted such that CPS is enforced? 15:59:42 ais523: But that's no issue with the actual calculus. 15:59:46 Not +continuations. 15:59:50 Continuations are done with CPS. 16:00:14 It's basically a variant of the lambda calculus that replaces nested application with continuation-passing style. (But CPS isn't inherent in the model; you don't /have/ to "normally" pass things to k.) 16:00:19 My god, Works is still around? 16:00:25 cpressey: apparently so 16:00:27 (As in, you don't have to write "normal" functions that don't do stupid shit with k.) 16:00:31 IIRC, Microsoft are trying to get rid of it though 16:01:03 The first hit on Google is under microsoft.com/uk/ 16:01:16 Maybe it's a British thing. 16:05:24 -!- oerjan has joined. 16:07:15 Hypothesis: It is impossible to be comfortable. <-- it is possible for short moments, although only by accident, and if you try to prolong it it backfires horribly. at least that's my experience. 16:07:28 HTH 16:07:54 cps (LApp f x) k = cps f $ Lam $ \k' f' -> App k' $ cps x $ Lam $ \k'' x' -> App f' x' (Lam (\k''' r -> App k r k''')) 16:07:55 I made an error. Dammit. 16:07:58 alise__: I haven't had the time to encode the theory of rationals in it, but I do have in my proof-checking language a proof of a statement in Peano arithmetic: http://dpaste.com/169965/ 16:08:06 You may commence talkin' smack about it. 16:08:09 oerjan: I mean physical comfort, not mental-anguish-comfort. :P 16:08:32 alise__: i mean both 16:08:38 cpressey: Well look at that, you have specification of theorems now :P 16:09:07 alise__: It's just for clarity; itrepeated in the body of 16:09:12 the proof anyway 16:09:35 Or rather, its the first step of the proof 16:09:44 cpressey: that doesn't look like the Peano axioms that you've assumed at the start, but rather something else 16:09:54 and those feed on each other. for example my mental comfort is now helped by chatting on the pc. but eventually i'll tense up physically from doing so. 16:10:05 also, I love that qed is a keyword 16:10:08 ais523: I'm kind of leaving out the ones I don't need. Actually I don't need the zero? 16:10:11 I /very/ much like proof/qed as structures, though. :-) 16:10:21 hmm yes, looks like you don't 16:11:05 Kind of disturbing that it only relies on a fragment of Peano arithmetic, but it is very simple I guess 16:11:52 I'm working on another one which is more practical: prove that find(x,tree) always returns true or false if tree is a proper tree. That'll probably require extending this syntax with cases 16:12:09 like, case tree -> branch A B ... case tree -> leaf X ... 16:12:15 it's actually Qed. 16:12:16 oerjan: i think you have depression :P 16:12:16 well 16:12:17 or are just /the/ /most/ cynical person there is 16:12:23 Which means non-deterministic rewrite rules :/ 16:12:38 oerjan: what do you think of ultrafinitism? :D 16:12:38 cpressey: no, not really 16:12:45 find x (branch A B) -> ... 16:12:50 find x (leaf X) -> ... 16:12:52 same rewriting thing 16:13:01 Well, not "non deterministic" so much as "ambiguous outside the presence of cases" 16:13:15 I mean, to describe what is a tree 16:13:29 tree -> (leaf X); tree -> (branch A B) 16:14:13 if you rewrite App [Expr] | Symbol String | Free String 16:14:13 cpressey: easy 16:14:14 have it be a predicate 16:14:14 App [Symbol "find", Free "X", App [Symbol "leaf", Free "X"]] 16:14:14 vs 16:14:14 tree (branch A B) -> true 16:14:14 tree (leaf X) -> true 16:14:15 tree X -> false 16:14:17 alise__: (1) quite possibly. (2) don't really know what it is. 16:14:44 -!- BeholdMyGlory has joined. 16:15:42 alise__: Not so easy; to have predicates would require building a theory of booleans 16:16:06 -!- alise has joined. 16:16:29 Which clearly could be done, and might be done first to make this easier 16:16:32 oerjan: a crazy, crazy mathematical position: http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/real.pdf 16:16:43 -!- MigoMipo has joined. 16:16:44 that everything that cannot exist in this universe - like sufficiently big integers - does not exist 16:16:48 But then, I wonder if I would have to use predicates to prove theorems about my theory of booleans :P 16:16:53 yay 16:17:06 correspondingly, that "real" analysis is completely bunk 16:17:23 Or at least, that it does not "exist" 16:17:25 and that godel was wrong because all the impossible proveys are in fact merely meaningless 16:17:40 well not "wrong" but 16:18:08 (ii) the traditional real line is a meaningless concept. Instead the real REAL `line', is neither real, 16:18:10 (ii) the traditional real line is a meaningless concept. Instead the real REAL `line', is neither real, 16:18:11 oops 16:18:13 (ii) the traditional real line is a meaningless concept. Instead the real REAL `line', is neither real, 16:18:16 When a mathematican says "exist" they mean something quite specific 16:18:19 nor a line. It is a discrete necklace! In other words R = hZp, where p is a huge and unknowable 16:18:21 Oh "real" too :) 16:18:30 (but xed!) prime number, and h is a tiny, but not innitesimal , `mesh size'. 16:18:37 cpressey: the worst thing is /this guy is a professor/ 16:18:48 -!- alise__ has quit (Ping timeout: 252 seconds). 16:19:06 alise: That's bad, but there are worse, much worse, out there. This guy, being a mathematician, is relatively harmless. 16:19:12 Since mathematics is irrelevant. 16:19:16 (Sorry, I couldn't resist) 16:19:37 :-) 16:19:39 * oerjan beats cpressey with the saucepan of doom ===\__/ 16:20:23 * cpressey 's skull goes "BLONG" 16:20:31 alise: planck length anyone? 16:20:32 ais523: bleh, /you/ implement CPS for that calculus :P 16:20:40 oerjan: Planck length... OF THE REALS 16:21:29 For all reals R1 and R2 there exists a real R3 where R1 < R2 < R3. And by "exists" I mean "I CAN TOUCH IT" 16:21:41 Damn, scambled the order of those. 16:21:48 *R1 < R3 < R2 16:22:28 ais523: so, do you know what the bootstrap progam will look like for feather? 16:22:47 alise: not yet; I tried to write it in Scheme, but went mad 16:22:48 Also, Kronecker was wrong. God invented the *primes*. The integers I blame on the devil. 16:22:50 well R3 can be taken rational. although you still get problems with the sufficiently big integers. 16:23:05 ais523: well clearly it must be written in the lambda calculus of continuations! 16:23:05 cpressey: clearly then addition is demonic 16:23:16 cpressey: Ooh, a number system based entirely on primes? Tell me more 16:23:30 oerjan: that's the thing though, ultrafinitism means that not even infinite rationals exist 16:23:38 because you run out of integers to put on either side 16:23:42 alise: the problem was an infinite loop in trying to define "atoms", which is the next stage in the bootstrapping 16:23:57 alise: Well they have this remarkable property that, when you multiply them together, you can get any integer you want, so long as it's black. 16:24:01 ais523: hmm... atoms as in symbols, I presume 16:24:05 alise: yes 16:24:13 they're basically objects that can be compared to other atoms 16:24:15 atoms aren't the same thing as symbols :) 16:24:19 ais523: clearly you need renormalization :D 16:24:22 ais523: easy: 16:24:23 alise: atom as in Prolog 16:24:34 alise: the issue is making them forward-compatible with actual Feather atoms 16:24:46 you can use a fake-object at the start of the bootstrapping, but not later 16:24:58 symbol : a = (() -> ((b = (b -> bool)), a)) 16:25:02 also, the next bit is basically impossible to explain because a) I don't know how it works myself, and b) it's complicated anyway 16:25:12 alise: doesn't work 16:25:21 and the reason it doesn't work is, there's no implementation for the symbol you could use 16:25:35 That is, symbol is a function taking any old object (), and returning a pair of (a function whose type is (a function taking an object of the type of this function, and returning a boolean)), and another function of the same type as symbol. 16:25:44 ais523: well, symbols are identified by their name, right? 16:25:49 no two symbols have the same name 16:25:59 then make them lists of church numerals 16:26:18 yep, you can do that; but how do you return it using that typing? 16:26:44 Return it? What do you think this is, a library book? 16:26:55 * cpressey detonates an atomic symbol 16:26:57 ais523: well, you don't 16:27:04 you just implement: 16:27:09 'foo -> foo 16:27:15 because, presumably, your input is a string of characters 16:27:17 i.e. list of church numerals 16:27:19 so you have it right ther 16:27:21 implementing 16:27:26 sym= : symbol -> symbol -> bool 16:27:57 * alise runs into seeming issue with his LCC definition: typed magic means that, I think, I can't write a parser for LCC a :( 16:28:43 alise: typeclass restriction on a maybe? 16:29:06 (just a wild guess) 16:29:14 oerjan: hmm? 16:30:07 alise: say when deriving Read instances of things of the form T a, you frequently get the requirement that a also is a Read instance 16:30:21 -!- alise_ has joined. 16:30:25 s/things/types/ 16:30:27 everything said after (just a wild guess)? 16:30:35 alise: say when deriving Read instances of things of the form T a, you frequently get the requirement that a also is a Read instance 16:31:01 -!- fax has joined. 16:31:49 ah. 16:32:17 ais523: I'm writing a syntax for the Lambda Calculus of Continuations 16:32:23 alise_: this doesn't actually work, but http://pastebin.ca/1830205 16:32:29 that's the start of an attempt to implement Feather 16:32:44 if you run it, you get an infinite loop, due to the failed attempt to implement everything in terms of everything else 16:32:49 it'll provide sugar for the most common case of application 16:32:53 so e.g. this is what S will look like: 16:33:11 erm, never mind S 16:33:15 (haven't written sugar for that yet :D) 16:33:22 but, say you want to make a list 16:33:28 -!- alise has quit (Ping timeout: 252 seconds). 16:33:38 cons1 := cons 1; 16:33:45 erm 16:33:51 cons1 := cons 1 nil; 16:33:54 I can't even remember the difference between a fakeobject and an object offhand 16:33:55 cons2 := cons 2 cons1; 16:33:58 ais523: argh 16:33:59 shaddup 16:34:01 cons1 := cons 1 nil; 16:34:03 cons2 := cons 2 cons1; 16:34:09 cons3 := cons 3 cons2; 16:34:15 k cons3 16:34:26 that's k (cons 3 (cons 2 (cons 1 nil))) 16:35:20 I think K will be: 16:35:45 \x. <- (\y. <- x) 16:36:07 <- is bound to the most recent explicit lambda-abstraction's return argument if a name wasn't provided 16:36:09 so I think S would be 16:36:38 \x. <- \y. <- \z. xz := x z; yz := y z; r := xz yz; <- r 16:37:16 ais523: does that seem like a reasonable syntax to you? 16:37:17 hmm, I just realised my definition is incorrect, in that continuations shouldn't get continuation arguments themselves 16:37:18 ideally, it'd be possible to implement feather in it 16:37:19 hello! 16:37:31 ais523: it lets you do naming quite nicely 16:37:38 alise_: vaguely reasonable, yes 16:37:39 foo := id (\x. ...); 16:37:39 hi fax 16:39:21 cwcc := id (\f. r := f <-; <- r) 16:39:26 have a problem 16:39:35 that is the same thing as just (\f. f <-) lol :P 16:39:43 I need to (today and tommorow) solve some problems 16:40:14 ais523: you'd do IO by making the final continuation not in the lambda calculus of continuations, instead in the host, and returning a lazy stream of church numerals 16:40:15 but what will probably happen is I just sit on the computer doing nothing 16:40:49 fax: akrasia! or, well, the case more commonly known as procrastination 16:41:39 I need to solve lots of ODEs so that I am able to do it quicky and accurately (REALLY USEFUL SKILL!!) 16:42:13 my foot 16:46:46 -!- alise has joined. 16:46:48 http://us.metamath.org/mmsolitaire/mms.html 16:46:50 metamath solitaire 16:47:24 -!- alise_ has quit (Ping timeout: 252 seconds). 16:47:50 alise have you see sokoban in coq? 16:48:00 playing the game <=> proving a level has a solution 16:48:02 that one you wrote? 16:48:07 I didn't write it 16:48:10 (i stalked all your blog :P) 16:48:11 ok 16:48:12 then no 16:48:38 04:39:47 I'm not convinced that (\x. f x) is the same function 16:48:38 04:40:04 it certainly isn't in a strict lang if determining the value of f has side effects 16:48:48 it's not even true in haskell 16:48:57 haskell isn't pure though 16:48:59 cf seq 16:49:11 and it has the most evil thing of all 16:49:18 unsafe 16:49:19 RECURSION! 16:49:21 Perform 16:49:24 IO! 16:49:24 and 16:49:24 undefined! 16:49:27 fax: *GENERAL recursion 16:49:30 seq (\x -> undefined x) is different from seq undefined 16:50:07 fax: recursion is not the problem for eta reduction though 16:50:17 hm? 16:50:35 eta reduction : identifying \x -> f x with f 16:51:11 oh right I understand 16:51:11 it's consistent with pure lambda calculus, which can do recursion using the y combinator 16:51:21 -!- kar8nga has joined. 16:51:55 ais523: i have a real live copy of word 2007 here, let's see who was right about it 16:52:11 alise: metacontext? 16:52:23 as in, who said what to be right or wrong? 16:52:38 I said it probably isn't so bad, you said it's horrible 16:52:51 * fax needs help 16:53:06 btw there is an evaluation order called superstrict or something, which solves the problem of \x -> f x being f by actually evaluating f inside the lambda :) 16:53:17 that's sounds scary 16:56:38 oerjan: I used that (where legal under the as-if principle) in at least one of my Underload interps 16:56:49 for optimisation purposes 16:56:53 -!- zeotrope has joined. 16:56:55 hmm, or was it an Underlambda interp? 16:57:42 flit 16:57:56 flit? 16:58:10 `define flit 16:58:21 I know what it normally means, but it doesn't seem to make sense in this context 16:58:22 * a sudden quick movement \ * move along rapidly and lightly; skim or dart; "The hummingbird flitted among the branches" \ * a secret move (to avoid paying debts); "they did a moonlight flit" 16:59:00 I like Word 2007's equation editor 16:59:04 ;_; 16:59:07 clearly the second meaning is intended 16:59:24 Like flip but less upside-down; like blit but more fly. 16:59:53 flit would be a god name for an esolang 17:00:08 *good 17:03:43 -!- jcp has joined. 17:09:11 fax: constructivist metamath! 17:09:19 -!- tombom has joined. 17:09:21 -!- tombom has quit (Changing host). 17:09:21 -!- tombom has joined. 17:10:43 ?? 17:11:21 my proposal is more modest 17:11:23 fax: imagine metamath, but constructivist 17:11:33 it would be sweet 17:11:44 alise, do you want to do this? 17:11:49 and I mean literally do this 17:11:55 i think i do 17:12:03 it would certainly be cool. 17:12:27 I think so too 17:12:37 define this though 17:15:52 "filt" would be language with no explicit looping, but data being passed between components? 17:16:15 flit, not filt :P 17:16:38 Ah. 17:17:21 `define filt 17:17:22 * La Federazione italiana lavoratori trasporti il sindacato dei lavoratori iscritti alla Cgil che operano nel campo dei trasporti e della viabilit. \ [13]it.wikipedia.org/wiki/Filt \ 17:17:45 Molto relevante 17:22:47 there is also sv:flit 17:22:58 which I'm not completely sure of how to translate to English 17:23:01 `translate 17:23:08 var sl_select, tl_select, web_sl_select, web_tl_select;var ctr, web_ctr, h;var tld = ".com";var sug_lab = "Contribute a better translation";var sug_thk = "Thank you for contributing your translation suggestion to Google Translate.";var sug_exp = "Contribute a better translation:";var dhead = "Dictionary";var dmore = "View 17:23:10 err 17:23:14 how does one use it? 17:23:33 `translate sv en flit 17:23:35 En flit 17:23:38 err no 17:23:49 `translate en flit 17:23:52 A prolific 17:23:56 no! 17:24:35 well google translate gives: 17:24:37 "noun 17:24:37 1. DILIGENCE 17:24:37 2. INDUSTRY 17:24:37 3. ASSIDUITY 17:24:37 4. APPLICATION" 17:24:46 the second one seems completely wrong 17:24:52 the third one I have no clue what it means 17:25:00 the last one also seems suspect 17:25:38 oh, I know the concept you mean 17:25:46 "industry" has two meanings in English 17:25:50 oh? 17:26:00 `translate no en flid 17:26:01 so all 4 words give much the same meaning 17:26:02 no one industry 17:26:10 oerjan, I think I used it wrong 17:26:15 `translatefromto no en flid 17:26:17 diligence 17:26:25 AnMaster: in multiple words, think "tendency to work hard" for the second meaning 17:26:35 ais523, isn't that the meaning for the first one? 17:26:55 hey guyses :D 17:27:01 ais523, and that would be sv:flitig, flit is as google said a noun 17:27:08 the more common meaning is a collective noun for all the companies/factories that manufacture things 17:27:18 ais523, indeed 17:27:30 and "tendency to work hard" is a noun, as tendencies are nouns 17:27:49 fax: yeah i think constructivist metamath would be really awesome 17:27:57 especially if the proofs were actually in executable form 17:28:06 AnMaster: i think the second one uses a more original meaning of industry 17:30:08 Heh 17:30:19 I thought that was some kind of government slogan 17:30:33 DILIGENCE! INDUSTRY! ASSIDUITY! APPLICATION! 17:30:35 No One Industry, or Tendency To Work Hard? 17:30:40 oh :D 17:31:12 Adherence to these principles makes our society strong! 17:31:17 anyway, I think I know what sv:flit means 17:31:22 first word of Swedish I know! 17:32:15 ais523: from now on, you can choose from a veritable smörgåsbord of them 17:34:03 fax: it seems to me that for simple constructivist proofs, a list of the theorems/axioms (given standard proofs/values) you use along with their types is the best way of presenting a proof 17:34:18 And will help us solve a large number of ODEs in a short amount of time! 17:34:29 cpressey: wait, what? 17:34:43 assuming ODE = ordinary differential equation, that makes no sense 17:34:47 unless it's some sort of pun I don't getg 17:34:48 *get 17:35:04 ais523: i think it's a hint to fax 17:35:09 along with the type of the resulting composition 17:35:28 ais523: fax said e had to do a bunch of them a while ago 17:35:35 ah 17:35:52 ais523: I was riffing on what fax was saying earlier 17:35:53 also, whats with the Agoranese? 17:36:06 fax: + nested proofs, perhaps that's tc 17:36:07 the nose of agora 17:39:57 Thank you ais523, I am now exactly as confused about feather as I was before. 17:40:08 cpressey: so am I 17:40:15 There are fake things in it. I can tell that much. 17:40:21 Feather is ALL FAKE 17:40:22 For some meaning of "fake" 17:40:26 actually, that's an implementation technique 17:40:28 ais523: _clearly_ you need renormalization 17:40:39 Drat, so even the fake stuff is... fake 17:40:42 yes 17:40:57 well, no, because the details of the implementation are relevant to the actual lang 17:41:00 fake(fake(X)) -> fake(X) 17:41:03 hmm, I may have to leave again, my head's hurting 17:41:21 exists P. Component(Feather,P) & Fake(Fake(X)) 17:41:27 -> exists P. Component(Feather,P) & Fake(X) 17:41:35 So yes, there are fake things in Feather. 17:41:40 Even if they're not actually in it. 17:41:42 Q.E.D. 17:41:54 OK, so "relevant, but somewhat arbitrary" =/= fake, true 17:42:28 Fake(Fake(X)) -> Fake(X) is justified because a fake thing is fake. The fact that the thing was already presumed to be fake is irrelevant. 17:42:29 If a fake fake thing isn't fake, then what? 17:42:48 and how is something fake, true? 17:42:49 basically, a fakeobject is something that obeys a subset of the restrictions necessary to be considered an object 17:42:59 Fakeobjects, although fake, are actually real? So they're legitimate objects? No. 17:43:01 Feather, to me, sounds like a way to fold nondeterminism. For some ill-defined notion of "fold" 17:43:01 Nothing fake is true, obviously. 17:43:05 Now go make a logical system where ~~p -> ~p. 17:43:07 fakeobject != object 17:43:26 I must now goify for... 15 minutes? Do that logical system. Nao. 17:43:31 cpressey: that's an interesting analogy; and about as close to the truth as anything else about Feather that I've managed to put into words 17:44:07 cpressey: the poker sense 17:46:32 feather is folding nondeterminism because instead of giving a variable its multiple possible values at once, you give it them later on 17:46:39 so all previous continuations in some way account for this 17:46:44 potential nondeterminism 17:46:45 bye now 17:49:33 bye 17:56:27 I'm still trying to wrap my head around the plain ol' logical system. Namely, how to state proofs about the properties of the booleans, without invoking boolean logic. 17:57:32 Like, assume A and B are finite. Then rewriting (and A B) always terminates in one of these normal forms: {true, false}. 17:57:51 *finite and boolean expressions. 17:58:11 ? 17:58:43 I need to prove that I've implemented "and" correctly! Clearly, such complex functions are not to be trusted without proofs 17:58:52 :( 17:59:08 (I'm not serious) 17:59:42 But figuring this out might give me insight on how to approach more practical proofs 18:00:19 cpressey, I don't understand.... 18:00:49 you want to prove that a term with type bool is a boolean? 18:01:34 fax: Ah, see there is where I am in different waters from you and alise. My terms don't have types. 18:02:34 maybe this is the problem :P 18:07:27 Lack of types shouldn't be a huge barrier. 18:07:45 http://www4.informatik.tu-muenchen.de/~schulz/WORK/e-examples.html 18:08:14 * fax thinks if you don't have a type system you will implement it 18:08:38 which leaves the type system you choose to implement, up to you 18:08:43 -!- jcp has quit (Read error: Connection reset by peer). 18:08:48 oh well 18:08:51 "type" just means "set of values", anyway. 18:09:59 I'm having more trouble with variables 18:10:23 -!- jcp has joined. 18:11:17 cpressey, what about variables? 18:18:52 http://dpaste.com/170053/ <-- have cases now, but still need to tackle induction 18:19:28 fax: Well, I'm not sure. If I have variables, types look like predicates. If I don't, they look like nondeterministic/ambiguous rewrite rules. 18:20:30 It probably works out saner with the variables. But I'm finding it easier to do the other way. 18:22:21 The nice thing about this is, if you prove that terms of some form always reduce to some other form, you haven't just proved their type, you've also proved that they're total. 18:22:59 really?? 18:23:19 if you have a diverging term, can't you just prove it's anything? like a bool or a frog or whatever 18:23:32 (by baseless induction) 18:24:06 Well, if evaluating (and X Y) always results in a bool when X and Y are finite boolean expressions, then you know (and X Y) always results in *something*, therefore (and X Y) is total 18:24:19 If you have a diverging term, yes. 18:24:36 Hard to prove the type of a diverging term... 18:24:40 At least in this 18:33:27 grr, now i keep reading the word as "boo-lean" 18:33:32 Boo! 18:33:36 * cpressey tilts to the right 18:33:56 frightfullean 18:34:24 So, induction. Yeah. Fun stuff, teaching a computer how to do mathematical induction. 18:34:48 In MI one of your cases relies on the other. 18:34:54 Is it fair to call the base case a lemma? 18:35:03 of course 18:35:13 cpressey: an example of how better deptypes are 18:35:13 induction = recursion 18:35:23 you prove induction and the function it results in does recursion 18:35:32 induction is not recursion :P 18:35:57 Types are a crutch 18:35:59 the elaboration you did is good but "induction = recursion" is nonsense 18:36:57 Awkward to state it as a lemma because it only proves certain cases 18:36:59 yes i know 18:37:10 Awkward to have cases depend on previous cases too, though 18:37:20 cpressey, types are not a crutch, types are my wheelchair! I couldn't even move without them! 18:37:41 -!- alise_ has joined. 18:37:47 fax: I was going to say, dependent types are an ambulance :) 18:37:48 induction ~ recursion 18:37:49 is what i meant 18:38:11 now that's vauge enough for me not to be able to attack :P 18:38:44 cpressey: yes, they take suffering programmers and, after a while, where they undergo a change in their entire philosophy due to a near-death experience, they are converted into happy progammers 18:38:48 *programmers 18:39:09 too much dependent types and you'll need an ambulance 18:39:29 better dependent than delinquent 18:39:33 * alise_ bans oerjan from life 18:39:59 also it took me a while to realise that (exists (x:T). a) is a dependent tuple... 18:39:59 FWIW hardly anyone can actual program with dependent types 18:40:07 fax: MY LANGUAGE WILL FIX THAT 18:40:14 including alise :p 18:40:22 I don't think I can do the base case as a lemma in my system. A case isn't complete. So I think I have to go with cases being able to depend on previous cases 18:40:26 That's not SO bad, is it? 18:40:38 fax: why did you use sum rather than exists for the exists symbol btw? 18:41:03 convention 18:41:08 -!- ais523 has quit (Remote host closed the connection). 18:41:13 also 'exists' is a proof thing, Sigma is the data version 18:41:14 cpressey: forall P:Nat->*, P 0 -> (forall n:Nat, P n -> P (succ n)) -> forall n:Nat, P n 18:41:18 Prop vs Type 18:41:24 fax: why not have it polymorphic on both 18:41:26 -!- alise has quit (Ping timeout: 252 seconds). 18:41:41 i guess i'm still seeing proof elimination as an optimisation 18:42:22 fax: also is \sum or \sigma more correct? I think \sum since you have \prod for forall 18:42:30 although wait, doesn't that mean that \prod is the data version of forall? 18:42:33 Sigma 18:42:37 uppercase 18:42:42 er right 18:42:48 so \Pi is functions and \forall is just for profs 18:42:51 *proofs 18:43:07 which I think is taking it too far. which is why I think I disagree with separating \Sigma and \exists 18:44:13 feel free to tell me i'm stupid tho :P 18:44:30 fax: so \Sigma or \exists? 18:44:40 erm 18:44:40 I mean 18:44:43 fax: so \Sigma or \sum? 18:44:54 since we also have \Pi or \prod i bet sum 18:45:06 as the coincidence is a bit too much to accept 18:45:23 I don't know what \Sigma or \sum is 18:45:40 uh basically \sum is a big \Sigma like you use for sums.. 18:45:44 same with Pi vs prod 18:45:45 http://dpaste.com/170070/ <-- there's my stab at MI. 18:45:47 different unicode chars 18:46:19 cpressey: Not confluent! Waah! 18:46:25 * fax thinks "mathematical" induction should be primitive, and the other sort should be called "idiotic wrong induction" 18:46:52 wait, what /other/ induction does cpressey have? 18:46:56 alise_: What makes you think it's not confluent? Or are you complaining I haven't proved it such? 18:47:10 it... looks sorta nonconfluent :P 18:47:41 It pisses me off that I can't do (Foo (x:T). a) syntax myself 18:47:48 just (Foo T (\x. a)) 18:47:52 well 18:47:55 I guess 18:48:00 Foo_._ would work if you have (x:T) 18:48:01 | 18:48:01 |\ 18:48:02 presumably \exists and \forall are sums and products in a suitable category... 18:48:05 but (x:T) isn't anything coherent by itself 18:48:08 oh wait 18:48:09 I have no idea if "expand at least once on the LHS" and "expand to anything you want that's legal on the RHS" actually works, it only seems to, to me, right now. 18:48:13 Foo_(_:_)._ 18:48:22 oerjan: yes 18:48:23 duh 18:48:24 I have to prove properties about my proof system :/ 18:48:33 and then define Foo_._ ... but that's ambiguous I think 18:48:33 | 18:48:34 /< 18:48:44 myndzi: oh god not again 18:49:19 Any mathematicians here know anything about Galois connections? 18:49:20 Off by one too 18:49:22 fax: so data ∃(_:_)._ : (a : Set) → (P : a → Prop) → Set where right? 18:49:28 not -> Prop 18:49:30 -!- hiato has joined. 18:49:33 because you use exists to do the computable reals 18:49:36 oh no, off by one error \o/ 18:49:36 | 18:49:36 /`\ 18:50:06 oh wait Foo(_:_)._ isn't acceptable because i need to bind the var and stuff 18:50:52 myndzi: plus ten for that 18:50:53 No wait, case 2 doesn't rely on case 1 18:50:55 confused 18:51:02 galois connections rings a bell... 18:51:04 that can't be good 18:51:54 cpressey: just come to the dark side. 18:52:13 Uh, I need to prove boolexpr ~> boolean, that implies (not boolexpr) ~> boolean 18:52:38 obvious : ∀(P:Prop). Obvious P → P 18:52:50 Give me a proof that a certain proof is obvious, and I'll give you the proof! 18:52:54 Simple! 18:53:06 Obvious "P" -> P 18:53:21 fax: oh, good point 18:53:26 wait, no 18:53:29 it'd be more like 18:53:37 Obvious (x === x) 18:53:41 well forall x that is 18:53:52 hmm maybe you're right 18:57:03 It's not confluent in the sense that if you just used these rules in a rewriting system, and rewrote the term "boolexpr", you would generate infinite boolean expressions 18:58:14 But that is what "boolexpr" means (to me) (right now) (and this is loosely connected to Galois connections) and it certainly seems possible to ignore "runaway" cases when you give an explicit derivation. 18:59:25 Maybe those rules should be backwards, though. 18:59:33 true -> boolean, false -> boolean 18:59:57 That means true and false are indistinguishable 19:00:13 fax: I would use guillemets, though: 19:00:14 In a type system, they are. They're both booleans. I wanted a boolean result, great I have one. 19:00:15 obvious : ∀(P:Prop). Obvious «P» → P 19:01:04 The problem comes in that you don't want to rewrite them too early. Oh wait, I control that with the explciit derivation! 19:01:16 i'm not sure infinitely growing expressions is a problem for confluence, provided that at any step you can start reducing back down instead 19:01:22 *are 19:01:46 cpressey: a -> b doesn't mean that when you choose to rewrite a it results in b 19:01:50 it means that a is /just an alias/ for b 19:02:09 alise_: Not what it means to me 19:02:12 fax: I've been thinking about the interaction axiom 19:02:18 Not even sure what "just an alias" is supposed to mean in this context 19:03:19 axiom interact : Interaction pre final transform result → (ω:Worldish) → pre ω → (result → transform ω → Φ Worldish (λω₁ → final ω₁)) 19:03:24 (where capital phi was my dependent tuple) 19:03:25 or 19:03:26 axiom interact : Interaction pre final transform result → (c:Conditions) → pre c → (result → transform c → Φ Conditions (λc₁ → final c₁)) → (ω:World) → (conditions ω ≡ c) → World 19:03:30 both are unacceptable for the same reason 19:03:38 i.e., that the previous world/conditions don't become unacceptable 19:03:40 to use 19:03:44 so I need to eliminate them, somehow 19:09:34 -!- ais523 has joined. 19:09:39 "a little-known feature of the C standard: it explicitly states that pointer arithmetic is defined only for pointers belonging to the same memory block (i.e. statically or dynamically allocated array or structure). So when you write (char*)malloc(1) - (char*)malloc(1) you get undefined behavior" 19:09:41 ais523: verify? 19:09:49 apparently that's how the memory-safe C compiler works 19:10:01 alise_: yes, that's correct 19:10:08 ha 19:10:29 in fact, even comparing with < can cause a crash in some compilers 19:11:15 anyway, someone posted something in another channel that made Konversation segfault, apparently 19:11:22 I'm not sure whether to shout at them or congratulate them 19:11:46 * hiato chuckles to himself (c2h?) 19:12:35 ais523: hmm... this is making me want to write a pure c compiler 19:15:31 That's not such a little-known feature; it was mentioned on this very channel not many days ago. Though coincidentally only. 19:16:33 -!- alise has joined. 19:16:42 Why does -4^4 = -256 instead of 256? I'm only a high school student, but I know for a fact that -4^4 = 256 and not negative 256. 19:16:43 Is the typed ski + fix turing-complete? 19:16:55 http://community.wolframalpha.com/viewtopic.php?f=32&t=6774 19:17:00 fax: precedence 19:17:05 it's being parsed as -(4^4) 19:18:36 it was a quote 19:19:12 -!- alise_ has quit (Ping timeout: 252 seconds). 19:20:31 alise: it can do everything you need with church numerals can it not 19:20:44 so all recursive functions 19:20:55 oerjan: The point is that typed SK isn't turing-complete, presumably (because typed LC is not). 19:21:03 I'm talking idiotically typed, here 19:21:07 as in arrow and Base 19:21:19 The world’s best browser. Free download for Mac + PC. 19:21:24 So is idiotically-typed SKF complete? 19:21:26 they don't have a Linux version, though 19:21:32 ais523: Correct. 19:21:35 And? 19:21:38 the download page is specifically a Windows one, and they directed me to it 19:21:46 heh 19:21:55 I was messing about with browserchoice.eu 19:22:10 all their advertising doesn't say "os x and windows", but "mac and PC" 19:22:21 alise: hm iirc everything that can be typed in ML can be typed in simply typed lambda calculus with fix, just by duplicating things used with more than one type 19:22:39 vague recall as usual 19:23:28 anyone have that nice ~> symbol? 19:23:34 http://dpaste.com/170084/ <-- last cleanup for now. 19:24:00 ⇝ 19:24:03 is not so nice in my font 19:24:08 -!- kar8nga has quit (Remote host closed the connection). 19:24:14 -!- alise_ has joined. 19:24:17 no, it's just like --> 19:24:21 but the -- is wavy 19:24:38 ⇝ is the closest I can find 19:24:41 ais523: It is in the interest of both Apple and Microsoft to confuse people into thinking that the computer and OS are intrinsically bonded. 19:24:41 I can barely see the squiggling at this font size, but it's there 19:24:43 "rightwards squiggle arrow2 19:24:44 *" 19:25:02 Gregor: I suppose so 19:25:12 except then, why do Apple advertise Parallels? 19:25:16 Maybe it's just a latex thing 19:25:18 Gregor: More so Apple than Microsoft. 19:25:28 nah 19:25:32 pikhq: I would say about equal. 19:25:37 apple even have parallels on their apple store computers 19:25:42 Since Microsoft doesn't care *too* much so long as their OS is running on it. 19:25:46 you think microsoft would advertise mac compatibility? 19:25:55 apple are a hardware company, microsoft not 19:26:04 ais523: They don't advertize Parallels as something to run Linux on, they advertize it as if Windows is just as magically bonded to it as to a PC. 19:26:04 ok then, what about the => char? 19:26:07 that is also acceptable 19:26:10 Apple is first and foremost a hardware manufacturer, and sells their hardware based on OS features. 19:26:16 Gregor: ah, maybe 19:26:52 Although their reasons for wanting people to think there's a magical bond are different, they both have the same want, and probably about to the same degree. 19:26:52 As long as Apple are not a grammar company. 19:27:16 For Apple it's about getting money for something that has little to no benefit in and of itself, for Microsoft it's about squashing all competition. 19:28:00 -!- alise has quit (Ping timeout: 252 seconds). 19:28:41 What Microsoft wants is to confuse people into thinking that "Microsoft" == "program". 19:29:35 Dude, I downloaded this Microsoft, but I think it was spyware, it installed like eight other Microsofts on my Microsoft! 19:29:52 Yes, exactly. 19:30:13 static discharge against a car *through thick gloves* 19:30:13 wth 19:30:16 Gregor: what has little to no benefit? 19:30:18 anyone can explain that? 19:30:45 AnMaster: woolen, or leather? 19:31:01 alise_: The hardware, without the software. It's pretty good as hardware goes, but it's not so good to be worth its rather high price :P 19:31:15 ais523, wool/acrylic mix I think 19:31:27 Gregor: I actually investigated that a while ago. It turns out that actually it's pretty reasonably priced for the components and the boutiqueness of Apple. 19:31:29 possibly some cotton as well 19:31:39 The markup is something like 30% on the lower-end models, typical of boutique products. On the higher end models? Less. 19:31:40 "Boutiqueness" 19:31:45 Yes :P 19:31:50 WTF is "boutiqueness" 19:31:57 AnMaster: well, there are probably air gaps inside the gloves; pushing against the car (say to pull a handle) would have compressed it to the extent that you could get a spark between your skin and the metal of the car through them 19:32:03 The image of it being a high quality product because of its social/fashion status. 19:32:07 Cachet. 19:32:17 alise_: Uhh, isn't that exactly my point? 19:32:27 Gregor: Yes, but it's not a hugely unreasonable margin. But. 19:32:40 For instance the 27" iMac is pretty good value, actually. Just the 27" IPS display would cost about as much as the lowest-end model of it. It's a very expensive component. 19:32:42 ais523, actually by that point I had just laid my finger against it, hadn't yet had time to push the door closed 19:32:58 so it must have been a huge charge 19:32:59 The higher-end model of it comes with a Core i7 - at that point the profit margins just keep diminishing. 19:33:03 the issue is not that Macs are overly expensive for a high-end model, IIRC, but that they don't offer low-end models 19:33:06 still feels somewhat from it in my thumb 19:33:13 It's something like $3k for the whole lot. Add in the huge cost of the the-whole-fucking-thing-is-one-gigantic-bit-of-aluminium... 19:33:28 And the top-of-the-range 27" iMac is probably the cheapest way to get all those components. 19:33:30 I don't think we fully understand static electricity 19:33:31 ais523: pretty much 19:33:37 and its low range has a higher-than-average profit margin 19:34:01 cpressey, oh? 19:34:02 I have seen it be very bad in humid environments and very mild in dry environments in the winter 19:34:12 Which is not how I was told it was supposed to work 19:34:21 cpressey, I usually see the reverse of that 19:34:28 a *lot* when try 19:34:29 dry* 19:34:35 and not very much when humid 19:34:45 I don't doubt it, but maybe there is some other correlate 19:35:06 cpressey, perhaps something specific to that environment? Or was the observation made in different places? 19:35:09 cpressey: static electricity discharges through the air faster when it's humid, but that isn't to say you can't charge it up 19:35:37 the way static electricity discharges from humans work is, you normally build it up over time walking on carpets, etc, and when you touch metal it discharges through that 19:35:43 and if it had charged up far enough, you can feel it 19:35:50 Different geographical locations, yes, I would guess it might vary on something else that was different between them 19:36:09 alise_: what about ↝ 19:36:46 ais my cats ears 19:37:20 Ohhey, looks like we traded out Miss Piggy. 19:37:48 It's now a fax. 19:40:17 Yup 19:40:37 Gregorification. 19:40:52 GreGLORIFICATION 19:40:56 lol 19:41:17 GregLOLification 19:41:37 How Gregarious it is to Greglorify. 19:42:01 dulce et gregorum 19:42:53 Definition DiscreteDerivative (f : Z -> Z) (x : Z) := f (x + 1) - f x. 19:43:34 Notation "∆" := DiscreteDerivative. 19:43:39 alise paying attention?? 19:45:05 huh what now i am 19:45:16 fax: what about it 19:49:21 http://pastie.org/861902.txt?key=71fbadzjph5ovvw9xvbkxa this is pretty but not valid 19:49:42 because `⟪∗⟫ = ∀a. SKF a` means that ⟦_⟧ is too fancy for its own type :( 19:49:44 re. your earlier question: YES 19:50:02 I've forgotten the earlier question. I ask so many... 19:50:31 SKI is equivalent to STLC, but STLC + fix is recursive 19:50:53 by SKI I assume you mean STSKI there 19:50:56 yes 19:51:36 so cool 19:51:46 if my interpreter wasn't broken i'd have done sum tc'ing 19:51:50 mind it is particularly pretty broken code 19:55:25 fax: so why did you define discrete derivative there? 19:55:43 making sure coq is ready for the new age of ultrafinitism? :D 20:01:20 * alise_ tries to devise a logic in which !!x = !x 20:01:41 I'm implementing the finite calculus! 20:02:56 fax: cool 20:02:57 how does Notation work btw? 20:03:42 |||||||||||||\\\\\\\\ 20:04:51 finitists can't have limits either? How do you do calculus at all? 20:05:07 just numerically, with some estimate of the error? 20:05:25 lament, finite calculus is about finite sums :D 20:05:29 lament: i'm talking ultrafinitists here 20:05:32 -!- Azstal has joined. 20:05:40 like Sum[i=1..n] i^2 20:05:46 if IE wasn't being a bitch I'd link you 20:06:03 what specifically's the problem with IE? 20:06:14 thanks, i don't really wanna know 20:06:17 lament: http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/real.pdf 20:06:21 lament: oh you do, it's hilarious 20:06:29 no i really don't trust me 20:06:35 YES YOU DO :| 20:06:42 ais523: all keyboard shortcuts and commands are being ignored 20:06:51 err, wow 20:06:57 lament: basically there's some defined mesh size of the reals 20:06:58 I'm pretty sure that isn't intentional behaviour 20:07:03 and you treat it as an infinitesimal 20:07:15 (actual, real mesh size, as a "universal constant") 20:07:39 let's say it's 1 20:07:58 since it's gotta be scale-invariant anyway 20:08:11 nice. Reals = Integers. 20:08:16 lament: in real.pdf he does it paramaterisabled 20:08:19 ified 20:08:21 -!- Asztal has quit (Ping timeout: 258 seconds). 20:08:25 -!- Azstal has changed nick to Asztal. 20:08:27 cpressey: and the integers are finite 20:08:31 or more precisely the integers don't exist 20:08:32 probably easier to prove it's scale-invariant and then set it to 1 20:08:40 fax: vacuous : ∀a, (P : ⊥ → ⋆), (x:⊥). P x! 20:08:55 "exist" is more precise than "finite" now is it 20:09:05 ⋆? 20:09:06 cpressey: :D 20:09:14 fax: supertype of set and prop 20:09:43 but what's the ultrafinitist perspective on nullity?? 20:09:55 lament: it's totally yeah man 20:10:25 needs more skolemization 20:10:31 alise_: is that pdf meant to be serious? 20:10:37 ais523: yes 20:10:41 zeilberg is a fucking nutcase :) 20:10:42 I can't tell whether it's a parody, or just deluded people 20:10:56 btw this guy is a professor 20:11:16 vacuous {_} {_} {x} = explosion x 20:11:19 hooray for ex falso quodlibet 20:11:43 "truer" 20:11:47 the best thing is though you can say that 20:11:50 I totally agree. 20:11:57 ∀(x:⊥). x ≠ x 20:12:14 and all sorts of fun stuff besides 20:12:26 "Analogously, my own best ideas, far surpassing anything in my ‘serious’ papers, are contained in my annual April Fool’s jokes, sent to my E-correspondents and posted on my website. This way I can express my ‘off the wall’ ideas without being considered a crackpot." 20:13:00 isn't a similar principle used for distributing INTERCAL? 20:13:05 alise_: if you define !x = x then you get !!x = !x for free ;D 20:13:16 oerjan: hahaha no. 20:13:51 another option is the modal necessity operator 20:13:57 alise_: it's unprovable that all that is wrong; no matter how small a number you suggest, it's always possible that the mesh size is smaller 20:14:02 -!- alise has joined. 20:14:17 alise_: it's unprovable that all that is wrong; no matter how small a number you suggest, it's always possible that the mesh size is smaller 20:14:26 -!- oklokok has joined. 20:14:46 ais523: yep, except not quite 20:14:50 it can't be smaller than the planck length 20:15:02 well unless you pack multiple bits of info into one tiny particle 20:15:07 well 20:15:09 who says that maths and physics have the same fundamental measurements? 20:15:12 i guess not in zeilberger's ultrafinitism 20:15:23 but most ultrafinitists are such because of physical limits 20:15:35 i.e. you can't have an infinite set of natural numbers because you can never compute it all 20:15:54 you can't have a really tiny rational because there isn't the space to show its tininess 20:16:16 I love the talk about sqrt(2) not actually existing after all, because distances don't exist, just areas 20:16:39 Math is a consistent fiction. 20:16:47 Guess what? It's the consistent part that's important. 20:16:55 *"consistent" 20:17:04 "consistent" fiction 20:17:06 LIKE ZFC 20:17:22 ZFC is too powerful for my taste. 20:17:30 -!- alise_ has quit (Ping timeout: 252 seconds). 20:17:32 I like simple theories. 20:17:36 Like !x = x. 20:17:53 I thought you liked consistency :P 20:18:15 ais523: I like how he says that Goedel is "irrelevant" because the things it applies to have no meaning 20:18:16 Well, I ilke !x -> x better. 20:18:20 but that isn't even implied by rejecting all infinites 20:18:26 goedel numbers are huge but not infinite... 20:18:34 and certainly not so huge that we can't represent them 20:19:31 I'm restarting IE. 20:19:45 * fax wonders how to write (x+1)x(x-1)...(x-m+2)-x(x-1)...(x-m+2)(x-m+1) in a proof assistant 20:19:53 fax: just write it :P 20:19:55 "..." means induction I guess 20:20:14 fax: zeilberger will love you 20:20:19 are you defining R := his definition too? :D 20:20:20 mesh size! 20:21:41 -!- alise_ has joined. 20:22:02 -!- whtspc has joined. 20:22:03 what I missed I desire elaboration upon 20:23:14 -!- whtspc has quit (Client Quit). 20:23:39 Wow, what insane garbage. It's not that I inherently object to his premise, either. It's far more that he tries to buttress it with crap. 20:24:03 His writing style is putrid. I'd much prefer my own whiny. 20:24:50 -!- alise has quit (Ping timeout: 252 seconds). 20:24:52 Also, I have an unstoppable urge now to define his paramaterisable finite universe. 20:24:54 "Suppose x is even." "Well suppose it's not!" 20:25:52 hehe 20:28:42 Presumably the mesh size h is an ultrafinitist-rational. 20:28:44 And p is an ultrafinitist-natural. 20:28:49 I imagine he'd just freak out at concepts like "Turing-complete". I mean, you *can't* have infinite memory. You just *can't*. 20:29:13 The problem is that the Ultrafinitism module is paramaterised over h and p, so how do you do it? 20:29:29 I didn't read it as being parameterized. 20:29:36 I read it as h is a constant. 20:29:47 A very small, unidentified constant. But not variable. 20:29:52 Oh, yes. 20:30:01 But he parameterises it later in his analysis. 20:30:06 Oh nice. 20:30:15 (Because you don't know what it is.) 20:30:22 And, of course, we don't know their True Universal Values, so for now we must specify it 20:30:31 Trying very very hard not to LOL, natch. 20:30:34 (me) 20:30:46 Until the Ultrafinitist Physicist Association of America completes its experiments. 20:31:40 With their grant from NAO2^{80}PSA, the National Aeronautics and Observable 2^80 Particles of Space Administration. 20:33:23 fax: are you sure you don't have the link to that site 20:33:28 what site? 20:33:41 it says it was a book that claimed to be from the future, with a bunch of formalised mathematical proofs in it 20:33:50 saying that oh in the past they did this all by hand ha ha ha 20:33:50 I told you I don't know what you're talking about 20:33:53 and it defined a bunch of maths in it 20:33:56 ugghh yes you do you linked to it 20:37:35 just explain it so that I understand what you meanl 20:37:38 fax: it was either in maple or ... i think coq 20:37:48 its name was an acronym, i think a deliberately-amusing one 20:37:51 Ah Zeilbergers book! 20:38:02 haha same guy? 20:38:04 http://www.math.rutgers.edu/~zeilberg/GT.html 20:38:09 how come it wasn't ultrafinitist 20:38:20 Zeilberger is one of my idols 20:38:23 well 20:38:33 you /idolise/ this insane man? 20:38:38 I don't really have idols but I really enjoy his work 20:38:40 he doesn't believe there are any infinite sets... 20:38:50 have you ever seen an infinite set? 20:39:19 (and don't say, yeah in my ZFC textbook: I can write "magic rainbow unicorn" on a bit of paper too) 20:39:27 no, i mean exist as in mathematically 20:39:36 he thinks the definition of the reals is R = hZ_p 20:40:04 No, he thinks it should be 20:40:06 yes, but he's /talking/ about abstract systems 20:40:19 that's radical 20:40:33 and talks about the REAL real line 20:40:33 as if anything abstract is "real" 20:40:37 -!- Gracenotes has joined. 20:40:38 I think if you gave me an infinite amount of time and an infinite lifetime and an infinite supply of paper I could show you an infinite set 20:40:49 *lifespan 20:40:51 -!- alise has joined. 20:40:58 fax: it's a word starting with r 20:40:58 but not radical 20:41:00 i'd go for retarded 20:41:23 no you couldn't, {a^n | n \in N} doesn't contain an infinite word 20:42:25 That's true, it doesn't even, at that. 20:42:53 All the more reason to go ultrafinitish! 20:42:57 fax: seriously the fact that you don't see real.pdf and immediately realise that this guy is completely idiotic shakes my faith in things you say 20:43:29 But wait, it's still an infinite *set*, right? 20:43:58 :P 20:44:08 N = {0, 1, 2, 3, ..., p} 20:44:11 hmm, actually 20:44:18 he never says p is the biggest natural 20:44:19 you are young alise, sometimes you say things which rembind me of that 20:44:20 or indeed the biggest prime 20:44:30 obviously it must be the biggest prime or the definition of R would make no sense 20:44:45 so |N| = p and a bit :P 20:44:54 cpressey: yeah, but at any point you'll have an element of {{a^n | n = 0, ..., k} | k \in N} 20:45:00 -!- alise_ has quit (Ping timeout: 252 seconds). 20:45:11 -!- alise_ has joined. 20:45:33 "oh you don't understand the subtle adultness of considering ultrafinitism... you have to be older to know these things... one day... one day" bullshit 20:45:50 lol 20:47:20 I would probably describe myself as a mathematical generativist, or something. 20:47:36 constructivism, hells yeah 20:47:49 Not exactly constructivist. 20:48:24 i was just asserting my own position 20:48:39 I was just clarifying my own :) 20:49:02 -!- alise has quit (Ping timeout: 252 seconds). 20:50:03 alise_: why wouldn't the definition of R make sense if p wasn't prime? 20:50:24 needs a prime p to be a field ? 20:50:26 i don't really even believe in finite numbers, actually i often wonder whether i exist 20:51:00 It's a matter of whether you regard computations to "halt" or not, I think. 20:51:01 it's not a field, p is so big you can't actually do division 20:51:03 now THAT is radical 20:51:31 CA's never "halt" unless I have some way to recognize what I want "halt" to look like 20:51:33 oklokok: nonono, he asserts that it is prime 20:51:33 but it makes no sense to arbitrarily restrict R's size when the whole point is "there is a limit to these things" 20:51:33 fax: it's not a field, big + n is undefined 20:51:33 oh wait it's modulo 20:51:42 TMs are assumed to "halt" because recognizing it is trivial 20:51:58 * cpressey loves the alisedumps 20:52:06 at least that's how i see ultrafinitism, p sets the bound on anything we do, so if we wanna divide, we run out of Z_p when we try to find the number near p that's the inverse 20:52:45 there is an inverse but it's incredibly big so it's irrelevant 20:53:06 cpressey: alisedumps? 20:53:08 i'd say inverses come from assuming we have such big numbers that when dividing them by each other the rounding errors don't matter :o 20:53:12 no coppro is the poo-lovin' guy 20:54:17 cpressey: what's a matter of whether to regard computations to halt or not? 20:54:26 the constructing an infinite set thing? 20:54:43 alise_: Every so often 4 or 5 lines from you show up at the same time, presumably due to your web->irc gateway thing 20:55:06 cpressey: just 3g stick lag 20:55:08 oklokok: Whether there are finite numbers, or not, or infinite numbers, or not 20:55:17 1 = 1.0000000000.... 20:55:24 i don't see a connection 20:55:42 1 has halted 20:55:44 is 1.0000... an infinite number? 20:55:49 1.0000000.... never halts 20:55:56 Why wouldn't it be? 20:56:18 well it's impossible for 1 to be finite and 1.000... to be infinite, because they are the exact same object 20:56:34 so in fact we're working in some sort of universe of representations here? 20:56:57 * cpressey shrugs 20:57:08 * oklokok too 20:58:04 -!- oklokok has changed nick to o|{|_o9o|_. 20:58:09 i'm not very leet 20:58:24 -!- alise_ has set topic: arys. 20:58:28 oops 20:58:32 i should go clean up random parts of the apartment 20:58:33 -!- alise_ has changed nick to arys. 20:58:42 ~~> 20:58:47 Of course, the ultrafinitist, along with their unacceptance of the concept of Turing-complete, will find the Halting problem trivial. All machines always halt, due to entropy. 20:58:56 -!- arys has set topic: q. 20:59:41 -!- ais523 has set topic: "Gwandocu (n): Extremely strong evidence, far beyond a reasonable doubt." | alise sighting counter currently out of sequence | http://tunes.org/~nef/logs/esoteric/?C=M;O=D. 21:01:19 due to entropy? 21:01:21 DFEHGJIKGMLINGPOQIKG$L5RS&TUMVGJI@WJX)YZE)[\R?G^]NEHGJIKGLINGMSR?'aOcbML5R?d5GJVI@L5[\eS&TUMVGJI@WJf - zeilberger 21:01:21 oops 21:01:22 fucking copy from pdf 21:01:33 http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/goodwin.pdf 21:01:41 he isn't even consistent about ultrafinitism 21:01:44 see first paragraph 21:02:07 joke paper, but 21:02:46 Perhaps he believes Aleph is a finite value. 21:03:02 p+1? 21:04:45 -!- lament has quit (Ping timeout: 245 seconds). 21:04:45 now now he never said that x in N -> x < p 21:04:46 he just /strongly implied/ that there is no bigger prime than p 21:04:59 -!- alise has joined. 21:06:51 -!- lament has joined. 21:06:53 fax: should i learn coq? 21:07:45 how i stopped worrying and learned to love the coq 21:09:12 -!- arys has quit (Ping timeout: 252 seconds). 21:09:49 Eval compute in Discrete_Definite_Integral 1 5 (fun x => x). 21:09:55 = 10 21:09:55 : Z 21:12:00 paste the code somewhere 21:12:16 = 1 + 2 + 3 + 4 + 5 21:12:47 10 =/= 1 + 2 + 3 + 4 + 5 21:12:49 * fax is about to prove Fundamental_Theorem_Of_Finite_Calculus 21:12:52 fax: err... 21:12:53 yeah :P 21:12:58 cpressey, it's correct within experimental error 21:13:01 Unless it does 21:13:06 OK, I'll buy that 21:13:09 fax: experimental error my arse :P 21:23:14 So, my woes are all because a mock object is not sufficiently mocking the the thing it set out to mock, huh? 21:23:22 Nice. 21:32:48 the discrete definite integral from 1 to 5 is the sum from 1 to 4 21:32:59 = 10 21:34:27 -!- hiato has quit (Quit: leaving). 21:35:24 fax: show yer koed 21:35:46 it's because given f we're computing a function g such that g(x+1) - g(x) = f(x), so the sum of f(x), where x goes from a to b is g(b+1) - g(a) 21:36:21 The code sounds like it would be trivial to me. 21:36:28 Who's the o guy...ah, should've guessed 21:36:35 should be pretty trivial 21:37:04 cpressey: yeah but proving fundamental theorem of finite calculus will be fun 21:37:25 what i just said is basically the proof 21:37:38 although i skipped it completely because it's obvious 21:37:54 i mean the "it's because given f ..." thing 21:38:45 no wait actually what's the fundamental theorem 21:38:58 alise, I will when it's done 21:39:12 I'm still working on proving Fundamental_Theorem_Of_Finite_Calculus 21:39:23 can you link the paper? 21:39:27 o|{|_o9o|_: inversitude 21:39:34 presummyby 21:39:43 woah you guys are talking about finite calculus too! what a coincidence 21:39:48 * ais523 reads about the Trojan Horse found in the drivers for a battery charger 21:39:58 fax: because of you :P 21:40:02 aren't we talking about finite calculus because you brought it up? 21:40:23 it's funny seeing the arguments "well, if a battery charger connects to the Internet there's probably something wrong with it" vs. "why on earth would a battery charger company check to see if it connects to the Internet anyway?" 21:42:26 so what's the fundamental theorem? 21:42:35 or alternatively can someone link the paper? 21:42:57 the finite calculus paper? http://www.stanford.edu/~dgleich/publications/finite-calculus.pdf ? 21:43:02 thanks 21:43:12 I thought you already had it 21:44:58 okay yeah then i proved it by saying it's obvious 21:45:10 well i did, i didn't know i did 21:45:41 I don't know how to correct that impression 21:46:32 the theorem doesn't actually have any mathematical content, it's just stated for convenience, so you don't have to think about what happens on the boundaries of the sum and the integral every time 21:46:51 not so! 21:47:12 I'm not some open source hater by any means, but I think the chances that someone who gave a shit about the source of a freaking battery charger driver would be exactly the type of person who would never be dumb enough to buy a battery charger that needs a windows driver install. 21:47:18 this is one of the best flamewars I've seen for a while 21:48:35 It makes me sad 21:49:26 * fax proved the fundamental theorem :D 21:49:49 Right on. 21:49:55 #esoteric is full of proofs today 21:50:00 Maybe we'll open up the bonus level 21:50:03 i really don't see what there is to prove 21:50:18 o|{|_o9o|_, I mean formal proof 21:50:38 if you sum adjacent values of f(x+1)-f(x)'s, obviously all but the left and rightmost ones cancel out 21:50:41 oh in coq? 21:51:02 then i obviously have no idea how hard it is 21:51:04 o|{|_o9o|_, oh and, I used "The Fundamental Theorem" as my definition, which means MY fundamental theorem is their definition 21:51:33 not very hard because Z has already a fair bit of theory in the standard library, without that -- this would not be possible 21:51:54 i believe you 21:51:55 clearly you need to use coq's "obvious" tactic 21:53:12 -!- alise has quit (Ping timeout: 252 seconds). 21:53:33 -!- Daexpos has joined. 21:54:00 Who is the exoterisc? 21:54:38 Him! 21:54:39 Pene 21:54:40 * cpressey points 21:54:44 -!- Daexpos has left (?). 21:55:07 And all present were enlightened, I'm sure. 21:55:15 Pene. 21:55:35 that's the ablative of penis, right? 21:55:56 Fax intends to ablate your penis. 21:56:14 fricative 21:56:16 I don't know what ablate means, but it sounds painful. 21:56:16 ouch 21:56:23 `define ablate 21:56:26 * wear away through erosion or vaporization \ * remove an organ or bodily structure \ [14]wordnetweb.princeton.edu/perl/webwn 21:56:37 It is in fact quite painful. 21:56:47 `define fricative 21:56:49 * fricative consonant: a continuant consonant produced by breath moving against a narrowing of the vocal tract \ * of speech sounds produced by forcing air through a constricted passage (as `f', `s', `z', or `th' in both `thin' and `then') \ [18]wordnetweb.princeton.edu/perl/webwn 21:56:51 Or at best, very shocking. 21:57:01 `define fricate 21:57:03 * Frication - Fricatives are consonants produced by forcing air through a narrow channel made by placing two articulators close together. ... \ [13]en.wikipedia.org/wiki/Frication \ * frication - friction; turbulent and noisy airflow 21:57:08 Darn. 21:57:12 ;) 21:57:19 force air through narrow channel 21:59:07 i forced.... ughr 21:59:17 oh, fricate. not fornicate. 22:01:57 -!- werdan7 has quit (Ping timeout: 619 seconds). 22:02:10 -!- Gracenotes has quit (Quit: Leaving). 22:07:16 hey alis 22:07:17 hey alise 22:08:14 -!- werdan7 has joined. 22:10:29 lament: can you believe I was banned??? :( 22:12:11 Quadrescence: from where? 22:12:18 #nm 22:12:41 and after all this time I thought I was an asset to the channel :((((((((((((((((((((((((((((((((((((((((((((( 22:13:58 what holy shit 22:14:27 lament: |Steve| did because I banned him from ~m 22:15:01 [otherwise no other reason] 22:15:47 wow, what a jerk! 22:16:00 such tit-for-tat brinkmanship 22:16:38 he should have turned the other cheek and made you an op so you can ban him in #nm 22:17:51 * oerjan seems to be having troubles with his sarcasm meter 22:18:29 -!- MigoMipo_Zwei has joined. 22:18:41 -!- MigoMipo has quit (Ping timeout: 260 seconds). 22:19:02 -!- MigoMipo_Zwei has changed nick to MigoMipo. 22:20:14 Quadrescence: i'm using all my diplomatic finesse to get you unbanned 22:20:20 so expect a permaban, probably in #math too 22:20:36 lol 22:20:41 lament: awww 22:20:55 OK, that was funny. 22:20:57 Noooo don't get yourself in trouble 22:21:24 nono i'm not getting *myself* in trouble :D 22:21:37 Hahaha okay good 22:21:49 - famous last words 22:23:42 "oerjan: lol" <<< is it just me or is this really out of character 22:24:06 or was that just the first thing ever you found funny here 22:24:14 I found this quite funny: [16:17.27] * oerjan seems to be having troubles with his sarcasm meter 22:24:20 also god i hate this nick 22:24:50 oerjan leaks this constant flow of hilarious humor 22:24:59 -!- cpressey has changed nick to cpressez. 22:25:41 Quadrescence: i found lament's comment hard to measure 22:25:51 I know 22:25:53 it was funny 22:25:58 the way you said it 22:26:03 at the time you said it 22:26:50 -!- muni_ has joined. 22:27:18 "I love you." "LOL!" 22:27:52 I suppose that's better than "I love you." "ROTFL" 22:28:14 lol 22:28:35 (yeah i'm just messing with o|{|_o9o|_ now) 22:28:50 (ok, and laughing) 22:29:04 limh 22:29:08 (laughing in my head) 22:29:32 why did alise just disappear like that? 22:29:32 sounds painful 22:29:46 fax: THEY found him 22:29:56 yeah not funny 22:31:54 it's an unfunny in-joke in bad taste 22:32:07 the best kind 22:32:12 maybe i should ban myself 22:32:25 can you? 22:32:32 okklopkuabp 22:32:32 presumably 22:32:37 -!- tombom has quit (Quit: Leaving). 22:32:39 yep, he has ops nowadays 22:32:40 you didn't respond 22:32:44 -!- o|{|_o9o|_ has changed nick to oklopol. 22:33:18 didn't respond to what? if it was in pm, i had a different nick for a while, not sure if you noticed because there were only typographical differences 22:33:25 8:/ 22:33:50 you asked me whether 8, or what? 22:34:02 _clearly_ 8 22:34:13 The ratio between 8 and / 22:34:15 that much is obvious 22:34:30 -!- MigoMipo has quit (Remote host closed the connection). 22:34:42 -!- muni_ has left (?). 22:35:03 cpressez: you zuddenlee look very french 22:35:43 this is really frustrating 22:37:01 fax are you hot 22:37:45 Si pressez-vous la bouton 22:38:10 * Quadrescence presse la bouton. 22:38:21 Le monde explode! 22:38:46 Que galère!!! 22:39:11 -!- cpressez has changed nick to cpressey. 22:39:13 Well enough of that. 22:39:33 -!- alise has joined. 22:39:46 -!- jcp has quit (Ping timeout: 258 seconds). 22:39:57 *explose 22:40:00 darn french 22:40:04 depose* 22:41:08 -!- jcp has joined. 22:43:51 bzflag 22:43:54 i remember that game 22:44:07 13:46:32 the theorem doesn't actually have any mathematical content, it's just stated for convenience, so you don't have to think about what happens on the boundaries of the sum and the integral every time 22:44:07 | 22:44:07 /\ 22:44:13 everything that is true is an obvious tautology :P 22:44:25 *facepalm* 22:44:38 *kneeear* 22:44:45 etc. 22:44:49 * Quadrescence snickers 22:44:57 lawl 22:44:57 There are no trivial mathematics, only trivial mathematicians! 22:45:24 myndzi: was that supposed to look dirty? 22:45:28 cpressey: you're quite limber, i take 22:45:48 oerjan: I am on IRC, at least. 22:45:56 ah 22:46:15 argh 22:46:20 -!- BeholdMyGlory has quit (Remote host closed the connection). 22:46:27 \o/ \o/ \o/ \o/ 22:46:27 | | | | 22:46:28 /| |\ /| /| 22:46:39 \o/\o/\o/\o/ 22:46:39 | | | | 22:46:39 |\ |\ >\/\ 22:46:50 /´\ 22:47:01 \o/ 22:47:02 | 22:47:02 /| 22:47:04 \o/\o/\o/ 22:47:05 | | | 22:47:05 >\ >\ >\ 22:47:26 \o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/ 22:47:26 | | | | | | | | | | | | | | | | | 22:47:26 >\/| /| /< /< /'\/\/< /< /< |\ |\/`\ |\/< |\/| 22:47:30 \o/ 22:47:30 | 22:47:31 /| 22:47:34 wow awesome 22:47:37 very few of them have dicks. 22:47:38 that is the coolest thing ever 22:47:48 i know \o/ 22:47:48 | 22:47:48 |\ 22:47:57 _o/ 22:47:58 | 22:47:58 /'\ 22:48:01 HAHA 22:48:02 are there actually spaces before? if so, my client strips them >_< 22:48:13 there used to be iirc 22:48:15 get a client that doesn't suck 22:48:24 \m/ \m/ 22:48:25 `\o/ 22:48:25 | 22:48:25 (_|'\ 22:48:25 |_) 22:48:35 LOL WUT 22:48:47 \m/ 22:48:53 \m/ 22:48:55 \m/ \m/ 22:49:03 14:27:52 I suppose that's better than "I love you." "ROTFL" 22:49:04 -!- cheater2 has quit (Read error: Connection reset by peer). 22:49:06 \m/ \m/ 22:49:06 `\o/ 22:49:06 | 22:49:06 /'\ 22:49:06 (_| |_) 22:49:07 *ROTFUL 22:49:27 o 22:49:30 -!- cheater2 has joined. 22:49:34 _o_ 22:49:35 | 22:49:35 /| 22:49:41 wowowowow 22:49:44 that is so cool 22:49:53 -!- alise has left (?). 22:49:59 -!- alise has joined. 22:50:40 that script is the only reason i go to #esoteric 22:50:47 "alise: are there actually spaces before? if so, my client strips them >_<" <<< first whitespace i've ever seen that nnscript *doesn't* strip 22:51:15 in the logs it's spaces /and/ some other char 22:52:07 lament: ur the only reason I go to #esoteric~ 22:52:38 Quadrescence: ur the only reason fax goes to #esoteric 22:52:46 FU*K 22:52:50 -!- cpressey has left (?). 22:52:57 fax has acne and boils 22:53:22 #~esoteric is either the most interesting channel I can think of, or the least, depending on what #esoteric is at the time, 22:53:53 well, I guess it's #(~esoteric), not ~(#esoteric) 22:53:54 so most boring 22:54:10 oh shut up 22:54:45 (I was talking to EgoBot not you alise) 22:54:47 it's transitive 22:54:53 EgoBot is talking? 22:55:05 yeh 22:57:03 !echo I'm human! 22:57:07 I'm human! 22:57:36 he's just using facilitated communication 22:58:33 oerjan: <3 22:58:51 lament: http://i.imgur.com/ZFlbv.jpg 22:59:09 i'm not opening anything at work 22:59:14 * alise wonders if that's the same image Quadrescence linked to me before 22:59:18 if so, lament made the right choice :p 22:59:22 -!- coppro has joined. 22:59:37 "However, under Japanese rules, the game is already considered to have ended. The players attempt to ascertain which groups of stones would remain if both players played perfectly from that point on. (These groups are said to be alive.) In addition, this play is done under rules in which kos are treated differently from ordinary play. If the players reach an incorrect conclusion, then they both lose." 22:59:50 alise: the situation for a disputed endgame in Go is even funnier than I thought 22:59:58 :D 22:59:58 coppro: if you ever need latex help, you're welcome to ask me instead of going to #latex where people treat you like you're 8.5 years old 23:00:14 You get nothing! You LOSE! Good DAY sir. 23:00:14 I love the way that the double loss is given for getting it wrong, rather than for disagreement 23:00:57 i wonder how many famous games of go are actually platonically a double loss 23:01:02 but nobody's realised 23:01:12 alise: except with more honorifics 23:01:41 i wonder how many chess games actually ended with the white winning, but the players thought black won. 23:01:42 alise: probably not that many in famous games, you'd expect the players to get it right 23:02:04 for draws, there probably are such instances 23:02:16 oklopol: a few famous ones (if you allow vice versa); there was one where one of the players lost on time, and the referee accidentally turned the clock round and gave the win to the wrong player 23:02:18 oklopol: None :P 23:02:20 in a relatively publicised tournament 23:02:31 ais523: that's cheating 23:02:35 :P 23:02:50 alise: by the referee? 23:02:53 it was a mistake, rather than deliberate 23:02:58 I wonder how many chess games actually ended with the X winning, but the players thought Y won, and the game ended by the taking of a king, where X =/= Y. 23:03:03 ais523: i mean as an example 23:03:03 it's cheating as an answer to my wonderingment 23:03:06 yeah 23:03:40 Note that X or Y can be "draw" 23:03:41 well, xor 23:03:45 -!- FireFly has quit (Quit: Leaving). 23:04:20 -!- lament has quit (Ping timeout: 245 seconds). 23:05:01 there was a case (again in a serious tournament) where a player offered a draw, his opponent said "make a move first", the player moved, then the opponent resigned 23:05:07 legally, you can still take the draw in that situation 23:05:26 (it's a rule against draw offer spam; if someone offers a draw, you can accept until the end of your next move) 23:05:38 (so there's no point in offering more than once in the same move) 23:05:49 but anyway i think it's technically possible that black moves a piece so that the king can't move anymore, and neither player realizes there's a distant piece making it a checkmate instead of a stalemate 23:06:29 yep, I suppose so vaguely 23:06:33 http://sci.tech-archive.net/Archive/sci.logic/2006-10/msg00751.html 23:06:34 i keep 23:06:34 -!- lament has joined. 23:06:35 reading this 23:06:36 as a 23:06:37 poem 23:06:39 and it 23:06:40 is really 23:06:41 annoying 23:06:41 actually, there are probably loads of draws on time which were claimed as wins on time by mistake 23:06:59 (draw on time: if your opponent runs out of time, but it's theoretically impossible to win given the material on the board) 23:07:15 alise "Yessenin-Volpin"? wow a THIRD ultra-finitist?? 23:07:28 fax: they don't even include what'shisname in that list 23:07:32 the guy we've been talking about 23:07:35 japanese rules allow draws on time??? 23:07:36 so there are FOUR??? 23:07:39 fax: oh crap 23:07:47 no wait, three 23:07:53 fax: the number of ultrafinitists is getting dangerously big 23:07:56 lament: Chess, not Go 23:08:02 this movement has gained its maximum possible mass (I don't believe in 4) 23:08:05 fax: what if it overflows??? 23:08:06 lament, lol 23:08:15 it's always theoretically possible to play Go so badly that your opponent wins 23:08:18 lament: damn you made the same joke as me but beter 23:08:18 lament: dammit stealing my joke 23:08:25 hahaha 23:09:59 alise, you know Freek Wiedijk 23:10:00 ? 23:11:01 i do now 23:11:01 fax: resend your latest /msg, i closed the tab by mistake 23:11:11 ais523: that can't possibly be true, do you see why?? 23:11:19 DUCY??? 23:11:34 lament: the game lasts an infinite length of time if both people try it 23:11:45 i'm sure everyone thought of the joke 23:11:50 hmm, unless you enforce superko, in which case my statement is indeed incorrect 23:12:14 It depends on the form of superko 23:12:20 ais523: why would either of them capture at all? They would pass. 23:12:45 oh, good point 23:12:46 they ought to pass when there's one empty point remaining 23:12:54 I somehow assumed that you'd capture with only one point left 23:12:57 if the game ends 23:13:02 too much exposure to the stupid stupid Yahoo auto-go thing 23:13:11 which has a bug where you can run an opponent out of time by repeated passing 23:13:22 i'm not sure what's the status if the game ends but i guess it's seki 23:13:33 either seki or "both players lose" 23:15:33 SEKSI 23:15:55 what would be funny would be if you somehow got half a stone onto the board 23:15:59 and then claimed a draw despite komi 23:17:19 very easy with cheap chinese stones, they break all the time 23:17:50 Here's a thought: hybridize Go and Chess by simply having a chess board, where the intersections are the points on a Go board, every turn you do either a Chess or a Go move, and the Go game works as usual, including taking out Chess pieces :P 23:18:45 who wins? 23:19:00 Whoever either checkmates or takes out the opponent's king. 23:19:23 Which, I suppose, is problematic for the Go component ... 23:19:27 do you need to surround a piece on four sides to capture is? 23:19:30 -!- ais523 has quit (Remote host closed the connection). 23:19:30 Needs some rough edges smoothed out. 23:19:31 *it 23:19:37 lament: That was the idea? 23:19:39 lament: you could take it with a chess piece 23:19:43 or surround it 23:19:44 Well, yes. 23:19:48 does go have a winning condition? 23:19:50 I don't actually know 23:19:50 Gregor: well it's not quite how Go works 23:19:55 alise: no, people just fuck around. 23:20:20 erm 23:20:20 i mean 23:20:21 an endgame condition 23:20:21 apart from like... running out of pieces 23:20:21 or time 23:21:01 oh 23:21:10 both players pass 23:21:25 note that sometimes you're forced to pass due to not having any valid moves 23:21:32 but in principle a game could go on forever 23:21:44 Gregor: Checkmate/taking out/both passing = game ends. 23:21:47 there's an optional rule, which nobody uses, that disallows repetition 23:21:58 Then you can invent a hybrid chess/Go winning condition to be applied at endgame. 23:22:20 Well, that makes sense since both passing is an endgame condition for Chess anyway, stalemate :P 23:22:36 From what little I know about Common Lisp, I despise it 23:22:46 The problem is that in chess, endgame almost always is because of someone winning. 23:22:49 funcall? Really? 23:22:54 alise: Yuh 23:22:55 In Go that appears to be calculated after the fact. 23:23:00 Sgeo: So you can name a variable "list". 23:23:27 Gregor: You could redefine instead Go's endgame condition to be because of someone winning somehow. 23:23:41 The Go pieces would be controlling areas of the board ... you couldn't move there because you'd be instantly surrounded by opposing pieces. Maybe that's bad :P 23:24:03 Maybe that's AWESOME. 23:24:10 Maybe! 23:24:16 So how does a Chess piece take a Go piece? Maybe jumping over it. 23:24:25 I wasn't considering that possibility ... 23:24:33 Say you have a Go piece to the top-left of a pawn. If the pawn moves one space top-left, the Go piece is taken 23:24:34 etc. 23:24:57 So, Bishops have free take-out powers :P 23:25:21 For knights... No fucking clue. 23:25:23 Gregor: They do anyway :P 23:25:25 I don't think you would use typical Go notions of control 23:25:38 coppro: Probably not quite. 23:25:45 It's not a hybrid if you significantly modify G1+G2 23:25:52 control really just means an area that if you put a piece in, it will die eventually 23:25:53 It's your own game inspired by G1, G2. 23:26:04 alise: Oh nooooooooes 23:26:08 G0? 23:26:15 The only modifications should be to resolve contradictions. 23:26:59 so if you add the ability to leave the area or take one of the controlling pieces, there's no sense in preventing a piece from entering a controlled area 23:27:35 Gregor: You made Chesskers. 23:27:42 Yes, I did :P 23:27:47 You're making Gochess. 23:27:53 So, Gochesskers. 23:27:55 Yes, I am :P 23:27:59 You should add Othello to that mix. 23:28:11 Gothellochesskers. 23:28:16 Yes, I ... wait, whaaaa? 23:28:20 Go, Othello, Chess and Checkers. Living in perfect disharmony. 23:28:20 * Sgeo would never have discovered FICS if XP had "Internet Chess" 23:28:40 Gregor: Wait, what? :D 23:28:49 Haha, imagine Chess pieces flipping colour because you connect a line. 23:29:21 Then subsequently taking Go pieces, which then surround a Checker piece, eliminating it. 23:29:40 Combine ALL board games into one! 23:29:44 Throw some Risk in there! 23:29:49 I think we need some 18xx! 23:29:52 And where's Clue?! 23:29:52 No :P 23:30:02 But Go, Othello, Chess and Checkers are all fundamentally similar. 23:30:27 Abstract pieces on a uniform board, with uniform rules throughout, involving pieces "getting rid" of other pieces, with complex strategy underlying simple rules. 23:30:43 And any two are quite easily hybridised. So.. 23:31:26 * Sgeo wishes FICS had a way of defining your own game that used a chessboard and chess pieces 23:31:40 With some simple not-necessarily-TC scripting language 23:31:49 Sgeo: fork the source 23:32:04 coppro: it's closed 23:32:07 the latest version of the server at least 23:32:09 it is? 23:32:23 well wikipedia says an old version was open and is mum about the current, so.. 23:32:28 *so... 23:32:37 (directly next to each other) 23:32:39 Easy enough to ask 23:33:02 "MAd(1): no" 23:35:32 And now ... 23:35:34 FINLANDIA! 23:36:25 Also, LaTeX's default title font is disturbingly similar to the "font" used for the title of the original publication of Finlandia. 23:36:41 COMPUTER MODERN: Disturbing 23:37:20 not so modern after all 23:37:39 somewhere, on a forgotten sumerian clay tablet... 23:38:18 the first ug was typeset by knuth 23:38:42 definition: a game A totally wins the game B if there's a winning strategy in the mixed game A|B that uses only moves of A 23:40:09 hm is this related to surreal number ordering? 23:40:58 Totally wins; terminology first used by Euclid in his Elements. 23:41:01 Specifically: 23:41:23 "Let there be the games A, B. I say that A totally wins B. 23:41:41 First, let there be a strategy of A. 23:42:04 Let it be that when this strategy is used in AB, it is winning. 23:42:05 i can confirm this because strategy is a greek word. 23:42:20 If this is not so, then instead I say B totally wins A." 23:42:35 that's my piss-poor attempt at emulating the style of Elements... 23:42:39 oh but totally winning is a proper partial order! 23:42:57 so in fact it's not necessarily true that B totally wins A if A does not totally win B 23:43:36 right but that's a modern development of Winning theory 23:43:47 Euclidean winning theory doesn't have that 23:44:09 definition: if A does not totally win B, and B does not totally win A, then we say A|B is not ridiculous 23:44:27 ah 23:44:44 -!- oerjan has quit (Quit: Good night). 23:44:54 now the obvious question is, is go|chess a ridiculous idea? 23:44:54 (Euclid considered "That all entities must be ordered. Take entities A and B and A is not more than B, and B is not more than A. Then A appears before B, and B appears before A. This is an absurdity. So all entities must be ordered.") 23:45:22 :D 23:46:01 oklopol: you're abusing notation, A|B is the common parts of the games A and B 23:46:13 go|chess would be a board with things that move around and remove other pieces, but past that undefined 23:46:17 you mean AB 23:46:41 (euclid wrote A|B as superscript A, subscript B.) 23:46:58 winning theory is like game theory but more indie 23:47:34 (In complex expressions the notation A above B is often used to save space, but for more complex expressions the super/subscript format is used.) 23:47:43 Erm, that is, as a component of complex expressions. 23:49:34 | is an OR-like character, AB is multiplication which is an AND-like operation 23:49:55 exactly 23:50:13 remember that euclid thought of games as primitives 23:50:15 so A|B is the mix of the games, and AB is the common parts. 23:50:35 as such, (go chess) was go & chess, i.e. both go and chess. 23:50:50 that's what AND and OR mean in the philosophy of fuzziness. 23:50:55 eh fine :P 23:51:08 go fish 23:53:28 the common parts operation probably actually makes sense in some cases, because either you get the empty game or you get some basic moves or something. i guess stuff like winning might be completely removed though 23:53:48 is there a good definition for board games somewhere? 23:54:30 clearly winning theory is our chance to invent it. 23:54:37 game theory is to board games sort of what category theory is to algebras, imo 23:54:49 also, euclid didn't even consider common parts by itself to be a valid formula. 23:54:57 he always built it up from there to a full game 23:55:03 -!- MizardX has quit (Ping timeout: 240 seconds). 23:55:13 maybe, maybe 23:56:13 in algebra, the common parts of two algebras are usually directly an algebra, but the mix of two algebras needs to be extended to be a full algebra 23:57:51 game theory doesn't talk about board games at all. 23:58:13 and the second rule of game theory: Do not talk about board games