00:01:39 <bsmntbombdood> SimonRC: no, it kills connections longer than like 5 seconds
00:25:58 <ihope> Google kills connections longer than 5 seconds?
00:26:02 -!- Tritonio_ has quit ("Bye...").
00:26:40 -!- GregorR-L has quit ("Leaving").
03:04:10 <SimonRC> hehehe http://i-am-bored.com/bored_link.cfm?link_id=24130
03:17:38 <oklopol> i'm pretty sure i was doing something just now
03:37:03 <ihope> I should make a two-dimensional esoteric language.
03:37:20 <ihope> Declarative, since everyone knows declarative languages are The Way Forward.
03:37:29 <pikhq> Make an n-dimensional one that's not brainfuck-based.
03:37:50 <pikhq> I even grant you the usage of the "0.0.0" portion of Dimensifuck syntax, since that's not Brainfuck-based at all. ;)
03:37:51 <ihope> Or brainfuck-based?
03:38:09 <pikhq> Not brainfuck-based. . . Befunge-based *could* be interesting.
03:38:26 <pikhq> Mainly, the idea is to have it not be Dimensifuck. ;)
03:38:28 <ihope> (Actually, they're The Natural Way, since most natural languages I've seen are declarative.)
03:38:33 <ihope> bsmntbombdood: they are?
03:38:47 <pikhq> bsmntbombdood: Do you approve of n-dimensional ones?
03:38:48 <ihope> Malbolge, on the other hand...
03:39:16 <pikhq> n is any integer greater than 0.
03:39:30 <ihope> One language for all such integers?
03:39:43 <pikhq> http://esolangs.org/wiki/Dimensifuck Like this.
03:40:53 <ihope> bsmntbombdood: "this is true, that is true" rather than "do this, do that".
03:41:31 <ihope> Prolog. Haskell. Epigram.
03:41:55 <ihope> bsmntbombdood: can be done in... maybe at least one language.
03:42:00 <ihope> Yes, it essentially is.
03:42:11 <ihope> I guess it's not really declarative so much as just functional.
03:42:14 <oklopol> declarative is kinda like funxxxional
03:42:31 <oklopol> except it's even more snuggy
03:42:49 <ihope> Greatly because... um, hmm, maybe they're actually not relateD?
03:43:01 <ihope> You can have an imperative functional language quite easily.
03:43:11 <ihope> I believe Python and JavaScript are both... that.
03:43:48 <ihope> Declarative non-functional languages are possible as well.
03:44:00 <ihope> bsmntbombdood: what's the status on removing lambda?
03:44:05 <ihope> I see it's still here for now, at least.
03:44:40 <ihope> ~exec sys.stdout(sys.stdout)
03:44:40 <bsmnt_bot> <__main__.IRCFileWrapper instance at 0xb7c5fb0c>
03:44:44 <ihope> No you haven't. :-P
03:44:47 <oklopol> i'm never gonna touch it again if lambda dies
03:45:47 <ihope> You can grab an older version of Python and present it to... um, the functional people.
03:45:54 <oklopol> if i was, then it's because i own.
03:46:04 <ihope> The Old Python people.
03:46:21 <oklopol> ihope: great idea about a 2d declarative lang
03:46:41 <oklopol> they're always so completely imperative, all these one-char=one-command langs
03:46:56 <ihope> Inspired by... um, that language that I think isn't Ithkuil.
03:47:12 <oklopol> are you saying this grea idea was not yours?
03:47:46 <oklopol> if i went to sleep now, i could... sleep
03:48:00 <ihope> Well, I think Ilaksh is a constructed language written in two dimensions.
03:48:06 <ihope> That's as far as the inspiration goes.
03:48:06 <bsmntbombdood> * bsmnt_bot (n=bsmnt@abacus.kwzs.be) has joined #esoteric
03:48:08 <oklopol> one the other hand, i could just stay here and stare stupid at the screen
03:48:15 <bsmntbombdood> that's the first time bsmnt_bot appears in my logs
03:48:43 <ihope> Not a programming language, but still made up.
03:48:53 <oerjan> bsmntbombdood: that did not have any time on it
03:48:58 <ihope> I have yet to see a natural programming language. :-P
03:49:21 <ihope> Maybe they exist; I dunno.
03:49:24 <oklopol> oerjan: it was manually givezored
03:49:30 <oklopol> <bsmntbombdood> Dec 19 21:15:29
03:49:43 <oklopol> ihope: what do you mean by that?
03:49:56 <ihope> "Hey, if I do this, the computer behaves in certain ways!"
03:50:02 <oklopol> bsmntbombdood: what year was that?
03:50:06 <ihope> User figures out a programming language based on the computer's responses.
03:50:21 <oerjan> ihope: when toddlers start learning to program, perhaps?
03:50:32 <ihope> Nah, it was this year.
03:51:01 <ihope> You... just sort of figured out qbasic?
03:51:08 <oklopol> i used to code on bare metal with a laser pointer
03:52:04 <ihope> I did all my programming on a pool table.
03:52:14 <ihope> I invented this thing called a Feynman gate.
03:52:27 <ihope> And "Feynman" just happens to be the name of some... intellectual.
03:52:36 <pikhq> I started when I was 8 on Apple BASIC. . .
03:53:14 <ihope> Put a ball in 1, get a ball out A. Put a ball in 2, get a ball out B if there was a ball in 1 or C if there wasn't.
03:54:22 <oklopol> ihope: did you invent that?
03:54:25 <ihope> If you have an infinite pool table with an infinite number of obstacles, it's Turing-complete.
03:54:31 <ihope> Nope. Found it all online.
03:55:04 <oklopol> i'm a bit too tired to understand that many words
03:57:34 <oklopol> ihope: how does that scale into a bigger table?
04:00:02 <ihope> How does what scale?
04:00:11 <ihope> Bigger table, bigger computer.
04:00:22 <oklopol> i mean, that's for three holes
04:00:35 <oklopol> when there's a forth, what do you do with it
04:00:44 <ihope> Well, there aren't necessarily any holes at all.
04:01:00 <ihope> You have your balls and you have some sort of obstacles.
04:01:11 <ihope> You can have holes if you want, I guess.
04:01:47 <ihope> But given that this is all about building tiny, energy-efficient computers, don't expect them to work :-P
04:01:50 <pikhq> I wish I had a turtle; I'd teach it LOGO.
04:02:07 <oklopol> trying to catch each other
04:02:23 <oklopol> so they do the decreasing rectangle
04:02:48 <oklopol> yes, but what a rectangle.
04:07:47 <oklopol> i made a 3d flight simulator once with logo
04:08:07 <oklopol> though it wasn't really a 3d flight simulator.
04:08:15 <oklopol> but you flew around and tried to hit the other guy
04:08:54 <oklopol> i also made a 2d flight simulator with eye view
04:09:51 <oklopol> that was... visual basic iirc :P
04:10:09 <oklopol> 4 hour project... i was pretty good at vb
04:10:16 <oklopol> but then i found out it sucked ass :<
04:15:17 <oklopol> you gotta love the graphics.
04:16:33 <oklopol> god i've done a lot of crappy games
04:16:44 <oklopol> i must've had an empty childhood.
04:25:45 <oklopol> hehe, this one is pretty nice www.vjn.fi/gz/sdlluolis.exe :P
04:27:00 -!- ihope has quit (Read error: 110 (Connection timed out)).
04:28:59 <oklopol> how'd you like a game where you move around a 2d screen with one button?
04:29:58 <oklopol> www.vjn.fi/gz/onokki.exe eve though i'm pretty sure no one is gonna open these :P
04:35:24 <oklopol> (btw in case you try onokki, i can move to anywhere on the screen in ~ 6 seconds)
04:46:38 <oerjan> "The program cannot start because SDL.dll does not exist"
04:47:12 <oklopol> this is why no one is going to run them
04:49:58 <oklopol> that was the link to the dll, by the way, don't know if you just thought it was another gamme
04:50:22 <oerjan> i guessed dep meant "dependencies"
04:50:45 <oklopol> i named it but i never remember it :P
04:51:46 <oklopol> i wish i still got great ideas like making a game that's controlled with one button
05:00:29 <oerjan> mind telling me what that button is?
05:00:31 -!- boily has joined.
05:00:55 -!- pikhq_ has joined.
05:00:58 <oklopol> 'enter' for green, '1' for red
05:01:10 <oerjan> (also, your program is evil, i need ctrl-alt-del to quit...)
05:01:37 <oklopol> when i run it, a console is also opened
05:01:44 <oklopol> shutting that down kills the program
05:01:54 <oklopol> bsmntbombdood: you are lol
05:02:40 -!- pikhq has quit (Nick collision from services.).
05:02:42 -!- pikhq_ has changed nick to pikhq.
05:02:46 <oklopol> oerjan: did you figure how to move around? :)
05:03:50 <oklopol> even though the idea is very trivial
05:04:29 <oklopol> the first thing i could think of
05:07:56 <oklopol> even though there is just one button, there are actually two kinds of manouvering
05:08:56 <oerjan> well i did manage to get stuck in a corner for a while, still haven't broken the code
05:09:39 <oklopol> just think what happens when the button is donw and what happens when it's not
05:10:04 <oklopol> just pressing the button won't help in cracking teh code
05:10:30 <oklopol> heh, i became invincible, muahahaa
05:12:46 <oklopol> i remember we used to play that game with 7 players xD
05:13:14 <oklopol> the beauty of having just one button per player is that 7 players can use the same kayboard
05:13:24 <oklopol> though it gets a bit cramped
05:17:17 <oklopol> tell me if you want clues :D
05:17:37 <bsmntbombdood> is casting a void* -> function pointer legal in C?
05:18:42 <bsmntbombdood> and me and someone are arguing over whether it's legal or not
05:19:03 <oklopol> i can't say i actually *know*
05:19:13 <oklopol> i've assumed wrong about c before :)
05:20:08 <oklopol> of course you can do that, any pointer is just a normal number
05:20:38 <oklopol> why would a function pointer be a special pointer :\
05:21:19 <oklopol> if it's not legal, i'll kill 'em
05:22:58 * oklopol refuses to do what he's supposed to
05:56:16 -!- boily has quit ("WeeChat 0.2.5").
06:04:52 -!- boily has joined.
06:13:19 -!- oerjan has quit ("Good night").
06:29:52 -!- boily has quit (Remote closed the connection).
07:02:54 -!- Izak has joined.
07:03:13 <pikhq> Welcome to insanity.
07:03:43 <pikhq> bsmntbombdood: Casting void* -> any pointer is, by definition, legal. ;)
07:51:43 -!- edwardk has joined.
07:51:52 -!- Izak has quit (Read error: 110 (Connection timed out)).
07:53:28 <edwardk> are the esoteric languages in question here esoteric as in hard to use/pointless brainf*ck kind of things or esoteric as in non-mainstream, unusual and interesting?
07:55:23 <edwardk> been working on a toy interpreter/compiler for a lazy programming language with first class subset/quotient types and looking for a place to talk to people about it, that fit the general gamut of this place?
07:56:24 <edwardk> i can stop drowning out the rest of the chatter on ##logic then ;)
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:00:23 <edwardk> basically what i have right now is an interpreter written in haskell for this thing, and a compiler i've been slowly working on bootstrapping in it. the language is sort of a kitchen-sink repository of anything cool-but-undecidable-in-general in type theory circles.
08:01:10 <pikhq> Just with the word "haskell", you've gotten Oerjan's approval (although he's not here ATM)
08:01:21 <edwardk> hopefully in a couple months i should have something stable enough to start being useful
08:01:40 <pikhq> Just one question: is it sufficiently odd/quirky to count as an esoteric language?
08:01:55 <edwardk> i don't know, pikhq thats kind of what i was hoping to find out ;)
08:02:03 <pikhq> May very well be. . .
08:02:29 <pikhq> Non-mainstream, unusual, and interesting, I believe you have covered.
08:02:39 <pikhq> So, even if not techincally esoteric, you fit in perfectly.
08:02:58 <edwardk> bsmntbombdood: : the idea is that you can define a subset type of an existing type by stating a predicate using the syntax of the base language for the predicate. so example Nat = { x : Int | x >= 0 } would be a subset type taken from the Ints
08:03:13 <pikhq> (although I'm thinking about making Brainfuck knowledge mandatory for the channel. :p)
08:03:29 <edwardk> or if i have sorted : Ord a => [a] -> Bool as a predicate written in the base language
08:03:46 <edwardk> sort : Ord a => [a] => { result : [a] | sorted result }
08:04:07 <edwardk> using a subset type on the result to specify that the result will satisfy the in-language predicate above
08:04:13 <pikhq> edwardk: Hmm. I like, so far. . . Not sure I'll be able to wrap my head around all of it, though. :p
08:04:16 <edwardk> appealing to abstract interpretation to check it at compile time
08:05:02 <edwardk> f : { x : T1 | pre x } -> { y : T2 | post x y } defines a compile-time-checked contract of the pre and post conditions on f
08:05:10 <edwardk> they can't be proven in general, but surprisingly many can
08:05:38 <edwardk> so if i can prove it you hear nothing from the compiler, if i can concretely disprove it with a counter example you get an error and the counter example, shrunk haskell quickcheck style
08:05:58 <edwardk> if i can't prove it you get a warning and an option to insert a runtime check for the condition, since the predicate is written in the base language
08:06:15 * pikhq goes to the comfort of a Brainfuck interpreter. Could someone that's actually taken computer science make edwardk feel welcome, instead? :p
08:06:44 <edwardk> you know its bad when your language makes someone seek comfort in Brainfuck
08:07:22 <pikhq> Not really. I actually enjoy coding in BF.
08:07:50 <edwardk> anyways thats one undecidable-but-cool feature, and its probably the most useful one that I have been working towards
08:08:21 <pikhq> Hmm. . . I *think* you've managed to describe something superTuring.
08:08:45 <edwardk> yeah, like i said, type checking the above tries to prove it, if it can, and if it can't, it falls back on inserting a runtime check
08:08:58 <edwardk> so a lot of things like array bounds checking can be caught that way at compile time
08:09:24 <edwardk> quotient types are a little harder to motivate and unfortunately lack the runtime fall-back.
08:11:10 <edwardk> subset types let you define an arbitrary subtype for any type in the language by using predicates defined in the language. quotient types let you go the other way and let you define arbitrary supertypes for types in the language by redefining equality on them and incurring a proof burden every time you use them in argument-position to a function that is defined over the base type.
08:11:30 <edwardk> so, hrmm, Parity = Int \\ (\x y -> x mod 2 == y mod 2)
08:11:35 <edwardk> would be a quotient over the integers
08:11:48 <edwardk> where we say that two values are equal if they have the same remainder mod 2.
08:12:00 <edwardk> then even = 0 :: Parity; odd = 1 :: Parity
08:12:35 <edwardk> and if you ask of 4 == even, it'll say yes because 4 :: Parity == 0 :: Parity since 4 mod 2 == 0 mod 2
08:13:28 * pikhq is too much of a fan of a lack of syntax. . .
08:13:42 <edwardk> pikhq: that would explain the love of BF =)
08:13:50 <pikhq> edwardk: And of Tcl.
08:14:04 <pikhq> And my worshipfulness of Lisp, in spite of not knowing it.
08:14:09 <edwardk> i would have thought we would have lost you to scheme or lisp by now
08:15:54 <edwardk> anyways syntax-like its kind of like haskell, with the addition that you use the same function syntax at the type and term levels -- giving it somewhat less syntax to learn there, but blowing the syntax budget on polymorphic records, etc.
08:16:07 <pikhq> What, do you have anything against people using: puts "2 + 2 == [+ 2 [* 5 6]]"
08:16:26 <pikhq> What the hell did I write?
08:16:41 <pikhq> (it's 2:00. Forgive me.)
08:25:49 <edwardk> anyways it probably doesn't qualify as esoteric, simply because its designed to be useful ;)
08:30:20 <pikhq> Currently, I'm in CST. Will be back in Mountain soon.
08:30:57 <pikhq> edwardk: It's an interesting concept for a programming language. I'd say it fits with the populace here if not the topic. ;)
08:31:39 <pikhq> BTW, some of the oddest esoteric languages have been designed with some sort of usefulness in mind. . .
08:32:00 <edwardk> basically my goal right now is to get the compiler bootstrapped and generate some decent code from it
08:32:15 <edwardk> and to finish mucking around with the syntax so much =)
08:32:49 <pikhq> (I believe one was designed to disprove the strong claim of the wire crossing problem
08:34:37 <pikhq> Scratch that: multiple esolangs have been designed with that in mind.
08:35:18 <pikhq> Another esolang was designed with the idea of making it trivial to design cellular automatons.
08:38:12 <edwardk> yeah i've actually checked in on them over the years here and there
09:19:06 -!- sebbu has joined.
11:00:23 -!- jix has joined.
12:08:49 -!- RedDak has joined.
13:03:55 -!- RedDak has quit (Remote closed the connection).
13:06:59 -!- jix has quit ("This computer has gone to sleep").
13:08:28 -!- jix has joined.
13:08:32 -!- jix has quit (Remote closed the connection).
13:24:52 * SimonRC tries to figure out wtf Luolis does
13:33:30 * SimonRC can't figure out onokki either
13:42:57 -!- RedDak has joined.
14:43:35 -!- ihope_ has joined.
15:23:48 -!- RedDak has quit (Remote closed the connection).
15:56:01 -!- RobAtWork has quit (Read error: 110 (Connection timed out)).
16:12:29 -!- edwardk has quit (Read error: 110 (Connection timed out)).
16:29:44 -!- pikhq has quit (Read error: 110 (Connection timed out)).
16:39:25 -!- sebbu2 has joined.
16:51:56 -!- sebbu has quit (Nick collision from services.).
16:52:01 -!- sebbu2 has changed nick to sebbu.
18:07:18 -!- pikhq has joined.
18:25:29 -!- ihope_ has changed nick to ihope.
18:34:23 -!- jix has joined.
18:46:35 <ihope> So, a two-dimensional declarative language...
18:56:53 <ihope> ...lemme conjure up something from topology.
19:09:13 <ihope> Okay. Statements are subsets of RxR, which is the plane.
19:09:26 <SimonRC> it should be Тетрис-based!
19:09:46 <ihope> If there's a continuous bijection between RxR and RxR that maps S onto T, then S and T are equivalent.
19:10:18 <ihope> (A scary thing until you finish digesting it. After you do, it seems... easy.)
19:11:02 <ihope> Let's call the existence of such a bijection "morphability".
19:11:17 <ihope> There's probably a term for it already, but mine works.
19:12:51 <ihope> And... egad, there's so much stuff that's so easy to grasp intuitively yet so hard to express formally...
19:15:23 <ihope> The idea I'm wanting to capture is that of what could easily be written by a pen such that a little bit of sloppiness doesn't matter.
19:16:02 <ihope> Something like the letter O would be invalid because the starting and ending points would have to match perfectly.
19:16:36 <ihope> Same for the letter T: the one end of the vertical line has to go exactly as far as the horizontal line.
19:17:00 -!- edward1 has joined.
19:47:30 -!- edward1 has changed nick to edwardk.
19:50:09 <ihope> Well, we'll say that a statement has to be a union of finite curves with endpoints such that the only "special points" are where a curve goes through a curve.
19:50:36 <ihope> Er, endpoints where a curve goes through a curve
19:50:44 <ihope> Er, endpoints *and* where a curve goes through a curve
19:52:12 <ihope> "Special point" meaning singular point, I guess.
19:53:11 <ihope> A statement has to be a union of finite curves with endpoints such that all singular points are stable!
20:18:21 <lament> it's hard to figure out what a "line" is when dealing with lines drawn on paper.
20:28:12 -!- chuck has joined.
20:28:36 -!- chuck has left (?).
20:41:31 -!- RedDak has joined.
21:09:50 <ihope> I think I've captured it decently well.
21:13:59 <ihope> Hey, I could turn this into a grid notation thing...
21:14:52 <ihope> + is an intersection, | is a straight line, - is a straight line... I guess some creativity is needed for corners.
21:15:17 <SimonRC> since no two lines may end at a point
21:15:36 <ihope> They don't end at points; they end at edges.
21:15:50 <ihope> + alone is two lines crossing.
21:16:33 <ihope> If you add a - to the side and | below, it might still be two lines crossing.
21:16:49 <ihope> You could use the same character for all crossings, though. How about %?
21:17:23 <ihope> Er, all corners, I mean.
21:38:15 <edwardk> For a second there I thought the curves involved were real curves, like NURBS or something. hrmm there is an esoteric language for you
21:39:16 <ihope> Well, if you find a good way to specify those things, they'll work as well.
21:39:36 <ihope> A little crazy, eh?
21:39:44 <edwardk> well, i was a computational geometer for a while, i'm pretty comfortable with NURBS ;)
21:41:01 <edwardk> now, try to explain to the end user what a sequence of knots and weights is supposed to do
21:42:00 <edwardk> non-uniform rational b-spline curves
21:42:30 <edwardk> its not a language, just a way to specify curves in a projectionally invariant manner
21:47:23 <ihope> Projectionally invariant?
21:47:34 <ihope> (No, spellcheck, I didn't mean "protection ally".)
21:47:35 <oklopol> innumerable brainfuck: a function and a range a...b is specified, then for every result of that function in that range is given it's own thread (infinite threads that is), so that every thread has a real number representing an infinite number of brainfuck instructions to execute (base 8 presentation); should a thread be given a faulty bf program it dies; the memory is shared, and it's continuous, > will move one derivative and has to be executed infinit
21:48:06 <oklopol> actually, if you lose that continuous memory, that can be written an interpreter
21:48:47 <oklopol> it has to give faulty bf programs except for certain values
21:49:05 <ihope> After faulty BF programs are disposed of... well, the result is still dense.
21:49:12 <edwardk> ihope: if you use a perspective projection on a bezier curve then subdivide it you get a different curve than if you subdivide it and then project it. NURBS provide the non-uniform subdivision necessary to be able to project something into 'viewspace' and get the same curve cutting it up there as before. it means its more useful for computer graphics applications
21:49:17 <oklopol> nope, if you give it a function where it's not
21:49:43 <oklopol> of course, running innumerable threads would be impossible even if we were given an infinite space to use for the computer :)
21:50:56 * edwardk takes off his geometer hat and goes back to being a code monkey ;)
21:51:26 <oklopol> edwardk: write me an innumerable bf interpreter!
21:51:44 <edwardk> oklopol: heh, busy with my own language compiler at the moment ;)
21:51:52 <ihope> putStr (repeat 'a') >> putStr (repeat 'b')
21:51:58 <oklopol> innumerable brainfuck is super^2turing :DDDDD
21:52:07 <ihope> Outputs infinitely many a followed by infinitely many b.
21:52:10 <ihope> oklopol: it's what?
21:52:18 <oklopol> it can predict the result of a superturing function.
21:52:45 <ihope> Predict the result meaning solve the halting problem?
21:52:49 <oklopol> i mean, you can write a program in it that can predict any superturing program's result.
21:53:18 <oklopol> a superturing program cannot be written that can analyze another one
21:53:25 <ihope> It can (solve the halting problem)^2 of a super-Turing program?
21:53:34 <edwardk> 'super-turing' is a turing machine with a halting oracle right?
21:53:47 <oklopol> but mine has a superoracle :)
21:54:00 <ihope> What do you call one that can just solve the halting problem of a super-Turing program?
21:54:25 <oklopol> super²turing was what i used
21:54:34 <oklopol> i'm pretty sure there's no official word
21:54:46 <edwardk> so 'super-turing' is the local lingo for Pi^2_0?
21:55:08 <ihope> There's a... where's that notation described?
21:55:09 <oklopol> edwardk: you're pretty smart, what've you been reading?
21:55:27 <ihope> (So a super^2-Turing program can solve the halting problem for super-Turing programs where a super-Turing program can solve the halting problem for a Turing program?)
21:55:28 <oklopol> but, indeed prettu obvious there was a notation for that
21:55:34 <edwardk> oklopol: been collecting masters degrees. =)
21:55:49 <oklopol> my future as well, hopefully
21:56:08 <ihope> Collecting... what?
21:56:34 <edwardk> ihope: let me find you a reference
21:56:47 <ihope> What if we say that a rank-0 machine is a Turing machine, and a rank-n machine is one that can solve the halting problem for rank_m machines for all m < n?
21:57:10 <oklopol> ihope: Pi^2_0 was what edwardk used
21:57:17 <edwardk> iirc grigori rosu used it when describing the complexity of proving the equivalence of two infinite streams last year at the ICFP but its an older notation
21:57:53 <ihope> Gets problematic when you get to an ordinal number n that can't be described by a rank-(n+1) machine.
21:58:11 <ihope> You know about ordinal numbers?
21:58:42 <ihope> I sort of accidentally invented them once, but they're well-known :-P
21:58:45 <edwardk> http://fsl.cs.uiuc.edu/index.php/Equality_of_Streams_is_a_Pi_2%5E0-Complete_Problem
21:59:28 <oklopol> ihope: what are they? 4th?
22:00:09 <oklopol> ah, there's some weird math thing about them i don't know
22:00:34 <ihope> ...here are two properties of ordinal numbers: for every set of ordinal numbers, there's a lowest ordinal number bigger than all those in the set; and for every ordinal number, there's a set containing exactly those ordinal numbers below that ordinal number.
22:02:20 <oklopol> cardinals don't have that?
22:02:54 <oklopol> to me, that's a tautology, but you've prolly read a lot more about infinities than me
22:04:24 <ihope> Cardinal numbers also have those properties.
22:05:05 <edwardk> http://www.mtnmath.com/whatrh/node51.html introduces Pi_2 mentioned above, and goes on to ordinals from there
22:05:08 <SimonRC> Cardinal nubers may become Pope
22:05:18 <ihope> Well, cardinal numbers actually have some meaning attached to them.
22:05:33 <ihope> I guess ordinal numbers do, too, but it's a different meaning.
22:06:32 <ihope> If a set is order isomorphic to a set of ordinal numbers containing exactly those ordinal numbers below n, then n is said to be the order type of that set.
22:07:22 <edwardk> http://ecommons.library.cornell.edu/bitstream/1813/6877/1/89-961.pdf also talks about it
22:15:05 <oklopol> ihope: how do you know this stuff, btw?
22:19:38 <edwardk> well the courses encountered in the course of earning it anyways
22:20:16 <lament> if you're talking about ordinals, [[Banana Scheme]] on the esoteric wiki.
22:20:18 <ihope> oklopol: Wikipedia, #math, brain, teacher for a class I'm not in yet.
22:20:41 <lament> Banana Scheme is all about proving the halting problem.
22:21:07 <edwardk> lament: its easy to prove there is a problem ;)
22:21:09 <ihope> And Google, #haskell.
22:21:40 <edwardk> My toy project has been all about 'nibbling at the edges' of undecidability there.
22:21:52 <edwardk> deciding it where it can figure it out and not sweating the ones it can't
22:34:39 -!- oerjan has joined.
22:36:10 <oerjan> ooh, it's 070707 today
22:36:27 <edwardk> wandered in here last night trying to find a place where talking about a language-in-progress wouldn't put everyone to sleep ;)
22:40:37 <oerjan> i thought i recognized you from #haskell
22:41:10 <edwardk> the reaction from last night went: (3:00:47 AM) pikhq: Just with the word "haskell", you've gotten Oerjan's approval (although he's not here ATM)
22:44:26 <edwardk> right now wrestling with my concrete syntax for named function arguments =/
22:45:23 <edwardk> what i have is basically a haskell-like syntax, from the standpoint of minimal keywords and you just say foo x y = .. to define a function, and give it a haskell like type signature
22:45:40 <edwardk> except for the fact that type level functions use the same syntax as term level ones
22:46:32 <edwardk> and that i have subset and quotient types for contract checking and polymorphic records and variants, to give you a reasonable OOP and extensible version of 'data' declarations, ala ocaml
22:46:56 <edwardk> oh, and in general everything is undecidable, i accept this.
22:47:11 <edwardk> kind of the cost of doing business with some of these features =)
22:48:09 <edwardk> but i noted that i can leverage the same syntax i use for field dereferencing for named arguments
22:48:39 <edwardk> map : Ord a => (.with : a -> b) -> (.over : [a]) -> [b]
22:48:54 <oerjan> is this an explicitly, dependently typed language?
22:48:59 <edwardk> then map.over [1,2,3] binds the second argument
22:49:07 <edwardk> i have a limited notion of dependent types at present
22:49:18 <edwardk> dependent types can only affect predicates, therefore they have limited runtime effect
22:49:50 <edwardk> though i have type families so thats not entirely true, there are other cases of dependent types, but basically they all resolve with phase distinction
22:49:59 * oerjan gives up trying to follow #haskell in the other window
22:50:00 <edwardk> and its implicitly typed for most things
22:50:53 <edwardk> so, hrmm, maybe a longer example?
22:51:19 <edwardk> say, we want to prove the correctness of a sort routine, but we don't want to go off and write it in coq
22:51:27 <edwardk> and we don't want to do any real explicit proofs
22:51:35 <edwardk> first we need a predicate for what it means to be sorted
22:51:48 <edwardk> sorted : Ord a => [a] -> Bool
22:51:59 <edwardk> good oldfashioned haskell modulo some syntax
22:52:07 <edwardk> we can even drop in :: to make you more at home
22:52:24 <oerjan> undecidability in theory is one thing, but the real question is whether the type inference can terminate on practical examples
22:52:52 <edwardk> in my case though you can make it so you can explicitly pass in the order there. sorted (.by : Ord a) => [a] -> Bool gives you the ability to explicitly pass the dictionary
22:52:58 <edwardk> i can always terminate and insert runtime checks
22:53:10 <edwardk> but i'll emit a warning if i have to give up
22:53:52 <oerjan> heh i noticed automatically greating *By functions was mentioned on #haskell before i gave up
22:54:02 <edwardk> so, going with the sorted example you can build it up like haskell sorted [] = True; sorted [x] = True; sorted (x:xs) = x <head xs && sorted xs
22:54:24 <edwardk> now, lets say what it means to be sorted
22:54:29 <edwardk> er for a sorting routine to sort
22:54:54 <edwardk> sort : (.by : Ord a) => [a] -> (xs : [a] | sorted xs)
22:55:33 <edwardk> where ( x : T | P x) is a predicate subtype, like mathematicians write { x : T | P x }, i just need { }'s for records so i swap unambiguously to ()'s
22:55:52 <ihope> Subset and quotient types?
22:55:54 <edwardk> now, that reads as a post-condition on sort's output
22:56:00 <edwardk> there is a subset type in action
22:56:10 <ihope> I've seen derivatives, but no quotients...
22:56:23 <edwardk> f : (x : T | pre x) -> (y : T | post x y)
22:56:49 <edwardk> specifies pre conditions necessary to call the function and post conditions of what it gaurantees
22:57:24 <edwardk> a quotient type is where you redefine equivalence over the type, in this case it interacts in somewhat interesting ways with the rest of the type system
22:57:32 <edwardk> think of it like a newtype redefining == on steroids.
22:57:55 <edwardk> a sort of generalized generalized newtype deriving ;)
22:58:59 <edwardk> anyways, we can define the sort above, sort [] = []; sort (x:xs) = insert x (sort xs) where insert : a -> (xs : [a] | sorted xs) -> (ys : [a] | sorted ys) has the obvious definition
22:59:05 <oerjan> reminds me of the little n-category stuff i remember
22:59:07 <edwardk> and the compiler incurs the proof obligation
22:59:17 * oklopol wishes he'd understand enough of that to be able to say something
22:59:41 <oerjan> oklopol: i found out how to move in your game
23:00:34 <edwardk> and if you don't want to limit the use of insert you can go to a more liberal definition: insert : Ord a => a -> (xs : [a]) -> (ys : [a] | sorted xs ==> sorted ys) --- er i forgot the Ord a => constraint in the insert above
23:00:53 <oklopol> now knowing how it's done is one thing, *moving* is a completely different story
23:01:13 <edwardk> anyways the compiler just uses a form of abstract interpretation and the octagon abstraction domain for integer operations
23:01:29 <edwardk> and tries to prove what it can
23:01:35 <oerjan> oklopol: pressing the button makes it go towards the accompanying swarm
23:01:58 <edwardk> if it can't prove the correctness of the output or input it insert a runtime check and warns, if it can provide a counter example at compile time it gives you that and a trace
23:02:39 <oklopol> oerjan: there is also a small quirk there, you see gravity is not 2d, but separate for both axes :)
23:03:13 <oerjan> not pushing the button seems to be a bit more vague
23:04:04 <oerjan> but it seems to interact with the wave pattern somethow
23:04:04 <oklopol> nope. just the other way around :)
23:04:14 <bsmntbombdood> * oklopol wishes he'd understand enough of that to be able to say something
23:04:27 <ihope> Wave pattern? What is this?
23:04:50 <edwardk> anyways, its my current obsession ;)
23:05:01 <oklopol> don't try to crack that, oerjan :D it should go towards the light spots, but it's just a quick add and doesn't work that well
23:05:27 <ihope> edwardk: you're obsessed with creating languages with obscure features, is it? :-)
23:05:28 <oklopol> ihope: a game i made some years ago
23:06:05 <oerjan> well it did seem like it tried to hunt those down vaguely
23:06:42 * ihope scans it for viruses
23:06:44 <oklopol> i think it find the lightest pixel around the ball on 32 pixel range and goes towards it
23:06:48 <ihope> It's taking a little while.
23:07:12 <oklopol> i have no idea whether i have a virus scan, i've never really believed in viruses :)
23:07:15 <ihope> csrss.exe is using all the CPU time again...
23:07:19 <bsmntbombdood> in haskell can you do the f (x+1) = ... with any function of x?
23:07:19 <edwardk> ihope: well, its not exactly an obscure feature, adding compile-time-checked contracts in the same language the end-user is already familiar with writing their code in strikes me as rather front-and-center from a usable powerful feature standpoint =)
23:07:20 <oklopol> neither computer nor human ones
23:07:32 <oerjan> it is hard to crack because unless you manage to get away from the swarm all the effects are so small
23:08:05 <ihope> bsmntbombdood: only constructors and a few other things, I think.
23:08:23 <oerjan> edwardk: so this is essentially a Haskell dialect?
23:08:27 <ihope> Try to do something like f (g x) = ... and... bad things happen.
23:08:34 <oerjan> with a bit ocamlized syntax
23:08:40 <ihope> That's sort of Curry's job, though.
23:09:04 <edwardk> bstmtb: you can do so only with + and only if the inferred type of the n+k pattern is a member of the Integral typeclass
23:09:25 <oerjan> bsmntbombdood: the x+n pattern is about the only thing which is a multiargument function
23:09:37 <oerjan> and it is considered by some a wart in haskell
23:09:38 <edwardk> oerjan: not really because i break everything else in the language on the way to get usable records and my type syntax looks nothing like it beyond the trivial examples
23:09:51 <edwardk> oerjan: but haskell is the easiest launching off point for me to take when explaining it
23:10:06 <edwardk> oerjan: example of a big syntactic change
23:10:29 <edwardk> doesn't require any statement that nat is a type or capitalization on the tycon
23:11:27 <edwardk> also, you can give classes names which dramatically changes the semantics of passing them, since an instance is just a dependently typed record you guarantee to exist
23:11:58 <oklopol> oklotalk can invert functions, -Func will do it... unfortunately that's one of the superturing things that will most like just crash :)
23:12:08 <edwardk> that way you can HAVE multiple instances of Ord for Int, one default, a bunch named, and you can pass in the named one to sort using that sort .by foo syntax
23:12:33 <edwardk> first class extensible records with subtyping also mucks with a lot of the haskell properties
23:12:57 <oerjan> what if you have a function that uses two different ord instances?
23:13:26 <oklopol> bsmntbombdood: i'd say it is
23:13:40 <edwardk> oerjan: you can refer to their members by the name you gave the dictionary inside the function if the typing is ambiguous otherwise if there is only one way to unify it'll choose the right one
23:13:41 <oklopol> but that's just a hunch, i don't know why it would be
23:13:47 <ihope> How do you know it isn't super-Turing?
23:14:17 <oerjan> ihope: you can just search for the inverse
23:14:36 <ihope> What if the range is uncountable?
23:14:44 <oklopol> oerjan: if it's a real -> real function, that's uncountable as ihope said
23:14:50 <oerjan> computable things are not uncountable
23:14:56 <ihope> ...or is it the domain that I mean?
23:15:09 <edwardk> so in the above with sorted : (.by : Ord a) => [a] -> Bool; sort (x:xs) = x <=_by head xs && sorted xs exploits the fact that i allow foo.bar and bar_foo to be used as synonyms so that you can to infixed operators looked up in records.
23:15:31 <bsmntbombdood> there has to be a better way than searching for the inverse
23:15:50 <ihope> Especially if you have access to quantum mechanics.
23:15:51 <edwardk> so <=_by and `by.<=` would be identical in that case
23:16:25 <ihope> bsmntbombdood: and the results?
23:17:09 <edwardk> dictionary passing is a bit more complicated by the fact that i want to pass a single polymorphic dictionary record when possible, so multiparameter type classes incur some weirdness
23:18:05 <ihope> Good thing there was no emesis.
23:18:25 <oklopol> just searching for the answer in deed isn't superturing
23:18:48 <ihope> The problem is doing it quickly.
23:19:21 <oklopol> the idea why i'm making stuff like that in oklotalk is to make them work with simple math expressions
23:19:22 <ihope> Doing it quickly means you can construct a function proof -> sentence and invert it to prove any provable sentence :-)
23:20:02 <edwardk> oerjan: anyways thats the rough idea
23:21:04 -!- edwardk has quit (Read error: 104 (Connection reset by peer)).
23:22:18 <oerjan> ihope: as far as i know quantum computing is not known to be sufficient to invert all functions quickly, as in there is no quantum algorithm to solve NP-complete problems in polynomial time
23:22:31 <ihope> Depends on how you define "quickly".
23:22:45 <oerjan> i just did in the second halg
23:23:16 <ihope> Inverting gets weirder when you bring foralls in: forall a. a -> * = (exists a. a) -> * whose inverse is * -> exists a. a
23:23:23 <oerjan> *no _known_ quantum algorithm
23:23:43 <oerjan> they are np but not np-complete
23:23:57 <ihope> Checking for primeness?
23:24:00 <oklopol> np-complete one that any np can be converted to or smth?
23:24:24 <oerjan> no they definitely are np, since that includes all the weaker ones
23:24:28 <ihope> NP-complete problems are the hardest ones.
23:24:38 <oklopol> factoring and primechecking are essentially the same thing
23:25:02 <ihope> Isn't that far from proven and much suspected to be false?
23:25:13 <oerjan> there _is_ a known algorithm in P for checking primes
23:25:16 <ihope> oklopol: give me a factoring algorithm given a prime checking algorithm.
23:25:30 <oklopol> oerjan: isn't it err... how do you say it
23:26:02 <ihope> You're such a naab indeed. :-P
23:26:13 <oklopol> yeah, but so eager to learn.
23:26:32 <oerjan> and also more inefficient than the probabilistic algorithms
23:27:19 <oklopol> actually, i'm pretty sure read there isn't one, and that was less than a year ago
23:27:33 <oklopol> and i'd say that was in wikipedia
23:27:50 <oerjan> oklopol: there is an algorithm for checking if a number is a prime in polynomial time
23:27:53 <bsmntbombdood> if prime checking was the same as factoring most public key cryptographic algorithms would be pointless
23:28:13 <oerjan> there is not one known to factorize a number if it isn't prime
23:28:45 * oerjan is checking wikipedia now
23:28:51 <oklopol> bsmntbombdood: i mean it's the same if you just care about p/np and assume it needs to be deterministic
23:29:22 <oerjan> http://en.wikipedia.org/wiki/AKS_primality_test
23:29:26 <oklopol> oerjan: i might recall wrong, my memory likes to carefully change all the new facts to what i assumed myself
23:29:42 <oerjan> oklopol: thus proving SimonRC's theory :)
23:30:53 <oklopol> actually i'm not sure if i believe that
23:31:04 <oklopol> i was referring to that exact theory.
23:31:52 <oerjan> but since you remember the theory you must believe in it, by the theory :)
23:32:04 <oerjan> bsmntbombdood: what language?
23:32:48 <oerjan> it means modulo the ring ideal generated by n and m
23:33:16 <oklopol> oerjan: isn't that circular logic?
23:33:33 <oerjan> oklopol: you got me ;)
23:33:38 -!- edwardk has joined.
23:33:53 <oerjan> bsmntbombdood: i'll try to explain it
23:34:55 <oerjan> in the (mod n, x^r-1) case it means that you first take the remainder of a polynomial division by x^r-1, then you mod all coefficients of the result by n
23:35:34 <oerjan> so you end up with a polynomial of degree < r, with all coefficients < n
23:37:17 <oerjan> well let's say you have x^3 + 5 (mod 3, x^2 + 1)
23:38:54 <oerjan> first you divide x^3 + 5 by x^2 + 1, now x^3 + 5 = x*(x^2 + 1) - x + 5, so the remainder is - x + 5
23:40:51 <oklopol> i have no idea how modulo is defined for negative numbers
23:41:15 <oerjan> by definition, a == b (mod n) means that n divides a-b.
23:42:43 <oklopol> - 2 = 1 (mod 3) <=> (-2 - 1) / 3
23:42:46 <oerjan> there is not always agreement on that: Haskell has mod and rem that behave differently with negative numbers
23:42:57 -!- edwardk has left (?).
23:43:50 <oklopol> one correction per correction is enough.
23:47:35 <oerjan> to be a little more precise, since there might be some choices of m and n where my approach subtly fails:
23:47:59 -!- Tritonio has joined.
23:48:26 <oerjan> a == b (mod m, n) means that a-b = m*x + n*y, where x and y are elements of the ring (in the article case, polynomials with integer coefficients)
23:49:19 <ihope> You know, a language based on the topologies of things like http://pastebin.ca/607871 actually would be a little insane.
23:50:02 * oerjan sees no topology in that
23:50:05 <oklopol> oerjan: i can't see any relation between those two :P
23:50:24 <ihope> oerjan: turn it upside down, and it's still pretty much the same thing.
23:51:20 <ihope> It's a crossing of two lines.
23:51:41 <oerjan> oklopol: you talking about my two mod approaches?
23:52:21 <ihope> There are no nodes.
23:53:01 <ihope> Because instead of a closed loop, it's... something else.
23:53:14 <oerjan> the first approach reduces an expression to a simpler one (mod m, n), this is sound but if we were dealing with two polynomials rather than one number and one polynomial as in the article, then you might not necessarily reach a unique form just by doing it in sequence
23:53:15 <ihope> Nearly headless 8.
23:53:20 <oklopol> seems i don't know what topologies are :)
23:54:15 <oerjan> as in, it might be possible to continue dividing by m and n alternately without immediately reaching the same result
23:54:33 <oerjan> perhaps you could even cycle, i am not quite sure
23:55:11 <oklopol> oerjan: i understand how you do that, but i can't really figure out what it actually means :P
23:57:02 <oerjan> oklopol: it is all about quotient rings. You get the ring of integers mod n by identifying every two integers that have the same remainder mod n
23:57:27 <oerjan> == whose difference divides n
23:57:56 <oerjan> but then you want to do two sets of identifications simultaneously
23:58:35 <oerjan> and the way to do that is to look at the set that identifies with 0.
23:58:44 <oerjan> this set is what is called an ideal.