00:11:45 <oren> Fail. The lecture slides for my course, I just realized their mtime is in 2006, indicating this guy has been giving the same lectures with the same material for 9 years.
00:12:56 * oren idly wonders if he makes new tests...
00:13:18 <boily> helloren. which course?
00:14:45 <oren> Knowledge Representation and Reasoning, i.e. the out-of-fashion kind of AI
00:15:44 -!- GeekDude has joined.
00:18:18 -!- bb010g has quit (Quit: Connection closed for inactivity).
00:34:33 <elliott> well, if it's out-of-fashion...
00:35:19 <oerjan> the AIs are just keeping it out of fashion to prevent competition hth
00:35:25 <zzo38> I have a digital cable box (I don't need it, but someone else here uses it); I figured out how to access the diagnostics menu, user setting menu, and in the review configuration menu pushing the FAV button displays many additional screens of information; I don't know what all of them mean, but on some screens pushing A allows entering a command with the numbers, the GuideNet screen lists them.
00:35:38 <oren> elliott: good point. perhaps not much work has been done beyond what is in the text. everyone and their mother is doing neural networks now
00:35:41 <zzo38> Some screens display IP addresses. Unfortunately I don't know what any of that is or how to use any of it
00:37:03 <boily> couldn't you write a GUI in VB to track them?
00:38:07 -!- Lymee has joined.
00:40:25 <zzo38> I don't know what GuideNet means or what the IP address and other information under "interactive status" means either; Wikipedia has no information. I was able to look up DOCSIS and MoCA on Wikipedia though.
00:41:04 -!- Lymia has quit (Ping timeout: 265 seconds).
00:41:50 <oren> what happens if you put the ip into browser?
00:42:33 <zzo38> I tried connecting using netcat to various port numbers and found nothing.
00:43:11 <boily> do you feel courageous enough to nmap the fungot out of those IPs?
00:43:11 <fungot> boily: they make a movie out of " disk" space...) stuff. i just think you're an abomination" :)
00:43:18 <fungot> boily: discordianism is almost not a joke really, because the first
00:43:30 <zzo38> I don't have nmap though
00:44:07 <zzo38> One of them seems to be a LAN address; even though my internet is on the same cable as the television, I cannot connect to it.
00:44:52 <zzo38> I didn't try UDP though; I don't know if maybe that's what I need.
00:45:09 <boily> oerjan: on a completely off-topic subject, you know I still have PHHHMHSD?
00:45:38 <boily> (Post Hej Hej Hemst Micket (sorry for the orthograph) Hej Syndrome Disorder)
00:46:41 <oerjan> i recommend exposure therapy hth
00:48:24 <zzo38> I don't know what that means though
00:48:29 <int-e> https://en.wikipedia.org/wiki/Exposure_%28photography%29 ?!
00:48:42 <boily> zzo38: you do well. continue not knowing. it's good for you.
00:50:31 <oren> I recommend crazy frog therapy
00:51:15 <boily> I like the rick-roll-I-get-knocked-down mashup.
00:52:29 <zzo38> Now I figured out the .XI so I am fixing AmigaMML to support loading .XI instruments when in Extended mode (you can't use .XI in Amiga mode though).
00:53:36 <boily> zzo38: mods, trackers, chiptunes and generic 8-bit music and stuff like that?
00:54:03 <zzo38> boily: I don't know what you are asking; can you please be more specific?
00:55:11 <boily> sorry, I'm drawing a phantomatic blank here... I have this feeling I'm forgetting a word, but I'm not sure.
00:55:36 <boily> you are doing stuff that has to do with playing music through an Amiga emulator?
00:55:58 <boily> what's an .xi then?
00:56:12 <zzo38> Other than being able to output in .MOD format, it hasn't anything to do with Amiga.
00:56:36 <oerjan> boily: is the word amortized hth
00:56:37 <zzo38> A .xi is a instrument file for Fasttracker. AmigaMML has two modes, Amiga mode (which is the original mode), and Extended mode.
00:56:58 <boily> oerjan: no. tdnh, bio.
00:57:12 <boily> zzo38: aaaaaaaaaaaah. ic.
00:57:47 <zzo38> AmigaMML is a program that you can write music and then compile into .MOD and .XM files.
00:58:22 <boily> oerjan: that did not help, but it's okay hth
00:59:38 <MDude> Does that stand for music markup language or music macro language?
00:59:47 <zzo38> MDude: Music macro language
01:00:03 <boily> go HackEgo go! go HackEgo go!
01:00:34 <MDude> Thanks, I wasn't sure a quick search for AmigaMML dind't bring up much.
01:00:53 <MDude> Also also both of those languages exist, being cofusingly similarly named.
01:00:55 <oerjan> `learn A hand in the bush is better than a stoned bird hth
01:00:59 <HackEgo> Learned 'hand': A hand in the bush is better than a stoned bird hth
01:01:27 <zzo38> Well, this is the Redmine page for AmigaMML: https://devlabs.linuxassist.net/projects/amigamml
01:01:44 <zzo38> In case it helps you at all.
01:01:50 <oerjan> `learn A hand in the bush is better than a stoned bird.
01:01:54 <HackEgo> Learned 'hand': A hand in the bush is better than a stoned bird.
01:02:06 <shachaf> oerjan: also what's with the drugz jokez lately
01:02:22 <boily> shachaf: did you just pluralise y'all?
01:02:38 <oerjan> y'all y'all need to stop doing that
01:02:42 <shachaf> the plural of "y'all" is "all y'all" hth
01:02:53 <shachaf> hope this helps you at all
01:03:01 <zzo38> Isn't "y'all" already plural?
01:03:16 <shachaf> not when addressing one person hth
01:03:40 <oerjan> zzo38: you know of the euphemism threadmill? in english, second person pronouns have a plurality threadmill
01:03:45 <MDude> It does, I'll check this out.
01:03:55 <int-e> zzo38: all of you are correct :P
01:04:36 <zzo38> MDude: Yes I know, MML can refer to both, but in this case it is music macro language. There are other programs to do music macro language too, such as SakuraMML, ppMCK, CsoundMML, and probably others I don't know about.
01:04:37 <oerjan> which probably started as part of the euphemism threadmill, anyway
01:04:43 <int-e> (To my mind, the "you" may be singular, the phrase isn't.)
01:05:14 <int-e> I wonder how a threadmill works.
01:05:27 <boily> it mills threads. next!
01:05:30 <MDude> I didn't know it was made for Windows, or that you made it. I am pleasantly surprised on both counts.
01:05:38 <oren> int-e it makes nylon thread hth
01:05:45 <int-e> Do you put threads in and grind them, or is it cleverly arranged such that threads come out?
01:06:07 <shachaf> the way the mill cpu implements fork() will be revealed soon
01:06:24 <zzo38> MDude: Well, it isn't only Windows; it should be possible to compile AmigaMML for other systems too, if you have a C compiler. I don't actually know if it will actually run on a Amiga computer though.
01:06:24 <int-e> I guess it would also make an excellent name for a scheduler.
01:07:15 <MDude> I was more worried it wouldn't run on anything but Amiga. Or Linux, since Linux was in the url.
01:07:21 <oerjan> is a spaghetti machine a threadmill?
01:07:26 <MDude> But it turns out that isn't the case.
01:07:53 * oerjan suddenly regrets not spelling it spagetti
01:08:08 <oerjan> (which btw is the correct norwegian spelling.)
01:08:33 <shachaf> that would be a good pun for all the norwegian speakers in this channel
01:08:49 <zzo38> Linux Assist is just the Redmine server for FOSS projects; it isn't only for programs specific to Linux.
01:11:15 <oren> oerjan: I would have pronounces that as /spædʒetī/
01:12:37 <oerjan> that's not norwegian hth
01:13:05 <oren> it's the correct pronounciation for that spelling if it were italian
01:13:22 <oren> (up to my knowlege of italian)
01:13:32 <oerjan> (we don't have /dʒ/ except in loanwords)
01:14:13 -!- bb010g has joined.
01:14:22 <oerjan> why the bar over the i
01:14:57 <oren> oh, I forgot in IPA long vowels are supposed to have : not overbar
01:15:39 <oerjan> you learn something every day
01:16:03 <oerjan> boily: what language is that twh
01:16:39 <oren> shachaf: I don't know, but the one in spaghetti is when I hear italians say it...
01:17:02 <oren> (I live in Little Italy in Toronto)
01:17:46 <boily> oerjan: a parody of low-class country bums in then Eastern Townships.
01:19:24 <boily> shachaf: boilognese. he he he! I'll remember that one.
01:19:39 <oren> p. nifty? is that the name of a rapper?
01:20:45 -!- doesthiswork has joined.
01:21:30 <oren> yo, ma name's p. nifty, an' i'm pretty shifty, watch me spit these riffs like a tokyo drift king.
01:24:22 <Jafet> Are Tokyo drifters known to spit riffs?
01:24:42 <Jafet> (Do drifters drift? I suppose not.)
01:25:59 <oren> I don't think so, but it makes about as much sense as many real reaps I've heard...
01:26:26 <oren> shit s/har/hear
01:27:14 <boily> Jafet: does an otter ott?
01:28:28 <oren> Hmm the oldest woman in the world died again
01:30:38 <oren> Wow it isn't in the English news yet
01:32:15 <oren> hmm, I wonder how long it takes for a typical story to reach English-speaking news channels, and whether it depends on the language zone that the story comes from
01:33:07 * boily sings “mushroom mushroom ♪”
01:33:19 <oren> damn neat me to it
01:33:32 <oerjan> <oren> Hmm the oldest woman in the world died again <-- this keeps happening, they should do something to stop it hth
01:34:00 <oren> In this case it was ookawa misao, 117.
01:34:09 <zzo38> oerjan: Not necessarily.
01:34:25 -!- oerjan has set topic: RIP Ookawa Misao | I'm a fungot trapped in a channel full of weirdos | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/.
01:35:27 <zzo38> Having a cable box at least allow me to know what show is on at 3AM and stuff like that, because the TV guide doesn't list shows at that time. But when I watch television I use the VCR in the basement instead.
01:35:34 <oren> So the question is when will it reach Google news search?
01:35:50 <zzo38> But, I also like to learn how the diagnostics and stuff in the cable box is working anyways.
01:36:27 <boily> zzo38: I'll be at my parents' this weekend. remind me to hack their cable box then ^^
01:36:34 <boily> meanwhile, 'night all!
01:36:38 -!- boily has quit (Quit: PREMOLAR CHICKEN).
01:36:42 <shachaf> it seems to be unconfirmed hth
01:36:43 <int-e> On this strange day... http://news.asiantown.net/r/47594/mexican-woman-dies-at
01:37:04 <zzo38> Unfortunately I don't know how to hack it, but I can tell what some of the undocumented functions are at least; that can still help
01:37:39 <int-e> ("oldest person on earth" must be one of the most unreliable (and short-lived...) attributions)
01:37:41 <oren> I have been noticing a significant delay between NHK and the anglospheric news when anything happens in Japan.
01:38:07 <pikhq> Are you in Japan these days?
01:38:31 <pikhq> Well, presumably. It's possible but unlikely you're watching NHK outside of Japan.
01:38:39 <oren> No but reading NHK online is good practice
01:39:39 <oren> for example, I knew about the deal with Nintendo and DeNA five hours before it reached Google News
01:39:41 <zzo38> I am not at Japan but do want to order something; I bought a Famicom at a store locally and then I asked them next time if they can get the keyboard too so that I can buy from them, but they have not done.
01:40:02 <pikhq> That keyboard is pretty rare, isn't it?
01:40:02 <int-e> Ah, wikipedia half-knows... https://en.wikipedia.org/wiki/Misao_Okawa (lists date of death, but has not otherwise been updated)
01:40:14 <zzo38> I don't know how rare it is.
01:40:36 <pikhq> At least it is relative to the Famicom. :)
01:41:35 <oren> Yeah but there are a ton of fake famicoms on the market
01:41:55 <pikhq> Yeah, but not really any that are trying to pass themselves off as real ones.
01:42:05 -!- adu has joined.
01:42:30 <oren> wikipedia now says "was"
01:42:43 -!- oerjan has set topic: RIP Misao Okawa | I'm a fungot trapped in a channel full of weirdos | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/.
01:43:21 <pikhq> God, if you consider Famiclones the damned things might be the single most common computing device on the planet.
01:44:05 -!- LordCreepity has joined.
01:44:15 <oren> 6502 - the perfect eternal processor
01:44:45 <oren> (technically they use a modified version)
01:45:10 <zzo38> Famicom uses 6502 with a few traces cut off so that decimal mode won't work.
01:45:24 <zzo38> However, all other functions of NMOS 6502 including unofficial functions still work.
01:45:44 <pikhq> I thought they had decimal mode on there?
01:45:58 <pikhq> I coulda sworn the only modification was sticking some sound hardware on the die.
01:46:21 <pikhq> Oh, no, it is lacking.
01:46:22 <oren> I thought they removed the decimal mode to make room of something
01:46:23 <zzo38> Decimal mode doesn't do anything on Famicom; you can turn it on and off but it doesn't affect operation of arithmetic.
01:46:40 <LordCreepity> has anyone in here ever taken a look at the instruction set of the EDSAC?
01:46:50 <zzo38> oren: No, all they did is cut a few traces so that decimal mode doesn't work. Other than that it actually is a 6502.
01:46:54 <oerjan> hm in 2-3 years there may not be anyone left alive born in the 19th century
01:47:01 <zzo38> They use the same mask.
01:47:49 <pikhq> Ah, yep, they literally removed 5 transistors in the mask.
01:47:55 <oerjan> 115 years old seems a particularly dangerous age
01:48:37 -!- mihow has joined.
01:48:46 <pikhq> There was a patent on the decimal mode that Nintendo did not want to license.
01:48:49 <int-e> oerjan: well 9 "confirmed" people left... https://en.wikipedia.org/wiki/List_of_living_supercentenarians
01:49:08 -!- Lymia has joined.
01:49:35 <shachaf> If I said Θ(f) ≤ Θ(g), would people understand what I mean?
01:49:46 <oren> oerjan: i was recently like o_O upon seeing a pamphlet for a piano recital my grandmother gave in 1944
01:50:33 <oren> shachaf: if that is big theta notation yes. if that is an emoticon then no.
01:51:09 <pikhq> If you look at the die shot you can see that it is literally a 6502's mask with apparently those transistors missing, and some sound hardware. That is really interesting.
01:51:13 <shachaf> But a non-standard use of it.
01:51:21 -!- Lymee has quit (Ping timeout: 256 seconds).
01:51:49 <int-e> shachaf: you could just write f \in O(g) ...
01:51:59 <int-e> (f = O(g), but I dislike that notation)
01:52:12 <shachaf> int-e: Yes, but then I have to remember what o/O/Θ/Ω/ω mean.
01:52:26 <shachaf> It's ridiculous. Why invent a new letter for each of those things?
01:52:37 <int-e> You have to do that anyway, at least the three capital things.
01:52:42 <oren> big theta means a bound above and below right?
01:53:03 <shachaf> It's much easier to remember what </≤/=/≥/> mean.
01:53:22 <int-e> shachaf: not really, when it applies to sets.
01:53:24 <shachaf> Since I use those all the time. Why should this particular preorder get special symbols?
01:54:12 <oren> O above, Omega below, Th both
01:54:13 -!- mihow has quit (Quit: mihow).
01:54:34 <int-e> shachaf: I would go as far as calling Θ(f) ≤ Θ(g) *wrong*, because the standard definition A <= B is a <= b for all a in A and b in B.
01:54:44 -!- oerjan has quit (Quit: Nite).
01:54:53 <shachaf> That definition isn't very standard.
01:55:08 <shachaf> At least I can't remember ever seeing it.
01:55:31 <shachaf> If you want I can use a different symbol instead of Θ. The point is that I'm putting this partial order on the equivalence classes.
01:55:32 <int-e> It's the standard way of extending relations to sets, if there is any standard way at all.
01:55:44 <int-e> shachaf: I would agree more with O(f) \subseteq O(g).
01:56:14 -!- variable has changed nick to trout.
01:56:24 <shachaf> What do you gain over f ∈ O(g) there?
01:56:35 <oren> I should get a LaTeX mode on my IME
01:56:44 <shachaf> ↓{Θ(f)} can mean what O(f) means, though admittedly that notation is less common.
01:56:52 <int-e> shachaf: you can use O(f) = O(g) for f \in \Theta(g)
01:58:08 <shachaf> Oh, I see. You can just use ⊆ instead of ≤ and it gives you the order I want?
01:58:16 <int-e> shachaf: So I think this would accomplish what you wanted: having only one of O/\Theta/\Omega to remember.
01:59:09 <shachaf> So you're saying, O(f) ⊂/⊆/=/⊇/⊃ O(g)
01:59:36 <int-e> I'm not yet sure about o.
02:00:30 <shachaf> "f ∈ o(g)" just means "f ∈ O(g) and f ∉ Θ(g)", doesn't it?
02:00:51 <int-e> mainly because there are non-monotone functions like f(n) alternating between n (for even numbers) and 0...
02:01:23 <int-e> No, f \in o(g) means that the limit of f(n)/g(n) as n goes to infinity is 0.
02:01:44 <shachaf> Hmm. Maybe my other order was too simplistic too.
02:02:13 <int-e> Which I currently believe is stronger that f \in O(g) and g \notin O(f).
02:02:57 <int-e> taking that alternating function as f, and g(n) = n.
02:06:24 <shachaf> What are you saying about these f and g?
02:06:53 <int-e> that f \in O(g) and g \notin O(g) and f \notin o(g).
02:09:39 <int-e> Which demonstrates that f \in o(g) is different from O(f) \subsetneq O(g).
02:10:11 <int-e> Sorry, I didn't make the definitions.
02:10:22 <shachaf> You should be in #-lens or #-blah or one of the other channels that I was talking about this.
02:11:43 -!- LordCreepity has quit (Quit: Leaving).
02:12:19 -!- LordCreepity has joined.
02:14:30 <int-e> Perhaps, but I'm on too many channels already, and neither -blah nor -lens really interest me.
02:28:18 <Sgeo> shachaf: Prismata is having an April Fools Day event
02:28:24 <Sgeo> With 9 fake new units and 1 real new unit
02:34:01 <zzo38> I must have made a mistake in the .XI loading code because it doesn't quite work properly.
02:38:02 -!- LordCreepity has quit (Quit: Page closed).
02:43:41 -!- LordCreepity has joined.
02:43:50 -!- LordCreepity has quit (Client Quit).
02:51:33 <zzo38> Now all of the updates are on the Redmine too.
02:55:33 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
02:55:46 <Sgeo> I love /r/todayilearned's CSS
02:56:28 <Sgeo> They're making every comment look like it's saying conspiracy stuff
02:58:10 -!- infinitymaster has joined.
02:58:58 <infinitymaster> !zjoust Iron_Will_and_a_Clear_Conscience >(-)*15>(+)*15(>++>--)*3>([(+)*15[-]]>)*21
02:58:59 <zemhill_> infinitymaster.Iron_Will_and_a_Clear_Conscience: points -3.40, score 17.03, rank 35/47
03:14:44 -!- MoALTz has joined.
03:16:21 -!- heroux has quit (Ping timeout: 256 seconds).
03:16:55 -!- heroux has joined.
03:17:14 -!- MoALTz__ has quit (Ping timeout: 252 seconds).
03:30:46 -!- GeekDude has quit (Ping timeout: 264 seconds).
03:31:57 -!- Lyrr has joined.
03:32:03 -!- GeekDude has joined.
03:36:02 <Sgeo> Is it weird that I enjoy Internet April Fools so much?
03:39:37 -!- MDude has changed nick to MDream.
03:40:42 -!- vodkode_ has quit (Ping timeout: 248 seconds).
03:41:18 -!- Lyrr has left.
03:49:05 -!- GeekDude has quit (Ping timeout: 265 seconds).
03:49:18 <zzo38> quintopia: What is thx tdh?
03:49:47 -!- GeekDude has joined.
03:50:22 -!- vodkode_ has joined.
03:51:46 -!- hjulle has joined.
03:54:17 -!- oren has quit (Quit: Lost terminal).
03:56:58 <Sgeo> Tagpro has an April Fools Day event, but it only runs the first 15 minutes of every hour
03:57:16 <Sgeo> It is driving me crazy, I'm timing my life around it right now
03:57:40 <Sgeo> Which, I think, involves me playing less tagpro than usual, ironically enough
03:59:19 -!- adu has quit (Quit: adu).
04:07:58 -!- doesthiswork has quit (Quit: Leaving.).
04:15:02 -!- adu has joined.
04:15:16 -!- adu has quit (Client Quit).
04:18:57 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)).
04:22:56 -!- Lymia has quit (Ping timeout: 265 seconds).
04:25:23 -!- adu has joined.
04:29:04 -!- Decim has joined.
04:30:16 -!- vodkode_ has quit (Ping timeout: 245 seconds).
04:39:16 -!- vodkode_ has joined.
04:48:06 -!- infinitymaster has quit (Quit: Leaving...).
04:49:34 -!- MoALTz_ has joined.
04:52:18 -!- MoALTz has quit (Ping timeout: 246 seconds).
04:57:05 -!- adu has quit (Quit: adu).
05:22:47 -!- vodkode_ has quit (Ping timeout: 272 seconds).
05:23:53 <Sgeo> I think my graphics card's video decoding is broken
05:24:06 <Sgeo> Videos stopped working for me until I told Chrome not to use hardware decoding
05:27:40 -!- adu has joined.
05:41:16 <Sgeo> https://com.google/
05:41:35 -!- vodkode_ has joined.
05:48:29 -!- Welcome has joined.
05:48:29 -!- Decim has quit (Read error: Connection reset by peer).
05:55:37 <Sgeo> "Think of Smartbox as Google’s attempt to reinvent physical mail. It has smart folders, filters, and even apps. Oh, and you can take Smartbox with you, wherever you go."
05:55:40 <Sgeo> Ugh I want this for real
06:04:41 -!- zadock has quit (Quit: Leaving).
06:19:31 -!- adu has quit (Quit: adu).
06:25:04 -!- Welcome has quit (Ping timeout: 255 seconds).
06:47:22 -!- zadock has joined.
07:11:05 -!- trout has quit (Ping timeout: 272 seconds).
07:30:52 -!- Lymia has joined.
07:48:32 -!- Patashu has joined.
07:57:10 <shachaf> λ> typeRep (Proxy :: Proxy A) == typeRep (Proxy :: Proxy B)
07:57:10 <shachaf> λ> typeRep (Proxy :: Proxy (Proxy A)) == typeRep (Proxy :: Proxy (Proxy B))
07:57:32 <shachaf> int-e, oerjan: Any ideas for what to do with that?
08:03:40 -!- cpressey has joined.
08:03:58 <cpressey> fungot: did you enjoy your outage?
08:03:58 <fungot> cpressey: scheffig is the scheme48 native compiler coming along? ( sorry, i didn't
08:06:57 <izabera> http://home.web.cern.ch/about/updates/2015/04/cern-researchers-confirm-existence-force
08:16:41 <b_jonas> fungot, do you like april?
08:16:41 <fungot> b_jonas: what did you do
08:21:02 -!- shikhin has joined.
08:21:09 <mroman> b_jonas played a 1. April prank on fungot!
08:21:09 <fungot> mroman: i know im an asshole.
08:23:01 <mroman> fungot: Well then you deserve the prank.
08:23:02 <fungot> mroman: ok, here's a *great* example. ( there was a roshambo bot called iocane. :) the interpreter i've used.
08:36:41 -!- lambdabot has quit (Remote host closed the connection).
08:42:33 -!- lambdabot has joined.
08:43:34 -!- vodkode_ has quit (Ping timeout: 252 seconds).
08:54:25 <izabera> https://imasheep.hurrdurr.org/
08:54:36 <izabera> kernel.org redirects there ^^
09:03:31 <izabera> it's because linux 4.0 is codenamed hurr durr ima sheep
09:05:06 <izabera> linus started a test poll on google+ and one of the options was hurr durr ima sheep ^^
09:06:26 <cpressey> https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/commit/?id=c517d838eb7d07bbe9507871fab3931deccff539
09:06:26 <lifthrasiir> http://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/commit/?id=c517d838eb7d07bbe9507871fab3931deccff539
09:11:59 <b_jonas> oh, so that's why it redirects!
09:12:11 <b_jonas> and the title has changed too
09:12:17 <b_jonas> it says "The Hurr Durr Archives"
09:16:43 -!- lambdabot has quit (Quit: ...).
09:21:06 -!- zzo38 has quit (Ping timeout: 246 seconds).
09:21:53 -!- lambdabot has joined.
09:49:24 <Jafet> https://en.wikipedia.org/wiki/List_of_Linux_kernel_names
09:51:19 <cpressey> those need to be displayed prominently upon boot
10:10:39 <int-e> shachaf: well, are those types actually different so that it breaks gcast in connection with a type family?
10:10:59 <shachaf> They're different types with different kinds.
10:11:15 <shachaf> Which is why Proxy gets different TypeReps.
10:13:37 <int-e> So it doesn't break gcast then.
10:13:51 <int-e> I *believe* that's fine.
10:14:40 <shachaf> I can't think of a way to write unsafeCoerce with it, at least.
10:18:16 <shachaf> A is () :: *, b is () :: Constraint
10:20:06 <int-e> typeRep (Proxy :: Proxy (Proxy :: * -> *)) == typeRep (Proxy :: Proxy (Proxy :: (* -> *) -> *)) is also true.
10:21:17 <int-e> Sorry, I have 7.10.1 installed but 7.8.3 is still my default.
10:26:34 -!- boily has joined.
11:06:50 -!- Phantom_Hoover has joined.
11:20:54 <cpressey> all i'm saying is that if we have codata we might as well redefine our entire foundation of mathematics to use it. clearly, 1/0 is a corational. clearly, - can be defined over the corationals, and 1/0 - 1/0 = 0.
11:20:57 -!- roasted42 has joined.
11:21:24 -!- roasted42 has quit (Changing host).
11:21:24 -!- roasted42 has joined.
11:21:24 -!- roasted42 has changed nick to TheM4ch1n3.
11:23:41 -!- boily has quit (Quit: IDENTIFIABLE CHICKEN).
11:23:53 <int-e> cpressey: your use of "clearly" is clearly wrong, hth.
11:24:43 <cpressey> int-e: you didn't find that entertaining?
11:25:19 <int-e> No, because I tried to make sense of "1/0 is a corational".
11:25:45 <int-e> Failing that, annoyance was the dominating reaction.
11:27:23 <cpressey> you make it sound like your failure to make sense of a concept is a bad thing
11:29:01 <int-e> Sorry I tend to overanalyze things.
11:31:51 <int-e> oh my. https://github.com/lambdabot/lambdabot/issues/114
11:33:15 <int-e> I think I'll wait a day before closing that one :P
11:40:51 -!- Patashu has quit (Ping timeout: 256 seconds).
11:52:54 -!- Sgeo has quit (Ping timeout: 250 seconds).
11:59:43 -!- oerjan has joined.
12:22:47 -!- shikhin has quit (Ping timeout: 256 seconds).
12:25:29 <oerjan> <Sgeo> https://com.google/ <-- it doesn't change the link targets DISAPPOINTED
12:26:53 <lambdabot> Not in scope: type constructor or class ‘A’
12:27:15 <oerjan> typeRep (Proxy :: Proxy A) == typeRep (Proxy :: Proxy B)
12:27:41 <oerjan> > typeRep (Proxy :: Proxy (() :: *)) == typeRep (Proxy :: Proxy (() :: Constraint))
12:27:43 <lambdabot> Not in scope: type constructor or class ‘Constraint’
12:27:43 <lambdabot> Perhaps you meant ‘Contains’ (imported from Control.Lens)
12:28:57 <oerjan> shachaf: i cannot say, i haven't installed 7.10 yet. what is preventing you from just slotting it into one of the versions at http://oerjan.nvg.org/haskell/TypeableExploits ?
12:29:15 <oerjan> > typeRep (Proxy :: Proxy (() :: *))
12:30:14 <oerjan> int-e: import GHC.Exts.Constraint plz twh
12:31:34 <oerjan> pesky sleeping americans
12:32:26 <int-e> The real problem is that GHC.Exts is not trustworthy. So I have to wrap it... haven't bothered yet.
12:32:53 <int-e> (It's easy, that's what lambdabot-trusted is for. But it
12:33:14 <int-e> 's not limited to changing a single line in Pristine.hs.)
12:33:17 <oerjan> hm they should make a GHC.Exts.Safe then
12:34:11 <int-e> https://ghc.haskell.org/trac/ghc/ticket/9724
12:34:48 <int-e> that one fell through the cracks (I forgot about it myself, too)
12:37:15 <int-e> silly. https://com.google/
12:37:35 <oerjan> int-e: 3rd time's the charm
12:38:06 <lambdabot> monochrom says: Welcome to #haskell, where your questions are answered in contrapuntal fugues.
12:38:39 <HackEgo> 475) <monqy> mmm these music samples are still so tasteful \ 552) <oerjan> i am sorry to disappoint you, but my musical taste is on the side abba, verdi, and celine dion. i know this may not be popular and that you would have preferred me to be a satanist. \ 1235) <fungot> boily: the proc is invoked. before or after the evaluator transfers control
12:42:51 <int-e> anyway ... I need to stop procrastinating, there's a deadline (review for a conference, so not a flexible one) today.
12:46:08 -!- GeekDude has joined.
12:55:56 <cpressey> "foo is a bar" is an inductive definition; "if B is a bar, expr(B) is a bar" is an inductive definition; if I and J are inductive definitions, "I; J" is an inductive definition
12:57:48 -!- GeekDude has changed nick to GibVent.
13:01:12 <cpressey> that allows non-well-founded definitions, & could stand to be improved
13:02:51 <oerjan> if it's non-well-founded surely it must be coinductive.
13:04:00 * oerjan might be half joking there
13:04:10 <int-e> Perhaps y'all should apply soundiness to math: http://soundiness.org/documents/InDefense2.pdf
13:04:27 <b_jonas> I've seen very few april's fool things today
13:04:51 <int-e> (That soundiness thing isn't an April's fool, I'm afraid.)
13:05:23 <cpressey> oh they have their own domain now do they?
13:05:39 <cpressey> "well, that escalated" i can't do it
13:07:23 <cpressey> they have a Soundiness Statement Generator
13:08:24 <cpressey> In case you are too lazy to write, yourself, "Our analysis does not soundly handle X, Y and Z"
13:09:40 <cpressey> perhaps the next step is for them to write a Soundiness Analyzer which takes your analyzer and tells you just in what ways it is unsound
13:09:52 <int-e> We present a soundy (i.e., unsound and incomplete) analysis of Brainfuck program termination, building on previous work in random number generation.
13:11:23 * oerjan briefly thinks it's a shame healthy ends with y already
13:11:42 <oerjan> i guess one could reverse the construction
13:12:22 -!- shikhin has joined.
13:12:36 <int-e> Ooh. Right, "sound" is a noun. So a soundy thing would have to make noises. They do that quite successfully, I suppose.
13:13:26 <oerjan> int-e: a very smarty deduction
13:15:19 <oerjan> is there any way to get the type (() :: Constraint) without mentioning Constraint
13:15:55 -!- SopaXorzTaker has joined.
13:15:59 -!- SopaXorzTaker has quit (Remote host closed the connection).
13:16:56 -!- SopaXorzTaker has joined.
13:17:15 <cpressey> i can't help thinking that if people were more used to the idea of a subset of a programming language, the whole soundiness thing would be moot. your analysis is sound on some subset of the language, that's all. not a hard concept, is it?
13:17:48 -!- ProofTechnique has quit (Ping timeout: 272 seconds).
13:18:16 <cpressey> but people aren't UNused to that idea either, so i don't know. the various sub-industries, each has their own weirdness
13:18:48 <int-e> the weird is strong in oerjan.
13:19:13 <cpressey> HPC folks treat "code" as a count noun while almost everyone else treat it as a mass noun
13:22:16 <int-e> Hmm, I would've expected that of cryptographers, but not of HPC.
13:23:13 <int-e> Or cryptologists, more generally.
13:23:23 <oerjan> :k forall a. (Ord Int,a) ~ (Ord Int,()) => Proxy a
13:23:24 <lambdabot> The second argument of a tuple should have kind ‘Constraint’,
13:23:51 <oerjan> it looks impossible to get it to infer that () is a Constraint without putting it on explicitly :(
13:26:19 * oerjan hopefully checks if they got the Platform out yet
13:40:13 <cpressey> seriously though i should probably look into codata more because it seems like you could do some really interesting things with reified codata
13:42:25 -!- ProofTechnique has joined.
13:43:10 <oerjan> It's annoying when you start writing an answer to a 1 hour old stackoverflow question and someone else beats you by 10 seconds :(
13:44:02 -!- shikhin has quit (Ping timeout: 244 seconds).
13:44:21 <oerjan> well it _was_ a better answer than i was writing.
13:44:24 <mroman> oerjan: You're just being a copycat!
13:45:06 <cpressey> they probably could've hopped on IRC and gotten an answer in 5 minutes (if they were willing to put up with the belittling)
13:45:44 <oerjan> maybe. it was a little subtle.
13:45:46 <cpressey> and the "why do you want to do that, anyway?"
13:46:28 <oerjan> it's actually sort of a type bug in the API interface of the haskeline interface, that means you have to give a stupid type annotation for a type you're about to throw away...
13:47:37 <oerjan> http://stackoverflow.com/questions/29390884/ambiguous-type-variable-with-haskeline-auto-completion#29392412 fwiw
13:48:28 <mroman> fungot: Can you cook with a water cooker?
13:48:28 <fungot> mroman: neither one of these days. but rack is close enough to programming any features you want, and what we still need more optimizations.
13:48:52 <oerjan> i am not sure fungot understands the concept of water
13:48:53 <fungot> oerjan: esoerl for esoteric and erlang maybe?)
13:49:00 <oerjan> no, fungot, that is not it.
13:49:00 <fungot> oerjan: you just don't take them if you used block for begin) depending on the ordering of the for clauses...)
13:49:47 <mroman> `learn Water is a squishy substance that creeps along the floor and can suddenly fall from the heavens.
13:49:55 <HackEgo> Learned 'water': Water is a squishy substance that creeps along the floor and can suddenly fall from the heavens.
13:50:07 <cpressey> ah well, the best part of stackoverflow is the list of trending questions on the right
13:56:44 <mroman> You can get a fully functional kitchen with 200CHF.
13:57:28 <mroman> That is, if you hand wash your dishes .
13:57:51 <mroman> fungot: Do you hand wash your dishes?
13:57:51 <fungot> mroman: http://paste.lisp.org/ display/ fnord
13:58:04 <fungot> Available: agora alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc* iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp youtube
13:58:23 <fungot> Selected style: darwin (Books by Charles Darwin -- you know, that evilution guy)
13:58:35 <mroman> fungot: Your thoughts about morphic fields?
13:58:36 <fungot> mroman: dr., on corals fnord themselves." " 27. on this account i went in yesterday, and was recopied before being sent to/ lacrymal glands. this salt was first exported in 1830: in one mid-styled plant, but was withdrawn on/ appointment :) royal commissioners, that ordinary doctors know little or nothing to tell you a fnord, not by means :) its ferment, 94, 95, and generally to/ male.
13:58:44 <mroman> morphic fields even explain evolution!
13:59:42 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: morphic: not found
14:02:33 -!- shikhin has joined.
14:03:20 <fungot> Selected style: irc (IRC logs of freenode/#esoteric, freenode/#scheme and ircnet/#douglasadams)
14:03:32 <mroman> fungot: Who's douglas adams?
14:03:33 <fungot> mroman: right... it's gonna be.
14:06:20 -!- `^_^v has joined.
14:20:20 -!- shikhin has quit (Ping timeout: 265 seconds).
14:21:04 -!- MDream has changed nick to MDude.
14:35:55 <quintopia> zom3one point me to the best pranks
14:36:44 <oerjan> see #esoteric logs hth
14:36:58 <oerjan> i mean, http://home.web.cern.ch/about/updates/2015/04/cern-researchers-confirm-existence-force
14:39:07 <oerjan> too critical for the world
14:42:08 <oerjan> oh typeRep already takes a Proxy of course
14:42:55 <oerjan> ok that does seem like unsafeCoerce is hard to get from this.
14:45:19 <oerjan> it's too damn hard to find flags from inside ghci
15:02:24 -!- SopaXorzTaker has quit (Remote host closed the connection).
15:16:14 -!- zadock has quit (Quit: Leaving).
15:21:17 <oerjan> in this case it was -fprint-explicit-kinds
15:21:56 -!- TheM4ch1n3 has quit (Ping timeout: 255 seconds).
15:22:23 -!- clog has quit (Ping timeout: 264 seconds).
15:24:48 <oerjan> <int-e> oh my. https://github.com/lambdabot/lambdabot/issues/114 <-- you just have to tell them the truth; that haskell has been surpassed by befunge for this use.
15:30:26 -!- clog has joined.
15:37:37 <cpressey> fungot is actually a UFAI that is simulating you. true fact
15:37:37 <fungot> cpressey: it's done there just to show that
15:37:44 -!- roasted42 has joined.
15:38:09 -!- roasted42 has quit (Changing host).
15:38:09 -!- roasted42 has joined.
15:38:09 -!- roasted42 has changed nick to TheM4ch1n3.
15:50:03 <FireFly> fungot: what is your favourite joke today?
15:50:03 <fungot> FireFly: given a list, a sublist isn't the same as its argument a quantified noun
15:50:34 <FireFly> fungot: I'm.. I'm not sure if I get it
15:50:35 <fungot> FireFly: it does seem to be fnord.
15:52:22 -!- SopaXorzTaker has joined.
15:52:54 -!- shikhin has joined.
15:53:46 <cpressey> look, if the singularity told you a joke, do you think you'd be able to understand it? of course you wouldn't.
15:54:17 <cpressey> mroman: well, fungot, obviously
15:54:17 <fungot> cpressey: most of the stuff i do at work, and it seems i do :-o dear me.
15:58:14 -!- bb010g has quit (Quit: Connection closed for inactivity).
15:59:05 <int-e> oerjan: how about this? (I commented on that #114)
16:01:42 -!- variable has joined.
16:04:27 <int-e> oerjan: pity, I can't assign the issue to the lambdabot organization :)
16:10:52 <pikhq> http://com.google/
16:19:04 -!- cpressey has quit (Quit: leaving).
16:25:32 -!- ais523 has joined.
16:33:01 <ais523> is there any particular set of april 1 festivities I should be looking at?
16:33:32 <oerjan> well people keep linking http://com.google/
16:34:28 <ais523> oh, Google got their TLD after all?
16:34:43 <ais523> IIRC they applied for like five or six TLDs for internal use only
16:35:25 <pikhq> com.google's their first use of it for much of anything.
16:35:32 <pikhq> (publicly, at least)
16:36:25 <pikhq> Microsoft announced MS-DOS Mobile.
16:42:02 <pikhq> Oh yeah, gentoo.org was pretty good too.
16:43:29 <pikhq> And it'll be to zzo's liking too...
16:43:36 <pikhq> gopher://gopher.gentoo.org/
16:45:48 -!- oerjan has quit (Quit: Latër).
16:46:43 -!- Koen_ has joined.
16:51:54 -!- ais523 has quit.
16:52:04 -!- ais523 has joined.
16:53:14 <int-e> pikhq: I'm not sure, serving html + css + javascript over gopher just doesn't feel right
16:53:46 <int-e> (the only thing that's "proper" gopher are the directory listings)
16:54:31 -!- ais523 has quit (Client Quit).
16:54:36 -!- callforjudgement has joined.
16:55:22 -!- callforjudgement has changed nick to ais523.
16:58:47 -!- mihow has joined.
17:24:10 -!- mihow has quit (Ping timeout: 272 seconds).
17:28:11 -!- callforjudgement has joined.
17:28:22 -!- ais523 has quit (Remote host closed the connection).
17:28:35 -!- callforjudgement has changed nick to ais523.
17:30:21 -!- shikhin has quit (Ping timeout: 256 seconds).
17:33:07 -!- shikhin has joined.
17:33:31 -!- mihow has joined.
17:35:29 -!- ais523 has quit (Remote host closed the connection).
17:35:38 -!- ais523 has joined.
17:39:11 -!- TheM4ch1n3 has quit (Ping timeout: 255 seconds).
17:39:40 -!- ^v^v has quit (Read error: Connection reset by peer).
17:40:07 -!- ^v^v has joined.
17:41:45 <HackEgo> [wiki] [[Language list]] http://esolangs.org/w/index.php?diff=42254&oldid=42233 * Rottytooth * (+15) /* T */ added Time Out
17:42:16 -!- zadock has joined.
17:43:06 -!- callforjudgement has joined.
17:43:20 -!- ais523 has quit (Disconnected by services).
17:43:28 -!- callforjudgement has changed nick to ais523.
17:45:33 -!- roasted42 has joined.
17:45:47 -!- roasted42 has quit (Changing host).
17:45:47 -!- roasted42 has joined.
17:45:48 -!- roasted42 has changed nick to TheM4ch1n3.
17:46:43 -!- SopaXorzTaker has quit (Ping timeout: 265 seconds).
17:50:52 -!- callforjudgement has joined.
17:54:03 -!- ais523 has quit (Ping timeout: 248 seconds).
17:54:11 -!- callforjudgement has changed nick to ais523.
18:03:39 <int-e> hehe. "reason for data loss: guru meditation #00000025.65045338 press left mouse button to continue"
18:04:14 -!- oren has joined.
18:14:53 -!- oren has quit (Read error: Connection reset by peer).
18:16:12 -!- ais523 has quit (Read error: Connection reset by peer).
18:16:28 -!- ais523 has joined.
18:16:35 -!- ais523 has quit (Changing host).
18:16:35 -!- ais523 has joined.
18:41:19 -!- oren has joined.
18:45:27 -!- ais523 has quit (Read error: Connection reset by peer).
18:45:38 -!- ais523 has joined.
18:48:51 -!- ais523 has quit (Read error: Connection reset by peer).
18:49:03 -!- ais523 has joined.
18:49:20 -!- TheM4ch1n3 has quit (Quit: l8r, about 30m).
18:50:51 -!- variable has changed nick to trout.
18:59:15 -!- shikhin_ has joined.
19:02:36 -!- shikhin has quit (Ping timeout: 265 seconds).
19:04:43 -!- shikhin_ has changed nick to shikhin.
19:11:16 -!- oren has quit (Quit: Lost terminal).
19:11:58 <shachaf> oerjan: All of the unsafeCoerces I know how to write involve taking the TypeRep of something other than the problematic type itself.
19:12:28 -!- cpressey has joined.
19:12:29 <shachaf> E.g. F (Proxy A) vs. F (Proxy B), which is really F (Proxy * A) vs. F (Proxy Constraint B)
19:16:06 <cpressey> ais523: a coworker of mine really liked the products ThinkGeek is advertising today, but I failed to distinguish them from their regular fare
19:16:28 <ais523> cpressey: I seem to remember that at least one of their joke products was popular enough that they figured out how to manufacture it
19:16:54 -!- nys has joined.
19:26:39 -!- cpressey has quit (Ping timeout: 256 seconds).
19:27:27 -!- cpressey has joined.
19:30:01 <cpressey> fungot: want to hear a joke? not april fool's-related, i promise
19:30:01 <fungot> cpressey: gimme link! _") will put a string into an s-exp ( the kind which is planted in the garden
19:30:58 <cpressey> great, now i have to write it into a pastebin somewhere i guess
19:31:31 <ais523> this is what happens when you ask fungot things, sometimes it gives you an answer you don't want
19:31:31 <fungot> ais523: i only found at the top level, should a woodchuck chuck if a woodchuck could chuck and would chuck some amount of attention to the details.
19:31:32 <FireFly> fungot: do you plant strings in your garden?
19:31:33 <fungot> FireFly: that's fine. that's what i mean is, you can probably get a good idea if it still sleeps
19:31:59 <cpressey> except now i'm distracted about thinkinzg about what kind of s-exps are planted in the garden.
19:32:04 <cpressey> some kind of riddle, obviously
19:32:09 <ais523> the sort that you use to protect strings
19:32:49 <quintopia> i kind of want to implement tge EnCounter using fitbit's data streams
19:32:50 <int-e> I find the idea of "chucking some amount of attention to the details" quite eery.
19:32:53 <cpressey> support for some sort of convoluted scarecrow, maybe
19:32:58 <fungot> int-e: not many resources in scheme48's vm are shared, other than miranda and unlambda?
19:33:18 <int-e> fungot: you got that right
19:33:18 <fungot> int-e: prefer html? if so, that's fine, i'm sure
19:33:36 <ais523> cpressey: now you have to paste your joke in HTML, for int-e
19:33:57 <int-e> fungot: I want plain text.
19:33:57 <fungot> int-e: even though i reported it. multiple times. :p they claim that not wanting a on the end
19:34:22 <int-e> I guess that means I'm being overruled. By a bot. *pouts*
19:35:07 <b_jonas> fungot, have you ever cut your finger when trying to wash up a kitchen knife and you held the blade to wash the handle?
19:35:07 <fungot> b_jonas: or get a stamp. like " hey, i'm using safari 3.1.1
19:35:32 <b_jonas> fungot: on what operating system?
19:35:32 <fungot> b_jonas: i don't see where it transforms non-tail calls into tail calls if possible. don't force awkward programs on yourself to do some ffi stuff with it and need to be
19:37:06 <olsner> fungot: need to be what?
19:37:07 <fungot> olsner: ( letrec ( ( a ()
19:37:14 <int-e> fungot: shy gypsy slyly spryly tryst by my crypt
19:37:14 <fungot> olsner: with the blue squares on the cover of the book is solely based on scheme
19:37:14 <fungot> int-e: here's my article in english ( as in, a java system doesn't map nicely onto scheme.
19:41:00 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: thankx: not found
19:41:01 -!- cpressey has quit (Ping timeout: 252 seconds).
19:42:00 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: found: not found
19:42:51 -!- cpressey has joined.
19:42:59 <int-e> This might become worse than edirc.
19:43:29 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: thanks,: not found
19:43:57 <HackEgo> Thanks, Thursday. Thursday.
19:44:03 <ais523> haha, I was wondering what would happen if the argument was shorter than 2 chars
19:44:12 <HackEgo> Thanks, biblegia. Thiblegia.
19:44:31 <ais523> hmm, is it picking random `words?
19:44:35 <HackEgo> cary ency acet mare brodworf aam jaokson overe paliquitin marta sre oee ymblicl hical ric smarque fini alto fig nisti
19:45:00 <HackEgo> -rwxr-xr-x 1 5000 0 18 Jan 6 17:40 bin/`
19:48:42 -!- hjulle has quit (Ping timeout: 250 seconds).
20:00:29 -!- callforjudgement has joined.
20:01:09 -!- Patashu has joined.
20:02:45 -!- ais523 has quit (Ping timeout: 244 seconds).
20:02:46 -!- scarf has joined.
20:02:52 -!- callforjudgement has quit (Read error: Connection reset by peer).
20:07:44 <cpressey> consider a universal turing machine U; it reads a turing machine description T, and simulates it, but while it is simulating it it also searches for a proof that T does not terminate; U terminates if T terminates OR if U finds a proof.
20:08:30 <scarf> cpressey: we already have basically that on the wiki, I think
20:08:34 -!- scarf has changed nick to ais523.
20:08:50 <ais523> leading to a language which contains no provably nonterminating programs
20:08:55 -!- mihow has quit (Quit: mihow).
20:09:20 <ais523> but which is still probably TC despite that?
20:09:56 <cpressey> it's certainly TC, it just terminates "more often" than a naive UTM does
20:14:45 -!- cpressey has quit (Ping timeout: 252 seconds).
20:17:47 -!- MDude has quit (Ping timeout: 245 seconds).
20:17:58 -!- ais523 has changed nick to no.
20:18:01 -!- no has changed nick to ais523.
20:22:54 -!- cpressey has joined.
20:23:34 <cpressey> to make it strictly-dotted-i's-crossed-t's-TC, make it loop forever once it's found the proof
20:24:11 -!- Patashu has quit (Ping timeout: 264 seconds).
20:24:22 <cpressey> but if you're willing to accept "It doesn't terminate and here's why" as a substitute for not terminating, it's definitely close enough
20:24:39 <ais523> cpressey: ah, that's a slightly different idea from the language I'm thinking of
20:25:17 <cpressey> i don't know which one you're thinking of, but it did sound similar... only non-provably-non-terminating programs don't terminate
20:25:24 <ais523> cpressey: http://esolangs.org/wiki/Onoz
20:26:17 <cpressey> btw, it occurs to me that if we have flexibility in how turing machines are defined, we can't avoid flexibility in what counts as "turing-complete"
20:26:41 <ais523> "turing-complete" is a badly defined concept as-is
20:26:48 <ais523> there are some things that definitely fall on one side or the other of the line
20:26:52 <ais523> but there are also things that are much clsoer
20:28:03 <cpressey> well, "does the TM 'take input'" is one of the big obvious points of flexibility
20:28:39 <ais523> we have the phrase "bf-complete"
20:28:45 -!- FrogLeg has joined.
20:28:46 <cpressey> and yeah, onoz is... close... but not exactly what i was thinking... i think
20:29:00 <ais523> right, it doesn't match your description exactly
20:29:40 <cpressey> ok, so, brainfuck <-> turing machines with input and output tapes
20:31:24 <cpressey> well... ok... maybe not; what i was thinking of was unary. i think that just affects complexity, not computability
20:31:37 <cpressey> but wow does it ever affect complexity, ftr
20:31:53 -!- ais523 has quit.
20:32:07 -!- ais523 has joined.
20:33:38 -!- ais523 has quit (Read error: Connection reset by peer).
20:33:47 -!- ais523 has joined.
20:36:58 <cpressey> anyway, now that i have the construction, all i need to do is... find the proof it's used in
20:38:59 -!- FrogLeg has quit (Excess Flood).
20:39:23 -!- FrogLeg has joined.
20:39:56 -!- nycs has joined.
20:41:52 -!- `^_^v has quit (Ping timeout: 246 seconds).
20:42:02 -!- mihow has joined.
20:53:48 <cpressey> I do not understand this "GLooP" language. none of the wikis describe it (except to say it goes along with BLooP and FLooP.) the CLooP page seems to suggest it has an infinite parallel operation.
20:54:58 -!- FrogLeg has set topic: This Topic is now Hot. B===D~ B===D~ B===D~ B===D~ B===D~.
20:56:56 <cpressey> specifically, I don't see what the conditions for CLooP's infinite parallel "join" are. do all the (infinite number of) "threads" have to terminate?
20:57:03 <ais523> cpressey: GLooP was defined by Douglas Hofstader as "more powerful than FLooP, but computable"
20:57:09 <cpressey> if not, how many threads have to terminate?
20:57:13 <ais523> he concluded it didn't exist
20:57:35 <cpressey> if it's "all threads", the CLooP implementation of http://esolangs.org/wiki/Brainhype will... just not work
20:57:45 -!- ais523 has quit (Read error: Connection reset by peer).
20:58:04 -!- ais523 has joined.
20:58:48 <ais523> can someone put the topic back to something containing the log URLs?
20:58:53 <ais523> I tried to but my client crashed
20:59:14 -!- cpressey has set topic: RIP Misao Okawa | I'm a fungot trapped in a channel full of weirdos | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/.
20:59:15 -!- FrogLeg has set topic: http://meatspin.com/.
20:59:19 <ais523> also, FrogLeg, Freenode has a rule about being open about logging in channels
20:59:22 -!- cpressey has set topic: RIP Misao Okawa | I'm a fungot trapped in a channel full of weirdos | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/.
20:59:24 -!- ChanServ has set channel mode: +o ais523.
20:59:31 -!- ais523 has set channel mode: +b FrogLeg!*@*.
20:59:32 -!- ais523 has kicked FrogLeg trolling.
20:59:34 -!- shikhin has quit (Ping timeout: 265 seconds).
20:59:38 -!- ais523 has set channel mode: -o ais523.
20:59:57 -!- cpressey has set topic: RIP Misao Okawa | I'm a fungot trapped in a channel full of weirdos | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/.
20:59:59 <ais523> benefit of the doubt with one relatively harmless topic change
21:00:13 <ais523> no benefit of the doubt with shock site links
21:01:30 <cpressey> ais523: so DH *defined* GLooP to be "more powerful" without actually, uh, constructively defining how it was intended to go about that?
21:01:44 <cpressey> that would explain absence of descriptions of it
21:02:34 <ais523> cpressey: I think he intended it to not exist
21:02:41 <ais523> and brought it up as a teaser
21:04:03 -!- shikhin has joined.
21:04:09 <cpressey> i posit that CLooP's "GLooP mode" does not actually add any more power to the language, and specifically, it can't be used to implement Brainhype, and i guess i'll edit the page at some point if i feel like putting in the effort, ugh
21:04:21 <Taneb> It has been a while since I have read GEB
21:04:28 <int-e> cpressey: that non-termination proving TM is interesting, but it still runs afoul of diagonalization. (let U(x,y) be a TM that terminates with 1 if the TM x accepts y, and with 0 if it could prove that x(y) does not terminate. Then consider M(x) that first executes U(x,x), terminates if it halts with 0, and loops forever if it halts with 1. Then U(M,M) will not terminate, assuming that th...
21:04:34 <int-e> ...e formal system used by U for proving nontermination is sound.
21:05:05 <int-e> I guess you have the escape hatch that soundness of that system is not provable
21:05:55 <int-e> But in that sense we cannot hope to prove anything of interest (so, at least as strong as Peano arithmetic) at all.
21:09:00 -!- cpressey has quit (Ping timeout: 272 seconds).
21:09:54 -!- cpressey has joined.
21:12:04 -!- oerjan has joined.
21:12:41 <cpressey> int-e: I'm not sure what you're getting at
21:13:23 <cpressey> As I said, if T doesn't terminate, and there if no proof of this fact, U doesn't terminate
21:13:23 -!- ProofTechnique has quit (Ping timeout: 250 seconds).
21:13:47 <int-e> cpressey: "only non-provably-non-terminating programs don't terminate" <-- the notion of nonprovability also exists on a meta level.
21:14:50 <cpressey> I have no idea what you mean by "a meta level", sorry.
21:15:01 <cpressey> My wording there may've been sloppy
21:15:05 -!- augur_ has quit (Ping timeout: 244 seconds).
21:15:29 <int-e> It's the same kind of reasoning that says that Gödel's sentence is false in the standard model of Peano arithmetic, provided that Peano arithmetic is consistent.
21:15:40 <cpressey> The only T's for which U doesn't terminate are those for which U cannot find a proof (of T's non-termination)
21:17:00 <cpressey> I'm still not sure what you're getting at, and I'm getting the impression you think I think U is more powerful than it actually is...?
21:17:45 <int-e> No. The whole point here is that I can reason about programs in ways that U can't.
21:18:32 <cpressey> int-e: that would seem to be a dreadfully strong claim w.r.t. the computationalist theory of mind...
21:18:44 <int-e> That's what I did, I described a program that will not terminate (under consistency assumptions), but that U cannot prove nonterminating.
21:19:09 <cpressey> and for that program, U doesn't terminate -- as per my definition -- and...?
21:19:25 <HackEgo> [wiki] [[Hexadecimal Stacking Pseudo-Assembly Language]] N http://esolangs.org/w/index.php?oldid=42255 * SuperJedi224 * (+960) Created page with "The '''Hexadecimal Stacking Pseudo-Assembly Language''' (HSPAL) is a programming language by [[User:SuperJedi224|SuperJedi224]] in which a program is represented by a list of ..."
21:20:03 <int-e> cpressey: But we can prove that it doesn't terminate, whereas U can't. (Honestly, it's the consistency assumption that will bite me in the end.)
21:20:15 <HackEgo> [wiki] [[Hexadecimal Stacking Pseudo-Assembly Language]] http://esolangs.org/w/index.php?diff=42256&oldid=42255 * SuperJedi224 * (+11)
21:21:27 <HackEgo> [wiki] [[Mmmm()]] http://esolangs.org/w/index.php?diff=42257&oldid=42235 * SuperJedi224 * (+18)
21:21:51 <HackEgo> [wiki] [[Hexadecimal Stacking Pseudo-Assembly Language]] http://esolangs.org/w/index.php?diff=42258&oldid=42256 * SuperJedi224 * (+45)
21:22:51 <HackEgo> [wiki] [[Turing Script]] http://esolangs.org/w/index.php?diff=42259&oldid=42141 * SuperJedi224 * (+18)
21:23:23 <HackEgo> [wiki] [[GridScript]] http://esolangs.org/w/index.php?diff=42260&oldid=41337 * SuperJedi224 * (+16)
21:23:34 <int-e> cpressey: And no, it doesn't contradict the computationalist theory of mind either. We can implement that reasoning in a Turing machine, but it will be a different one from U.
21:23:47 -!- AnotherTest has joined.
21:23:57 -!- cpressey has quit (Ping timeout: 256 seconds).
21:24:18 <coppro> int-e: it's not necessarily meta-logic
21:24:45 <coppro> you can just throw in more axioms to any logical system
21:25:05 <coppro> since any TM will only include finitely many axioms encoded, you can always make a "stronger" termination-checker TM
21:25:36 <HackEgo> [wiki] [[HSPAL]] N http://esolangs.org/w/index.php?oldid=42261 * SuperJedi224 * (+59) Redirected page to [[Hexadecimal Stacking Pseudo-Assembly Language]]
21:25:58 <HackEgo> [wiki] [[Language list]] http://esolangs.org/w/index.php?diff=42262&oldid=42254 * SuperJedi224 * (+12) /* H */
21:26:59 <HackEgo> [wiki] [[Hexadecimal Stacking Pseudo-Assembly Language]] http://esolangs.org/w/index.php?diff=42264&oldid=42258 * SuperJedi224 * (+0)
21:27:45 <HackEgo> [wiki] [[Hexadecimal Stacking Pseudo-Assembly Language]] http://esolangs.org/w/index.php?diff=42265&oldid=42264 * SuperJedi224 * (+6)
21:30:07 -!- cpressey_ has joined.
21:30:52 <cpressey_> <int-e> cpressey: But we can prove that it doesn't terminate, whereas U can't. <-- yes, U just tries forever, and fails to find a proof, consistent with its definition
21:31:51 <cpressey_> other than thinking you've misread my definition, I can't see what the problem is here.
21:32:20 <cpressey_> what about U makes it incapable of taking any proof strategy that an arbitrary TM could take?
21:32:34 <cpressey_> I honestly can't see anything stopping it from that
21:33:17 <int-e> Ultimately it's because soundness of formal systems is so elusive.
21:33:33 <cpressey_> U is no more sound than any other UTM
21:33:55 <cpressey_> it just terminates on some T's that a naive UTM wouldn't terminate on
21:34:13 <cpressey_> apologies if I was giving some other impression. I didn't think I was.
21:34:59 <ais523> <cpressey_> <-- yes, U just tries forever, and fails to find a proof, consistent with its definition ← that was the basic idea behind onoz too
21:35:01 <int-e> Look, all I did was take your innocent use of "provable" and apply it to a formal system that is not embedded in U.
21:35:21 <cpressey_> sorry, should've said "provable by Turing machine", I guess
21:35:54 <cpressey_> ais523: yes, onoz is basically this with a few small twists (it checks inside loops only, for example)
21:36:00 <int-e> (Though it could be embedded in a different Turing machine, U')
21:38:48 <cpressey_> BT certainly isn't helping, tonight
21:39:02 <int-e> Sorry, but then you're missing the point of Gödel's incompleteness.
21:39:57 <cpressey_> Can you phrase it in terms of the Halting Problem, instead of Goedel's incompleteness?
21:40:21 <oerjan> there's no concept of "provable by Turing machine" without saying _which_ Turing machine.
21:40:22 <int-e> U will either have embedded an inconsistent nontermination prover (and thus there will be Turing machines that actually halt, but that U will declare as non-terminating) or one can *construct* a non-terminating program from U that U cannot show non-terminating, because non-provability rests on a consistency assumption, and consistency of the systems can't be proved inside the system.
21:41:21 <int-e> cpressey_: I did that already above:
21:41:24 <int-e> Let U(x,y) be a TM that terminates with 1 if the TM x accepts y, and with 0 if it could prove that x(y) does not terminate. Then consider M(x) that first executes U(x,x), terminates if it halts with 0, and loops forever if it halts with 1. Then U(M,M) will not terminate, assuming that the formal system used by U for proving nontermination is sound.
21:42:44 <int-e> cpressey_: Note that this implies that M(M) does not terminate, but U cannot prove that fact.
21:44:04 <cpressey_> "one can *construct* a non-terminating program from U" -- let's call this Y
21:44:32 <cpressey_> at 22:43 I said "OK -- give me a second" but BT is just awful tonight
21:44:58 -!- ProofTechnique has joined.
21:45:46 <lambdabot> Local time for cpressey_ is Wed Apr 1 22:47:42 2015
21:46:22 -!- ^v^v has quit (Read error: Connection reset by peer).
21:46:29 <oerjan> cpressey_: you're not that lagged accordingly to lambdabot
21:46:44 -!- ^v^v has joined.
21:47:16 <int-e> 23:47:44 <oerjan> @time cpressey_ ==> <lambdabot> Local time for cpressey_ is Wed Apr 1 22:47:42 2015 <-- time travel, but maybe *I*'m lagging...
21:47:36 <oerjan> ok _now_ it is lagging.
21:47:44 <lambdabot> Local time for oerjan is Wed Apr 1 23:49:44 2015
21:47:47 -!- boily has joined.
21:48:12 <oerjan> CTCP PING reply from int-e: 0.855 seconds
21:48:20 -!- cpressey_ has quit (Read error: Connection reset by peer).
21:49:01 -!- cpressey has joined.
21:49:19 <cpressey> int-e: let's assume uses ZFC for its proof system. we don't know it's consistent, of course
21:49:21 <int-e> FireFly: I'm sorry btw, I intended it to be an innocent remark, I didn't expect this to result in such a lengthy string of misunderstandings on various levels.
21:49:40 <cpressey> int-e: i'm also going to assume we both know what Y refers to
21:50:30 <oerjan> the "we don't know it's consistent, of course" rather ruins it, i think.
21:51:12 <cpressey> look, if ZFC's inconsistent we'll just find a ZFC' that we think is probably not inconsistent and carry on
21:51:36 <int-e> cpressey: Well, U either terminates because Y terminates, or it terminates because it has proven that Y doesn't terminate, or it runs forever.
21:51:43 <cpressey> so if you're going to say "ah but ZFC might be inconsistent" there's no bloody point
21:52:05 <cpressey> int-e: and that was not captured by my definition... how exactly?
21:52:32 <int-e> cpressey: but in the first case Y cannot terminate. and in the second case Y actually terminates (so either the system is inconsistent or this cannot happen).
21:53:06 <int-e> I refined your definition: "Let U(x,y) be a TM that terminates with 1 if the TM x accepts y, and with 0 if it could prove that x(y) does not terminate."
21:54:04 <int-e> (I also spearated the Turing machine from its input because it's technically more convenient. This is not essential.)
21:54:31 <cpressey> why would U prove that Y doesn't terminate (the second case, as you called it) if Y does in fact terminate?
21:55:42 <int-e> cpressey: because the formal system used for proving non-termination might be inconsistent; classically that means it can prove anything at all; I expect that intuitionistically it's almost as bad (but I'd have to think about this a bit more)
21:56:13 -!- MDude has joined.
21:56:26 <cpressey> ok, I am, for practical purposes, assuming it's using ZFC and assuming that ZFC is consistent. so the second case cannot happen.
21:56:42 <int-e> Right. Then only the third case remains.
21:57:07 <int-e> I.e., Y doesn't terminate and U(M,M) cannot prove this.
21:57:17 <cpressey> I still fail to see the problem. Unless the problem is "Oh noes, ZFC might not be consistent."
21:57:18 <int-e> (In its internal non-termination prover.)
21:58:58 <int-e> There is no problem, just a strange tangle that is not quite a loop: We have a program that we know (provably, assuming consistency; this is and will always be the weak point) doesn't terminate, but the formal system embedded in U is too weak to show that.
22:01:53 <cpressey> I mean, I might be a brain in a vat, too. I don't usually worry about such things.
22:07:20 -!- AnotherTest has quit (Remote host closed the connection).
22:09:20 <cpressey> int-e: are you *sure* you can't rephrase your point in terms of the HP? because I would find that a lot easier to understand.
22:10:57 -!- nycs has quit (Quit: This computer has gone to sleep).
22:12:42 <oerjan> > flip showsTypeRep "" $ typeRep (Proxy :: Proxy ())
22:13:00 <oerjan> > flip showsTypeRep "" $ typeRep (Proxy :: Proxy (Proxy ()))
22:13:07 <cpressey> http://www.scottaaronson.com/blog/?p=710 seems to strongly suggest this sort of thing can all be done with TM's. i've only skimmed it so far though.
22:14:01 -!- shikhin has quit (Quit: leaving).
22:14:03 <int-e> No, I think I need diagonalization, i.e. the proof method used for showing that the halting problem is undecidable.
22:14:53 <int-e> In any case I generally find the former easier than trying to shoe-horn proofs to only use the latter.
22:15:20 <lambdabot> Local time for tswett is Wed Apr 1 22:17:21 2015
22:15:35 <tswett> [18:17:21] <lambdabot> Local time for tswett is Wed Apr 1 22:17:21 2015
22:15:56 <int-e> nice, your client replies in UTC :)
22:15:58 <tswett> Apparently my IRC client disagrees with itself as to the time.
22:16:32 <lambdabot> Local time for djanatyn is Wed, 01 Apr 2015 15:18:33 -0700
22:16:33 * int-e needs a script to hook into the ctcp time replies.
22:17:18 <tswett> So, you know lenses in functional programming?
22:17:24 <tswett> Those can be interpreted in any category, right?
22:17:56 <tswett> Well, any category with... binary products?
22:18:13 <tswett> Has anyone actually studied those?
22:19:01 <ais523> tswett: are you thinking of products or tensors?
22:19:25 <tswett> Just plain ol' categorical products, I'm pretty sure.
22:19:38 <tswett> A lens consists of arrows A -> B and (A * B) -> A such that blah blah blah.
22:20:53 <shachaf> Lenses can be lots of things.
22:20:55 <oerjan> edwardk: i think the above question is for you ^
22:21:21 <shachaf> But type-changing lenses are much nicer than the other kind.
22:21:34 <shachaf> And type-changing is really some sort of naturality.
22:21:49 <shachaf> Anyway this has been discussed in #haskell-lens
22:23:08 <HackEgo> 895) <shachaf> Taneb: STOP TRYING TO GET LENS INTO EVERYTHING <shachaf> Bike: You should use lens! <Taneb> NEVER <Bike> shachaf: i'm getting mixed messages here \ 984) <shachaf> Bike: I think you're ready to learn about lens. <Bike> oh god <Bike> fiora help somebody help <Bike> anybody \ 1186) <oerjan> in that thread Taneb admits to his sins
22:25:57 <tswett> Arrows g : A -> B and s : (A * B) -> A such that g . s : (A * B) -> B is the right projection, s . (A * g) . (\x -> (x,x)) : A -> A is the identity, and s . (s * B) . (\(x,y) -> (x,y,y)) : (A * B) -> A is s.
22:26:18 -!- cpressey has quit (Quit: leaving).
22:30:54 -!- ProofTechnique has quit (Ping timeout: 264 seconds).
22:35:56 <boily> @ask Bike where are you?
22:38:01 -!- Koen_ has quit (Quit: The struct held his beloved integer in his strong, protecting arms, his eyes like sapphire orbs staring into her own. "W-will you... Will you union me?").
22:41:13 -!- trout has quit (Ping timeout: 246 seconds).
22:43:04 -!- augur has joined.
22:59:19 <HackEgo> [wiki] [[User:Vriskanon]] M http://esolangs.org/w/index.php?diff=42266&oldid=42224 * Vriskanon * (+0) /* Vriskanon */ Typo
23:21:30 -!- oren has joined.
23:25:20 <oren> today my only achievement was eating 500g of bacon
23:27:18 <oren> i wonder how many calores that is.
23:35:33 -!- ProofTechnique has joined.
23:36:53 <boily> helloren. baconinging?
23:36:59 <boily> (bacon binge. baconinge.)
23:37:43 -!- Decim has joined.
23:38:04 -!- vodkode_ has joined.
23:38:58 -!- Lymee has joined.
23:40:39 <boily> Good evening, shachaf.
23:42:04 -!- Lymia has quit (Ping timeout: 256 seconds).
23:55:49 -!- Lymia has joined.
23:56:57 -!- Lymee has quit (Ping timeout: 265 seconds).
23:58:50 -!- Lymia has quit (Remote host closed the connection).
23:59:35 -!- Lymia has joined.