00:00:02 <alise_> 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 <fax> fundamental theorem was solutions of XY = YX?
00:00:15 <fax> oklokok, okay but can you give me one hint on OR?
00:00:25 <fax> because right now I am just sort of lost
00:00:43 <fax> oklokok but this finite calculus is so cool!
00:00:44 <cpressey> alise_: How would you prove that pop(push(X,Stack)) == Stack ?
00:00:53 <alise_> 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 <cpressey> 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 <alise_> i.e., a function taking (f, |f e1 - f e2| < e1 + e2), also known as a computable real
00:01:20 <oklokok> yeah fundamental theorem was your pet name for the commutation thing
00:01:21 <fax> 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 -!- bsmntbombdood_ has joined.
00:01:48 <cpressey> fax: A better example to prove would be most welcome, then
00:01:52 <fax> cpressey (if P reduces to P' then a proof of P is a proof of P')
00:02:00 <alise_> cpressey: I gave you one.
00:02:10 <cpressey> alise_: I don't have functions in my language
00:02:16 <oklokok> okay for OR, the first thing is to reduce it to a=b OR a=c.
00:02:24 <alise_> cpressey: You don't need reals.
00:02:25 <fax> oklokok, I think it has something to do with sequence of lydon words.. (because you told me that)
00:02:25 <alise_> I just defined the reals.
00:02:33 -!- bsmntbombdood has quit (Ping timeout: 245 seconds).
00:02:39 <fax> oklokok, okay byebye!
00:02:41 <oklokok> at least i think that's the easiest way
00:02:42 <cpressey> alise_: You're too quick for me.
00:02:54 <alise_> cpressey: The tuple (f : Q+ -> Q, forall e1, e2 : Q+, |f e1 - f e2| < e1 + e2) is a computable real.
00:03:03 <alise_> (Which is just like the reals, except without things like chaitin's constant)
00:03:07 <oklokok> fax: nope, lyndon's aren't useful at all, i just like them.
00:03:15 <fax> oklokok, oh :p
00:03:19 <alise_> cpressey: The second element is a property of the first, a function.
00:03:22 <fax> I thought they were integral to this
00:03:34 <oklokok> ah, sorry if i gave you that impression
00:03:44 <alise_> cpressey: (Basically pi 0.1 = 3.1, pi 0.01 = 3.14, etc)
00:03:45 -!- coppro has joined.
00:04:00 <alise_> cpressey: So, substitute whatever is the best analogue for a function.
00:04:07 <alise_> How do you construct the proof?
00:04:15 <cpressey> alise_: I'm not going to be able to prove that without defining some axioms for ordering and stuff.
00:04:30 <alise_> cpressey: You don't need any axioms above the standard for this
00:04:45 <oklokok> 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 <cpressey> 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 <oklokok> oh well actually chapters 1 and 2
00:05:25 <alise_> cpressey: So construct the computable reals.
00:05:41 <oklokok> where "lectured" == "listed theorems as exercises" ;)
00:05:43 <cpressey> alise_: No. What am I proving about them? Their existence?
00:05:43 <fax> anyway I better go to bed
00:06:09 <alise_> Okay, let me express this in Haskell-ish things for you.
00:06:15 <cpressey> "for all positive rationals e1 and e2, |f e1 - f e2| < e1 + e2" is closer, but requires, like, numbers and shit.
00:06:36 <alise_> data Real = Real (Q+ -> Q) (forall (e1:Q+), (e2:Q+). abs (f e1 - f e2) < e1 + e2)
00:06:40 <alise_> The latter bit is the dependent part.
00:06:45 <alise_> So, to construct a computable real, we do
00:06:50 <alise_> Real f (proof of that property of f)
00:07:02 <alise_> 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 <alise_> 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 <cpressey> 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 <alise_> Since all your proofs are just simply proving that x evaluates to x', it's pointless.
00:07:44 <alise_> The proof is nonexistent; x equiv-to x' by virtue of evaluating to it.
00:07:47 <alise_> So the proof is that x = x.
00:07:57 <alise_> cpressey: *positive rational, not rational.
00:07:58 -!- lament has quit (Ping timeout: 264 seconds).
00:08:20 <alise_> It is only true for some functions. Obviously.
00:08:32 <alise_> Our constructor takes a function f, and a proof that that holds /for only the single function f that we give/.
00:08:52 <cpressey> That's a proof *schema* in my book.
00:08:52 <alise_> 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 <alise_> So, how would you structure such a thing?
00:09:13 <alise_> I bet you can't, because your proof construct is uber-limited.
00:09:25 -!- lament has joined.
00:09:58 <cpressey> alise_: Nowhere did I say I was writing a *prover*, only a *proof checker*
00:10:12 <cpressey> What is the problem with specifying f in my proof?
00:10:25 <alise_> You cannot even /express the proof/ in your language, because you can only prove things of the form x = eval x
00:10:37 <alise_> And you cannot check a proof you can't express.
00:10:51 <cpressey> 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 <alise_> You prove it for some given function f.
00:11:46 <cpressey> Right, so give me some function f.
00:12:18 <alise_> i : Q -> R; i q = (\_. q, ...proof...)
00:12:21 <cpressey> Like I said, what you gave sounds like a proof schema to me.
00:12:27 <alise_> Write the proof in your language.
00:12:37 <alise_> \x. e being lambda, of course.
00:13:45 <cpressey> How am I supposed to read that?
00:14:10 <cpressey> i takes the rationals to the reals; i is some function...
00:14:48 <alise_> i : Q -> R -- i is a function from rationals to reals.
00:15:23 <alise_> type R = (f : Q+ -> Q, forall (e1,e2 : Q+). abs (f e1 - f e2) < e1 + e2)
00:15:42 <alise_> \_.q is a function taking one argument, ignoring it, and returning q
00:16:00 <alise_> you must now prove that for all positive rationals e1 and e2, |(\_. q) e1 - (\_. q) e2| < e1 + e2
00:16:10 <alise_> you must now prove that for all positive rationals e1 and e2, |e1 - e2| < e1 + e2
00:16:13 <alise_> but you can't just assume that
00:16:18 <alise_> do it methodically with your proof construct
00:16:20 <alise_> (I don't believe you can)
00:17:01 <cpressey> "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 <cpressey> Well, no. I mean, |a - b| = a + b
00:18:04 <alise_> you must now prove that for all positive rationals e1 and e2, |(\_. q) e1 - (\_. q) e2| < e1 + e2
00:18:29 <alise_> the argument to the function i. pay attention
00:18:32 <alise_> => for all positive rationals e1 and e2, |q - q| < e1 + e2
00:18:36 <alise_> => for all positive rationals e1 and e2, |0| < e1 + e2
00:18:40 <alise_> => for all positive rationals e1 and e2, 0 < e1 + e2
00:18:53 <alise_> => for all positive rationals e1 and e2, true
00:19:02 <alise_> but you must prove it /with your proof construct/
00:19:07 <alise_> that's the whole point; it's verified
00:19:46 <cpressey> 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:23 <alise_> You know Haskell. Correct?
00:21:03 <cpressey> 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:10 <pikhq> Seems to be more functions of the type (i :: a -> R)
00:21:10 -!- cpressey has left (?).
00:21:49 <pikhq> No, wait, more specific, :: Q -> R. Anyways.
00:22:21 -!- alise has joined.
00:22:29 <alise> If you didn't know Haskell I couldn't explain it in a million years.
00:23:04 <Gregor> Sounds like a personal problem.
00:23:10 <pikhq> Sure you could. You could give a Haskell tutorial.
00:24:15 <alise> Gregor: Do you have any idea what dependent type theory is?
00:24:20 <alise> 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 <Gregor> I have no formal experience with dependent type theory, only indirect.
00:25:16 <Gregor> Erm, indirect isn't the right word.
00:25:21 <oklokok> i don't remember what peanuts taste like, but i'm sure i love them
00:26:33 <Gregor> What a tragic statement :P
00:29:26 <Gregor> I keep looking down, not seeing a tie, and thinking "?!"
00:30:10 -!- werdan7 has quit (Ping timeout: 624 seconds).
00:32:58 -!- BeholdMyGlory has quit (Read error: Connection reset by peer).
00:34:02 <Gregor> Clothes are for the weak.
00:34:44 <oklokok> i mean you wear all sorts of different clothes, which is weird if you, like normal humans, hate wearing clothes
00:35:03 -!- werdan7 has joined.
00:35:14 <Gregor> Just a barrel, a bear skin and a necktie.
00:35:26 <Gregor> Well, on a dressier day.
00:35:32 <Gregor> I lose the barrel on average days.
00:35:43 <Oranjer> which days are the average days?
00:35:47 <oklokok> somehow i feel i'm the only one being serious
00:35:50 <Oranjer> how does one calculate that
00:35:55 <Gregor> Pretty much anything other than going to a wedding or whatnot.
00:36:06 <Oranjer> weddings are the outliers of my life!
00:36:19 <Gregor> Hence why they're not the normal days.
00:44:00 <alise> http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/real.pdf
00:44:04 <alise> The ramblings of a crazy man.
00:46:18 <Sgeo> I learned something great from Ruby: Fibers!
00:46:33 <alise> "Andrew Wiles's alleged `proof' of FLT, while a crowning human achievement, is not rigorous, since"
00:46:34 <Sgeo> I think Fibers would be very useful in the C# project I'm working on
00:46:42 <alise> "it uses continuous analysis, which is meaningless."
00:46:44 <alise> Sgeo: fibers are shit
00:47:04 <madbr> yeah looking at this pdf... it's crazy
00:47:05 <Sgeo> Howso? And is there ANYTHING that isn't?
00:50:02 -!- FireFly has quit (Quit: Leaving).
00:50:05 <madbr> Well, for instance, he's telling us stuff like "sqrt(2) doesn't exist"
00:50:13 -!- jcp has joined.
00:50:16 <alise> he is talking to me
00:50:21 <alise> Sgeo: because fibers are like continuations and coroutines but shittier
00:51:18 <Sgeo> Well, I want something that lets me resume the current .. thing later
00:51:33 <Sgeo> I'm willing to work with whatever exists the most in .NET
00:51:38 <alise> Sgeo: continuations. coroutines.
00:55:30 <Sgeo> Continuations exist in .NET?
00:55:50 <alise> no, but .net is almost useless for programming.
00:56:24 <alise> if you hate yourself.
00:56:31 <pikhq> Continuations can be done in .Net.
00:56:42 <pikhq> By which I of course mean CPS.
00:56:59 <Sgeo> I understand call/cc better than CPS
00:57:31 <pikhq> Sgeo: CPS is simply the act of transforming the usage of return values to a function that takes a value.
00:57:57 <pikhq> Instead of "x = function_call(bar);", you do "function_call(bar, \x -> ...);"
00:58:14 <pikhq> And that was a delicously odd hybrid of C and Haskell syntax.
01:03:21 <Gregor> So, Chrome maps the numpad keys, with numlock on, to the keyCodes 97 etc.
01:03:31 <Gregor> 97, for the non-ASCII-inclined, is lower-case 'a'.
01:03:41 <Gregor> (The key 'A' sends a capital A, 65)
01:05:26 <Gregor> Oh look, Firefox does it too.
01:13:08 -!- alise has quit (Ping timeout: 252 seconds).
01:28:25 -!- Asztal has quit (Ping timeout: 265 seconds).
01:29:11 <madbr> weird html5 keyboard handling?
01:35:05 -!- oklokok has quit (Read error: Connection reset by peer).
01:52:40 <Gregor> Weird blaming of HTML5 for totally irrelevant things? :P
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 <coppro> ugh, people in #latex treating me like I've never used a text editor before; much less LaTeX
03:49:51 -!- myndzi\ has joined.
03:50:18 -!- myndzi\ has changed nick to myndzi.
03:53:26 <coppro> 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 <Sgeo> <eporim> a "tnx you badass" would have been appreciated...
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 <coppro> I discovered http://www.periodicvideos.com/ today :(
06:01:15 <coppro> now I'll never get to sleep
06:08:05 <coppro> the one guy looks like your stereotypical professor
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 <AnMaster> <coppro> anyone know a LaTeX equivalent of OO.o Math's csub? <--- what does csub do?
07:09:29 <AnMaster> coppro, but I'm genuinely interested!
07:09:32 <coppro> busy watching videos that tell me things I already know in humourous manner
07:09:43 <coppro> AnMaster: positions a subscript directly below the principal
07:09:55 * Sgeo will attempt to learn E tomorrow
07:10:19 <Sgeo> http://www.erights.org/elang/
07:10:36 <Sgeo> Supposed to be secure distrubuted language thingy
07:10:56 <coppro> sure that isn't Erlang?
07:11:02 <coppro> (that you're thinking of; not the site)
07:12:01 <Sgeo> I'm pretty sure
07:17:09 <AnMaster> <coppro> I discovered http://www.periodicvideos.com/ today :( <--- looks interesting
07:18:06 <AnMaster> <Sgeo> Supposed to be secure distrubuted language thingy <coppro> sure that isn't Erlang? <-- "secure" isn't a way I would describe erlang. Not insecure either though.
07:18:24 <AnMaster> I mean, it isn't specifically geared towards security
07:18:50 <coppro> I mentioned it specifically because it's 'elang'
07:19:22 <fizzie> 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 <coppro> sulphur is a really good video
07:20:38 -!- fungot has joined.
07:53:48 -!- tombom has quit (Quit: Leaving).
07:55:22 <coppro> 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 <alise> Hypothesis: It is impossible to be comfortable.
12:26:00 <alise> 19:42:24 <coppro> ugh, people in #latex treating me like I've never used a text editor before; much less LaTeX
12:26:12 <alise> Most users of LaTeX are near computer-illiterate, I think.
12:26:19 <alise> Mostly mathy people.
12:27:03 <alise> Sgeo: E is interesting but not nearly as magical as you think.
12:27:17 <alise> And it requires a good understanding of its principles to use.
12:28:23 <Quadrescence> and too bad coppro isn't here; I could help him
12:28:24 <alise> You mean my LaTeX remark? "Most users of LaTeX are near computer-illiterate" = >50% of LaTeX users are computer-illiterate.
12:28:43 <Quadrescence> alise: thank you, you're saying there's a >50% chance I'm computer illiterate
12:29:00 <alise> Quadrescence: No, because there is a large deluge of other evidence to suggest you are not.
12:29:04 -!- ais523 has joined.
12:29:09 <alise> For instance, anyone in #esoteric is almost certainly highly computer literate.
12:30:24 <ais523> I have a seminar in half an hour, but am happy to talk until then
12:30:40 <alise> ais523: about Feather.
12:31:00 <ais523> well, if you have questions...
12:31:07 <ais523> I haven't thought much further on it, though
12:31:12 <alise> ais523: What is Feather, in detail?
12:31:34 <alise> <ais523's thoughts> god dammit, you asshole!
12:31:38 <ais523> well, I'm not sure myself
12:31:41 <alise> <ais523's thoughts> We were sane for a while there!
12:32:09 <ais523> let's see... you start with a very small TC language
12:32:16 <ais523> I'm planning to use lambda calculus + continuations
12:32:30 <ais523> and a very small bootstrap program, written in that language
12:33:18 <ais523> 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 <ais523> wait, it has to be correct
12:33:37 <ais523> but it doesn't matter if it has no error handling or something like that
12:33:57 <ais523> now, the bootstrap program has to be written in a vaguely object-oriented style
12:34:17 <ais523> 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 <alise> lambda calculus + continuations; interesting
12:34:38 <ais523> and the property, that each of those parts can be retroactively replaced
12:34:39 <alise> I'm going to implement that
12:35:18 <ais523> 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 <alise> ais523: are you sure you absolutely need lambda if you have continuations?
12:35:33 <alise> calculus of continuations!
12:35:52 <ais523> alise: I'm not, but it's likely to make the self-interp shorter and easier to write
12:35:59 <alise> ais523: also, LC sucks, make it combinator calculus
12:36:13 <alise> LC has syntactic stupidities like (\f x.f x) vs f
12:36:14 <ais523> and Subtle Cough was proved non-TC, so you need /something/ other than call/cc, at least
12:36:20 <alise> and (\x. x) vs (\y. y)
12:36:28 <alise> de bruijn indexes solve the latter but you still need n-conversion
12:36:43 <ais523> alise: planned Feather syntax is [ x | f x ]
12:37:02 <alise> semantics (\f x. f x) = semantics f
12:37:03 <ais523> alise: because if I didn't say, AnMaster would ask
12:37:20 <ais523> hmm, semantics (\x. f x) = semantics f
12:37:27 <alise> semantics (\x. x) = semantics (\y. y)
12:37:32 <alise> De Bruijn indexes solve that one:
12:37:37 <alise> semantics (\0) = semantics (\0)
12:37:43 <alise> but not n-conversion:
12:37:52 <ais523> the same problem happens even with combinators
12:38:04 <alise> erm oops I wrote it wrong
12:38:12 <alise> semantics (\x. f x)
12:38:13 <ais523> and, well, in general because you can't compare functions in general in a TC language
12:38:25 <alise> ais523: you compare syntactic structure
12:38:37 <alise> anyway n-conversion + de bruijn indexes make it work
12:38:39 <ais523> well, ``skk is semantically equal to i, for instance
12:38:40 <alise> but n-conversion is ugly
12:38:46 <alise> converting (\{f} 0) to {f}
12:38:52 <alise> where {f} is f's current identifier number
12:39:09 <alise> ais523: that's irrelevant though
12:39:21 <alise> (\x. f x) is literally /the same function/ as f
12:39:24 <alise> just written a different way
12:39:30 <alise> skk is more like a different implementation of the same thing as i
12:39:47 <ais523> I'm not convinced that (\x. f x) is the same function
12:40:04 <ais523> it certainly isn't in a strict lang if determining the value of f has side effects
12:40:15 <alise> then f isn't a value :P
12:41:01 <ais523> yep; this argument only works if f is a function constant
12:41:14 <ais523> perhaps the issue here is, that constant folding on functions is a fool's errand
12:41:28 <ais523> 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 <ais523> Quadrescence: it's the sort of discussion we have here
12:42:38 <alise> 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 <Quadrescence> although I credit alise and him talking about de bruijn seqs
12:42:42 <ais523> anyway, anything remotely related to Feather is inherently weird
12:42:53 <alise> Quadrescence: de bruijn indexes
12:42:58 <ais523> alise: as an optimisation?
12:43:34 <alise> hmm... the type of continuations is really strange
12:43:55 <alise> well, of callCC, specifically
12:44:14 <ais523> continuations have a relatively simple type (function from some type to bottom)
12:44:21 <alise> ((a -> X) -> a) -> a
12:44:25 <alise> where X is forall b. b
12:44:28 <ais523> call/cc, yes, that's weird
12:44:35 <alise> which is actually exists b. b
12:44:44 <alise> which is actually isomorphic to () :-)
12:44:53 <alise> but we have it as forall for convenience...
12:45:19 <ais523> alise: the isomorphism there is misleading, I think
12:45:34 <alise> type-theoretically
12:45:40 <ais523> yes, but rather vacuous
12:45:59 <alise> T (except the opposite of _|_) really is the supertype of all types, theoretically
12:46:04 <alise> in practice, you implement it like data T = T
12:46:11 <alise> because they're the same thing
12:46:13 <alise> (it also represents truth)
12:46:22 <alise> (where false is the empty type, _|_)
12:46:48 <alise> App :: LC (a -> b) -> LC a -> LC b -- it annoys me that you can't do this
12:47:00 <alise> because it stops you writing `semantics :: LC a -> a`
12:48:11 <ais523> modal logic is weird; it has _|_, T, 0, and 1 as logic values
12:48:27 <ais523> where 0 and 1 vaguely correspond to false and true, T to both, and _|_ to neither
12:48:33 <alise> The fundamental theorem of type theory: all types are sandwiched between an act of gay sex, top to bottom.
12:49:08 <ais523> also, "bottom" is a stupid name for it
12:49:22 <alise> it's at the bottom of the type hierarchy
12:49:24 <ais523> I've seen "eet" used for the same symbol ("tee" spelt backwards), for instance
12:49:42 <ais523> alise: I know why it has that name; but it's too many syllables and looks nothing like the symbol
12:51:18 <Quadrescence> alise: Maybe I should recruit you for helping me design my language
12:51:37 <Quadrescence> since you seem more competent about type theory and stuff than I originally imagined
12:51:47 <ais523> Quadrescence: alise is an expert on that sort of stuff
12:51:51 <alise> 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 <ais523> I tend to care more about the practice than the theory
12:52:08 <alise> Hey, I'm no expert.
12:52:32 <alise> Hmm. I could fold App's type into Lam.
12:52:41 <alise> So we have LamApp and LamVar.
12:52:48 <alise> But then we can't have a top-level application.
12:52:54 <alise> But I can model that to applying the main function to, say, id.
12:53:35 <alise> LamApp :: LCC (a -> b) -> LCC (b -> c) -> LCC (a -> c) -- Hey, look. It's compose.
12:57:18 <alise> Yeah, this model isn't workable.
13:00:00 <ais523> oh well, time for my seminar
13:07:14 <alise> 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 <alise> I now have an interpreter for the Lambda Calculus of Continuations, but no pretty-printer, so I can't test it.
13:24:18 <Gregor> So, put differently, you have nothing.
13:24:57 <alise> Well, I'm going to write a type-inferrer so that I can see the sort of results.
13:25:03 <alise> Any hey, I can make it loop forever.
13:25:26 <alise> Wait, all LC expressions have the type a = a -> a.
13:25:45 <alise> The AST isn't terribly conducive to pretty-printing:
13:25:52 <alise> App :: LCC Lam -> LCC Lam -> LCC Lam -> LCC App
13:25:54 <alise> Lam :: (LCC Lam -> LCC Lam -> LCC t) -> LCC Lam
13:26:50 <Sgeo> 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 <Sgeo> Don't know if CL has one, but from what I gathered..
13:28:07 <alise> 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 <alise> 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 <Sgeo> ...who said anything about sockets?
13:30:23 <alise> The prototypical example of a "practical" "standard" "library">
13:32:39 <alise> Quadrescence: So, uh, tell me about your language.
13:34:30 <Sgeo> 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 <Quadrescence> 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 <alise> PLT Scheme [...] is rubbish.
13:35:06 <alise> Use SISC, or Scheme48, or Chicken, or ...
13:35:24 <alise> Quadrescence: Computer algebra system: You want a term rewriting language. (Trust me.)
13:35:40 <alise> A typed one is an endeavour I've looked into before, and one that is very interesting.
13:36:04 <alise> Quadrescence: But as for the untyped-leave-to-runtime... Why not just have a more powerful type system?
13:36:39 <Sgeo> In what way is PLT rubbish?
13:36:52 -!- ztirf4 has joined.
13:37:17 <alise> Sgeo: To understand the reasons why you'd have to understand Scheme.
13:37:22 <alise> Trust ze sexperts.
13:37:40 <Quadrescence> 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 <Sgeo> alise, how well do I have to understand Scheme? I think I understand the basics at this point
13:38:14 <alise> Quadrescence: Well, I agree that most dependently-typed languages aren't too nice to use.
13:38:17 <alise> Sgeo: almost entirely.
13:38:26 <Quadrescence> Sgeo: Knowing some functions and stuff won't make you "know" scheme
13:38:30 <alise> Quadrescence: But, I mean, my main project is to make dependently-typed languages nice.
13:38:33 <Quadrescence> You really have to "see the light" to know scheme
13:38:37 <alise> Quadrescence: So you must understand that I'll push for that. :-)
13:38:56 <alise> 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 <Sgeo> So, what Scheme is most recommended for newbies?
13:39:09 <alise> Quadrescence: Right. My opinion is that you can make them nice /and/ mandatory.
13:39:25 <alise> Sgeo: Well, not SISC, too barebones... Scheme48 or Chicken. Chicken has more librarooz.
13:39:28 <Quadrescence> alise: That might be possible, and if so, I'd probably enforce that
13:39:49 <Quadrescence> alise: You might agree that less libraries = better for a new schemer
13:39:56 <alise> 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 <alise> Quadrescence: Yes, but Sgeo's obsessed with libraries. And really most eggs are fine.
13:40:15 <alise> Besides, SISC is Java. :-P
13:40:29 <Quadrescence> but I think the "point" of Scheme will be missed
13:40:49 <Sgeo> Is "SRFI" what is meant by libraries?
13:41:07 <alise> 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 <alise> 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:35 <alise> Quadrescence: Oh, I forgot S48.
13:41:38 <alise> Sgeo: Use Scheme48.
13:42:12 <Sgeo> The Windows distribution is "experimental"
13:42:15 <Quadrescence> 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 <Quadrescence> Sgeo: Oh, you're on windows, no wonder why you are attached to dr scheme
13:42:50 <Sgeo> Is Notepad++ any good with Scheme?
13:42:59 <alise> Or Edwin, even, lol.
13:43:05 <alise> with Quack, I suggest.
13:43:10 <alise> Anything else will fail. Horribly. Do not even bother.
13:43:24 <alise> Set to R5RS at least
13:43:26 <Quadrescence> Since you're on windows, there's little you can really do
13:43:29 <alise> Think of the /children/
13:43:47 <Sgeo> Notepad++ seems to have Scheme support
13:43:58 <alise> 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 <alise> Sgeo: It has rudimentary highlighting, probably.
13:44:05 <Sgeo> And no nice indentation thingy
13:44:14 <alise> If you are not going to trust the opinions of people who /know/ what they're talking about, why ask?
13:44:15 <Sgeo> I typed (let ((a 5) and hit enter
13:44:19 <Sgeo> It didn't autoindent
13:44:33 <alise> Sgeo: Same with Emacs. Technically. (Ctrl-J :P)
13:44:42 <alise> Quadrescence: Name it
13:44:57 <alise> yeah dr scheme at least has a workable editor for newbz
13:44:59 <alise> Quadrescence: (the channel)
13:45:47 <Sgeo> Does PLT in r5rs mode support the SRFIs that PLT is supposed to support?
13:46:10 <alise> Quadrescence: Well I wouldn't want to usurp your holy rights as a Platonic-space-excavator. :P
13:46:41 <alise> Quadrescence: No, Libster and base3 will just start attempting to troll me again.
13:46:42 <alise> Keyword "attempting".
13:47:34 <alise> Anyway, let's just do #rewritetypes so there's no flood.
13:47:40 <alise> Unless someone /else/ has that channel...
13:48:05 <Quadrescence> but we can make a new channel if you so desire
13:48:10 -!- augur has joined.
13:48:22 <alise> The holy institution of making a new channel, a.k.a. /j #foo :-P
13:51:14 <Sgeo> Are there any socket thingies in any SRFIs?
13:52:13 <alise> I shouldn't have even bothered.
13:52:48 <Sgeo> I'll take that as a "No, and you're completely missing the point"
13:53:15 <alise> But not yes. Actually not even mu, I meant exactly what I said. But yes, you are missing the point.
13:57:24 <Sgeo> What is the point, exactly?
13:57:37 <Sgeo> Maybe I should just stick with Haskell >.>
13:58:27 <alise> I doubt you get Haskell's point either.
13:58:37 <augur> tomorrow i turn 2^3 * 3 years old. :D
14:02:35 <fizzie> That spacing is misleading, since the exclusive-or binds less tightly than multiplication there.
14:03:49 <alise> Or 3, if you interpret it like he said.
14:03:57 <ais523> hmm... INTERCAL can do Roman Numerals, at least for output
14:04:12 <ais523> maybe Common Lisp was just making implementing it easier?
14:04:43 <alise> ais523: Have you any opinions on how to best represent an Othello board?
14:04:46 <alise> (Functional language.)
14:05:10 <alise> 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 <ais523> alise: I don't think I can come up with correct opinions
14:05:42 <augur> alise: not exclusive or.
14:05:46 <ais523> 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 <alise> Incorrect ones are fine too, ais523.
14:05:51 <alise> augur: Ohh you don't say
14:05:58 <ais523> no matter what the correct representation actually was
14:06:10 <augur> i could've done something more interesting
14:06:28 <fizzie> Wilful misinterpretation is the norm here, isn't it?
14:06:33 <ais523> 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:57 <ais523> nicely abstracted and extensible, but otherwise terrible
14:07:51 <alise> Quadrescence will back me up on this... i hope
14:08:16 <Sgeo> Ok, so what doesn't suck?
14:08:55 <alise> Me! It'd be illegal.
14:09:44 <fizzie> Speaking of which, where does the "put a sock on it" expression come from? (And don't reply with a line number.)
14:11:41 <alise> slib blows... anuses
14:12:37 <Sgeo> So... does this mean for networking stuff, I'd be using the implementation's stuff?
14:12:46 <Sgeo> Or is there anything else?
14:18:02 -!- MizardX has quit (Ping timeout: 248 seconds).
14:18:08 -!- ztirf4 has quit (Quit: Nettalk6 - www.ntalk.de).
14:29:53 <alise> axiom interact : Interaction pre final transform result β (Ο:Worldish) β pre Ο β (result β transform Ο β Ξ¦ Worldish (Ξ»Οβ β final Οβ))
14:30:04 <alise> I think Worldish has to be an opaque type.
14:30:21 <alise> That still lets us use the old world, though...
14:31:55 <alise> 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 <alise> Except with all the bits involving World omitted.
14:32:09 <alise> Except then you just move the problem of worlds to the conditions.
14:32:27 <Sgeo> I think I'm going to try learning Common Lisp
14:36:41 <Sgeo> 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:51:19 -!- MizardX has joined.
14:54:07 -!- ais523 has quit (Ping timeout: 265 seconds).
14:54:45 -!- ais523 has joined.
14:55:28 <ais523> my entire system was being really slow, for some reason
14:55:42 <ais523> the DNS server in particular; I'm not sure if that's deliberate or not, but I changed the DNS to level3's
15:00:03 <AnMaster> <ais523> alise: planned Feather syntax is [ x | f x ] <-- yay Feather!
15:00:25 <ais523> AnMaster: I thought you only had one line of scrollback? or did alise invent that?
15:00:45 <AnMaster> ais523, it's from the esoteric false rumours file
15:01:00 <ais523> haha, #esoteric so needs a rumors.tru and rumors.fal
15:01:01 <alise> ais523: he read the logs
15:01:19 <AnMaster> I read highlights and their context in logs
15:01:19 <alise> rumors.tru: alise is a girl pretending to be a man pretending to be a girl.
15:01:26 <alise> latex genii: how do i make an invisible char the same width as another given char?
15:01:28 <ais523> rumors.fal: #esoteric's logs come from sustainable forest
15:01:46 <ais523> I know it's possible, and where to find out how, but not the actual command
15:02:03 <alise> rumors.mu: This rumour is false.
15:02:08 <ais523> alise: that sounds right, yes
15:02:16 <alise> hphantom, I think ,yes
15:02:22 <alise> even works in TeXmacs
15:02:32 <AnMaster> there is a vertical version too iirc
15:02:41 <alise> AnMaster: gah, but it seems to treat it as not italic
15:02:43 <ais523> or just \phantom generally
15:02:44 <AnMaster> and possible one that does both vertical and horizontal (not sure about that)
15:02:54 <alise> very, very subtle spacing issues
15:03:03 <ais523> alise: you could italicise inside the \phantom, or doesn't that work?
15:03:15 <AnMaster> ais523, did I mention I put a -6 em vertical spacer at the top of a minipage yesteday?
15:03:26 <ais523> AnMaster: no, or at least not to me
15:04:00 <alise> nope, it's still too long
15:04:10 <AnMaster> 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 <alise> I'm trying to make _! look the same as the n! in the definition
15:04:24 <alise> so I'm doing \underline{\phantom{n}}, but the first line is too long
15:04:26 <AnMaster> so I had to move it up using negative spacer
15:04:41 <ais523> alise: oh, try \phantom{$n$}
15:04:46 <ais523> that's a math n, not an italic n, presumably
15:05:20 <AnMaster> ais523, err? does phantom inside math mode exit math mode?
15:05:46 <ais523> AnMaster: I don't actually know; is it a math mode command, though?
15:06:16 <AnMaster> ais523, I think it works in either
15:07:03 <AnMaster> 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:48 <ais523> 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 <AnMaster> what exactly is alise trying to do?
15:10:04 <AnMaster> I mean, I saw what he said, but he didn't say what part of it should align
15:10:07 <alise> ais523: ! isn't italic
15:10:22 <alise> _ and n should have same width
15:10:22 <AnMaster> alise, if you want those to align on the : and = ?
15:10:25 <alise> i.e., ! and ! should align
15:10:30 <alise> AnMaster: no, I already handle that
15:10:49 <AnMaster> alise, I was about to suggest eqnarray environment or something
15:11:08 <AnMaster> alise, also since n and _ are not in monospace there I assume?
15:11:21 <AnMaster> then it might be hard to make them equal width
15:11:49 <alise> they're italicy variably thingy
15:11:59 <ais523> AnMaster: why are you even suggesting monospace for a TeX-typeset document?
15:12:02 <alise> it's not an actual _ character
15:12:12 <alise> \underline{\phantom{n}}
15:12:17 <alise> but that's wider than n, somehow
15:12:20 <alise> perhaps the underline has padding
15:12:38 <AnMaster> alise, perhaps, why not add a negative spacer in there to compensate!
15:12:47 <ais523> AnMaster: because that is missing the point of TeX
15:13:05 <ais523> 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 <alise> AnMaster: because i'd have to get it totally exact
15:13:30 <AnMaster> 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 <AnMaster> ais523, wrt. negative spacers and latex that is
15:13:59 <ais523> even positive spacers are normally semantically incorrect
15:14:03 <AnMaster> ais523, also I have used mono space in a LaTeX document, for a code listing
15:14:11 <alise> also, this is texmacs; so almost identical but slightly different typesetting algo
15:14:16 <AnMaster> but that is the only case I can think of
15:14:17 <alise> i imagine it's the same in tex thogh
15:14:46 <ais523> (/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 <ais523> AnMaster: because sometimes, it's faster not to use an IDE
15:15:10 <ais523> whether for programming, or for typesetting
15:15:18 <AnMaster> ais523, he said texmacs, not emacs
15:15:33 <AnMaster> and texmacs has the same idea as lyx basically
15:16:05 -!- alise_ has joined.
15:16:11 <alise_> AnMaster: because lyx is harder to use
15:16:16 <AnMaster> 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 <alise_> Someone paste the last few lines to me
15:16:26 <AnMaster> <ais523> (/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> <ais523> AnMaster: because sometimes, it's faster not to use an IDE
15:16:26 <AnMaster> <ais523> whether for programming, or for typesetting
15:16:26 <AnMaster> <AnMaster> ais523, he said texmacs, not emacs
15:16:27 <AnMaster> <AnMaster> and texmacs has the same idea as lyx basically
15:16:44 <AnMaster> alise_, the line above that was where I asked "why not lyx"
15:17:03 <alise_> 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 <AnMaster> alise_, I never found LyX hard to use once you learnt it
15:17:14 <alise_> It looks exactly like .ps TeX output to me
15:17:16 <AnMaster> further, I found it well worth the time it took to learn LyX
15:17:41 <AnMaster> <alise_> 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 <alise_> in LyX: click click click click click click click click
15:18:15 <AnMaster> alise_, no? there are keyboard shortcuts for everything in LyX reallyt
15:18:27 <AnMaster> and it shows them in the status bar when you select a command
15:18:29 <alise_> 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 <alise_> Go on then, what is the shortcut?
15:19:27 <AnMaster> alise_, I had to look up the latter, because I very rarely use it
15:19:35 <AnMaster> the former, "insert math formula" is ctrl-m
15:19:36 <ais523> AnMaster: the leading control-M isn't needed for alt-M shortcuts
15:19:50 <ais523> it's harmless to give it, but you can omit it as an abbreviation
15:19:51 <AnMaster> ais523, oh? well, since I so rarely use eqnarray
15:20:02 <AnMaster> I haven't bothered learning that one
15:20:09 <alise_> everything after what-is-the-shortcut took ages
15:20:19 <ais523> AnMaster: : he's lagging
15:20:39 <ais523> and that second : was a tab-complete fail, assume it's a stray newt or something
15:20:41 <AnMaster> and I'm not going to be like ehird and complain about other people lagging :P
15:20:41 <alise_> Alt-M T E. Well, may be acceptable.
15:20:42 <alise_> LyX has a windows binary, right?
15:21:44 <AnMaster> alise_, lyx tends to have somewhat emacs-y key bindings for some things, but you can configure that somewhere iirc
15:22:23 <AnMaster> 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 <alise> Maybe I'll try LyX next time, then.
15:23:32 <alise> I really ought to name my language someyear.
15:23:34 <AnMaster> 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 <AnMaster> interestingly opening preferences in lyx shows (dialog-show prefs)
15:24:33 <AnMaster> I wasn't aware lyx used anything lispish internally
15:24:46 <ais523> AnMaster: you mean WYSIWYM?
15:24:56 <AnMaster> ais523, ah yeah, thought it was "want"
15:24:57 <ais523> AnMaster: it uses sexp notation for commands, I think
15:25:02 <alise> *WYSIWYG. WYSIWY[WM] is a lie.
15:25:16 -!- alise_ has quit (Ping timeout: 252 seconds).
15:25:29 <ais523> 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 <AnMaster> 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:58 <ais523> also, it typesets relatively terribly, about as well as Word
15:25:59 <alise> What you see is not even what you get.
15:26:03 <AnMaster> plus floats are shown as boxes with a thingy saying it is a float at the top
15:26:05 <ais523> (although TeX typesets the finished product)
15:26:14 <ais523> AnMaster: yes, I mean onscreen
15:26:40 <AnMaster> alise, it can be set to instant preview math formulas though
15:26:55 <AnMaster> when you leave the equation it will render it, takes a split second
15:27:08 <alise> AnMaster: so can auctex for emacs (that mode is a work of art, btw)
15:27:13 <alise> (possibly the nicest typesetting environment ever created)
15:27:22 <AnMaster> alise, why aren't you using that then?
15:27:42 <alise> 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 <alise> speaking of can't be arsed to set things up on windows,
15:27:57 <alise> How should I install Ubuntu given that all I have is a costly 3G stick connection?
15:28:04 <alise> Ship-It is not an option.
15:28:10 <AnMaster> alise, well, lyx would need latex installed somewhere it can run it
15:28:21 <alise> AnMaster: Oh. TeXmacs is self-contained.
15:28:35 <alise> (It isn't actualy TeX. Or Emacs.)
15:28:36 <AnMaster> alise, perhaps the lyx windows installer includes latex?
15:29:40 <ais523> 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 <alise> http://www.gnu.org/software/auctex/img/preview-screenshot.png ;; yum
15:29:42 <AnMaster> 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:30:07 <alise> ais523: Well, I'll certainly try LyX now.
15:30:28 <ais523> I've used it; it seems to be decent enough for what it does, but has a few annoyances
15:30:37 <ais523> such as no easy way to type the prime character, as in a'
15:30:54 <ais523> pressing ' doesn't work
15:31:13 <AnMaster> ais523, it renders as a primelooking one in the instant preview for me
15:31:14 <ais523> you have to do M-m e M-m '
15:31:25 <ais523> AnMaster: oh, but as a plain quote in the ordinary window?
15:31:34 -!- alise_ has joined.
15:31:41 <ais523> because there is a way to do a superscripted prime that renders as one in LyX
15:31:48 <alise_> Not just since my last utterance; I probably missed things.
15:32:29 <ais523> ugh, sorry, this internet's being insanely slow today for some reason
15:32:37 <AnMaster> ais523, well, they *could* be different, but to me they look pixel identical. But yes when editing they look different
15:32:49 <ais523> http://pastebin.ca/1830126
15:32:54 <alise_> AnMaster: No, but that's /two/ page loads, and this connection is... well...
15:33:02 <ais523> also, this mouse is doing so badly I even just used control-C control-V to paste
15:33:09 <AnMaster> ais523, you could also type \prime
15:33:15 <ais523> umm, http://pastebin.ca/raw/1830126 for convenience
15:33:23 <ais523> AnMaster: wouldn't you have to unescape the \
15:33:32 <ais523> I thought \ means \ (as in, $backslash$) in LyX
15:33:37 <ais523> and it only did formatting if you told it to
15:33:37 <AnMaster> ais523, ? In math mode it doesn't
15:33:50 <AnMaster> ais523, it shows auto completion for \commands in math mode even
15:34:01 <ais523> especially as there's a perfectly sensible shortcut for command-introducer \
15:34:06 <ais523> although I forget what it is, offhand
15:34:09 -!- alise__ has joined.
15:34:16 <AnMaster> ais523, you mean insert a tex box?
15:34:21 <AnMaster> ais523, but looking at the view source I see: $ $$p^{\prime}'$
15:34:26 -!- alise has quit (Ping timeout: 252 seconds).
15:34:28 <alise__> So, 22.[15:27] <alise> How should I install Ubuntu given that all I have is a costly 3G stick connection?
15:34:29 <AnMaster> but yes, that renders as two prime symbols
15:34:51 <ais523> alise__: I'm not sure that you easily can
15:35:12 <ais523> do you live near enough to someone with a stock of them to just ask them for one?
15:35:19 <alise__> AnMaster: does lyx let me write A<tab>a<tab>(a<tab>->a<tab>) and get {forall} {greek a} ({greek a} {right arrow} {greek a})?
15:35:21 <AnMaster> ais523, anyway typing ^\prime was faster than the key combo you suggested
15:35:46 <AnMaster> ais523, what would the A<tab> do?
15:35:51 <alise__> alise__: No. I could get to Birmingham in some hours, though, and stalk you!
15:35:53 <ais523> AnMaster: you're turning me more and more off LyX as time goes on here
15:35:59 <alise__> Presumably you have at least one Ubuntu cD.
15:36:02 <ais523> alise__: nickping fail
15:36:07 <alise__> A<tab> gives forall symbol
15:36:10 <ais523> alise__: two, but they're both rather old versions
15:36:15 <AnMaster> alise__, \for<tab> completed the forall symbol here
15:36:24 <alise__> AnMaster: A<tab> is faster
15:36:33 <alise__> Does a<tab> give greek alpha?
15:36:38 <alise__> Wow, this is the most confusing maze of nickpings ever.
15:36:49 <AnMaster> alise__, why would it auto complete plain letters?
15:36:49 <alise__> AnMaster: Does -> give right-arrow?
15:36:51 <ais523> alise__: it's alt-M G a in LyX
15:37:02 <alise__> AnMaster: Does -> give right arrow?
15:37:22 -!- alise_ has quit (Ping timeout: 252 seconds).
15:37:27 <AnMaster> alise__, in math mode? No, but AltGr-i seems to insert the latex one
15:37:42 <alise__> Then LyX is useless to me.
15:37:54 <alise__> I use TeXmacs because it lets me mainly type ASCII-ish stuff and get what I want.
15:38:06 <AnMaster> alise__, well sure, if you don't like the exact key bindings
15:38:11 <alise__> NN->NN^+{right arrow key}->a<tab>
15:38:25 <alise__> {blackboard N} {right arrow} {blackboard n with superscript +} {right arrow} {greek alpha}
15:38:26 <AnMaster> alise__, does alpha<tab> give you a single alphpa?
15:38:48 <AnMaster> alise__, on what? last letter?
15:38:52 <alise__> for instance, |<tab> gives \vee
15:39:03 <AnMaster> also, what if I want aleph instead?
15:39:08 <AnMaster> alise__, how would one type that?
15:39:18 <alise__> \aleph. it probably has some shortcut
15:39:26 <alise__> also, @ is for circle stuff, so @@ = infinity, @+ = circled +, etc
15:39:30 <alise__> it's actually very, very handy
15:39:34 <alise__> AnMaster: maybe it is. maybe it's something else
15:39:44 <alise__> so it's probably not a<tab^N>
15:40:10 -!- cpressey has joined.
15:40:17 <AnMaster> alise__, what about an actual @?
15:41:00 <alise__> Which is actually \text<RET>@<right>
15:41:55 <alise__> Yeah, A-$ @ right is soooo horrible.
15:42:05 <AnMaster> alise__, I wouldn't write @@, since it is on altgr here, that is not so easy as \infty<any whitespace char>
15:42:06 <alise__> Especially as @ is /so/ /common/ in mathematics.
15:42:11 <alise__> Of course, @ outside of an equation still produces @.
15:43:08 <AnMaster> 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 <ais523> AnMaster: the issue's mostly with the interface
15:43:28 <ais523> I have no issues with the general concept, just the details
15:44:08 <AnMaster> ais523, I would hate to edit in Computer Modern on a "normal" dpi desktop monitor
15:44:17 <alise__> But you're okay with reading it?
15:44:23 <alise__> Also, TeXmacs allows you to choose among fonts
15:44:31 <AnMaster> alise__, well I wouldn't use CM unless I aim to print it
15:44:41 <alise__> So choose another font. You are boring.
15:44:48 <AnMaster> if it is primarily intended for on screen reading, I would use another font
15:45:34 <AnMaster> 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 <alise__> I don't feel like talking to you about this any more.
15:46:18 <AnMaster> well, I have other things to do as well
15:46:45 <alise__> I don't, but (nothing) is better than this.
15:46:51 <alise__> [15:46] == #Ο Illegal channel name
15:48:09 <AnMaster> ais523, if doing direct latex editing I found kile quite nice
15:48:23 <alise__> auctex. No competition at all.
15:49:46 <alise__> Microsoft Works is preinstalled on this computer.
15:50:15 <AnMaster> now you must use that instead!
15:50:18 <alise__> Apparently Ctrl - = delete and Ctrl + is increase font size, but it's also its own inverse.
15:51:00 <alise__> In Microsoft Works Word Processor.
15:52:07 <ais523> I know, I used to use it to some extent
15:52:09 <alise__> ais523: Also, I implemented the Lambda Calculus of Continuations.
15:52:24 <ais523> apart from the word processor; the computer came preinstalled with Works - word processor, and Word
15:53:35 <ais523> I was busy argumenting in two other channels, so was distracted even from a nickping
15:53:39 <alise__> ais523: Hey, it's for Feather.
15:53:53 <ais523> what did you implement it in? Haskell?
15:54:03 <AnMaster> alise__, how well does bibtex integrate with TeXmacs?
15:54:30 <alise__> AnMaster: TeXmacs is not tex at all.
15:54:49 <AnMaster> alise__, well, what does it use for a replacement of bibtex then?
15:55:46 <alise__> ais523: http://pastie.org/861515.txt?key=n5pnirguwnncksdk7homzq. So, we have two main structures:
15:56:13 <alise__> There are constraints: f must be a lambda expression, not another application.
15:56:25 <ais523> alise__: that's nice and short
15:56:28 <alise__> There are constraints: in f(x,k), f, x and k must be lambda expressions, not applications.
15:56:55 <alise__> In (\x,k.E), E must be an application. (I neglected to include this in my implementation)
15:57:03 <alise__> (LCC t should be LCC App).
15:57:23 <alise__> So, we have: no nested applications, and forced continuation "arguments".
15:57:39 <alise__> It has the interesting property of making application a triadic operation (since k isn't "really" an argument)
15:58:01 <alise__> Anyway, it's basicaly just the lambda calculus, except continuation-passing style is enforced.
15:58:16 <alise__> I'll probably write a CPS-converter for it.
15:58:40 <alise__> ais523: A disadvantage of my representation is that I can't pretty-print it without a lot of fuss.
15:59:38 <ais523> so what you've implemented is LC+continuations, but restricted such that CPS is enforced?
15:59:42 <alise__> ais523: But that's no issue with the actual calculus.
15:59:50 <alise__> Continuations are done with CPS.
16:00:14 <alise__> 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 <cpressey> My god, Works is still around?
16:00:25 <ais523> cpressey: apparently so
16:00:27 <alise__> (As in, you don't have to write "normal" functions that don't do stupid shit with k.)
16:00:31 <ais523> IIRC, Microsoft are trying to get rid of it though
16:01:03 <cpressey> The first hit on Google is under microsoft.com/uk/
16:05:24 -!- oerjan has joined.
16:07:15 <oerjan> <alise> 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:54 <alise__> 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:58 <cpressey> 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 <cpressey> You may commence talkin' smack about it.
16:08:09 <alise__> oerjan: I mean physical comfort, not mental-anguish-comfort. :P
16:08:38 <alise__> cpressey: Well look at that, you have specification of theorems now :P
16:09:07 <cpressey> alise__: It's just for clarity; itrepeated in the body of
16:09:35 <cpressey> Or rather, its the first step of the proof
16:09:44 <ais523> cpressey: that doesn't look like the Peano axioms that you've assumed at the start, but rather something else
16:09:54 <oerjan> 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 <ais523> also, I love that qed is a keyword
16:10:08 <cpressey> ais523: I'm kind of leaving out the ones I don't need. Actually I don't need the zero?
16:10:11 <alise__> I /very/ much like proof/qed as structures, though. :-)
16:10:21 <ais523> hmm yes, looks like you don't
16:11:05 <cpressey> Kind of disturbing that it only relies on a fragment of Peano arithmetic, but it is very simple I guess
16:11:52 <cpressey> 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 <cpressey> like, case tree -> branch A B ... case tree -> leaf X ...
16:12:16 <alise__> oerjan: i think you have depression :P
16:12:17 <alise__> or are just /the/ /most/ cynical person there is
16:12:23 <cpressey> Which means non-deterministic rewrite rules :/
16:12:38 <alise__> oerjan: what do you think of ultrafinitism? :D
16:12:45 <alise__> find x (branch A B) -> ...
16:13:01 <cpressey> Well, not "non deterministic" so much as "ambiguous outside the presence of cases"
16:13:15 <cpressey> I mean, to describe what is a tree
16:13:29 <cpressey> tree -> (leaf X); tree -> (branch A B)
16:14:13 <alise__> if you rewrite App [Expr] | Symbol String | Free String
16:14:14 <alise__> App [Symbol "find", Free "X", App [Symbol "leaf", Free "X"]]
16:14:17 <oerjan> alise__: (1) quite possibly. (2) don't really know what it is.
16:14:44 -!- BeholdMyGlory has joined.
16:15:42 <cpressey> alise__: Not so easy; to have predicates would require building a theory of booleans
16:16:06 -!- alise has joined.
16:16:29 <cpressey> Which clearly could be done, and might be done first to make this easier
16:16:32 <alise> 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 <alise> that everything that cannot exist in this universe - like sufficiently big integers - does not exist
16:16:48 <cpressey> But then, I wonder if I would have to use predicates to prove theorems about my theory of booleans :P
16:17:06 <alise> correspondingly, that "real" analysis is completely bunk
16:17:23 <cpressey> Or at least, that it does not "exist"
16:17:25 <alise> and that godel was wrong because all the impossible proveys are in fact merely meaningless
16:17:40 <alise> well not "wrong" but
16:18:08 <alise> (ii) the traditional real line is a meaningless concept. Instead the real REAL `line', is neither real,
16:18:10 <alise> (ii) the traditional real line is a meaningless concept. Instead the real REAL `line', is neither real,
16:18:13 <alise> (ii) the traditional real line is a meaningless concept. Instead the real REAL `line', is neither real,
16:18:16 <cpressey> When a mathematican says "exist" they mean something quite specific
16:18:19 <alise> nor a line. It is a discrete necklace! In other words R = hZp, where p is a huge and unknowable
16:18:30 <alise> (but xed!) prime number, and h is a tiny, but not innitesimal , `mesh size'.
16:18:37 <alise> cpressey: the worst thing is /this guy is a professor/
16:18:48 -!- alise__ has quit (Ping timeout: 252 seconds).
16:19:06 <cpressey> alise: That's bad, but there are worse, much worse, out there. This guy, being a mathematician, is relatively harmless.
16:19:12 <cpressey> Since mathematics is irrelevant.
16:19:39 * oerjan beats cpressey with the saucepan of doom ===\__/
16:20:31 <oerjan> alise: planck length anyone?
16:20:32 <alise> ais523: bleh, /you/ implement CPS for that calculus :P
16:20:40 <alise> oerjan: Planck length... OF THE REALS
16:21:29 <cpressey> 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 <cpressey> Damn, scambled the order of those.
16:22:28 <alise> ais523: so, do you know what the bootstrap progam will look like for feather?
16:22:47 <ais523> alise: not yet; I tried to write it in Scheme, but went mad
16:22:48 <cpressey> Also, Kronecker was wrong. God invented the *primes*. The integers I blame on the devil.
16:22:50 <oerjan> well R3 can be taken rational. although you still get problems with the sufficiently big integers.
16:23:05 <alise> ais523: well clearly it must be written in the lambda calculus of continuations!
16:23:05 <oerjan> cpressey: clearly then addition is demonic
16:23:16 <alise> cpressey: Ooh, a number system based entirely on primes? Tell me more
16:23:30 <alise> oerjan: that's the thing though, ultrafinitism means that not even infinite rationals exist
16:23:38 <alise> because you run out of integers to put on either side
16:23:42 <ais523> alise: the problem was an infinite loop in trying to define "atoms", which is the next stage in the bootstrapping
16:23:57 <cpressey> 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 <alise> ais523: hmm... atoms as in symbols, I presume
16:24:13 <ais523> they're basically objects that can be compared to other atoms
16:24:15 <alise> atoms aren't the same thing as symbols :)
16:24:19 <oerjan> ais523: clearly you need renormalization :D
16:24:23 <ais523> alise: atom as in Prolog
16:24:34 <ais523> alise: the issue is making them forward-compatible with actual Feather atoms
16:24:46 <ais523> you can use a fake-object at the start of the bootstrapping, but not later
16:24:58 <alise> symbol : a = (() -> ((b = (b -> bool)), a))
16:25:02 <ais523> 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:21 <ais523> and the reason it doesn't work is, there's no implementation for the symbol you could use
16:25:35 <alise> 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 <alise> ais523: well, symbols are identified by their name, right?
16:25:49 <alise> no two symbols have the same name
16:25:59 <alise> then make them lists of church numerals
16:26:18 <ais523> yep, you can do that; but how do you return it using that typing?
16:26:44 <cpressey> Return it? What do you think this is, a library book?
16:26:57 <alise> ais523: well, you don't
16:27:04 <alise> you just implement:
16:27:15 <alise> because, presumably, your input is a string of characters
16:27:17 <alise> i.e. list of church numerals
16:27:19 <alise> so you have it right ther
16:27:26 <alise> 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 <oerjan> alise: typeclass restriction on a maybe?
16:30:07 <oerjan> 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:27 <alise_> everything said after (just a wild guess)?
16:30:35 <oerjan> 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:32:17 <alise_> ais523: I'm writing a syntax for the Lambda Calculus of Continuations
16:32:23 <ais523> alise_: this doesn't actually work, but http://pastebin.ca/1830205
16:32:29 <ais523> that's the start of an attempt to implement Feather
16:32:44 <ais523> 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 <alise_> it'll provide sugar for the most common case of application
16:32:53 <alise_> so e.g. this is what S will look like:
16:33:15 <alise_> (haven't written sugar for that yet :D)
16:33:22 <alise_> but, say you want to make a list
16:33:28 -!- alise has quit (Ping timeout: 252 seconds).
16:33:54 <ais523> I can't even remember the difference between a fakeobject and an object offhand
16:33:55 <alise_> cons2 := cons 2 cons1;
16:34:03 <alise_> cons2 := cons 2 cons1;
16:34:09 <alise_> cons3 := cons 3 cons2;
16:34:26 <alise_> that's k (cons 3 (cons 2 (cons 1 nil)))
16:36:07 <alise_> <- is bound to the most recent explicit lambda-abstraction's return argument if a name wasn't provided
16:36:38 <alise_> \x. <- \y. <- \z. xz := x z; yz := y z; r := xz yz; <- r
16:37:16 <alise_> ais523: does that seem like a reasonable syntax to you?
16:37:17 <alise_> hmm, I just realised my definition is incorrect, in that continuations shouldn't get continuation arguments themselves
16:37:18 <alise_> ideally, it'd be possible to implement feather in it
16:37:31 <alise_> ais523: it lets you do naming quite nicely
16:37:38 <ais523> alise_: vaguely reasonable, yes
16:39:21 <alise_> cwcc := id (\f. r := f <-; <- r)
16:39:26 <fax> have a problem
16:39:35 <alise_> that is the same thing as just (\f. f <-) lol :P
16:39:43 <fax> I need to (today and tommorow) solve some problems
16:40:14 <alise_> 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 <fax> but what will probably happen is I just sit on the computer doing nothing
16:40:49 <alise_> fax: akrasia! or, well, the case more commonly known as procrastination
16:41:39 <fax> I need to solve lots of ODEs so that I am able to do it quicky and accurately (REALLY USEFUL SKILL!!)
16:46:46 -!- alise has joined.
16:46:48 <alise> http://us.metamath.org/mmsolitaire/mms.html
16:46:50 <alise> metamath solitaire
16:47:24 -!- alise_ has quit (Ping timeout: 252 seconds).
16:47:50 <fax> alise have you see sokoban in coq?
16:48:00 <fax> playing the game <=> proving a level has a solution
16:48:02 <alise> that one you wrote?
16:48:07 <fax> I didn't write it
16:48:10 <alise> (i stalked all your blog :P)
16:48:38 <oerjan> 04:39:47 <ais523> I'm not convinced that (\x. f x) is the same function
16:48:38 <oerjan> 04:40:04 <ais523> it certainly isn't in a strict lang if determining the value of f has side effects
16:48:48 <oerjan> it's not even true in haskell
16:48:57 <alise> haskell isn't pure though
16:49:11 <fax> and it has the most evil thing of all
16:49:19 <fax> RECURSION!
16:49:27 <alise> fax: *GENERAL recursion
16:49:30 <oerjan> seq (\x -> undefined x) is different from seq undefined
16:50:07 <oerjan> fax: recursion is not the problem for eta reduction though
16:50:35 <oerjan> eta reduction : identifying \x -> f x with f
16:51:11 <fax> oh right I understand
16:51:11 <oerjan> it's consistent with pure lambda calculus, which can do recursion using the y combinator
16:51:21 -!- kar8nga has joined.
16:51:55 <alise> ais523: i have a real live copy of word 2007 here, let's see who was right about it
16:52:23 <ais523> as in, who said what to be right or wrong?
16:52:38 <alise> I said it probably isn't so bad, you said it's horrible
16:52:51 * fax needs help
16:53:06 <oerjan> 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 <fax> that's sounds scary
16:56:38 <ais523> oerjan: I used that (where legal under the as-if principle) in at least one of my Underload interps
16:56:49 <ais523> for optimisation purposes
16:56:53 -!- zeotrope has joined.
16:56:55 <ais523> hmm, or was it an Underlambda interp?
16:58:21 <ais523> I know what it normally means, but it doesn't seem to make sense in this context
16:58:22 <HackEgo> * 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 <alise> I like Word 2007's equation editor
16:59:07 <oerjan> clearly the second meaning is intended
16:59:24 <fizzie> Like flip but less upside-down; like blit but more fly.
16:59:53 <alise> flit would be a god name for an esolang
17:03:43 -!- jcp has joined.
17:09:11 <alise> fax: constructivist metamath!
17:09:19 -!- tombom has joined.
17:09:21 -!- tombom has quit (Changing host).
17:09:21 -!- tombom has joined.
17:11:21 <fax> my proposal is more modest
17:11:23 <alise> fax: imagine metamath, but constructivist
17:11:44 <fax> alise, do you want to do this?
17:11:49 <fax> and I mean literally do this
17:12:03 <alise> it would certainly be cool.
17:12:27 <fax> I think so too
17:12:37 <alise> define this though
17:15:52 <Ilari> "filt" would be language with no explicit looping, but data being passed between components?
17:17:22 <HackEgo> * 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:22:58 <AnMaster> which I'm not completely sure of how to translate to English
17:23:08 <HackEgo> 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:24:46 <AnMaster> the second one seems completely wrong
17:24:52 <AnMaster> the third one I have no clue what it means
17:25:00 <AnMaster> the last one also seems suspect
17:25:38 <ais523> oh, I know the concept you mean
17:25:46 <ais523> "industry" has two meanings in English
17:26:01 <ais523> so all 4 words give much the same meaning
17:26:10 <AnMaster> oerjan, I think I used it wrong
17:26:15 <oerjan> `translatefromto no en flid
17:26:25 <ais523> AnMaster: in multiple words, think "tendency to work hard" for the second meaning
17:26:35 <AnMaster> ais523, isn't that the meaning for the first one?
17:27:01 <AnMaster> ais523, and that would be sv:flitig, flit is as google said a noun
17:27:08 <ais523> the more common meaning is a collective noun for all the companies/factories that manufacture things
17:27:30 <ais523> and "tendency to work hard" is a noun, as tendencies are nouns
17:27:49 <alise> fax: yeah i think constructivist metamath would be really awesome
17:27:57 <alise> especially if the proofs were actually in executable form
17:28:06 <oerjan> AnMaster: i think the second one uses a more original meaning of industry
17:30:19 <cpressey> I thought that was some kind of government slogan
17:30:33 <cpressey> DILIGENCE! INDUSTRY! ASSIDUITY! APPLICATION!
17:30:35 <alise> No One Industry, or Tendency To Work Hard?
17:31:12 <cpressey> Adherence to these principles makes our society strong!
17:31:17 <ais523> anyway, I think I know what sv:flit means
17:31:22 <ais523> first word of Swedish I know!
17:32:15 <oerjan> ais523: from now on, you can choose from a veritable smΓΆrgΓ₯sbord of them
17:34:03 <alise> 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 <cpressey> And will help us solve a large number of ODEs in a short amount of time!
17:34:43 <ais523> assuming ODE = ordinary differential equation, that makes no sense
17:34:47 <ais523> unless it's some sort of pun I don't getg
17:35:04 <oerjan> ais523: i think it's a hint to fax
17:35:09 <alise> along with the type of the resulting composition
17:35:28 <alise> ais523: fax said e had to do a bunch of them a while ago
17:35:52 <cpressey> ais523: I was riffing on what fax was saying earlier
17:35:53 <ais523> also, whats with the Agoranese?
17:36:06 <alise> fax: + nested proofs, perhaps that's tc
17:39:57 <cpressey> Thank you ais523, I am now exactly as confused about feather as I was before.
17:40:15 <cpressey> There are fake things in it. I can tell that much.
17:40:21 <alise> Feather is ALL FAKE
17:40:26 <ais523> actually, that's an implementation technique
17:40:28 <oerjan> ais523: _clearly_ you need renormalization
17:40:39 <cpressey> Drat, so even the fake stuff is... fake
17:40:57 <ais523> well, no, because the details of the implementation are relevant to the actual lang
17:41:00 <alise> fake(fake(X)) -> fake(X)
17:41:03 <ais523> hmm, I may have to leave again, my head's hurting
17:41:21 <alise> exists P. Component(Feather,P) & Fake(Fake(X))
17:41:27 <alise> -> exists P. Component(Feather,P) & Fake(X)
17:41:35 <alise> So yes, there are fake things in Feather.
17:41:40 <alise> Even if they're not actually in it.
17:41:54 <cpressey> OK, so "relevant, but somewhat arbitrary" =/= fake, true
17:42:28 <alise> 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 <alise> If a fake fake thing isn't fake, then what?
17:42:48 <oerjan> and how is something fake, true?
17:42:49 <ais523> basically, a fakeobject is something that obeys a subset of the restrictions necessary to be considered an object
17:42:59 <alise> Fakeobjects, although fake, are actually real? So they're legitimate objects? No.
17:43:01 <cpressey> Feather, to me, sounds like a way to fold nondeterminism. For some ill-defined notion of "fold"
17:43:01 <alise> Nothing fake is true, obviously.
17:43:05 <alise> Now go make a logical system where ~~p -> ~p.
17:43:26 <alise> I must now goify for... 15 minutes? Do that logical system. Nao.
17:43:31 <ais523> 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 <oerjan> cpressey: the poker sense
17:46:32 <alise> 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 <alise> so all previous continuations in some way account for this
17:46:44 <alise> potential nondeterminism
17:56:27 <cpressey> 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 <cpressey> 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 <cpressey> *finite and boolean expressions.
17:58:43 <cpressey> I need to prove that I've implemented "and" correctly! Clearly, such complex functions are not to be trusted without proofs
17:59:42 <cpressey> But figuring this out might give me insight on how to approach more practical proofs
18:00:19 <fax> cpressey, I don't understand....
18:00:49 <fax> you want to prove that a term with type bool is a boolean?
18:01:34 <cpressey> fax: Ah, see there is where I am in different waters from you and alise. My terms don't have types.
18:02:34 <fax> maybe this is the problem :P
18:07:27 <cpressey> Lack of types shouldn't be a huge barrier.
18:07:45 <cpressey> 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 <cpressey> 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:51 <cpressey> "type" just means "set of values", anyway.
18:09:59 <cpressey> I'm having more trouble with variables
18:10:23 -!- jcp has joined.
18:11:17 <fax> cpressey, what about variables?
18:18:52 <cpressey> http://dpaste.com/170053/ <-- have cases now, but still need to tackle induction
18:19:28 <cpressey> 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 <cpressey> It probably works out saner with the variables. But I'm finding it easier to do the other way.
18:22:21 <cpressey> 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:23:19 <fax> 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 <fax> (by baseless induction)
18:24:06 <cpressey> 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 <cpressey> If you have a diverging term, yes.
18:24:36 <cpressey> Hard to prove the type of a diverging term...
18:33:27 <cpressey> grr, now i keep reading the word as "boo-lean"
18:34:24 <cpressey> So, induction. Yeah. Fun stuff, teaching a computer how to do mathematical induction.
18:34:48 <cpressey> In MI one of your cases relies on the other.
18:34:54 <cpressey> Is it fair to call the base case a lemma?
18:35:13 <alise> cpressey: an example of how better deptypes are
18:35:13 <alise> induction = recursion
18:35:23 <alise> you prove induction and the function it results in does recursion
18:35:32 <fax> induction is not recursion :P
18:35:59 <fax> the elaboration you did is good but "induction = recursion" is nonsense
18:36:57 <cpressey> Awkward to state it as a lemma because it only proves certain cases
18:37:10 <cpressey> Awkward to have cases depend on previous cases too, though
18:37:20 <fax> 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 <cpressey> fax: I was going to say, dependent types are an ambulance :)
18:38:11 <fax> now that's vauge enough for me not to be able to attack :P
18:38:44 <alise_> 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:39:09 <oerjan> too much dependent types and you'll need an ambulance
18:39:29 <lament> better dependent than delinquent
18:39:59 <alise_> also it took me a while to realise that (exists (x:T). a) is a dependent tuple...
18:39:59 <fax> FWIW hardly anyone can actual program with dependent types
18:40:07 <alise_> fax: MY LANGUAGE WILL FIX THAT
18:40:14 <fax> including alise :p
18:40:22 <cpressey> 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:38 <alise_> fax: why did you use sum rather than exists for the exists symbol btw?
18:41:03 <fax> convention
18:41:08 -!- ais523 has quit (Remote host closed the connection).
18:41:13 <fax> also 'exists' is a proof thing, Sigma is the data version
18:41:14 <alise_> cpressey: forall P:Nat->*, P 0 -> (forall n:Nat, P n -> P (succ n)) -> forall n:Nat, P n
18:41:18 <fax> Prop vs Type
18:41:24 <alise_> fax: why not have it polymorphic on both
18:41:26 -!- alise has quit (Ping timeout: 252 seconds).
18:41:41 <alise_> i guess i'm still seeing proof elimination as an optimisation
18:42:22 <alise_> fax: also is \sum or \sigma more correct? I think \sum since you have \prod for forall
18:42:30 <alise_> although wait, doesn't that mean that \prod is the data version of forall?
18:42:48 <alise_> so \Pi is functions and \forall is just for profs
18:43:07 <alise_> which I think is taking it too far. which is why I think I disagree with separating \Sigma and \exists
18:44:13 <alise_> feel free to tell me i'm stupid tho :P
18:44:30 <alise_> fax: so \Sigma or \exists?
18:44:43 <alise_> fax: so \Sigma or \sum?
18:44:54 <alise_> since we also have \Pi or \prod i bet sum
18:45:06 <alise_> as the coincidence is a bit too much to accept
18:45:23 <fax> I don't know what \Sigma or \sum is
18:45:40 <alise_> uh basically \sum is a big \Sigma like you use for sums..
18:45:45 <cpressey> http://dpaste.com/170070/ <-- there's my stab at MI.
18:45:47 <alise_> different unicode chars
18:46:19 <alise_> 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 <alise_> wait, what /other/ induction does cpressey have?
18:46:56 <cpressey> alise_: What makes you think it's not confluent? Or are you complaining I haven't proved it such?
18:47:10 <alise_> it... looks sorta nonconfluent :P
18:47:41 <alise_> It pisses me off that I can't do (Foo (x:T). a) syntax myself
18:48:00 <alise_> Foo_._ would work if you have (x:T)
18:48:02 <oerjan> presumably \exists and \forall are sums and products in a suitable category...
18:48:05 <alise_> but (x:T) isn't anything coherent by itself
18:48:09 <cpressey> 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:24 <cpressey> I have to prove properties about my proof system :/
18:48:33 <alise_> and then define Foo_._ ... but that's ambiguous I think
18:48:44 <alise_> myndzi: oh god not again
18:49:19 <cpressey> Any mathematicians here know anything about Galois connections?
18:49:22 <alise_> fax: so data β(_:_)._ : (a : Set) β (P : a β Prop) β Set where right?
18:49:30 -!- hiato has joined.
18:49:33 <alise_> because you use exists to do the computable reals
18:49:36 <lament> oh no, off by one error \o/
18:50:06 <alise_> oh wait Foo(_:_)._ isn't acceptable because i need to bind the var and stuff
18:50:52 <hiato> myndzi: plus ten for that
18:50:53 <cpressey> No wait, case 2 doesn't rely on case 1
18:51:02 <oerjan> galois connections rings a bell...
18:51:54 <alise_> cpressey: just come to the dark side.
18:52:13 <cpressey> Uh, I need to prove boolexpr ~> boolean, that implies (not boolexpr) ~> boolean
18:52:38 <alise_> obvious : β(P:Prop). Obvious P β P
18:52:50 <alise_> Give me a proof that a certain proof is obvious, and I'll give you the proof!
18:53:06 <fax> Obvious "P" -> P
18:53:52 <alise_> hmm maybe you're right
18:57:03 <cpressey> 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 <cpressey> 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 <cpressey> Maybe those rules should be backwards, though.
18:59:33 <cpressey> true -> boolean, false -> boolean
18:59:57 <alise_> That means true and false are indistinguishable
19:00:13 <alise_> fax: I would use guillemets, though:
19:00:14 <cpressey> In a type system, they are. They're both booleans. I wanted a boolean result, great I have one.
19:00:15 <alise_> obvious : β(P:Prop). Obvious Β«PΒ» β P
19:01:04 <cpressey> 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 <oerjan> 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:46 <alise_> cpressey: a -> b doesn't mean that when you choose to rewrite a it results in b
19:01:50 <alise_> it means that a is /just an alias/ for b
19:02:09 <cpressey> alise_: Not what it means to me
19:02:12 <alise_> fax: I've been thinking about the interaction axiom
19:02:18 <cpressey> Not even sure what "just an alias" is supposed to mean in this context
19:03:19 <alise_> axiom interact : Interaction pre final transform result β (Ο:Worldish) β pre Ο β (result β transform Ο β Ξ¦ Worldish (Ξ»Οβ β final Οβ))
19:03:24 <alise_> (where capital phi was my dependent tuple)
19:03:26 <alise_> 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 <alise_> both are unacceptable for the same reason
19:03:38 <alise_> i.e., that the previous world/conditions don't become unacceptable
19:03:44 <alise_> so I need to eliminate them, somehow
19:09:34 -!- ais523 has joined.
19:09:39 <alise_> "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:49 <alise_> apparently that's how the memory-safe C compiler works
19:10:01 <ais523> alise_: yes, that's correct
19:10:29 <ais523> in fact, even comparing with < can cause a crash in some compilers
19:11:15 <ais523> anyway, someone posted something in another channel that made Konversation segfault, apparently
19:11:22 <ais523> I'm not sure whether to shout at them or congratulate them
19:11:46 * hiato chuckles to himself (c2h?)
19:12:35 <alise_> ais523: hmm... this is making me want to write a pure c compiler
19:15:31 <fizzie> 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 <fax> 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 <alise> Is the typed ski + fix turing-complete?
19:16:55 <fax> http://community.wolframalpha.com/viewtopic.php?f=32&t=6774
19:17:05 <ais523> it's being parsed as -(4^4)
19:19:12 -!- alise_ has quit (Ping timeout: 252 seconds).
19:20:31 <oerjan> alise: it can do everything you need with church numerals can it not
19:20:44 <oerjan> so all recursive functions
19:20:55 <alise> oerjan: The point is that typed SK isn't turing-complete, presumably (because typed LC is not).
19:21:03 <alise> I'm talking idiotically typed, here
19:21:07 <alise> as in arrow and Base
19:21:19 <ais523> <Safari download page> The worldβs best browser. Free download for Mac + PC.
19:21:24 <alise> So is idiotically-typed SKF complete?
19:21:26 <ais523> they don't have a Linux version, though
19:21:38 <ais523> the download page is specifically a Windows one, and they directed me to it
19:21:55 <ais523> I was messing about with browserchoice.eu
19:22:10 <ais523> all their advertising doesn't say "os x and windows", but "mac and PC"
19:22:21 <oerjan> 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:23:28 <alise> anyone have that nice ~> symbol?
19:23:34 <cpressey> http://dpaste.com/170084/ <-- last cleanup for now.
19:24:08 -!- kar8nga has quit (Remote host closed the connection).
19:24:14 -!- alise_ has joined.
19:24:17 <alise_> no, it's just like -->
19:24:38 <ais523> β is the closest I can find
19:24:41 <Gregor> 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 <cpressey> I can barely see the squiggling at this font size, but it's there
19:24:43 <ais523> "rightwards squiggle arrow2
19:25:12 <ais523> except then, why do Apple advertise Parallels?
19:25:16 <alise_> Maybe it's just a latex thing
19:25:18 <pikhq> Gregor: More so Apple than Microsoft.
19:25:32 <Gregor> pikhq: I would say about equal.
19:25:37 <alise_> apple even have parallels on their apple store computers
19:25:42 <pikhq> Since Microsoft doesn't care *too* much so long as their OS is running on it.
19:25:46 <alise_> you think microsoft would advertise mac compatibility?
19:25:55 <alise_> apple are a hardware company, microsoft not
19:26:04 <Gregor> 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 <alise_> ok then, what about the => char?
19:26:07 <alise_> that is also acceptable
19:26:10 <pikhq> Apple is first and foremost a hardware manufacturer, and sells their hardware based on OS features.
19:26:52 <Gregor> 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 <cpressey> As long as Apple are not a grammar company.
19:27:16 <Gregor> 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 <pikhq> What Microsoft wants is to confuse people into thinking that "Microsoft" == "program".
19:29:35 <Gregor> Dude, I downloaded this Microsoft, but I think it was spyware, it installed like eight other Microsofts on my Microsoft!
19:30:13 <AnMaster> static discharge against a car *through thick gloves*
19:30:16 <alise_> Gregor: what has little to no benefit?
19:30:45 <ais523> AnMaster: woolen, or leather?
19:31:01 <Gregor> 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 <AnMaster> ais523, wool/acrylic mix I think
19:31:27 <alise_> 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:39 <alise_> The markup is something like 30% on the lower-end models, typical of boutique products. On the higher end models? Less.
19:31:57 <ais523> 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 <alise_> The image of it being a high quality product because of its social/fashion status.
19:32:17 <Gregor> alise_: Uhh, isn't that exactly my point?
19:32:27 <alise_> Gregor: Yes, but it's not a hugely unreasonable margin. But.
19:32:40 <alise_> 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 <AnMaster> 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 <AnMaster> so it must have been a huge charge
19:32:59 <alise_> The higher-end model of it comes with a Core i7 - at that point the profit margins just keep diminishing.
19:33:03 <ais523> 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 <AnMaster> still feels somewhat from it in my thumb
19:33:13 <alise_> 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 <alise_> And the top-of-the-range 27" iMac is probably the cheapest way to get all those components.
19:33:30 <cpressey> I don't think we fully understand static electricity
19:33:37 <alise_> and its low range has a higher-than-average profit margin
19:34:02 <cpressey> I have seen it be very bad in humid environments and very mild in dry environments in the winter
19:34:12 <cpressey> Which is not how I was told it was supposed to work
19:34:21 <AnMaster> cpressey, I usually see the reverse of that
19:34:45 <cpressey> I don't doubt it, but maybe there is some other correlate
19:35:06 <AnMaster> cpressey, perhaps something specific to that environment? Or was the observation made in different places?
19:35:09 <ais523> 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 <ais523> 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 <ais523> and if it had charged up far enough, you can feel it
19:35:50 <cpressey> Different geographical locations, yes, I would guess it might vary on something else that was different between them
19:36:09 <ais523> alise_: what about β
19:36:46 <fax> ais my cats ears
19:37:20 <Gregor> Ohhey, looks like we traded out Miss Piggy.
19:40:37 <fax> Gregorification.
19:41:37 <Gregor> How Gregarious it is to Greglorify.
19:42:53 <fax> Definition DiscreteDerivative (f : Z -> Z) (x : Z) := f (x + 1) - f x.
19:43:34 <fax> Notation "β" := DiscreteDerivative.
19:43:39 <fax> alise paying attention??
19:49:21 <alise_> http://pastie.org/861902.txt?key=71fbadzjph5ovvw9xvbkxa this is pretty but not valid
19:49:42 <alise_> because `βͺββ« = βa. SKF a` means that β¦_β§ is too fancy for its own type :(
19:49:44 <fax> re. your earlier question: YES
19:50:02 <alise_> I've forgotten the earlier question. I ask so many...
19:50:31 <fax> SKI is equivalent to STLC, but STLC + fix is recursive
19:50:53 <alise_> by SKI I assume you mean STSKI there
19:51:46 <alise_> if my interpreter wasn't broken i'd have done sum tc'ing
19:51:50 <alise_> mind it is particularly pretty broken code
19:55:25 <alise_> fax: so why did you define discrete derivative there?
19:55:43 <alise_> 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 <fax> I'm implementing the finite calculus!
20:02:57 <alise_> how does Notation work btw?
20:04:51 <lament> finitists can't have limits either? How do you do calculus at all?
20:05:07 <lament> just numerically, with some estimate of the error?
20:05:25 <fax> lament, finite calculus is about finite sums :D
20:05:29 <alise_> lament: i'm talking ultrafinitists here
20:05:32 -!- Azstal has joined.
20:05:40 <fax> like Sum[i=1..n] i^2
20:05:46 <alise_> if IE wasn't being a bitch I'd link you
20:06:03 <ais523> what specifically's the problem with IE?
20:06:14 <lament> thanks, i don't really wanna know
20:06:17 <alise_> lament: http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/real.pdf
20:06:21 <alise_> lament: oh you do, it's hilarious
20:06:29 <lament> no i really don't trust me
20:06:42 <alise_> ais523: all keyboard shortcuts and commands are being ignored
20:06:57 <alise_> lament: basically there's some defined mesh size of the reals
20:06:58 <ais523> I'm pretty sure that isn't intentional behaviour
20:07:03 <alise_> and you treat it as an infinitesimal
20:07:15 <alise_> (actual, real mesh size, as a "universal constant")
20:07:58 <lament> since it's gotta be scale-invariant anyway
20:08:16 <alise_> lament: in real.pdf he does it paramaterisabled
20:08:21 -!- Asztal has quit (Ping timeout: 258 seconds).
20:08:25 -!- Azstal has changed nick to Asztal.
20:08:27 <alise_> cpressey: and the integers are finite
20:08:31 <alise_> or more precisely the integers don't exist
20:08:32 <lament> probably easier to prove it's scale-invariant and then set it to 1
20:08:40 <alise_> fax: vacuous : βa, (P : β₯ β β), (x:β₯). P x!
20:08:55 <cpressey> "exist" is more precise than "finite" now is it
20:09:14 <alise_> fax: supertype of set and prop
20:09:43 <lament> but what's the ultrafinitist perspective on nullity??
20:09:55 <alise_> lament: it's totally yeah man
20:10:31 <ais523> alise_: is that pdf meant to be serious?
20:10:41 <alise_> zeilberg is a fucking nutcase :)
20:10:42 <ais523> I can't tell whether it's a parody, or just deluded people
20:10:56 <alise_> btw this guy is a professor
20:11:16 <alise_> vacuous {_} {_} {x} = explosion x
20:11:19 <alise_> hooray for ex falso quodlibet
20:11:47 <alise_> the best thing is though you can say that
20:12:14 <alise_> and all sorts of fun stuff besides
20:12:26 <ais523> "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 <ais523> isn't a similar principle used for distributing INTERCAL?
20:13:05 <oerjan> alise_: if you define !x = x then you get !!x = !x for free ;D
20:13:51 <oerjan> another option is the modal necessity operator
20:13:57 <ais523> 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 <ais523> <ais523> 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 <alise> ais523: yep, except not quite
20:14:50 <alise> it can't be smaller than the planck length
20:15:02 <alise> well unless you pack multiple bits of info into one tiny particle
20:15:09 <ais523> who says that maths and physics have the same fundamental measurements?
20:15:12 <alise> i guess not in zeilberger's ultrafinitism
20:15:23 <alise> but most ultrafinitists are such because of physical limits
20:15:35 <alise> i.e. you can't have an infinite set of natural numbers because you can never compute it all
20:15:54 <alise> you can't have a really tiny rational because there isn't the space to show its tininess
20:16:16 <ais523> I love the talk about sqrt(2) not actually existing after all, because distances don't exist, just areas
20:16:47 <cpressey> Guess what? It's the consistent part that's important.
20:17:04 <alise> "consistent" fiction
20:17:22 <cpressey> ZFC is too powerful for my taste.
20:17:30 -!- alise_ has quit (Ping timeout: 252 seconds).
20:17:53 <alise> I thought you liked consistency :P
20:18:15 <alise> ais523: I like how he says that Goedel is "irrelevant" because the things it applies to have no meaning
20:18:20 <alise> but that isn't even implied by rejecting all infinites
20:18:26 <alise> goedel numbers are huge but not infinite...
20:18:34 <alise> and certainly not so huge that we can't represent them
20:19:31 <alise> 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 <alise> fax: just write it :P
20:19:55 <fax> "..." means induction I guess
20:20:14 <alise> fax: zeilberger will love you
20:20:19 <alise> are you defining R := his definition too? :D
20:21:41 -!- alise_ has joined.
20:22:02 -!- whtspc has joined.
20:22:03 <alise_> what I missed I desire elaboration upon
20:23:14 -!- whtspc has quit (Client Quit).
20:23:39 <cpressey> 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 <alise_> 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 <alise_> Also, I have an unstoppable urge now to define his paramaterisable finite universe.
20:24:54 <cpressey> "Suppose x is even." "Well suppose it's not!"
20:28:42 <alise_> Presumably the mesh size h is an ultrafinitist-rational.
20:28:44 <alise_> And p is an ultrafinitist-natural.
20:28:49 <cpressey> 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 <alise_> The problem is that the Ultrafinitism module is paramaterised over h and p, so how do you do it?
20:29:29 <cpressey> I didn't read it as being parameterized.
20:29:47 <cpressey> A very small, unidentified constant. But not variable.
20:30:01 <alise_> But he parameterises it later in his analysis.
20:30:15 <alise_> (Because you don't know what it is.)
20:30:22 <alise_> And, of course, we don't know their True Universal Values, so for now we must specify it
20:30:31 <cpressey> Trying very very hard not to LOL, natch.
20:30:46 <alise_> Until the Ultrafinitist Physicist Association of America completes its experiments.
20:31:40 <alise_> With their grant from NAO2^{80}PSA, the National Aeronautics and Observable 2^80 Particles of Space Administration.
20:33:23 <alise_> fax: are you sure you don't have the link to that site
20:33:28 <fax> what site?
20:33:41 <alise_> 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 <alise_> saying that oh in the past they did this all by hand ha ha ha
20:33:50 <fax> I told you I don't know what you're talking about
20:33:53 <alise_> and it defined a bunch of maths in it
20:33:56 <alise_> ugghh yes you do you linked to it
20:37:35 <fax> just explain it so that I understand what you meanl
20:37:38 <alise_> fax: it was either in maple or ... i think coq
20:37:48 <alise_> its name was an acronym, i think a deliberately-amusing one
20:37:51 <fax> Ah Zeilbergers book!
20:38:04 <fax> http://www.math.rutgers.edu/~zeilberg/GT.html
20:38:09 <alise_> how come it wasn't ultrafinitist
20:38:20 <fax> Zeilberger is one of my idols
20:38:33 <alise_> you /idolise/ this insane man?
20:38:38 <fax> I don't really have idols but I really enjoy his work
20:38:40 <alise_> he doesn't believe there are any infinite sets...
20:38:50 <fax> have you ever seen an infinite set?
20:39:19 <fax> (and don't say, yeah in my ZFC textbook: I can write "magic rainbow unicorn" on a bit of paper too)
20:39:27 <alise_> no, i mean exist as in mathematically
20:39:36 <alise_> he thinks the definition of the reals is R = hZ_p
20:40:06 <alise_> yes, but he's /talking/ about abstract systems
20:40:19 <fax> that's radical
20:40:33 <alise_> and talks about the REAL real line
20:40:33 <alise_> as if anything abstract is "real"
20:40:37 -!- Gracenotes has joined.
20:40:38 <cpressey> 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:51 -!- alise has joined.
20:40:58 <alise> fax: it's a word starting with r
20:41:00 <alise> i'd go for retarded
20:41:23 <oklokok> no you couldn't, {a^n | n \in N} doesn't contain an infinite word
20:42:25 <cpressey> That's true, it doesn't even, at that.
20:42:53 <cpressey> All the more reason to go ultrafinitish!
20:42:57 <alise> 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 <cpressey> But wait, it's still an infinite *set*, right?
20:44:08 <alise> N = {0, 1, 2, 3, ..., p}
20:44:18 <alise> he never says p is the biggest natural
20:44:19 <fax> you are young alise, sometimes you say things which rembind me of that
20:44:20 <alise> or indeed the biggest prime
20:44:30 <alise> obviously it must be the biggest prime or the definition of R would make no sense
20:44:45 <alise> so |N| = p and a bit :P
20:44:54 <oklokok> 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 <alise_> "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:47:20 <cpressey> I would probably describe myself as a mathematical generativist, or something.
20:47:36 <alise_> constructivism, hells yeah
20:48:24 <alise_> i was just asserting my own position
20:48:39 <cpressey> I was just clarifying my own :)
20:49:02 -!- alise has quit (Ping timeout: 252 seconds).
20:50:03 <oklokok> alise_: why wouldn't the definition of R make sense if p wasn't prime?
20:50:24 <fax> needs a prime p to be a field ?
20:50:26 <oklokok> i don't really even believe in finite numbers, actually i often wonder whether i exist
20:51:00 <cpressey> It's a matter of whether you regard computations to "halt" or not, I think.
20:51:01 <oklokok> it's not a field, p is so big you can't actually do division
20:51:03 <fax> now THAT is radical
20:51:31 <cpressey> CA's never "halt" unless I have some way to recognize what I want "halt" to look like
20:51:33 <alise_> oklokok: nonono, he asserts that it is prime
20:51:33 <alise_> 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 <alise_> fax: it's not a field, big + n is undefined
20:51:42 <cpressey> TMs are assumed to "halt" because recognizing it is trivial
20:52:06 <oklokok> 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 <oklokok> there is an inverse but it's incredibly big so it's irrelevant
20:53:08 <oklokok> 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 <alise_> no coppro is the poo-lovin' guy
20:54:17 <oklokok> cpressey: what's a matter of whether to regard computations to halt or not?
20:54:26 <oklokok> the constructing an infinite set thing?
20:54:43 <cpressey> 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 <alise_> cpressey: just 3g stick lag
20:55:08 <cpressey> oklokok: Whether there are finite numbers, or not, or infinite numbers, or not
20:55:44 <oklokok> is 1.0000... an infinite number?
20:56:18 <oklokok> 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 <oklokok> so in fact we're working in some sort of universe of representations here?
20:58:04 -!- oklokok has changed nick to o|{|_o9o|_.
20:58:24 -!- alise_ has set topic: arys.
20:58:32 <o|{|_o9o|_> i should go clean up random parts of the apartment
20:58:33 -!- alise_ has changed nick to arys.
20:58:47 <cpressey> 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:21 <arys> DFEHGJIKGMLINGPOQIKG$L5RS&TUMVGJI@WJX)YZE)[\R?G^]NEHGJIKGLINGMSR?'aOcbML5R?d5GJVI@L5[\eS&TUMVGJI@WJf - zeilberger
21:01:22 <arys> fucking copy from pdf
21:01:33 <arys> http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/goodwin.pdf
21:01:41 <arys> he isn't even consistent about ultrafinitism
21:01:44 <arys> see first paragraph
21:02:07 <arys> joke paper, but
21:02:46 <cpressey> Perhaps he believes Aleph is a finite value.
21:04:45 -!- lament has quit (Ping timeout: 245 seconds).
21:04:45 <arys> now now he never said that x in N -> x < p
21:04:46 <arys> 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 <alise> fax: should i learn coq?
21:07:45 <lament> how i stopped worrying and learned to love the coq
21:09:12 -!- arys has quit (Ping timeout: 252 seconds).
21:09:49 <fax> Eval compute in Discrete_Definite_Integral 1 5 (fun x => x).
21:12:00 <alise> paste the code somewhere
21:12:16 <fax> = 1 + 2 + 3 + 4 + 5
21:12:49 * fax is about to prove Fundamental_Theorem_Of_Finite_Calculus
21:12:58 <fax> cpressey, it's correct within experimental error
21:13:09 <alise> fax: experimental error my arse :P
21:23:14 <cpressey> So, my woes are all because a mock object is not sufficiently mocking the the thing it set out to mock, huh?
21:32:48 <o|{|_o9o|_> the discrete definite integral from 1 to 5 is the sum from 1 to 4
21:34:27 -!- hiato has quit (Quit: leaving).
21:35:24 <alise> fax: show yer koed
21:35:46 <o|{|_o9o|_> 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 <cpressey> The code sounds like it would be trivial to me.
21:36:28 <FireFly> Who's the o guy...ah, should've guessed
21:37:04 <alise> cpressey: yeah but proving fundamental theorem of finite calculus will be fun
21:37:25 <o|{|_o9o|_> what i just said is basically the proof
21:37:38 <o|{|_o9o|_> although i skipped it completely because it's obvious
21:37:54 <o|{|_o9o|_> i mean the "it's because given f ..." thing
21:38:45 <o|{|_o9o|_> no wait actually what's the fundamental theorem
21:38:58 <fax> alise, I will when it's done
21:39:12 <fax> I'm still working on proving Fundamental_Theorem_Of_Finite_Calculus
21:39:27 <alise> o|{|_o9o|_: inversitude
21:39:43 <fax> 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 <alise> fax: because of you :P
21:40:02 <o|{|_o9o|_> aren't we talking about finite calculus because you brought it up?
21:40:23 <ais523> 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:35 <o|{|_o9o|_> or alternatively can someone link the paper?
21:42:57 <fax> the finite calculus paper? http://www.stanford.edu/~dgleich/publications/finite-calculus.pdf ?
21:43:12 <fax> I thought you already had it
21:44:58 <o|{|_o9o|_> okay yeah then i proved it by saying it's obvious
21:45:41 <cpressey> I don't know how to correct that impression
21:46:32 <o|{|_o9o|_> 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:47:12 <ais523> <enkafan> 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 <ais523> this is one of the best flamewars I've seen for a while
21:49:26 * fax proved the fundamental theorem :D
21:49:55 <cpressey> #esoteric is full of proofs today
21:50:00 <cpressey> Maybe we'll open up the bonus level
21:50:03 <o|{|_o9o|_> i really don't see what there is to prove
21:50:18 <fax> o|{|_o9o|_, I mean formal proof
21:50:38 <o|{|_o9o|_> if you sum adjacent values of f(x+1)-f(x)'s, obviously all but the left and rightmost ones cancel out
21:51:02 <o|{|_o9o|_> then i obviously have no idea how hard it is
21:51:04 <fax> o|{|_o9o|_, oh and, I used "The Fundamental Theorem" as my definition, which means MY fundamental theorem is their definition
21:51:33 <fax> 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:55 <oerjan> 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:44 -!- Daexpos has left (?).
21:55:07 <cpressey> And all present were enlightened, I'm sure.
21:55:35 <oerjan> that's the ablative of penis, right?
21:55:56 <pikhq> Fax intends to ablate your penis.
21:56:16 <pikhq> I don't know what ablate means, but it sounds painful.
21:56:26 <HackEgo> * wear away through erosion or vaporization \ * remove an organ or bodily structure \ [14]wordnetweb.princeton.edu/perl/webwn
21:56:37 <pikhq> It is in fact quite painful.
21:56:49 <HackEgo> * 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 <pikhq> Or at best, very shocking.
21:57:03 <HackEgo> * 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:59:17 <lament> oh, fricate. not fornicate.
22:01:57 -!- werdan7 has quit (Ping timeout: 619 seconds).
22:02:10 -!- Gracenotes has quit (Quit: Leaving).
22:08:14 -!- werdan7 has joined.
22:12:11 <ais523> Quadrescence: from where?
22:12:41 <Quadrescence> and after all this time I thought I was an asset to the channel :(((((((((((((((((((((((((((((((((((((((((((((
22:14:27 <Quadrescence> lament: |Steve| did because I banned him from ~m
22:16:00 <lament> such tit-for-tat brinkmanship
22:16:38 <lament> 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 <lament> Quadrescence: i'm using all my diplomatic finesse to get you unbanned
22:20:20 <lament> so expect a permaban, probably in #math too
22:21:24 <lament> nono i'm not getting *myself* in trouble :D
22:23:42 <o|{|_o9o|_> "oerjan: lol" <<< is it just me or is this really out of character
22:24:06 <o|{|_o9o|_> or was that just the first thing ever you found funny here
22:24:14 <Quadrescence> I found this quite funny: [16:17.27] * oerjan seems to be having troubles with his sarcasm meter
22:24:50 <o|{|_o9o|_> oerjan leaks this constant flow of hilarious humor
22:24:59 -!- cpressey has changed nick to cpressez.
22:25:41 <oerjan> Quadrescence: i found lament's comment hard to measure
22:26:50 -!- muni_ has joined.
22:27:52 <cpressez> I suppose that's better than "I love you." "ROTFL"
22:28:35 <oerjan> (yeah i'm just messing with o|{|_o9o|_ now)
22:29:32 <fax> why did alise just disappear like that?
22:32:12 <oerjan> maybe i should ban myself
22:32:32 <fax> okklopkuabp
22:32:37 -!- tombom has quit (Quit: Leaving).
22:32:39 <ais523> yep, he has ops nowadays
22:32:40 <fax> you didn't respond
22:32:44 -!- o|{|_o9o|_ has changed nick to oklopol.
22:33:18 <oklopol> 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:50 <oklopol> you asked me whether 8, or what?
22:34:30 -!- MigoMipo has quit (Remote host closed the connection).
22:34:42 -!- muni_ has left (?).
22:35:03 <oerjan> cpressez: you zuddenlee look very french
22:35:43 <fax> this is really frustrating
22:39:11 -!- cpressez has changed nick to cpressey.
22:39:33 -!- alise has joined.
22:39:46 -!- jcp has quit (Ping timeout: 258 seconds).
22:41:08 -!- jcp has joined.
22:44:07 <alise> 13:46:32 <o|{|_o9o|_> 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:13 <alise> everything that is true is an obvious tautology :P
22:44:57 <fax> There are no trivial mathematics, only trivial mathematicians!
22:45:28 <oerjan> cpressey: you're quite limber, i take
22:45:48 <cpressey> oerjan: I am on IRC, at least.
22:46:20 -!- BeholdMyGlory has quit (Remote host closed the connection).
22:47:26 <lament> \o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/\o/
22:47:26 <myndzi> | | | | | | | | | | | | | | | | |
22:47:26 <myndzi> >\/| /| /< /< /'\/΄\/< /< /< |\ |\/`\ |\/< |\/|
22:47:37 <lament> very few of them have dicks.
22:48:02 <alise> are there actually spaces before? if so, my client strips them >_<
22:48:13 <alise> there used to be iirc
22:49:03 <alise> 14:27:52 <cpressez> I suppose that's better than "I love you." "ROTFL"
22:49:04 -!- cheater2 has quit (Read error: Connection reset by peer).
22:49:30 -!- cheater2 has joined.
22:49:53 -!- alise has left (?).
22:49:59 -!- alise has joined.
22:50:40 <lament> that script is the only reason i go to #esoteric
22:50:47 <oklopol> "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 <alise> in the logs it's spaces /and/ some other char
22:52:38 <lament> Quadrescence: ur the only reason fax goes to #esoteric
22:52:50 -!- cpressey has left (?).
22:53:22 <alise> #~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 <alise> well, I guess it's #(~esoteric), not ~(#esoteric)
22:54:53 <alise> EgoBot is talking?
22:57:36 <oerjan> he's just using facilitated communication
22:59:09 <lament> 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 <alise> if so, lament made the right choice :p
22:59:22 -!- coppro has joined.
22:59:37 <ais523> "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 <ais523> alise: the situation for a disputed endgame in Go is even funnier than I thought
22:59:58 <Quadrescence> 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 <alise> You get nothing! You LOSE! Good DAY sir.
23:00:14 <ais523> I love the way that the double loss is given for getting it wrong, rather than for disagreement
23:00:57 <alise> i wonder how many famous games of go are actually platonically a double loss
23:01:02 <alise> but nobody's realised
23:01:12 <oerjan> alise: except with more honorifics
23:01:41 <oklopol> i wonder how many chess games actually ended with the white winning, but the players thought black won.
23:01:42 <ais523> alise: probably not that many in famous games, you'd expect the players to get it right
23:02:04 <oklopol> for draws, there probably are such instances
23:02:16 <ais523> 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:20 <ais523> in a relatively publicised tournament
23:02:31 <alise> ais523: that's cheating
23:02:50 <ais523> alise: by the referee?
23:02:53 <ais523> it was a mistake, rather than deliberate
23:02:58 <alise> 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 <alise> ais523: i mean as an example
23:03:03 <oklopol> it's cheating as an answer to my wonderingment
23:03:40 <alise> Note that X or Y can be "draw"
23:03:45 -!- FireFly has quit (Quit: Leaving).
23:04:20 -!- lament has quit (Ping timeout: 245 seconds).
23:05:01 <ais523> 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 <ais523> legally, you can still take the draw in that situation
23:05:26 <ais523> (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 <ais523> (so there's no point in offering more than once in the same move)
23:05:49 <oklopol> 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 <ais523> yep, I suppose so vaguely
23:06:33 <alise> http://sci.tech-archive.net/Archive/sci.logic/2006-10/msg00751.html
23:06:34 -!- lament has joined.
23:06:41 <ais523> actually, there are probably loads of draws on time which were claimed as wins on time by mistake
23:06:59 <ais523> (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 <fax> alise "Yessenin-Volpin"? wow a THIRD ultra-finitist??
23:07:28 <alise> fax: they don't even include what'shisname in that list
23:07:32 <alise> the guy we've been talking about
23:07:35 <lament> japanese rules allow draws on time???
23:07:36 <alise> so there are FOUR???
23:07:53 <lament> fax: the number of ultrafinitists is getting dangerously big
23:08:02 <alise> this movement has gained its maximum possible mass (I don't believe in 4)
23:08:05 <lament> fax: what if it overflows???
23:08:06 <fax> lament, lol
23:08:15 <ais523> it's always theoretically possible to play Go so badly that your opponent wins
23:08:18 <alise> lament: damn you made the same joke as me but beter
23:08:18 <oerjan> lament: dammit stealing my joke
23:09:59 <fax> alise, you know Freek Wiedijk
23:11:01 <alise> fax: resend your latest /msg, i closed the tab by mistake
23:11:11 <lament> ais523: that can't possibly be true, do you see why??
23:11:34 <ais523> lament: the game lasts an infinite length of time if both people try it
23:11:45 <oklopol> i'm sure everyone thought of the joke
23:11:50 <ais523> hmm, unless you enforce superko, in which case my statement is indeed incorrect
23:12:14 <coppro> It depends on the form of superko
23:12:20 <lament> ais523: why would either of them capture at all? They would pass.
23:12:46 <lament> they ought to pass when there's one empty point remaining
23:12:54 <ais523> I somehow assumed that you'd capture with only one point left
23:13:02 <ais523> too much exposure to the stupid stupid Yahoo auto-go thing
23:13:11 <ais523> which has a bug where you can run an opponent out of time by repeated passing
23:13:22 <lament> i'm not sure what's the status if the game ends but i guess it's seki
23:13:33 <lament> either seki or "both players lose"
23:15:55 <ais523> what would be funny would be if you somehow got half a stone onto the board
23:15:59 <ais523> and then claimed a draw despite komi
23:17:19 <lament> very easy with cheap chinese stones, they break all the time
23:17:50 <Gregor> 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:19:00 <Gregor> Whoever either checkmates or takes out the opponent's king.
23:19:23 <Gregor> Which, I suppose, is problematic for the Go component ...
23:19:27 <lament> 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 <Gregor> Needs some rough edges smoothed out.
23:19:37 <Gregor> lament: That was the idea?
23:19:39 <coppro> lament: you could take it with a chess piece
23:19:48 <alise> does go have a winning condition?
23:19:50 <alise> I don't actually know
23:19:50 <lament> Gregor: well it's not quite how Go works
23:19:55 <lament> alise: no, people just fuck around.
23:20:21 <alise> an endgame condition
23:20:21 <alise> apart from like... running out of pieces
23:21:25 <lament> note that sometimes you're forced to pass due to not having any valid moves
23:21:32 <lament> but in principle a game could go on forever
23:21:44 <alise> Gregor: Checkmate/taking out/both passing = game ends.
23:21:47 <lament> there's an optional rule, which nobody uses, that disallows repetition
23:21:58 <alise> Then you can invent a hybrid chess/Go winning condition to be applied at endgame.
23:22:20 <Gregor> Well, that makes sense since both passing is an endgame condition for Chess anyway, stalemate :P
23:22:36 <Sgeo> From what little I know about Common Lisp, I despise it
23:22:46 <alise> The problem is that in chess, endgame almost always is because of someone winning.
23:22:49 <Sgeo> funcall? Really?
23:22:55 <alise> In Go that appears to be calculated after the fact.
23:23:00 <alise> Sgeo: So you can name a variable "list".
23:23:27 <alise> Gregor: You could redefine instead Go's endgame condition to be because of someone winning somehow.
23:23:41 <Gregor> 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 <alise> Maybe that's AWESOME.
23:24:16 <alise> So how does a Chess piece take a Go piece? Maybe jumping over it.
23:24:25 <Gregor> I wasn't considering that possibility ...
23:24:33 <alise> 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:57 <Gregor> So, Bishops have free take-out powers :P
23:25:21 <alise> For knights... No fucking clue.
23:25:23 <alise> Gregor: They do anyway :P
23:25:25 <coppro> I don't think you would use typical Go notions of control
23:25:38 <Gregor> coppro: Probably not quite.
23:25:45 <alise> It's not a hybrid if you significantly modify G1+G2
23:25:52 <coppro> control really just means an area that if you put a piece in, it will die eventually
23:25:53 <alise> It's your own game inspired by G1, G2.
23:26:15 <alise> The only modifications should be to resolve contradictions.
23:26:59 <coppro> 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 <alise> Gregor: You made Chesskers.
23:27:47 <alise> You're making Gochess.
23:27:59 <alise> You should add Othello to that mix.
23:28:11 <alise> Gothellochesskers.
23:28:16 <Gregor> Yes, I ... wait, whaaaa?
23:28:20 <alise> 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 <alise> Gregor: Wait, what? :D
23:28:49 <alise> Haha, imagine Chess pieces flipping colour because you connect a line.
23:29:21 <alise> Then subsequently taking Go pieces, which then surround a Checker piece, eliminating it.
23:29:40 <Gregor> Combine ALL board games into one!
23:29:44 <Gregor> Throw some Risk in there!
23:29:49 <Gregor> I think we need some 18xx!
23:30:02 <alise> But Go, Othello, Chess and Checkers are all fundamentally similar.
23:30:27 <alise> 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 <alise> 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 <Sgeo> With some simple not-necessarily-TC scripting language
23:32:04 <alise> coppro: it's closed
23:32:07 <alise> the latest version of the server at least
23:32:23 <alise> well wikipedia says an old version was open and is mum about the current, so..
23:32:37 <alise> (directly next to each other)
23:32:39 <Sgeo> Easy enough to ask
23:36:25 <Gregor> 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 <alise> COMPUTER MODERN: Disturbing
23:37:20 <oerjan> not so modern after all
23:37:39 <oerjan> somewhere, on a forgotten sumerian clay tablet...
23:38:18 <alise> the first ug was typeset by knuth
23:38:42 <oklopol> 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 <oerjan> hm is this related to surreal number ordering?
23:40:58 <alise> Totally wins; terminology first used by Euclid in his Elements.
23:41:23 <alise> "Let there be the games A, B. I say that A totally wins B.
23:41:41 <alise> First, let there be a strategy of A.
23:42:04 <alise> Let it be that when this strategy is used in AB, it is winning.
23:42:05 <oerjan> i can confirm this because strategy is a greek word.
23:42:20 <alise> If this is not so, then instead I say B totally wins A."
23:42:35 <alise> that's my piss-poor attempt at emulating the style of Elements...
23:42:39 <oklopol> oh but totally winning is a proper partial order!
23:42:57 <oklopol> so in fact it's not necessarily true that B totally wins A if A does not totally win B
23:43:36 <alise> right but that's a modern development of Winning theory
23:43:47 <alise> Euclidean winning theory doesn't have that
23:44:09 <oklopol> 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:44 -!- oerjan has quit (Quit: Good night).
23:44:54 <oklopol> now the obvious question is, is go|chess a ridiculous idea?
23:44:54 <alise> (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:46:01 <alise> oklopol: you're abusing notation, A|B is the common parts of the games A and B
23:46:13 <alise> go|chess would be a board with things that move around and remove other pieces, but past that undefined
23:46:41 <alise> (euclid wrote A|B as superscript A, subscript B.)
23:46:58 <alise> winning theory is like game theory but more indie
23:47:34 <alise> (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 <alise> Erm, that is, as a component of complex expressions.
23:49:34 <oklopol> | is an OR-like character, AB is multiplication which is an AND-like operation
23:50:13 <alise> remember that euclid thought of games as primitives
23:50:15 <oklopol> so A|B is the mix of the games, and AB is the common parts.
23:50:35 <alise> as such, (go chess) was go & chess, i.e. both go and chess.
23:50:50 <oklopol> that's what AND and OR mean in the philosophy of fuzziness.
23:53:28 <oklopol> 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 <oklopol> is there a good definition for board games somewhere?
23:54:30 <alise> clearly winning theory is our chance to invent it.
23:54:37 <oklopol> game theory is to board games sort of what category theory is to algebras, imo
23:54:49 <alise> also, euclid didn't even consider common parts by itself to be a valid formula.
23:54:57 <alise> he always built it up from there to a full game
23:55:03 -!- MizardX has quit (Ping timeout: 240 seconds).
23:56:13 <oklopol> 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 <lament> game theory doesn't talk about board games at all.
23:58:13 <fax> and the second rule of game theory: Do not talk about board games