00:09:47 -!- CakeMeat has changed nick to Lilin.
00:15:20 -!- Frooxius has quit (Quit: *bubbles away*).
00:16:58 -!- tromp has quit (Ping timeout: 250 seconds).
00:25:02 <Lilin> int-e: what was that solar flare site again?
00:25:48 <oerjan> the daystar is out there
00:28:42 <int-e> This one? http://www.tesis.lebedev.ru/en/sun_flares.html I don't recall for sure, I just googled for solar flares.
00:29:15 <FireFly> Hmm, perhaps BLC ought to be added to anagol
00:30:50 <int-e> may hard to sell with the "universal lambda" variant already there.
00:31:49 <boily> “Copyright 1953-2014”. nice.
00:48:56 -!- tromp has joined.
00:53:46 -!- S1 has quit (Quit: S1).
01:07:50 -!- shikhout has joined.
01:11:08 -!- shikhin has quit (Ping timeout: 256 seconds).
01:16:15 <CrazyM4n> So I've been reading up on turing tarpits
01:17:25 <Lilin> Dost thou needith a hug?
01:18:19 * oerjan swatteth Lilin for bad grammar -----###
01:18:52 <shachaf> oerjan: that's all it takest?
01:19:00 <oerjan> IT'S BECAUSE I'M A GRAMMAR NAZI
01:19:18 <Lilin> oerjan: is very dirty shachaf
01:19:43 <Lilin> He likes to hit people
01:22:57 * oerjan lives for the hit parades
01:23:23 <shachaf> And I like to be hit. And yet it doesn't work out.
01:33:22 <Lilin> Oh mai shachaf thats dirty
01:33:42 <shachaf> It would be nice if you stopped changing your nick every few days.
01:34:27 <Lilin> Its easier for me to lose myself
01:40:25 <oren> if P != NP why the heck can't we prove it?
01:41:29 <oren> i mean all you have to do is find ONE problem in NP and prove it's not in P, right?
01:43:38 <oren> but theres a million problems in NP. how many are not in P?
01:45:11 <oren> (how many are suspected to no tbe in P)
01:46:55 <oerjan> oren: one of the basic problems is that we don't have a real grip on how much power P itself has
01:47:49 <oerjan> so, it is very hard to prove that something _cannot_ be done in P, if none of the simple diagonalization tricks work.
01:47:49 -!- dianne has quit (Read error: error:1408F119:SSL routines:SSL3_GET_RECORD:decryption failed or bad record mac).
01:48:30 <oerjan> and it has been proved, essentially, that diagonalization _cannot_ work to prove P != NP
01:49:54 <oren> so it is essentially extremely hard to prove something is not in P
01:50:34 <oerjan> yeah. because of NP-completeness, we already _know_ which problems have to not be in P for it to be different.
01:50:42 -!- dianne has joined.
01:52:02 <oren> can we prove a subset of P? what about 'polynomial, degree below 4'
01:52:23 <oerjan> well there is a proof that SAT cannot be linear time iirc
01:52:30 <CrazyM4n> I figured out how to solve it, actually
01:53:07 <CrazyM4n> You can tell that the polynomial doesn't equal the thing that isn't a polynomial
01:53:12 <oren> because degrees above N^5 with a reasonable constant are almost useless anyway.
01:53:27 * oerjan swats CrazyM4n -----###
01:54:44 <shachaf> two swats on the same screen
01:55:07 <oren> so in other words, proving that an NP-complete problem can't be solved with degree N^4 or below would have most of the same practical consequences
01:55:09 <oerjan> shachaf: you have a big screen
01:55:53 <shachaf> my screen's resolution is so high that things break all the time :'(
01:56:05 <oerjan> oren: there's this thing i've seen mentioned - let me try to find it
01:58:06 <oerjan> hm http://blog.computationalcomplexity.org/2004/06/impagliazzos-five-worlds.html it's not as relevant to what you said
01:58:40 <oerjan> i'm sure the possibility of "P = NP but with high exponent" has been discussed here and there, though
02:01:18 -!- oerjan has quit (Quit: Good night).
02:01:59 <oren> like for example we have prime number tests in (logn)&6
02:04:30 <oren> with a large constant too
02:12:42 -!- AndoDaan has quit (Quit: bbl).
02:15:05 -!- qwertyo has joined.
02:18:20 <Jafet> @ask oerjan It hasn't been proven that SAT cannot be linear time (unless you forbid linear space)
02:25:12 <Sgeo> Aww I can't just go out and buy some Vantablack
02:25:19 * Sgeo is extremely dissappointed
02:27:27 <Lilin> Whenever you eat a chicken egg
02:27:34 <Lilin> You are eating its period
02:28:16 <Lilin> People always say im eating a chicken fetus
02:28:28 <Lilin> But you are eating something worse
02:49:07 <CrazyM4n> I wonder what Vantablack feels like
02:52:37 <boily> it's... it's disturbingly dark. I need to buy some.
03:08:26 -!- boily has quit (Quit: ULTRAVIOLET CHICKEN).
03:12:30 <oren> goths are gonna wear vantablack dresses
03:16:43 <elliott> oh man, it looks like a hole in the photos
03:19:17 -!- oren has quit (Ping timeout: 265 seconds).
03:24:09 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)).
03:51:23 -!- shikhout has quit (Ping timeout: 250 seconds).
04:16:29 -!- tswett has joined.
04:17:48 <tswett> So I'm trying to devise a type theory where, if a function is definable in the type theory, then the function's output length grows at most polynomially in its input length.
04:17:55 <tswett> Which raises a question.
04:18:19 <tswett> The type theory should allow higher-order functions, whose inputs are other functions. But what's the length of a function?
04:19:34 -!- AndoDaan has joined.
04:19:37 <tswett> Ah... I think you're right.
04:19:47 <nys> you're welcome
04:19:51 <Taneb> Obvious when you think about it
04:20:29 <tswett> Since the string "a function" contains ten letters, but the largest prime number no larger than ten is seven, so you have to add seven.
04:22:30 <Taneb> Conveniently, we don't have to add any more because 17 itself is a prime
04:24:10 <Taneb> More seriously, I think functions ought to be constant, because for something like concatMap the sizes you care about are the lists
04:25:56 <Taneb> Does that make sense?
04:26:05 <tswett> Well, I'm not sure what you mean by "ought to be constant".
04:27:15 <Taneb> Like, (a -> b) has the same size as ()
04:29:12 <Taneb> (I'm not experienced in type theory)
04:30:08 <Taneb> If you're dealing with polynomials, it doesn't matter which constant it is unless that is 0
04:30:27 <elliott> (forall a b. a -> b) is uninhabited
04:31:08 <Taneb> elliott, I meant for arbitrary a and b
04:31:31 <elliott> so (Int -> Void) should have one inhabitant? :p
04:31:46 <tswett> Well, a (() -> [()]) seems like it should have the same length as the corresponding [()].
04:32:46 <Taneb> elliott, I don't think size is the same thing as number of inhabitants in this context
04:32:59 <Taneb> tswett, that is a good point
04:33:06 <elliott> I didn't really look too much at the context, true.
04:33:50 <Taneb> Maybe something like RHS/LHS?
04:34:11 <Taneb> No, that's stupid...
04:34:29 <Taneb> And not constant for a particular function
04:35:39 <tswett> Let's consider concatMap. Its type is (a -> [b]) -> [a] -> [b].
04:36:14 <tswett> Certainly if f :: a -> [b] grows polynomially, then concatMap f :: [a] -> [b] grows polynomially, too.
04:36:29 <shachaf> I should understand the thing about groupoids having non-integer cardinality.
04:38:42 <tswett> How about the church numeral c2 :: (a -> a) -> a -> a; c2 f x = f (f x)?
04:39:29 <tswett> f could be the unary natural number squaring operator unat -> unat, where unat is [()].
04:39:52 <tswett> Then c2 f takes the fourth power.
04:40:00 <tswett> If f takes the 10th power, then c2 f takes the 100th power.
04:40:21 <tswett> There doesn't seem to be anything illegal going on here.
04:41:10 <tswett> I suppose we might be able to define "grows at most polynomially" without actually defining what length is.
04:41:44 <tswett> If you have an expression involving c2, then it doesn't seem to be possible to make the expression grow faster than polynomially.
04:42:16 <tswett> How about ap :: (a -> b -> c) -> (a -> b) -> a -> c; ap x y z = x z (y z)? Does that "grow at most polynomially"?
04:43:23 <tswett> Probably, I guess. It's not obvious to me how to define a function in STLC that doesn't "grow at most polynomially".
04:43:32 <tswett> Is that, in fact, possible?
04:44:46 <Taneb> In fact, "repeat" in Haskell
04:45:28 <tswett> I note that the number c2 c2 c2 c2 c2 is large. But c2 has a different type each time.
04:48:03 <tswett> So problems only seem to come in when you allow polymorphism or dependent typing.
04:48:22 <tswett> I'm not sure I want to know what the length of Type is.
04:50:32 <tswett> Lessee. A list of "a"s can be thought of as a "forall b, (a -> b -> b) -> b -> b". Presumably the length of a "forall b, (a -> b -> b) -> b -> b" should be (at most a polynomial in) the sum of the lengths of the elements.
04:52:10 -!- singingboyo has joined.
04:52:21 <tswett> But I think that's inconsistent. Since c2 :: (a -> a) -> a -> a is a list, it must have constant length, like 2 or something.
04:53:04 <tswett> But then the function \f g -> f g, taking two Church numerals and returning their exponentiation, is illegal, isn't it? We want \f g -> f g to be a legal function.
04:58:01 <Jafet> Forbid church numerals, or forbid applying them
04:58:38 -!- oren has joined.
05:02:02 -!- tswett_ has joined.
05:02:31 <tswett_> Well, what you can't do is apply two Church numerals of the same type together. That's exponential.
05:03:45 <tswett_> So every STLC function seems to be allowable. No STLC function takes two Church numerals of the same type and applies them together.
05:04:43 <tswett_> But there are STLC functions which add or multiply Church numerals of the same type.
05:05:35 -!- tswett has quit (Ping timeout: 272 seconds).
05:05:37 -!- tswett_ has changed nick to tswett.
05:11:54 -!- nys has quit (Quit: quit).
05:13:49 -!- supay has quit (Ping timeout: 272 seconds).
05:15:36 -!- supay has joined.
05:16:49 <tswett> Then I think we get a problem if we permit the dependently typed Church numerals. If c and d are dependently typed Church numerals, then \S -> c (S -> S) (d S) is their exponentiation.
05:17:38 <tswett> Simply typed Church numerals, good. Dependently typed Church numerals, bad.
05:19:45 <zzo38> What are dependently typed Church numerals supposed to mean?
05:21:30 -!- tswett has quit (Quit: Colloquy for iPhone - http://colloquy.mobi).
05:24:53 -!- Lilin has quit (Quit: Connection closed for inactivity).
05:26:32 -!- tswett has joined.
05:27:32 <tswett> A dependently typed Church numeral is a function of type (a : Type) -> (a -> a) -> a -> a.
05:29:28 -!- qwertyo has quit (Ping timeout: 258 seconds).
05:31:20 -!- qwertyo has joined.
05:31:58 -!- qwertyo has quit (Max SendQ exceeded).
05:32:36 -!- qwertyo has joined.
05:33:58 <oren> it is a function, mapping somthing of type a to a function, which maps functions from a to a to functions from a to a?
05:34:21 -!- atslash has quit (Read error: Connection reset by peer).
05:35:01 -!- atslash has joined.
05:35:58 <oren> a (*(*f(a))(a(*)(a)))(a)
05:36:25 <shachaf> No, its first argument is a type.
05:36:41 -!- tswett has quit (Ping timeout: 250 seconds).
05:37:09 <oren> so it maps a type a to a function mapping functions from a to a to functions from a to a?
05:37:42 <oren> that is seriously demented
05:38:32 -!- MDude has changed nick to MDream.
05:40:49 <oren> like i've heard of power sets, but this is like, a meta-powerset
05:41:35 <shachaf> It's a reasonable way to do polymorphism.
05:41:48 <shachaf> You don't even need dependent types for that sort of thing, just something like System F.
05:42:54 <oren> gyaaa... maybe if 'reasonable' is defined as 'probably will confuse more people than pointers do'
05:45:57 <zzo38> You can take a type like that even in Haskell by using Typeable and a few other stuff, I think?
05:46:02 <elliott> how weird and confusing and unreasonable to model something parameterised over types as having a type as a parameter
05:46:15 <elliott> what were type theorists thinking
05:47:24 <oren> having a type as a parameter isn't confusing, returning a member of the powerpowerset of the typeis
05:48:01 <shachaf> (a -> a) isn't the power set of a, if that's what you're getting at?
05:48:18 <elliott> the powerset of A is A -> Bool.
05:48:45 <oren> the space of functions from a to a is the powerset
05:49:00 <oren> then what is it called?
05:49:05 <elliott> powerset is 2^A i.e. A -> 2 i.e. A -> Bool
05:49:15 <elliott> endomorphism of the type A, I guess?
05:49:22 <oren> whatever you're returning some thing of the C type
05:49:29 <elliott> church numerals represent the natural n as functions taking a function f to f^n.
05:49:37 <elliott> so f has to be of type A -> A for some a.
05:49:46 <elliott> so it's (A -> A) -> (A -> A) and it works generically no matter what A is.
05:49:50 <oren> A (A (*)(A))(*)(A(*)(A))
05:49:50 <elliott> so it's (A : Type) -> (A -> A) -> (A -> A).
05:50:05 <elliott> yes, C has bad function pointer syntax, what's your point?
05:50:20 <elliott> people don't do functional programming in C. and anyway church numerals are a theoretical construct, nobody actually programs with them.
05:50:36 <oren> but how is that a "reasonable way to do polymorphism"?
05:50:51 <oren> i don't think it is
05:51:32 <elliott> that was referring to passing types as parameters.
05:51:45 <shachaf> Constructively (A -> Bool) and the power set are different. :-)
05:52:06 <elliott> oren: (church numerals *are* a perfectly reasonable way to represent the naturals in the lambda calculus, though)
05:52:18 <elliott> though they kind of suck type theoretically because you need parametricity to prove anything about them
05:53:05 <shachaf> Hmm, does Prop behave like the Sierpinski space?
05:53:38 <Jafet> The polynomial-time type system should probably be designed over terms, instead of unnatural things like numbers and lists
05:54:24 <oren> how are terms more natural than numbers?
05:54:43 <elliott> because one is a primitive notion in type theory and the other is something you build up
05:54:50 <Jafet> So the size of a term in STLC has a natural definition (after full normalization)
05:54:55 -!- qwertyo has quit (Ping timeout: 265 seconds).
05:55:06 <oren> well there's the limitation in your abstraction thn
05:55:11 -!- copumpkin has joined.
05:55:15 -!- qwertyo has joined.
05:56:01 <oren> you're taking the natural parts of your model as primitive instead of the primitive which real computers actually operate in O(1) on.
05:56:06 <Jafet> Existing polynomial-time languages need fiddly non-local restrictions though, I don't know if you can have a compositional type theory for lambda calculus
05:56:59 <elliott> oren: that's because we're talking about computer science, not computers
05:57:01 <oren> if you want to model real computers you need to insert parameters into your model which are dependent on how real computers operate
05:57:30 <elliott> you're making even more negative contributions to this discussion than I am with my whining
05:57:34 <Jafet> The only O(1) in real computers is circuit delay
05:58:38 <oren> real computers can add binary numbers of fixed size in O(1) time.
05:59:07 <oren> these numbers of fixed size come up often in real problems
05:59:15 <elliott> you only care about finite stuff? great, let's just say everything is O(1)
05:59:21 <Jafet> There was a paper on a language complete for P, but it's complicated to determine statically and I think the language was imperative
06:01:02 <oren> the size of the numeric type is fixed. the size of array types is not. you can use pragmatic principles to determine which parameters of your problem are fixed size in actual exapmles
06:01:37 <elliott> you're talking about irrelevant crap to criticise something you clearly don't understand at all. it's disruptive. please stop.
06:03:54 <HackEgo> Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: <http://esolangs.org/>. (For the other kind of esoterica, try #esoteric on irc.dal.net.)
06:05:07 <oren> it's not irrelevant to the time complexity of operations of church numbers to consider whether the church numbers are a good way of modeling your system in the first place?
06:05:22 -!- AndoDaan has quit (Ping timeout: 250 seconds).
06:05:33 -!- tswett has joined.
06:05:59 <elliott> did you even read the context? I mean I didn't at first but at least I didn't try and argue for half an hour about it
06:07:00 <elliott> actually I did, with you, but that was after I read the context
06:08:16 -!- tswett has quit (Client Quit).
06:08:24 <Jafet> Beta reductions can be implemented in polynomial time, so they can be considered as units
06:08:48 <oren> well the context involves input lengths, but church numbers have a different length than the corresponding binary numbers.
06:08:48 <Jafet> (As long as the intermediate terms grow polynomially)
06:09:02 -!- ChanServ has set channel mode: +o elliott.
06:09:05 -!- elliott has kicked oren oren.
06:09:07 -!- elliott has set channel mode: -o elliott.
06:09:30 <HackEgo> (.ten.lad.cri no ciretose# yrt ,aciretose fo dnik rehto eht roF) .>/gro.sgnalose//:ptth< :ikiw ruo tuo kcehc ,noitamrofni erom roF !tnemyolped dna ngised egaugnal gnimmargorp ciretose rof buh lanoitanretni eht ot emocleW
06:12:06 -!- drdanmaku has quit (Ping timeout: 272 seconds).
06:12:24 -!- oren has joined.
06:13:21 <oren> can you define length of a function as the number of instructions in it?
06:14:12 <oren> ellio why are you so angry?
06:15:11 <Jafet> You can use binary encoding for church numerals.
06:15:21 -!- drdanmaku has joined.
06:15:32 -!- adu has joined.
06:16:15 <oren> i guess but isn't that not the 'natural' encoding? I mean if a church number is a "function" should it not be encoded as code?
06:16:54 <oren> unless you never intend to apply it as a function?
06:17:03 -!- CrazyM4n has quit (Quit: sleep to do).
06:17:06 -!- dts|pokeball has quit (Read error: Connection reset by peer).
06:17:12 <Jafet> A polynomial-time language would probably need to distinguish between counting numbers and arithmetical numbers
06:17:46 <Jafet> If you use a number to determine the number of steps in the program, it would need to be in unary
06:18:00 -!- dts|pokeball has joined.
06:18:32 <oren> ah i get it now! but you do math with binary numbers of fixed size but these can't be used in loop conditons?
06:20:08 <oren> but how do you determine whether a number will end up being a loop condition or not?
06:21:25 <oren> oh i see church numbers are your loops?
06:22:44 <Jafet> Presumably tswett wants a compositional type theory that allows exactly the programs requiring a polynomial number of reductions on polynomial-sized terms, which is harder
06:24:00 -!- Lilin has joined.
06:24:26 -!- qwertyo has quit (Ping timeout: 250 seconds).
06:24:33 <oren> binary numbers are log sized while church numbers (in a natural encoding as code) would be O(N) sized
06:24:43 -!- qwertyo has joined.
06:27:49 <oren> am i wrong elliot?
06:30:22 <oren> hmm... elliot hates me now, just for saying that church numbers are unary.
06:31:10 <elliott> you're making a fool of yourself
06:31:18 <zzo38> Church numbers do not seem to be any base I think?
06:32:37 <oren> well the church number n is a function. the code for that function would apply that function n times. unless the code contains a loop, the code would be O(N) in te size of the code to appl the srgument once.
06:33:19 <zzo38> Such a function ca be made up from other function (other Church numbers) too though
06:33:31 <zzo38> Such as applying one to the other, to make exponentiation
06:34:19 <oren> oh crap. yeah it really depends on how the 'apply' operation is perforemed
06:34:58 -!- MoALTz has joined.
06:35:08 <oren> i assumed that constructing f(g()) is done by appending the code for f to the code for g
06:36:05 <oren> if the code for apply instead involves reparsing the function's code, then it is no longer O(1)
06:36:19 -!- qwertyo has quit (Ping timeout: 260 seconds).
06:36:30 -!- qwertyo has joined.
06:37:17 <oren> but then of course the church number n could simply be code for a loop that loops n times
06:38:07 <zzo38> Well, that is one way but it is not the only way; regardless of how it is defined it can be mathematically the same function though
06:38:29 <oren> yes but in terms of space and time complexity it matters
06:38:31 -!- qwertyo has quit (Client Quit).
06:38:57 <zzo38> Yes, the implementation does affect how efficiently it can be executed on a computer, of course.
06:42:24 <oren> but if we want to create a type system that only allows polynomial space and time,then the fact that binary numbers are log(n) space allows different things
06:42:52 <zzo38> How would a type system to only allow polynomial space and time?
06:43:14 <oren> i dunno but that is apparently what they were talking about earlier
06:44:26 <oren> a type system could certainly forbid exponential strcutures like trees to be built
06:45:26 <oren> you essentially forbid operations on your types, strategically...
06:46:58 <oren> if it were up to elliot i think all numbers would be bignums
06:48:04 <elliott> it's considerate that you misspell my name when saying crap so that it doesn't ping me but unfortunately I'm reading all of this anyway
06:48:38 <oren> so why do you hate me so much
06:49:11 <elliott> b/c I have a crush on you (I don't hate you)
06:49:30 <oren> you dislike trying to model real sytems soyou can predict real performance?
06:50:18 <elliott> 04:16:57 <tswett> So I'm trying to devise a type theory where, if a function is definable in the type theory, then the function's output length grows at most polynomially in its input length.
06:50:19 <oren> i would love a compiler that tells me how long the program will take to run...
06:50:28 <elliott> nothing you have said is relevant to what the discussion is actually about
06:50:41 <oren> input length defined in what symbols?
06:50:57 <oren> binary numbers? instructions?
06:50:59 <elliott> and saying that people should be "using" fixed-size binary integers instead of church numerals doesn't even make any sense given that the reason church numerals come up was to figure out what restrictions they'd end up having
06:51:28 <elliott> since you can define church numerals in the lambda calculus, but they allow doing too much unrestricted. it was an attempt to explore how the system would differ from more conventional type theories. I don't know why I'm explainign this to you.
06:52:26 <oren> but if you allow higher order functions you automatically allow church numbers?
06:52:50 <elliott> 04:17:05 <tswett> Which raises a question.
06:52:50 <elliott> 04:17:29 <tswett> The type theory should allow higher-order functions, whose inputs are other functions. But what's the length of a function?
06:53:24 <oren> yes i read that. the question still doe not have a real answer
06:53:28 <elliott> 05:01:40 <tswett_> Well, what you can't do is apply two Church numerals of the same type together. That's exponential.
06:53:31 <elliott> 05:02:55 <tswett_> So every STLC function seems to be allowable. No STLC function takes two Church numerals of the same type and applies them together.
06:53:34 <elliott> 05:03:53 <tswett_> But there are STLC functions which add or multiply Church numerals of the same type.
06:53:37 <elliott> 05:15:59 <tswett> Then I think we get a problem if we permit the dependently typed Church numerals. If c and d are dependently typed Church numerals, then \S -> c (S -> S) (d S) is their exponentiation.
06:53:41 <elliott> 05:16:48 <tswett> Simply typed Church numerals, good. Dependently typed Church numerals, bad.
06:53:44 <elliott> I'm just gonna paste everything said that answers the questions you're raising
06:54:32 <elliott> I propose a truce: both of us stop talking
06:54:41 <oren> so does the length of a functions have a legitimate answer?
06:55:29 <zzo38> I propose a different kind of truce which means, you can both ignore each other temporarily if you do not want to answer each other's questions.
06:55:34 <elliott> 04:40:19 <tswett> I suppose we might be able to define "grows at most polynomially" without actually defining what length is.
06:58:31 <oren> are the inputs allowed to be pointers?
07:00:17 <oren> e.g. so a data structure containing duplicates doesn't include the duplicates in its length
07:00:53 <oren> call them references. whatever
07:01:52 <oren> a type system allowing indirection is very different from one where everything is hieracrchical
07:02:55 <oren> e.g. consider the lisp lists cons(cons(a,a),cons(a,a)) vs. cons(a,a).
07:03:23 <oren> depending on encoding, the ratio of size is different between those two structures
07:06:31 <oren> python for instance uses immutable strings, so every string is basically stored only once.
07:07:01 <oren> while C++ copies everything every time
07:09:10 <oren> i guess elliott thinks this is irrelavnt because it is not math
07:11:16 <oren> nah i'll stop injecting any kind of reality.
07:12:10 <zzo38> A mathematical model of such thing could still be defined though, but such a model won't be useful if you do not define it at first.
07:13:05 <elliott> you'd think #esoteric would be the last place to get "um, but REAL COMPUTERS use BINARY NUMBERS" jokers re: a discussion of type theory, but no...
07:14:15 <oren> a language can be esoteric by being too real. consider subleq
07:14:47 <oren> or for that matter boolfuck
07:15:22 <oren> maybe real isn't the right word
07:15:50 -!- ZombieAlive has quit (Remote host closed the connection).
07:17:03 <oren> subleq has no abstractions is my point. you have to build any abstractions up from scratch
07:27:10 -!- Patashu has joined.
07:53:40 -!- AndoDaan has joined.
07:54:56 -!- cluid has joined.
08:00:23 -!- MoALTz has quit (Quit: Leaving).
08:05:45 -!- dts|pokeball has changed nick to pokeball|dts.
08:06:22 -!- pokeball|dts has changed nick to dts|pokeball.
08:47:35 -!- dts|pokeball has changed nick to dts|supersaiyan.
08:54:02 -!- adu has quit (Quit: adu).
08:54:56 -!- Lilin has quit (Quit: Connection closed for inactivity).
09:08:49 -!- Frooxius has joined.
09:21:51 -!- drdanmaku has quit (Quit: Connection closed for inactivity).
09:37:41 -!- AndoDaan has quit (Quit: bbl).
10:09:26 -!- oren has quit (Quit: leaving).
10:29:37 <elliott> we should, like, feature that language or something
10:30:00 <elliott> brainfuck has been featured for over a year because it's just that good
10:30:05 <elliott> unlike all the previous featured languages which only lasted months.
10:32:45 <int-e> elliott: we can make a poll, which was your first esoteric programming language? (Brainfuck here)
10:33:01 -!- oren has joined.
10:34:39 <fizzie> (Also I completely forgot about featuring something else for a chance.)
10:35:34 <oren> am i right in thinking that swapping two values in place is impossible in barinfuck?
10:37:53 <cluid> oren, yes you need a third cell
10:39:31 -!- ZombieAlive has joined.
10:42:56 -!- Vuk has joined.
10:43:36 <J_Arcane> A movement of Mahler's 1st symphony played by 12 networked ZX Spectrums (FF to around 7m for the music) https://www.youtube.com/watch?v=WiFEicJ6grM
10:43:40 <int-e> Though if you stretch the problem statement enough it may be possible: In Boolfuck, executing [>[<x]+<+x]>[+<+x]x will end up with two neighbouring cells swapped the first time any of the 'x' is reached.
10:46:04 <oren> the ZX spectrum had networking?
10:47:04 <fizzie> It had a rather custom "network" of sorts, too.
10:47:09 <oren> apparently there was somehting called "zx net" but wikipedia has no details
10:47:10 <fizzie> The http://en.wikipedia.org/wiki/ZX_Interface_1
10:47:12 <int-e> oh wow https://en.wikipedia.org/wiki/ZX_Interface_1
10:47:22 <fizzie> int-e: Fancy, isn't it?
10:48:40 <oren> like the old ethernet networks
10:49:58 <int-e> I see my "serial ports" guess wasn't far off the mark though :)
10:49:59 <fizzie> There's also a modern Ethernet interface for it, the "Spectranet": http://spectrum.alioth.net/doc/index.php/Main_Page
10:52:37 <cluid> it sounds really bad
10:52:46 <cluid> this attempt at "music" sucks
10:54:40 <oren> sounds like a kid with a brand new trumpet
10:55:27 <int-e> cluid: surely it can't be worse than the floppy disk drive music (eg https://www.youtube.com/watch?v=jEzXjJN1RH0 )
10:55:33 <oren> sounds better at 8:30 tho
10:56:44 <oren> holy crap how did he do taht?
10:57:05 <oren> are the floppy drives tuned?
10:57:10 <cluid> https://www.youtube.com/watch?v=bBpdvYkGtzs This guy makes the 1 bit speaker of the spectrum do great things
10:57:39 <fizzie> There's a lot of {floppy disk,printer,3D printer,...} music around.
10:58:30 <int-e> 3d printer ... of course there would be. step motors again...
10:59:36 <oren> because step motors can be run at any speed?
10:59:46 <int-e> within limits, yes.
11:00:23 -!- Vuk has quit (Ping timeout: 265 seconds).
11:00:42 <oren> do floppy drives have an interface providing such fine-grained control?
11:01:08 <oren> or is he bypasing the normal interface
11:04:36 <int-e> I don't know, but you can issue commands to the FDC to switch tracks, and you can do that at any frequency you desire as long as FDC + Floppy drive can keep up.
11:05:03 -!- J_Arcane_ has joined.
11:06:27 -!- J_Arcane has quit (Ping timeout: 240 seconds).
11:06:28 -!- J_Arcane_ has changed nick to J_Arcane.
11:07:43 <oren> these floppy drives have great bass
11:19:15 -!- boily has joined.
11:22:01 -!- oerjan has joined.
11:22:41 <lambdabot> Jafet asked 9h 4m 20s ago: It hasn't been proven that SAT cannot be linear time (unless you forbid linear space)
11:26:22 <fizzie> That seemed more like a statement than a question.
11:29:19 <oerjan> and also i remembered it when seeing it.
11:34:56 <shachaf> this is p. much Jafet: http://i.imgur.com/1NRLSoP.jpg
11:39:10 <oerjan> also it's not obvious from the picture that he's actually inside the library
11:41:40 <shachaf> http://www.reddit.com/r/firstworldanarchists/top/?sort=top&t=all is great
11:53:07 <int-e> Sticky web? (Sticky webs slow you down, with the potential of trapping you.)
11:56:44 <boily> I think the /topic may be a little bit misleading, and int-e is the eviler twin.
11:57:04 <shachaf> no claim was made regarding int-e's evilness
11:57:19 <shachaf> wouldn't you expect a correlation among twins, if anything?
11:57:48 <shachaf> int-e: that's from that game, isn't it
11:58:36 <oerjan> boily: the wisdom/ has clearly established that ørjan is the good twin. int-e is the redundant one.
11:59:01 <oerjan> he's so redundant we're not even triplets.
11:59:11 <HackEgo> Your evil overlord oerjan is a lazy expert in future computation. Also an antediluvian Norwegian who hates Roald Dahl. He can never remember the word "amortized" so he put it here for convenience.
11:59:15 <HackEgo> Ørjan is oerjan's good twin. He's banned in the IRC RFC for being an invalid character. Sometimes he publishes papers.
11:59:32 <oerjan> `learn int-e vet jag...
11:59:35 <HackEgo> Learned 'int-e': int-e vet jag...
12:01:16 <boily> is it a subtle horrible Norwegian pun?
12:01:35 <int-e> hint: I don't know anything about nordic languages. (this seems to be swedish?)
12:01:52 <int-e> (at least google found https://en.wiktionary.org/wiki/jag_vet_inte )
12:01:58 <HackEgo> shachaf sprø som selleri and cosplays Nepeta Leijon on weekends.
12:02:04 <shachaf> it seems that int-e is my twin
12:02:58 <oerjan> int-e: basically "i dunno" in swedish...
12:03:04 <int-e> /topic Baware of the evil triplets oerjan, shachaf and int-e | Beware of ricocheting jokes | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/
12:04:10 <shachaf> baware is a license for software released by sheep
12:04:20 <int-e> Though I have been made aware of that meaning of "inte" (on a non-IRC server that didn't like the dash)
12:05:41 <int-e> Did you know that "sheep" means "Schaf" in german?
12:06:55 <int-e> shachaf: Obviously I can't always avoid reading your nick that way.
12:07:27 <int-e> oerjan: Sorry, those Säue won't fly. The pronunciation is all wrong.
12:07:51 <fizzie> "ikk-e" would be a good nick.
12:08:45 <oerjan> int-e: i was going for slight misspelling, also that's norwegian not german
12:09:46 <shachaf> it's not germane either hth
12:10:20 -!- Patashu has quit (Ping timeout: 264 seconds).
12:10:44 <boily> y'où dont te sais.
12:11:12 <shachaf> boily: i am looking forward to poutine hth
12:11:17 <int-e> oerjan: Oh a false friend, funny it should be another kind of animal.
12:11:55 <shachaf> Beware of int-e's false friend oerjan
12:12:41 <int-e> oerjan: I hope you can appreciate the flying pigs reference anyway.
12:13:22 <oerjan> int-e: there's also the word "su" which means the same as the german but only farmers and crossworders know that one...
12:13:51 <shachaf> oerjan: also unix users hth
12:13:54 <oerjan> int-e: oh i missed that
12:14:09 <oerjan> shachaf: they don't know that word, only another one that is spelled the same way hth
12:14:28 <oren> am i the only one who uses su instead of sudo?
12:16:35 <int-e> (I can't explain why, except I'd rather have a root shell than a shell which might-or-might-not rememb that I just used my sudo password.)
12:19:47 <cluid> http://esoteric.codes/
12:20:17 <boily> shachaf: I'm waiting for your report.
12:20:36 -!- boily has quit (Quit: CONDENSED CHICKEN).
12:22:58 <oerjan> ...someone got a grant for writing an esolang blog?
12:26:44 <oerjan> (someone aka User:Rottytooth from the wiki)
12:26:59 <cluid> that guy is Rottytooth ?
12:28:51 <oerjan> i just looked up Light Pattern on the wiki
12:29:27 <oerjan> could also have looked up his real name, it's there on his user page
12:35:09 * oerjan prefers public chatting unless it's something actually secret.
12:35:28 <int-e> This is kind of neat. http://lightpattern.info/Basics/Machine/
12:37:59 <int-e> But I'm a bit disappointed by its use of shutter speed and aperture rather than actualy image features (beyond dominant channel in average color).
12:40:24 <int-e> Aww, really ... the corpse is actually dead and identified as Lady Selnikov?
12:40:36 -!- J_Arcane has quit (Ping timeout: 244 seconds).
12:41:12 <oren> yeah it should have 'dog' and
12:41:13 <int-e> Maybe it'll explode. There must be *some* twist!!!1
12:41:20 -!- J_Arcane has joined.
12:41:31 <oren> 'bike' as instructions
12:42:06 <int-e> RIGHT. https://xkcd.com/1425/
12:42:07 <oren> and it should perform image recognition to decide the outcome
12:43:05 <oren> hey it might be implable in 10 years, google have make progress
12:43:37 <oerjan> it's implable, but you need actual imps
12:44:58 <oren> lol yeah, to paint the pictures. don't run out of pink!
12:45:02 -!- shikhin has joined.
12:46:15 <int-e> oerjan: "implorable" has a shorter editing distance to "imblable" than "implementable", hth
12:47:06 <int-e> ("imps" needs no comment, I believe.)
12:47:21 <oren> well i thot it would be biguated by context
12:48:56 <int-e> I suck at context. As you can see I can't even distinguish between "oren" and "oerjan".
12:49:27 <cluid> how cant you? it's like apples and oerjans
12:51:05 -!- J_Arcane_ has joined.
12:52:29 -!- J_Arcane has quit (Ping timeout: 244 seconds).
12:52:31 -!- J_Arcane_ has changed nick to J_Arcane.
12:54:51 <int-e> oerjan: I *can* distinguish between oerjan and oerjan, but I tend to mix up the nicknames. :->
12:56:08 * oerjan looks sternly at int-e
12:56:55 -!- J_Arcane has quit (Ping timeout: 252 seconds).
13:01:30 -!- cluid has quit (Remote host closed the connection).
13:01:56 <oren> i'm the one from Canada hth
13:02:59 <oerjan> i've been in canada once hth
13:03:37 <oerjan> although mostly in waterloo
13:05:13 <fizzie> I've been over Canada, in a plane, if that counts.
13:05:36 <fizzie> Assuming the in-flight route map was telling the truth, anyway.
13:07:47 <oerjan> they all lie because in reality the earth is flat hth
13:08:24 -!- shikhout has joined.
13:09:55 <fizzie> I can't convince Google Maps to draw a line that wouldn't be curved with the "measure distance" option.
13:10:12 <fizzie> Since they're perpetuating the lie.
13:10:24 -!- oren has quit (Ping timeout: 265 seconds).
13:10:38 <int-e> time zones are the most elaborate part of the joke
13:10:50 <int-e> they actually had to invent time travel to make that work
13:11:07 <fizzie> Based on some eyeballing, depending on how it's flat, the direct line between Portland and Amsterdam might still cross Canada.
13:11:51 -!- shikhin has quit (Ping timeout: 265 seconds).
13:14:32 -!- oren has joined.
13:14:49 -!- tswett has joined.
13:16:52 -!- oren_ has joined.
13:17:48 -!- tswett has quit (Client Quit).
13:19:42 -!- J_Arcane has joined.
13:21:38 -!- J_Arcane_ has joined.
13:21:55 -!- J_Arcane_ has quit (Client Quit).
13:24:25 -!- J_Arcane has quit (Ping timeout: 252 seconds).
13:25:24 -!- augur_ has joined.
13:25:25 -!- augur has quit (Read error: Connection reset by peer).
13:37:25 -!- AndoDaan has joined.
13:43:17 -!- J_Arcane has joined.
13:48:34 -!- J_Arcane has quit (Ping timeout: 258 seconds).
13:51:08 -!- sebbu has quit (Ping timeout: 245 seconds).
13:59:26 -!- shikhout has changed nick to shikhin.
14:05:10 -!- Lilin has joined.
14:20:00 -!- AndoDaan has quit (Ping timeout: 258 seconds).
14:21:38 -!- sebbu has joined.
14:22:16 -!- sebbu has quit (Changing host).
14:22:16 -!- sebbu has joined.
14:25:39 <oerjan> @tell tswett I think a fundamental problem here is that there _is_ no measure on polynomial functions that fill allow the length of f(x) to be polynomial in the measure of f and the length of x. Because f includes the exponent which you need to apply to the length of x.
14:27:13 <oerjan> @tell tswett And |x|^|f| just isn't going to be polynomial in |x|.
14:30:21 <oerjan> @tell tswett Or at the very least, it seems impossible for f's with different exponent to have all the same type.
14:37:08 -!- MDream has changed nick to MDude.
14:43:30 -!- S1 has joined.
14:50:02 -!- atslash has quit (Quit: This computer has gone to sleep).
14:58:45 <HackEgo> [wiki] [[Truth-machine]] M http://esolangs.org/w/index.php?diff=41383&oldid=41366 * Oerjan * (+0) Ahem
14:58:48 -!- J_Arcane has joined.
15:02:28 -!- `^_^v has joined.
15:09:04 -!- dianne has quit (Ping timeout: 258 seconds).
15:35:26 <oren> wow the admins responded to my error report and got the patch in before breakfast! you never hear about the admins who do their jobs well...
15:35:30 <FireFly> Do bitwise operations have any interesting algebraic properties/identities in combination with usual operations? For instance, could I reason about (x + y) xor z algebraically anyhow?
15:35:45 <FireFly> (Seems on-topic enough for this channel)
15:36:15 <oren> umm... there is that weird sqrt trick i heard about
15:36:55 <FireFly> You mean http://h14s.p5r.org/2012/09/0x5f3759df.html ?
15:37:32 <oren> although there could be similar tricks involving integers
15:38:11 <FireFly> I was thinking more in terms of if I could solve equations involving bitwise operations by hand algebraically
15:38:20 <Jafet> Given that arx is a cryptographic primitive, probably not
15:38:47 -!- GeekDude has joined.
15:39:38 <oren> yeah the problem is that normal operations mix the bits while bitwise ones keep them separate
15:39:57 <oren> so reasoning is very hard
15:41:26 <Jafet> Well, if you omit rotations, you can propagate from the lowest bit
15:42:30 <FireFly> In this case I have a,b,r and want to find k such that (a - k) bxor (b - k) = r
15:43:11 <FireFly> I know that k is smallish, so it's easy enough to bruteforce, but.. it'd be neat if there's a way to reason about the solution
15:44:17 <oren> a + b = ((a & b)<<1) + (a ^ b)
15:44:43 <oren> there's one identity i know
15:45:32 <oren> unfortunately + appears on both sides
15:48:48 <oren> if you apply the above a number of times equal to the maximum bits in k, then it may reduce
15:51:14 -!- GeekDude has quit (Ping timeout: 258 seconds).
15:59:18 <oerjan> FireFly: well you can still propagate from the lowest bit
16:00:15 <oerjan> first, subtracting something common from the lowest bit doesn't change the xor, so you need a xor b = r (mod 2)
16:00:37 -!- mihow has joined.
16:01:33 <oerjan> *the lowest bit of the xor
16:02:15 <FireFly> That makes it "a bit" easier
16:02:52 <oerjan> and also the higher bits of k don't change whether the lower ones work
16:04:14 <oren> yeah, addition only propagates information up the bits
16:04:42 <oerjan> hm, in fact you need to choose the lowest bit of k such that it makes ((a-k0)>>1) xor ((b-k0)>>1) == (r>>1) (mod 2)
16:05:13 -!- skarn has joined.
16:05:44 <oerjan> it seems like at each step you can either reduce, keep or increase the number of possibilities alas
16:06:44 <oerjan> perhaps looking at the highest instead...
16:06:45 <oren> but we only need one k that works right? not every k?
16:07:28 <oerjan> sure but we cannot throw any away until we know they're not the only ones that work for the next bits...
16:09:08 <oerjan> the highest bit of k can never matter, i think
16:11:21 <oerjan> what matters is the carries/borrowings of the a-k and b-k subtractions
16:11:54 <oerjan> at each bit, it is determined whether those must be equal or different
16:12:18 <oren> which are equal to (a&(-k))<<1
16:13:22 <oren> they happen only when the bits of a and -k are both 1
16:13:54 <oren> oh right there are multiple carry rounds
16:15:34 <oerjan> i think it's easier to replace k with -k overall here...
16:15:51 <oerjan> addition is easier to think about than subtraction
16:16:18 <oren> well -k = ~k+1
16:16:25 <oerjan> that's not what i mean
16:16:43 <oren> oh you mean do that afterward
16:18:20 <oren> on the second bit, (a+b)>>1 = (a&b)+((a^b)>>1)
16:18:39 -!- SopaXorzTaker has quit (Changing host).
16:18:39 -!- SopaXorzTaker has joined.
16:18:42 <FireFly> Yeah, thinking in terms of additions is probably easier
16:19:01 <oerjan> FireFly: i have possibly changed my mind
16:19:44 <oren> when k is small, the high bits of -k are all 1
16:19:45 <oerjan> because to know whether a-k gives a borrowing, you need to know the ordering of a and k
16:20:18 <FireFly> There's no need to worry about borrows in my case
16:20:38 <oerjan> FireFly: with addition it's carries instead, of course
16:20:48 <oerjan> but that means you need the ordering of a and -k
16:20:54 <oren> does k have only one bit nonzero or something?
16:21:30 <oerjan> FireFly: the borrowings tell everything about which k work
16:21:44 <oerjan> that, and a xor b xor r
16:22:44 <oerjan> basically, if a bit of a xor b xor r is 0, you want the borrowings from that bit to be identical for a-k and b-k
16:22:52 -!- drdanmaku has joined.
16:23:08 <oerjan> while if it's 1, you want it to be different
16:23:48 <oren> so could you process it by shifting everything right
16:23:50 <oerjan> oh this is of course because if x is the borrowing bits for a-k, then a-k = x xor x xor k
16:25:04 <oerjan> so if y are the borrowing bits for b-k, then (a-k) xor (b-k) == x xor y xor a xor b
16:25:44 <oerjan> so you want to have x xor y == a xor b xor r
16:28:02 <oerjan> and say the 5th borrowing bit of a-k is determined by how a & 31 compares to k & 31, i think
16:29:22 <oerjan> so you want the order of a & 31, b & 31 and k & 31 to be one that gives the right bit
16:29:45 <oerjan> *the right xor of the borrowing bits
16:30:27 <oerjan> this gives you a set of ranges that the bits of k need to be within
16:30:47 <Jafet> More generally, since you can write addition as a big linear combination in GF(2) you can solve any problem involving addition and and and xor using linear algebra
16:31:03 <oren> that is integer programming isn;t it?
16:32:30 <oerjan> although it is possible that when you start intersecting those ranges, they split into several
16:34:01 <oerjan> also, it could be contradictory altogether, but i assume that's not your usecase since you say there will be a small solution
16:35:31 <FireFly> Well, I suppose rather that I want to know whether there's a "reasonably small" solution
16:35:42 <Jafet> Hmm, finding the numerically smallest solution could be a shortest vector problem
16:35:52 <Jafet> (the kth bit is weighted by 2^k)
16:36:27 -!- GeekDude has joined.
16:36:48 <oren> would it not be faster to iterate over the integers? (given that for "reasonably small" k we operate in O(1))
16:36:53 <oerjan> i am not sure whether Jafet is making sense or not, i'm dubious that this is really linear algebra.
16:37:07 <oerjan> oren: sadly, probably :P
16:37:11 <FireFly> oren: sure is. I mostly thought it was an interesting problem to ponder
16:37:16 <Jafet> It's linear algebra over GF(2)
16:37:22 <FireFly> In this case "reasonably small" means, say, <50 :P
16:37:43 <oren> oh i thought it meant less than 2^32
16:37:45 <oerjan> Jafet: i am not convinced addition of binary digits is a linear operation over GF(2).
16:38:12 <oerjan> you need multiplication to get the carries
16:38:40 <oerjan> xor you have, that's the addition in GF(2)
16:38:42 <Jafet> Oh, you end up with nested multiplications
16:39:13 <FireFly> The idea is that I have two messages encrypted with a stream cipher using the same key, and taking the xor of those messages reveals a 32-bit field that looks suspiciously like it'd hold the message length
16:39:17 <oerjan> but and you only have with constants, as long as you don't use the entire _ring_ GF(2)
16:39:34 <FireFly> (offset by some constant k)
16:39:36 <oerjan> (Which means you're beyond linear)
16:39:55 <oren> oh i see... back to linear algebra II.
16:42:57 <oerjan> FireFly: there would always be a chance of ambiguity here, because not all bits of k always matter
16:44:06 <oerjan> although i guess all information is good...
16:45:00 -!- FreeFull has quit (Quit: Dance).
16:46:06 -!- oerjan has quit (Quit: Dine).
16:47:11 <oren> the statement that A==B is the same as A^B == -1
16:47:54 <oren> yah. A==B => A^B == 0
17:04:24 <Jafet> Hmm, you can write addition as a polynomial in GF(2) but its size seems to be exponential
17:12:52 -!- skarn has quit (Remote host closed the connection).
17:20:47 <SopaXorzTaker> one operator for exchanging current memory cell and program at the current pointer
17:26:06 <fizzie> I don't remember its name, but something very much like that has surely been done.
17:26:28 -!- AndoDaan has joined.
17:27:00 <fizzie> There's so many brainfuck derivatives, it's hard to find any single one.
17:28:11 <fizzie> http://esolangs.org/wiki/Braintwist is not exactly that, but similar.
17:28:45 <fizzie> (The instruction it adds swaps the entire program and data tapes.)
17:30:10 <fizzie> If MediaWiki could take unions of categories, you could take the union of Category:Brainfuck_derivatives and Category:Self-modifying. I think I did that at least once manually.
17:35:45 <fizzie> (There are also at least four things that put the program in the data tape.)
17:35:49 <tromp_> you cant really change individual tokens of a program. as soon as you change one of [ ] you're left with nonsense
17:38:03 <fizzie> That doesn't really seem to be much of a problem, except slightly complicating the implementation (either rescan every time, or keep track of whether the region inside has been modified). You can just make it undefined to end up actually executing a [ or a ] that doesn't have a match.
17:43:59 -!- dts|supersaiyan has changed nick to dts|pokeball.
17:44:54 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)).
17:46:28 -!- skarn has joined.
17:46:44 -!- adu has joined.
17:50:56 <SopaXorzTaker> made a BF-like language with not--so-far nested loops and functions
18:06:09 -!- mihow has quit (Quit: mihow).
18:24:03 -!- S1 has quit (Quit: S1).
18:24:57 -!- Lilin has quit (Quit: Connection closed for inactivity).
18:42:47 <zzo38> I read that at some time they will make a computer program to solve FIDE chess, because "there aren't so many moves which are at all sound", but I expect you will need a mathematical proof of this in order to take advantage of it.
18:48:58 <b_jonas> zo38: http://www.inwap.com/pdp10/hbaker/hakmem/proposed.html#item95 expects about 10**40 positions
18:50:35 -!- mihow has joined.
18:51:21 <zzo38> It says "in most of them, one side is hopelessly lost", but that means you should determine how many of these it is as well as a mathematical proof that you really are hopelessly lost and doesn't just looks like it, as well as for a computer program intending to solve chess to identify such positions.
18:52:00 <zzo38> Still, it might be possible.
18:52:19 <b_jonas> zzo38: yes, it's just that 10**40 might not be that far off in the future
18:53:40 <b_jonas> zzo38: http://www.cube20.org/ is a computation with about 2**32 or 2**33 states, aggressively optimized, and before it appeared I expected it would take like ten or twenty more years of technology before it became possible
19:00:04 <zzo38> The source-codes says "They are written in a literate programming style using the CWeb system. You will need cweave to compile the programs." That isn't quite right; ctangle is needed to convert the .w into a .c to pass them to a C compiler, while cweave converts it into a .tex which can be typeset.
19:00:38 <b_jonas> zzo38: source codes where?
19:01:06 <zzo38> In http://www.cube20.org/src/
19:02:47 <zzo38> (Well, in this case they are C++ so you will need a C++ compiler; still ctangle is used to convert the .w into the .cpp file to pass to a C++ compiler then.)
19:03:38 <zzo38> However, the makefile will do the correct things, so that's OK.
19:07:09 -!- MoALTz has joined.
19:08:24 -!- shikhout has joined.
19:10:19 -!- MoALTz has quit (Read error: Connection reset by peer).
19:11:31 -!- shikhin has quit (Ping timeout: 244 seconds).
19:11:40 -!- adu has quit (Quit: adu).
19:12:25 -!- MoALTz has joined.
19:14:24 <zzo38> Someone ask a question about "At what point will humans alone be unable to devise a chess variant too complicated for computers to solve?" I expect never (until there is no human anymore, of course) because a game can be designed it isn't even possible to play this game by anyone in this universe even computer programs. That doesn't necessarily mean it cannot be solved, but suggests that it may be possible that some such games are too complicated t
19:16:41 -!- FreeFull has joined.
19:28:30 -!- atslash has joined.
19:40:49 -!- GeekDude has joined.
19:42:04 <int-e> zzo38: I think it's prudent to ask what the intended meaning of "solve" is.
19:42:48 <int-e> If solving a game means to play it better than humans then it's the standard AI question, with unclear answer.
19:43:30 <int-e> If solving means mathematically solving the game, then chess is a good candidate for a game that won't be solved.
19:44:05 <zzo38> To me, solving a game means mathematically solving the game. To play it better than humans isn't quite good enough.
19:44:34 <int-e> Yeah but it wasn't your question.
19:44:56 <zzo38> Yes, that is a good point though.
19:46:00 <zzo38> However, a lot of good AI for playing chess already exists. However, time odds can be used to allow grandmasters to play against a computer program at a reasonable level of play.
19:48:51 <int-e> Go has seen impressive advances in the last decade.
19:52:54 <int-e> (but it's still completely unclear how to beat professional go players; it's not going to be solved by increased computational resources.)
19:55:01 -!- shikhout has changed nick to shikhin.
20:06:13 -!- Patashu has joined.
20:08:23 -!- atslash has quit (Quit: This computer has gone to sleep).
20:26:52 -!- Patashu has quit (Ping timeout: 258 seconds).
20:55:56 -!- b_jonas has quit (Ping timeout: 260 seconds).
21:08:19 -!- b_jonas has joined.
21:19:13 <oren> it's easy to devise a game that can't be solved -- what is interesting is whether a game can be devised so that the best way of "solving" it is for the computer to simulate a human.
21:19:49 -!- cluid has joined.
21:20:27 -!- atslash has joined.
21:26:07 <cluid> i am bored, any ideas
21:27:00 <GeekDude> build a wiimote-controlled robot
21:27:11 <oren> i have been attempting to devise a language where all possible programs are polynomial time
21:27:55 <oren> based on C. essentially it will be a C header
21:28:57 <oren> one idea is that instead of allowing arbitrary loop conditions, you have only the repeat(n){} loop
21:31:15 <int-e> Sounds like LOOP programs, which give you primitive recursive functions.
21:31:48 <int-e> (The question here is, what is n?)
21:32:18 <oren> n is an integer, evaluated only once at the start of the loop
21:32:29 <int-e> If you can write things like m = 1; repeat(n) { m=2*m; }; repeat (m) { ... } you're way beyond polynomial time.
21:33:07 <oren> that's true. we need to nerf integers too i guess
21:34:39 <int-e> The usual approach for this that I know is to have different kinds of variables, those you may use as loop counts, and those that you can't use that way but can do computations with.
21:35:16 <oren> aha. the repeat statement needs to take a special type as input
21:35:38 <b_jonas> just limit the data space to 2**32 bytes, and ban all IO, then it can't run for more than 2**(2**32) time.
21:36:42 <oren> that is true but not useful because that is longer then the age of the computer.
21:37:02 <int-e> oren: https://www.cs.toronto.edu/~sacook/homepage/ptime.pdf is a restriction of primitive recursion but it's based on that principle; the recusion argument of a primitve recursive function acts as a loop count (that's how translations from primitive recursive functions to loop programs work)
21:37:41 <oren> ideally i would like to be able to pass a flag, which sets the maximum time complexity
21:37:58 <oren> and programs above it would not compile
21:39:36 <oren> hmm... you start with a loop count variable representing the data length...
21:39:40 <tromp_> go will not be solved, but at least it will be counted. i'm doing 18x18 right now
21:40:09 <tromp_> no hope of counting number of chess positions
21:44:11 -!- nycs has joined.
21:45:31 -!- `^_^v has quit (Ping timeout: 255 seconds).
21:50:40 -!- S1 has joined.
22:11:26 <int-e> tromp_: By "chess positions" do you mean those reachable from the starting position by a legal sequence of moves?
22:12:07 <int-e> (Go makes the reachability part easy...)
22:13:51 <tromp_> yes, i mean reachable positions
22:14:16 <tromp_> like, is White Kc3 Ba4 Black Kd1 Rb5 Bd5 reachable?
22:17:48 -!- AndoDaan has quit (Ping timeout: 245 seconds).
22:24:19 -!- oren_ has quit (Ping timeout: 265 seconds).
22:24:19 -!- oren has quit (Ping timeout: 265 seconds).
22:27:38 <int-e> Oh even better, since the answer is yes.
22:41:31 <tromp_> But with white ka3 the asnwer is no:)
22:46:57 -!- oerjan has joined.
22:50:06 <oerjan> <fizzie> If MediaWiki could take unions of categories, [...] <-- itym "intersection" hth
22:51:20 <int-e> tromp_: I wonder whether being a chess player helps or hurts in this problem
22:51:57 <int-e> (I'm not, but I do know enough of the rules)
22:56:50 -!- boily has joined.
23:01:16 <tromp_> you have to know some subtle rules
23:01:17 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)).
23:04:22 <cluid> https://github.com/nasser/---
23:04:31 <cluid> can I add this to the wiki? Maybe it is offensive to call it esoteric
23:04:53 <cluid> it feels like a cool language which should be on the wiki, but i am not if its appropriate
23:05:00 -!- Frooxius has quit (Quit: *bubbles away*).
23:05:26 <boily> cluid: is it a brainfuck clone?
23:06:17 <cluid> oh it is implemented in javascript rather than itself :/
23:06:19 <oerjan> i think it's at least honorary esoteric
23:06:41 <boily> the language it's implemented in usually doesn't matter.
23:07:00 <boily> (to wit, reference implementations of mine are in ruby or python...)
23:07:13 <cluid> http://nas.sr/%D9%82%D9%84%D8%A8/
23:07:55 <cluid> http://animalnewyork.com/2014/artists-notebook-ramsey-nasser/
23:08:14 <cluid> > The current name قلب means Heart, but is actually a recursive acronym for قلب: لغة برمجة pronounced ‘alb: lughat barmajeh meaning Heart: A Programming Language. Acronyms in Arabic are generally difficult to pull off, and قلب is the first recursive one I have seen
23:08:16 <lambdabot> <hint>:1:33: parse error on input ‘,’
23:08:51 <boily> ...LISP ekil skool siht
23:09:15 -!- CrazyM4n has joined.
23:12:15 -!- MoALTz_ has joined.
23:14:07 -!- skarn has quit (Killed (sinisalo.freenode.net (Nickname regained by services))).
23:15:15 -!- MoALTz has quit (Ping timeout: 245 seconds).
23:17:41 -!- nycs has quit (Quit: This computer has gone to sleep).
23:22:45 -!- adu has joined.
23:24:36 -!- oren has joined.
23:24:54 <HackEgo> [wiki] [[قلب]] N http://esolangs.org/w/index.php?oldid=41384 * Cluid Zhasulelm * (+968) created page
23:24:57 <HackEgo> [wiki] [[Eve]] http://esolangs.org/w/index.php?diff=41385&oldid=41374 * Oerjan * (-90) some proofreading
23:25:46 <CrazyM4n> https://gist.github.com/CrazyM4n/d02380667be743be1310
23:25:59 <CrazyM4n> And backspace occasionally doesn't work
23:27:33 <CrazyM4n> I also somehow got simplefunge to compile
23:27:40 <CrazyM4n> So everything is working out for me today
23:28:43 <cluid> Thhere is also http://nas.sr/godjs/
23:29:12 <cluid> im not sure if it counts
23:31:18 <CrazyM4n> I'm going to go reimplement simplefunge in python
23:34:29 -!- augur_ has quit (Remote host closed the connection).
23:35:05 -!- augur has joined.
23:39:41 -!- augur has quit (Ping timeout: 258 seconds).
23:41:42 -!- GeekDude has joined.
23:43:59 -!- skarn has joined.
23:44:56 -!- cluid has quit (Quit: Leaving).
23:53:26 <CrazyM4n> have I shown you the latest thing I've been working on?
23:53:32 <CrazyM4n> http://i.imgur.com/0V13wX1.png it's a funge editor
23:56:47 -!- qwertyo has joined.
23:57:37 <boily> fungot: do you like being edited?
23:57:37 <fungot> boily: he's absolutely hilarious though. the php compiler, from the bible the fact that its totally non-idiomatic examples from me? ;p
23:57:50 <boily> a biblical php compiler? AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAH!
23:59:07 <oerjan> because http://xkcd.com/224/ was not dark enough