00:09:23 <oren> Also you can get slate and chalk, but you can't make chalkboards!!
00:20:12 -!- tru23 has joined.
00:20:59 -!- tru23 has quit (Client Quit).
00:26:04 -!- Phantom__Hoover has joined.
00:26:47 -!- Phantom_Hoover has quit (Ping timeout: 264 seconds).
00:28:11 -!- adu has quit (Quit: adu).
00:31:41 -!- PinealGlandOptic has quit (Quit: leaving).
00:35:09 -!- mihow has quit (Quit: mihow).
00:47:44 -!- oerjan has joined.
00:59:56 <zzo38> Then you should tell them to fix it so that it is possible to make chalkboards
01:04:16 <zzo38> The specification for a Hamster archive format can fit on the back of your business card.
01:17:52 -!- Phantom__Hoover has quit (Ping timeout: 240 seconds).
01:24:56 -!- not^v has joined.
01:54:25 -!- ProofTechnique has joined.
02:06:05 -!- not^v has quit (Ping timeout: 250 seconds).
02:16:44 -!- adu has joined.
02:40:35 -!- hjulle has joined.
02:52:27 <oerjan> @tell int-e <int-e> Ah, the CHICKEN! have a history of Poulet! which appeared out of nowhere on 2012-08-08. <-- there are stray poulets even up to last october! also he took a _long_ time to get regular.
03:05:26 -!- Koen_ has quit (Quit: Koen_).
03:23:13 -!- ProofTechnique has quit (Ping timeout: 250 seconds).
03:56:02 -!- Lymia has quit (Remote host closed the connection).
03:56:36 -!- Lymia has joined.
03:58:16 -!- merdach has quit (Quit: WeeChat 1.0.1).
04:26:02 -!- Lymia has quit (Remote host closed the connection).
04:26:36 -!- Lymia has joined.
04:29:13 -!- GeekDude has quit (Quit: ZNC - http://znc.in).
04:45:19 -!- ProofTechnique has joined.
04:54:13 -!- Lymia has quit (Ping timeout: 250 seconds).
04:54:45 -!- Lymia has joined.
04:56:02 -!- MDude has changed nick to MDream.
05:09:52 -!- Lymia has quit (Remote host closed the connection).
05:10:17 -!- Lymia has joined.
06:02:26 -!- Lymia has quit (Remote host closed the connection).
06:04:21 -!- Lymia has joined.
06:31:48 -!- adu has quit (Quit: adu).
06:42:46 -!- merdach has joined.
06:46:31 <b_jonas> zzo38: there's an easy solution for constructing a Babson task like you asked
06:46:57 <zzo38> What is it then? I didn't try to figure it out much so I don't know
06:47:43 <b_jonas> The key is to use one of the dozens of cards that use "with the same name" in their rules.
06:49:57 <b_jonas> You have 6 life, opponent has 20. Opponent has Arcane Laboratory and Asceticism and Bedlam in play, you have a Squire. None of you have lands, but there's some suspended Lotus Blooms so that opponent gets 6 mana in his turn, then you get 6 mana in your turn, then you get 6 mana in your turn after that. It's the start of the opponent's turn.
06:50:18 <b_jonas> Both of you have some mathcing 1/1 creatures that are vanilla or have no relevant abilities (flying or first strike are ok), and you also have an Echoing Decay.
06:50:42 <b_jonas> Opponent may play a creature, and the only way you can win is by playing the same creature then playing Echoing Decay on your own creature next turn, then beat him with the Squire.
06:52:41 <b_jonas> This already allows tens of creatures (you may need Spellbooks to set it up), and can be extended to much more if you increase the life total of the opponent and replace Echoing Decay with Bile Blight so you can use creatures of size up to 3/3.
06:53:52 <zzo38> OK, although I was thinking of stuff that doesn't say "with the same name"; I have thought of a few other examples but not the way to combine them.
06:53:55 <ais523> construct something complicated involving a bounce-to-top-of-library card and Search the City
06:54:04 <ais523> just so that Search the City gets some use ;-)
06:54:25 <ais523> when I first saw it, I thought it'd be an interesting card at U
06:55:18 <b_jonas> zzo38: I'd still like to see a construction that doesn't use "same name", but instead relies on creature cards with different power-toughness.
06:55:27 <b_jonas> I think it's possible, but I haven't found one.
06:55:56 <zzo38> Something I thought of for example is Dark Depths and Aether Snap.
06:56:13 <b_jonas> I'd like to note though that there's lot more cards with "same name" then I thought, and I think half a dozen can be used for this construction
06:56:56 <b_jonas> (as in, they may need extra cards for the set up, but the basic idea is the same)
06:57:12 <b_jonas> besides Echoing Decay and Bile Blight, Detention Sphere also works,
06:58:03 <b_jonas> ais523: hmm, that might work
06:58:28 <b_jonas> Sever the Bloodline also works
06:59:01 <b_jonas> I think there are two cards that destroy enchantments with the same name, those can probably be made to work
06:59:09 <ais523> b_jonas: for power/toughness total, there's brainstorm + wild pair + whatever that card is that steals all creature spells when they're cast
07:01:06 <b_jonas> um, I don't really understand
07:03:16 <ais523> you don't even need brainstorm if the matching card is allowed to start in your library rather than your hand, that was just to put a card in hand back into your library
07:04:04 <b_jonas> I think it might be possible to set up something where it's the actual combat that matters, something with 4/1, 2/3, 0/5 creature cards, switching P/T of your creature, blocking, and making sure you get ahead in combat if you play the exact same creature.
07:04:12 <b_jonas> I'll have to think about whether there's such a construction.
07:14:53 -!- arjanb has quit (Quit: bbl).
07:21:06 -!- fractal has quit (Ping timeout: 265 seconds).
07:23:43 <b_jonas> also, some of what I said and more of what I thought about FFT yesterday was wrong
07:24:01 <b_jonas> I'll have to think more about that stuff
07:29:24 -!- fractal has joined.
07:41:09 -!- Patashu has joined.
07:58:12 <zzo38> The other one might be Airdrop Condor and Artificial Evolution.
07:59:24 <b_jonas> zzo38: hmm... something like that could work
07:59:53 <b_jonas> but then I don't see how you make sure I can't just play a higher power creature
08:01:52 <zzo38> Perhaps there isn't a higher power creatures
08:02:13 <b_jonas> but you have to make a Babson task with multiple creatures to choose from
08:02:41 <zzo38> I mean multiple cards to play; each one may be a different kind of effect
08:02:43 <b_jonas> that's why I want combat, so if you choose a creature with too low power, it can't kill the opponent's creature, but if you choose one with too low toughness, yours doesn't survive
08:05:21 <zzo38> Note also that Artificial Evolution says "The new creature type can't be Wall"; if it didn't say that then you couldn't stop them from activating Airdrop Condor before you are able to change it back, I think?
08:06:08 -!- ais523 has quit (Ping timeout: 252 seconds).
08:07:45 <zzo38> Maybe they want to change "Goblin" into "Dragon" but if you target the other Artificial Evolution to change "Wall" into "Dragon" then they can't. But otherwise once one spell resolves they can activate it before your spell resolves, because that is the cost of the activated ability
08:07:46 <b_jonas> Would it be very inelegant if I used multiple instants previously suspended with Delay?
08:08:53 <b_jonas> Hmm wait, you might not need that...
08:09:01 <zzo38> I don't really know
08:10:07 <b_jonas> Is there something like Otherworldly Journey that works on auras? I know you could use Otherworldly Journey too, but it would require heavy machinery, worse than Delay.
08:12:46 <b_jonas> hmm no, it'd be ugly to make those act through turns
08:14:33 <b_jonas> then Delay might be the easiest
08:20:50 -!- ais523 has joined.
08:21:42 <b_jonas> Is there an easy way to give someone only _one_ colored mana (and possibly multiple colorless mana) in a particular turn, the way Lotus Bloom gives three colored mana?
08:22:04 <b_jonas> Because that could let you get rid of Arcane Laboratory.
08:23:09 <b_jonas> You could give one mana the next turn, that's easier, but how do you give one mana the turn after that?
08:25:46 <b_jonas> Though for this simple construction with Echoing Decay, it's enough to give one colored mana next turn so you can only play one creature, and three colored mana with Lotus Blood the turn after that and make sure there's no black creatures so you're forced to play only Bile Blight
08:28:34 <b_jonas> I'll try to think of a combat-based solution.
08:31:57 <b_jonas> what if you just have much fewer life than your opponent, and multiple creatures, each of which is the only one that can block the same type of creature: a creature with flying, black creature with fear, a creature with shadow, a creature with horsemanship, and a red creature with intimidate?
08:32:16 <b_jonas> plus make sure you can cast only one creature, and you're done
08:32:20 <b_jonas> no need for any fancy p/t magic
08:32:34 <b_jonas> oh, and you'll need an extra vanilla creature
08:33:13 <b_jonas> plus maybe some toughness increasing effects to make sure your blocker survives
08:36:03 <b_jonas> that's not scalable to more than five to ten creatures, but still
08:42:45 <b_jonas> (I'll have to think whether that evasion-based method can be combined with a P/T-based method)
08:44:11 <zzo38> That is one idea too, yes
08:44:41 <zzo38> But, it is possible that your blocker might not need to survive
08:46:50 <b_jonas> zzo38: yes, it needn't survive actually
08:47:07 <b_jonas> zzo38: if you have 1 life, then you die next turn if you don't block
08:47:42 <b_jonas> and suppose you have a large creature that doesn't untap next turn, so you win your second next turn otherwise
08:48:00 <b_jonas> but making your blocker survive is easy enough
08:48:19 <b_jonas> you just need ten Veteran Armorers with Pacifism
08:49:48 <b_jonas> is there an instant that adds just _one_ mana to your mana pool?
08:50:36 <b_jonas> oh, there is, suspended Divergent Growth works if you have ten Reliquary Towers
08:51:07 <b_jonas> then you don't need Arcane Laboratory
08:51:37 <b_jonas> (or Rule of Law or Eidolon of Rhetoric)
08:53:44 <b_jonas> though if there are really three of these cards, all uncommon in accessible sets, then I might not need to avoid it
08:54:40 <b_jonas> there's also Curse of Exhaustion
08:59:50 <zzo38> Or you can win in another way, such as opponent has no card to draw
09:21:32 -!- FreeFull has quit (Ping timeout: 245 seconds).
09:24:51 -!- cpressey has joined.
09:25:28 <cpressey> "produce byte #n in O(1) time" <-> "compile the whole thing in O(n) time"
09:25:42 <cpressey> and it fails hard on C++, with its templates
09:26:08 <cpressey> (obviously, that's a bit out of scope for what you're interested in, but still)
09:26:59 <cpressey> oh -- also, I have no problem per se with "prepared tapes" or infinite CA playfields -- the problem I have is with comparing apples to oranges
09:27:59 <cpressey> the only way I see to fairly compare them is to convert the one to the other
09:29:52 <cpressey> as for "total"... most of my confusion has abated
09:30:34 <cpressey> I do not contest that Woulter Swierstra has written a total function which takes Brainfuck programs to possibly-infinite execution traces
09:30:56 <cpressey> I do not contest that Brainfuck is Turing-complete
09:31:14 <cpressey> (the turing-complete version of brainfuck, that is :))
09:32:31 <cpressey> I might not even contest calling Wouter's function "Turing-complete", but that term is sort of a rubbish bin at this point anyway
09:33:19 <cpressey> I'll try to give an example that illustrates my remaining reservations/nonplussedness
09:34:00 -!- jetpack333 has joined.
09:34:10 <cpressey> Person A writes a function which takes brainfuck programs to possibly-infinite execution traces, represented as lazy lists (a finite list + a continuation)
09:34:14 -!- jetpack333 has left.
09:34:38 <cpressey> Person B writes a function which takes brainfuck programs to possibly-infinite execution traces, represented as brainfuck programs
09:34:50 <cpressey> also known as, er, the identity function.
09:36:08 <cpressey> elliott or int-e or anyone else ^^^
09:37:25 <ais523> what's the non-Turing-complete version of brainfuck?
09:37:35 <ais523> (I assume you aren't referring to one of the many awful BF derivatives)
09:38:00 <oerjan> 30 Kb should be enough for everyone
09:38:11 <ais523> that's an awful BF derivative that predates BF
09:38:13 <cpressey> ais523: well, the version where you take the original implementation in C as god, and... yeah
09:38:27 <ais523> besides, writing off the end of an array is UB
09:38:35 <ais523> I can imagine a C implementation that reacts by extending the array
09:38:50 <ais523> also increasing the size of an int so that it can continue to index the array indefinitely
09:39:33 <ais523> actually I guess you have to increase the size of a char
09:39:40 <ais523> but then defining char_bit would be difficult
09:39:42 <cpressey> ais523: tantamount to throwing much of C out the window, but, ok
09:40:05 <ais523> the world needs more C impls that don't act anything like C
09:40:41 <cpressey> store the tape on a real tape and issue I/O commands by mapping a volatile variable to an I/O port
09:40:47 <cpressey> then you're only limited by the size of your tape reel
09:41:10 <ais523> or by using the stdio FILE * API
09:41:15 <ais523> that's even blessed by the standard
09:41:29 <ais523> and you can move around using relative seeks
09:41:50 <cpressey> ok, but I worry that it still might have some unfortunate verbiage in the spec that imposes a maximum somewhere
09:42:19 <ais523> I'm remembering from last time this subject came up
09:42:55 <cpressey> anyway, on that other note, it seems most "reasonable" languages do admit a "dumb" compiler to Turing-machines in O(n) time
09:43:04 <cpressey> dumb = non-optimizing, of course
09:43:19 <cpressey> maybe a little more than O(n) if you don't accept that hash tables are O(1)
09:43:40 * oerjan wonders if cpressey ever noticed his underload interpreter in emmental
09:44:09 <cpressey> oerjan: I must be going crazy, I swear I can hear your thoughts
09:44:12 <oerjan> dulla: both are esolangs
09:44:31 <oerjan> i made it around the time the wiki featured emmental
09:44:42 <dulla> So, I guess my hint is to look at all the concurrency esols
09:44:48 <ais523> dulla: http://esolangs.org/wiki/Underload
09:44:51 <ais523> if you haven't seen it, you should
09:44:54 <ais523> it's one of the Big Five
09:45:11 <int-e> cpressey: you can prefix an interpreter with a sequence of states that initialises the tape with the source code, which would be really stupid but O(n), no extras.
09:45:16 <ais523> (Befunge, Brainfuck, INTERCAL, Underload, Unlambda)
09:45:54 <oerjan> cpressey: http://oerjan.nvg.org/esoteric/emmental/ul.emm or slightly less evilly, the haskell generator http://oerjan.nvg.org/esoteric/emmental/EmmUnl.hs
09:47:31 <cpressey> "It uses Emmental's metacircular evaluation principles to _turn_ the Emmental interpreter into an Underload one" -- exactly the sort of thing I was hoping for
09:49:14 <ais523> oerjan: the Haskell generator uses lens
09:49:18 <ais523> and you're calling it less evil?
09:50:40 <oerjan> it was in fact the first haskell program where i used lens in earnest
09:50:50 <int-e> Hmm, is there a way to get Firefox use syntax highlighting if it sees Content-Type: text/x-haskell ?
09:51:08 <oerjan> ais523: it's less evil in so far as it is _plausible_ for humans to read
09:51:10 <ais523> it normally delegates to your editor, which will know how, IME
09:51:55 <int-e> (I have the "open in browser" plugin, so at least I can display the file in the browser rather than having to save it to disk)
09:51:58 <oerjan> fizzie: HackEgo didn't get back properly after Gregor restarted the server
09:52:06 <lambdabot> Taneb says: lens has got to be the only library with more contributors than people who know how it works
09:52:22 <ais523> oerjan: did you just call me "fizzie"? :-)
09:52:52 <ais523> also, aimake has more contributors than people who know how it works, but it's not technically a library
09:52:59 <int-e> ais523: he was alerting fizzie to a problem
09:55:04 <ais523> oerjan: technically you'd only need to impl (), : and ^ to prove fancy-L-completeness
09:56:26 <cpressey> if fancy-L is what I think it is, <3 this channel, doing all the computability dirty work that everyone else refuses to touch
09:56:55 <ais523> cpressey: it means "it's possible to write at least one interpreter for a TC language in this program"
09:57:16 <ais523> which may have been your definition?
09:57:37 <oerjan> ais523: i am addressing fizzie as the person most likely to be able to fix it, although he seems frightfully evil
09:57:51 <ais523> he can't be worse than lens, surely
09:58:00 <oerjan> worst brain typo this year so far, i think
09:59:38 <lambdabot> https://dibels.uoregon.edu/market/assessment/idel
10:01:05 <oerjan> <ais523> oerjan: technically you'd only need to impl (), : and ^ to prove fancy-L-completeness <-- it was of course more fun to try to cram (almost) everything in
10:01:18 <ais523> does the ():^ TCness proof use nested parens?
10:01:30 <ais523> if not, minimal-Underload might actually work quite well as a source language for TCness proofs
10:01:32 <zzo38> The other way to open the text file in the browser is if you write "view-source:" before the URL; not all browsers will accept this though
10:02:00 <ais523> oh wow, I remember learning about that when I was in school and Geocities was really popular and I didn't know what CGI was yet
10:02:29 <zzo38> O, do you like to ask too many questions/complaints to me please?
10:02:51 <oerjan> ais523: definitely needs some nesting, although it should be limited by O(states*symbols) of a universal minsky machine
10:03:10 <int-e> (FWIW, on my own webservers I tend to hack mime.types to produce text/plain for .hs files.)
10:03:29 <ais523> how do you measure states and symbols for a minsky machine?
10:03:46 <oerjan> i guess only states then
10:05:02 <b_jonas> "(Befunge, Brainfuck, INTERCAL, Underload, Unlambda)" is the big five? I haven't heared of that yet, but it sounds reasonable.
10:05:17 <oerjan> ais523: also you only need to add ~ to get a TM instead
10:05:18 <ais523> b_jonas: it was sort-of informally agreed here a while ago
10:05:30 <zzo38> On my own computer I have put a .htaccess in /dnd/recording/ in order to make it set the MIME type of the TeX source files to text/plain too
10:05:43 <ais523> oerjan: ~ is one of the hardest commands to impl, although I guess it's not much harder than : and might even be a little easier
10:06:17 <b_jonas> ais523: ok, then I'll propose a category on the wiki
10:06:28 <cpressey> <ais523> so you would consider the 2,3 machine to be sub-TC, then <-- iirc, it's not capable of halting, so no, I don't consider it TC
10:06:35 <ais523> cpressey: my version, it is
10:06:39 <ais523> I use a right-infinite tape
10:06:44 <ais523> halting is falling off the left end
10:07:00 <int-e> Perhaps one could use 2^k as the number of symbols of a Minsky machine with k counters.
10:07:02 <ais523> however, I'm considering simpler tape initializations that have more complex halt states
10:07:15 <cpressey> ais523: beh, i almost want to count that as an extra symbol
10:07:29 <cpressey> at any rate, you can't fairly compare it to a bi-infinite tape
10:07:33 <ais523> cpressey: I have an explicit extra-symbol representation too
10:07:52 <cpressey> ais523: fine, but then it's 2,4 (or 3,3 -- i can't remember)
10:07:58 <ais523> however, the mathematicians who looked over this said that Turing Machines weren't well-defined enough that it mattered
10:08:15 <ais523> and in fact, different papers are inconsistent on whether the tape's infinite both ways or just one way
10:08:16 <cpressey> then the whole argument doesn't matter
10:08:27 <cpressey> all we can say is "Sure is small!" Hyuk
10:08:29 <ais523> this happens a lot during research
10:08:47 <b_jonas> cpressey: by the way, thanks for the article you have recommended
10:08:47 <ais523> I discovered that one of my papers refers to a proof in another paper
10:09:05 <ais523> but the two papers are using different definitions, in a way that probably matters
10:09:09 <b_jonas> Bernstein, Multidigit multiplication for mathematicians
10:09:15 <ais523> or at least, it's nontrivial to prove that it doesn't matter
10:09:33 <cpressey> b_jonas: interesting, I'm completely drawing a blank on that. you're sure it wasn't someone else?
10:09:45 <int-e> b_jonas: that was me; you're welcome.
10:10:37 <int-e> and don't worry, I'm happy not to be the only one who mixes up people :)
10:11:04 <oerjan> int-e: my :()^ gets awkward if you have more than 2 counters, anyway. (you'd need to move across the representation of a counter to get to the other side)
10:11:21 <ais523> but you never need more than 2 counters
10:12:36 <b_jonas> you never need more than 2 counters if you're satisifed with double-exponential slowdown
10:13:04 <oerjan> indeed, it might be worth it still then
10:13:16 <ais523> well, the 2,3 machine proof is double-exponential, I think
10:13:21 <ais523> I might have got it down to single-exponential
10:13:28 <cpressey> oerjan: I'm interested in this "System T" thing of Goedel's, which is apparently decidable but > PR. Know anything about it?
10:13:28 <b_jonas> hmm, if Game of Life was invented before Intercal, does that mean Intercal isn't really the first esolang?
10:13:29 <ais523> or it might have been triple-exponential originally
10:13:31 <oerjan> (of course, you still have exponential for using minsky)
10:13:32 <ais523> I don't even really remember
10:13:37 <ais523> b_jonas: INTERCAL wasn't the first esolang
10:13:44 <oerjan> cpressey: not that i recall
10:13:57 <ais523> b_jonas: http://esolangs.org/wiki/Prehistory_of_esoteric_programming_languages
10:14:09 <b_jonas> ais523: no, the _origianl_ 2,3 machine proof is something-exponential, but it's got a new proof that I think only has a polynomial slowdown
10:14:24 <b_jonas> it's plain counter machines where you can't avoid the slowdown
10:14:38 <ais523> b_jonas: really? I would be very surprised at that
10:14:44 <ais523> (a polynomial slowdown)
10:14:49 <ais523> based on the properties of that machine
10:14:56 <ais523> (you are aware that I wrote the original proof, right?)
10:15:11 <cpressey> oerjan: I'm a bit suspicious, mainly because if it really was, I'd think it would be more well-known, and maybe have a complexity class named after it, but. Never heard of it before yesterday.
10:15:21 <b_jonas> I'm mixing it up with another small machine
10:15:40 <cpressey> i don't know how i'm going to get anyway work done if i'm sitting on this channel :)
10:15:46 <ais523> rule 30's harder to prove but believed to be probably also TC
10:15:48 <b_jonas> one of those with 2 states and 3 neighbours on a line
10:16:13 <b_jonas> but those are distinct from the Turing machines
10:16:32 <b_jonas> anyway, for counter machines, you clearly can't get below at least single exponential
10:16:49 <ais523> the 2,3 construction is from sequential tag
10:16:53 <b_jonas> and I suspect that for a two-counter machine the double exponential is necessary
10:17:38 <oerjan> ais523: if you used tag, then the down-to-polynomial construction for rule 110 might apply to yours too, iirc it's simply about proving _tag_systems_ not to need exponential overhead
10:18:30 <oerjan> by a more clever representation of a turing tape
10:18:52 <b_jonas> but isn't it trivial that tag systems don't need exponential overhead if you can use enough symbols and rules?
10:19:18 <oerjan> b_jonas: maybe, but someone got a paper out of applying it to rule 110 anyhow
10:21:36 <ais523> oerjan: I used cyclic tag, which is proved TC by compiling from tag
10:27:06 -!- Phantom_Hoover has joined.
10:27:21 <oerjan> cpressey: assuming this is the same as https://en.wikipedia.org/wiki/Dialectica_interpretation#Induction i would _almost_ interpret that section as saying it is _not_ decidable.
10:28:15 <oerjan> and on quick browsing i don't see anything in the article that says it _is_.
10:34:10 <oerjan> b_jonas: i assume the thing you've heard of is http://www.citeulike.org/user/cook/article/8904389
10:36:17 <oerjan> b_jonas: ais523: http://www.bcri.ucc.ie/FILES/PUBS/BCRI_52.pdf
10:36:39 <oerjan> ais523: it also uses cyclic tag
10:36:43 <ais523> wow, "P-complete" is a weird phrase
10:37:12 <oerjan> yes, usually you then use LOGSPACE-reductions
10:37:29 <oerjan> or sometimes even lower stuff
10:38:12 <oerjan> as in, the part it changes is between the TM and the cyclic tag stuff, so it should apply to your case as well
10:39:12 <Taneb> This channel has given me a great intuition and informal knowledge for my computability module, but almost none of the formalities
10:40:24 <ais523> the trick is to know that the formalities aren't really as precise as mathematicians would want them to be
10:40:45 <b_jonas> Taneb: there's some nice books telling the formalities
10:41:18 <Taneb> b_jonas, I just received an almost completely irrelevant textbook!
10:42:22 <cpressey> oerjan: I'm going on some very vague statements in Turner's "total fp" paper, plus this: http://home.utah.edu/~nahaj/logic/structures/systems/t.html which says "There is a decision procedure for T"
10:42:51 <cpressey> "decision procedure" might not mean what I think/want it to mean, here
10:43:11 <b_jonas> oerjan: yes, that paper is what I've heared of, for it's linked from http://www.scottaaronson.com/blog/?p=2070
10:43:48 <oerjan> cpressey: ic. i think we're definitely over my head.
10:44:13 -!- MDream has quit (Ping timeout: 264 seconds).
10:44:43 <cpressey> oerjan: Turner's paper also referred to https://en.wikipedia.org/wiki/Primitive_recursive_functional which that wp article refers to.
10:45:10 <cpressey> i think, once you allow values to be infinite... oh, such fun.
10:47:41 <cpressey> oerjan: (scroll up to where I give an example with "Person A" and "Person B" earlier this morning)
10:48:14 <oerjan> i'm sure i read that but also that my brain is approaching breaking point right now.
10:49:16 -!- oerjan has quit (Quit: Later).
10:50:10 -!- bluckbot has quit (Quit: bluckbot).
10:52:03 -!- bluckbot has joined.
10:54:13 <cpressey> my stubborn refusal to let things make sense to me is increasing the cognitive burden of the channel
10:55:09 <ais523> I'd better not try to explain Feather then
11:01:41 -!- skarn has quit (Ping timeout: 250 seconds).
11:06:18 -!- skarn has joined.
11:15:15 -!- bluckbot has quit (Remote host closed the connection).
11:17:04 <fizzie> @tell oerjan Uh-oh, I think my esowiki SSH key is only on the laptop and the fungot server, both of which are currently in the house-with-no-internet.
11:17:30 <zzo38> Are you going to copy it onto a disk?
11:19:50 <fizzie> I should probably put it onto this VPS system I'm ircing on, then I could access it from wherever.
11:23:39 -!- FreeFull has joined.
11:27:01 -!- boily has joined.
11:36:36 -!- mbrcknl_ has joined.
11:43:43 -!- mbrcknl has quit (*.net *.split).
11:44:19 -!- mbrcknl_ has changed nick to mbrcknl.
11:46:12 -!- Lymia has quit (Remote host closed the connection).
11:46:47 -!- Lymia has joined.
11:48:30 -!- ais523 has quit.
11:51:57 -!- Lymia has quit (Ping timeout: 250 seconds).
11:53:21 -!- Lymia has joined.
11:55:24 <boily> how are you? have you esΓΆlanged recently? boardgaming?
11:56:22 <Taneb> I have been trying to figure out if I can implement Eodermdrome by piggybacking on the implementation of a research language one my lecturers made
11:58:15 <Taneb> However I don't really know either language
11:58:52 <boily> Ε_Ε... woooah...
11:59:31 <b_jonas> the problem with Eodermdrone is how you choose an arbitrary injective homomorphism if there are multiple possible ones.
12:01:33 <Taneb> Can I get someone cleverer than me to look at http://arxiv.org/abs/1204.5541 and figure this out?
12:04:35 <Phantom_Hoover> b_jonas, the same way as in any ambiguous rewriting language, you pick one arbitrarily
12:05:27 <b_jonas> Phantom_Hoover: sure, but that could make it hard to debug programs
12:05:52 <b_jonas> because then it's easily possible that your program works well in this implementation, but not in other implementations that pick other choices
12:06:10 <boily> is the choice part of a finite set?
12:06:12 <Taneb> I don't think that many esolangs make debugging particularly easy
12:07:22 <boily> then can you score the arbitrary performance of each possibility, and deterministically go with the best?
12:07:55 <boily> Taneb: there's befunge, where tracing the execution is at least as interesting as running the program itself.
12:08:19 <b_jonas> boily: um, by what measurement of performance?
12:08:57 <boily> b_jonas: some arbitrary measurement >_>'...
12:09:13 * boily mumbles mumbles something about optimisation problems
12:11:02 <Phantom_Hoover> b_jonas, if you write ambiguous substitutions then you'll end up with undefined behaviour, the solution is to make your substitutions unambiguous
12:17:50 -!- Tritonio has quit (Remote host closed the connection).
12:21:09 -!- Phantom_Hoover has quit (Ping timeout: 250 seconds).
12:22:48 -!- Tritonio has joined.
12:23:01 -!- boily has quit (Quit: SHAPED CHICKEN).
12:35:14 -!- Patashu has quit (Ping timeout: 245 seconds).
12:41:15 -!- MDude has joined.
12:44:22 -!- CADD has joined.
12:45:23 -!- SopaXorzTaker has joined.
12:50:45 -!- SopaXorzTaker has quit (Read error: Connection reset by peer).
12:50:45 -!- SopaXT has joined.
13:15:52 -!- ProofTechnique has quit (Ping timeout: 240 seconds).
13:22:54 <elliott> cpressey: I forget if the total FP paper covers the fact that ackermann is actually primitive recursive if you have higher-order functions
13:24:31 <Taneb> My AI textbook arrived today and I am using it as a mousemat
13:24:52 <elliott> in a sense the dependently typed languages get a lot of their expressivity from the fact that you can do "fancy" recursion by returning functions or types, and by allowing you to structurally recurse over any structure you want (rather than just naturals on zero and successor)
13:25:15 <elliott> without actually having a fundamentally more complicated criteria for what recursion is allowed
13:33:01 <cpressey> elliott: it does mention that. what the heck complexity class does that correspond to, though? ackermann isn't contained in PR afaik
13:33:27 <elliott> cpressey: well: "The primitive recursive functions are among the number-theoretic functions, which are functions from the natural numbers (nonnegative integers) {0, 1, 2, ...} to the natural numbers."
13:33:51 <elliott> the trick is just to relax that return type criteria. (it already can't exactly be true, anyway, since ackermann sort of has more than one argument...? there's probably some better definition in The Literature.)
13:34:03 <elliott> (well, either that or the input type has to change, of course.)
13:34:16 <elliott> I doubt it has a name; "higher-order primitive recursive" or something
13:34:31 <cpressey> i consider the nat thing kind of incidental... exanoke has lists, for example; doesn't seem to change much
13:34:37 <cpressey> all you need is some well-founded data
13:34:49 <elliott> yeah but it isn't because adding functions gives you more in some sense
13:34:56 <elliott> actually maybe you can do ack by going via some data-type?
13:35:14 <cpressey> well i know there are rewrite systems by which ack can be proved to terminate
13:35:27 <cpressey> i assume there's some way to draw a correspondence between those systems and types
13:36:01 <elliott> I think the main thing is that you can get a lot out by just being able to generate other kinds of inductive data through the induction principles, rather than just the same type
13:36:07 <elliott> and then recurse on those themselves
13:37:12 <elliott> I don't think I've ever seen a "reasonable" function you can't define in Coq or Agda directly due to termination checking (even if it's really awkward to define) that isn't "interpretation-y stuff" (which I expect to be that way).
13:37:13 <cpressey> til eodermdrome is an oilipoian thing. and that eodermdrome the esolang is a lot like thue, except on graphs, and it has a nicer approach to input imo
13:38:13 <b_jonas> cpressey: the fun part is that eodermdrone would actually be easy to program if you had an unlimited number of letters. the programs might not be efficient of course, but easy to write.
13:38:31 <cpressey> elliott: yes. in the "real" world, most people would consider NEXP too inefficient to be practical anyway. and PR >= NEXP. the problem is that some functions are awkward or inefficient when written in PR style
13:38:32 <b_jonas> but the way it is, it's not even turing complete, because there are only finitely many valid eodermdrone programs
13:38:48 <b_jonas> and the limitation that you have only 26 letters is very severe
13:39:13 <elliott> the "real" world of proving things :)
13:39:35 <cpressey> b_jonas: well that would let you make bigger graphs, but... you can chain smaller graph rewrites into a larger one. but yes i can see how that would be a pita
13:39:53 <elliott> but yeah, you can write things a lot nicer than the usual awkward mathematical primitive recursion in dependent type theory, but it can still get ugly.
13:40:35 <b_jonas> alternately, 26 nodes would be enough if we had more than one type of edge distinguished, possibly even directed
13:40:51 <b_jonas> say, with numbers written between the letters
13:41:12 <b_jonas> then it would be almost as easy to use as an ordinary pointer machine
13:41:12 <elliott> especially when you need to go to the level of well-founded recursion (basically defining your own "smaller than" relation and proving that you can recurse a data type in a way that always gets smaller -- this lets you do things like recurse on (x/2) on naturals, rather than just (x-1). you can define it all in type theory though, no need to extend its notion of recursion, it's just fun with induction pr
13:41:18 <cpressey> b_jonas: um... i think it's TC actually
13:41:18 <elliott> inciples and vaguely higher-order stuff)
13:41:38 <cpressey> b_jonas: you do realize the letters only describe how the graph is formed, right?
13:41:54 <b_jonas> cpressey: no it's not, because there's less than about 2**(2**(26**2)) valid programs (give or take a few
13:42:21 <elliott> now that's some practical limitation
13:42:32 <cpressey> b_jonas: that's not how i understood it, but i could be wrong. maybe ais523 can shed light on it
13:42:40 <elliott> my new esolang: brainfuck but you only get, like, G_64 tape cells
13:44:10 <Taneb> elliott, are the cells bounded at TREE(3)?
13:44:59 <cpressey> b_jonas: ok, i see what you're referring to -- I think this puts it in fancy-L territory -- you can't write arbitrary programs in it but you can write an interpreter for a TC language in it
13:46:20 <fizzie> Taneb: Is it the Russell & Norvig one, or something else?
13:46:33 <cpressey> there are 6906900 eodermdromes (the oulipo kind) if I'm not mistaken. which is cool, because that number looks a little like an eoderdrome itself (but it isn't.)
13:46:39 <Taneb> fizzie, yeah, Artificial Intelligence: A Modern Approach
13:47:19 <fizzie> (Okay, the third edition isn't all that old.)
13:47:28 <Taneb> And this is 4th Ed
13:48:07 <fizzie> People here keep numbering floors wrong.
13:48:16 <Taneb> Or rather, was thinking about the computation theory textbook I plan to order soon
13:48:21 <fizzie> (The whole ground floor / first floor thing.)
13:48:26 <Taneb> fizzie, are they forgetting that G is a natural number
13:48:50 <fizzie> Back in Finland we had 1 at street level, and so on.
13:49:25 <Taneb> Where are you now?
13:50:21 <fizzie> It hasn't been all that bad.
13:50:25 -!- ProofTechnique has joined.
13:53:53 <Taneb> Although if you do ever head further north, give me a bell
13:57:13 <fizzie> There was this talk (sometime last year) about meeting up in... Birmingham?
13:59:39 <Taneb> Birmingham is indeed further north than London
13:59:51 <Taneb> Although considerably further south than anywhere in the UK I've lived
14:00:22 -!- GeekDude has joined.
14:01:00 <Taneb> And yes, I think that was mentioned
14:01:05 <Taneb> Nothing was planned, though
14:03:47 <cpressey> Actually I think it's more like 34534500 because there are 5 possible starting positions
14:03:58 <cpressey> Meeting in Brum, what a bizarre yet intriguing idea
14:05:31 <cpressey> (no wait, there are also 5 possible rotations, they should be captured by the permutation right? i keep forgetting i don't like combinatorics)
14:06:34 <cpressey> elliott: the thing is, I *am* burned out, but can't retire yet
14:06:52 <cpressey> deciding to leave irc open during the day will be my downfall
14:07:40 -!- supay has quit (Ping timeout: 252 seconds).
14:07:48 <elliott> are you still doing, uh, web stuff
14:09:05 <cpressey> no wait, no, i am changing the world!!!1!
14:09:20 <cpressey> it will be a better place after our gamble succeeds
14:10:58 -!- bb010g has quit (Ping timeout: 252 seconds).
14:11:49 <oren> I am now at 6:32 mark of a ten hour video
14:14:24 <oren> http://snag.gy/Fd1Sh.jpg whoops, actually 11hours
14:18:22 <oren> I was thinking about explicit control of evaluation.
14:18:52 <oren> Suppose you have two separate syntax elements:
14:19:50 <oren> level 0 statements define, in a declarative style, the values to compute
14:20:41 <oren> level 1 statements would then in an imperative style, tell the program what order to reduce them in
14:20:46 <elliott> http://www.cs.bham.ac.uk/~pbl/cbpv.html
14:21:21 <elliott> but that's sort of what call-by-push-value is except not really.
14:21:28 <elliott> but it does the explicit evaluation control thing.
14:23:12 -!- supay has joined.
14:26:16 <oren> studentt distribution? what is this madness
14:30:25 <oren> Anyway, so what I am struggling to define is a good syntax for referring to a node in a evaluation tree.
14:32:49 <cpressey> I don't know what an evaluation tree is, but: 1.1.2.1
14:34:39 <oren> That could work. An evaluation tree would be a tree representing a set of values whihc depend on values in their children.
14:40:44 <oren> My idea is to isolate state changes to one level, and the entirety of math to zero level.
14:44:07 -!- bb010g has joined.
14:53:02 <cpressey> @tell shachaf I don't understand the question
14:57:11 -!- `^_^v has joined.
15:04:21 -!- Lymia has quit (Ping timeout: 250 seconds).
15:20:20 -!- Lymia has joined.
15:21:51 <fizzie> Taneb: I'll also be going to Oban at some point, but just for touristy things.
15:37:39 -!- CADD has quit (Remote host closed the connection).
15:40:59 <cpressey> elliott: btw, did you see my "Person A", "Person B" example from this morning. apparently it was too much for oerjan (who, in fairness, had just tried to tackle Goedel's System T)
15:42:19 -!- vanila has joined.
15:43:44 -!- CADD has joined.
15:44:23 <elliott> was it the brainfuck thing
15:44:41 <elliott> my brain filed it under the same category as "here's my self-interpreter: eval" and "my /bin/cat quine"
15:47:31 <cpressey> elliott: yes it was probably that thing, it was "here is a total function which maps any program to its infinite execution trace; its infinite execution trace is represented as a finite object like a lazy list; this finite object is the original program" making it the identity function
15:49:24 <vanila> to be honest the codata stuff seems to me like you're syaing.. "here's a game of life interprete" and then providing a function that computes n steps of game of life
15:50:07 <cpressey> and then saying "and you can call it as many times as you like"
15:50:22 <cpressey> which is fine, programming-wise
15:50:29 <cpressey> computability-wise, it's really not useful
15:50:55 <vanila> https://personal.cis.strath.ac.uk/conor.mcbride/pub/Totality.pdf
15:51:15 <cpressey> totality is a red herring imo (today). in fact, halting is a red herring too! (cf. Rice's theorem)
15:51:43 <elliott> vanila: that's even exactly what it is if you use like Stream
15:51:53 <elliott> since life : Board -> Stream Board is exactly life : Board -> Nat -> Board
15:52:22 <elliott> whereby exactly I mean... not in any language that currently exists. but the language everyone is thinking in, anyway
15:52:23 <oren> vanila: that would not be useful to someone unless they learn how to call said function
15:52:29 -!- kapil___ has quit (Quit: Connection closed for inactivity).
15:52:57 <oren> A function /= a fully functional program
15:54:27 <oren> there isn't a standardized encoding for conway gol initial states.
15:57:45 -!- supay has quit (Remote host closed the connection).
15:57:45 -!- bb010g has quit (Remote host closed the connection).
15:57:46 -!- ocharles_ has quit (Remote host closed the connection).
16:00:59 <oren> hm... technically, you could extract a primitive command-line interface from a function's argument types and numbers
16:02:58 <mroman> game of life interpreters could stop once a stable state has been achieved
16:03:01 -!- SopaXT has quit (Ping timeout: 250 seconds).
16:03:05 <mroman> or once a repeating state has been achieved
16:03:41 <oren> but only if every type is given a standard bijection
16:03:46 -!- variable has quit (Quit: I found 1 in /dev/zero).
16:04:04 <b_jonas> mroman: or just have the input mark a particular cell, and make the program stop when that cell is alive
16:04:09 <Taneb> mroman, I think determining if a state is repeating is uncomputable
16:04:42 <b_jonas> I have a crazy game of life program at http://www.perlmonks.com/?node_id=1008395
16:06:01 <cpressey> undecidable is also semi-decidable. glass half full, and all that
16:06:40 <Taneb> Yeah, I think for a finite initial state, it is actually computable, thinking about it
16:06:44 * cpressey forgot what he was going to rant about
16:06:46 <oren> Because of gliders, most states never repeat
16:06:46 <Taneb> As long as you know the time
16:08:03 <Taneb> And the initial state
16:08:28 <Taneb> Because it can only expand at a maximum of 1 cell per tick in any direction, right?
16:09:48 <cpressey> http://catseye.tc/installation/Schr%C3%B6dinger%27s_Game_of_Life fwiw
16:10:56 <b_jonas> yes, that's why it's better to have an end marker cell or something similar rather than watching for repeating states
16:11:01 <cpressey> there might be any number of conditions under which you want to consider a gol config "halted", also fwiw
16:11:06 <b_jonas> just stop the program when the cell (0,0) is live
16:11:12 <cpressey> which brings me back to Rice's theorem
16:13:30 <cpressey> might as well just define all turing machines as not being able to halt, and instead have a "scream state" which, if they ever enter it, they scream, and call it the Screaming Problem
16:14:24 <cpressey> if I have an infinite stream of codata representing the execution trace of a TM, ... that still doesn't help me tell if screams or not
16:14:50 <cpressey> So I'm very wary of Turner starting out with "it's total, which means it terminates" to "it's total, and you get infinite streams"
16:15:44 -!- SopaXT has joined.
16:15:55 <cpressey> besides! even if we had the most kick-ass language that let me prove all the properties I wanted about my program, it still wouldn't help!
16:16:29 <cpressey> because who writes to a spec, anyway? half of all software is written, not to a spec, but to a fuzzy notion of what will make the company money while not pissing off the users *too* badly
16:16:53 <elliott> you're definitely burnt out hehe
16:17:14 <cpressey> and those who do write to a spec -- their spec is like a gigantic legal document. maybe, if they're lucky, they've checked it for consistency
16:17:49 <cpressey> but they probably still don't know if it captures the requirements
16:18:05 -!- not^v has joined.
16:18:43 <cpressey> which will change tomorrow anyway
16:19:12 -!- spiette has joined.
16:19:30 <oren> cpressey: Or the coders interpret the spec differently then the customers
16:20:20 -!- CADD has quit (Remote host closed the connection).
16:22:26 <oren> "I thought by 'heart bar' you meant a line of hearts, not a heart with a red bar beside it!!"
16:24:15 <Gregor> Or a steel bar impaling a human heart.
16:25:34 <vanila> does anyone here write their own OS?
16:25:59 <oren> Vanila: I wrote part of one for a course...
16:28:12 -!- not^v has quit (Ping timeout: 245 seconds).
16:28:28 -!- ocharles_ has joined.
16:28:31 <cpressey> well, you start with a system, then you teach it to operate
16:28:42 <cpressey> actually -- it's mostly about interrupts.
16:28:55 -!- bb010g has joined.
16:30:30 -!- mihow has joined.
16:31:44 <oren> The overall structure was, some machine-specific stuff in assembler, followed by setting up the interrupt vector and resources for syscalls, then set up the file system (we didn't have to write the hard disk driver ourselves thank god) and then basically you pass control to a userland program which is the command interpreter.
16:32:06 -!- spiette has quit (Ping timeout: 265 seconds).
16:32:30 <oren> Overall the project was a half-assed version of UNIX.
16:33:38 <vanila> ill have to pay special attention to interrupts
16:36:45 -!- supay has joined.
16:41:42 -!- not^v has joined.
16:43:48 -!- spiette has joined.
16:53:27 -!- not^v has quit (Ping timeout: 256 seconds).
16:53:47 -!- not^v has joined.
16:55:44 <oren> So unicode might get color modifiers for face characters, for the sake of not being racist, but that didn't stop them from putting in π± π² π³ .
16:56:52 <cpressey> overlapping boxes containing hexadecimal digits are very racist indeed
16:57:45 <oren> `unidecode π±π²π³
17:02:18 <cpressey> i suspect, whatever that was supposed to do, it didn't work
17:02:30 <cpressey> or perhaps the bot is just really, really lagged
17:02:45 <oren> Hmm... Anyway those characters are "PERSON WITH BLONDE HAIR" "MAN WITH GUA PI MAO" and "MAN WITH TURBAN" respectively.
17:03:20 <oren> that is, Japanese stereotypes of Europeans, Chinese and Indians.
17:03:21 <cpressey> I see. those sounds like emoji imports
17:03:53 <vanila> I hate unicode so much!!!!!!!!
17:04:04 <vanila> 127 characters is already far too many
17:04:10 <cpressey> emoji which github supports. i always wondered why I'd ever need to pur a man with a gua pi mao in a pull request, though
17:05:39 <oren> "Woman with bunny ears" because the Playboy brand must last for all the ages
17:07:07 -!- not^v has quit (Quit: http://i.imgur.com/Akc6r.gif).
17:14:19 <b_jonas> vanila: do you want 60 characters, in two planes of 30 characters you can switch among with shifts?
17:16:12 <vanila> i dont know what that is sorry
17:16:52 <vanila> I want ride of everything from 01-1F in ascii (except newline)
17:18:13 <oren> What about tab?
17:29:54 -!- CADD has joined.
17:33:52 -!- Phantom_Hoover has joined.
17:33:55 -!- SopaXT has quit (Remote host closed the connection).
17:45:35 -!- Phantom_Hoover has quit (Ping timeout: 256 seconds).
18:02:25 -!- J_Arcane has quit (Quit: ChatZilla 0.9.91-rdmsoft [XULRunner 32.0.3/20140923175406]).
18:02:54 -!- J_Arcane has joined.
18:17:34 -!- vanila has quit (Quit: Leaving).
18:30:04 -!- bb010g has quit (Quit: Connection closed for inactivity).
18:31:50 -!- cpressey has quit (Quit: leaving).
18:40:42 -!- FreeFull has quit.
19:31:48 -!- arjanb has joined.
19:56:18 -!- AnotherTest has joined.
20:09:07 -!- Lymia has quit (Ping timeout: 265 seconds).
20:12:30 -!- PinealGlandOptic has joined.
20:14:22 -!- PinealGlandOptic has quit (Client Quit).
20:22:02 -!- Tritonio has quit (Ping timeout: 252 seconds).
20:22:50 -!- nycs has joined.
20:23:12 -!- TieSoul has quit (Ping timeout: 245 seconds).
20:24:07 -!- Tritonio has joined.
20:26:12 -!- `^_^v has quit (Ping timeout: 264 seconds).
20:29:11 -!- TieSoul has joined.
20:31:12 -!- PinealGlandOptic has joined.
20:44:52 -!- ProofTechnique has quit (Ping timeout: 240 seconds).
20:48:24 -!- bb010g has joined.
20:59:59 <oren> Yay, I'm this close to flooding the nuiverse with magma.
21:00:55 <oren> one level at a time, I'll flood it with water and magma, thus converting everything to obsidian
21:01:08 <b_jonas> oren: the whole universe, or just the surface of the planet?
21:01:19 <b_jonas> it's not so easy to flood a whole universe with magma
21:01:52 <oren> Well I have a pump stack that can bring magma or water to the highest level.
21:02:21 <oren> I need to build a second one for the other fluid
21:03:14 <b_jonas> oren: is this Dwarf Fortress or Minecraft?
21:03:24 <oren> Dwarf Frotress
21:03:47 -!- ais523 has joined.
21:04:29 <oren> Once I make it self powered, I'll lock one dwarf into my life support chamber and wait a few days.
21:05:17 <b_jonas> for how long can the dwarf survive in that chamber?
21:05:32 <b_jonas> and what are the walls for the chamber made of?
21:06:44 <oren> The walls are natural obsidian except the entrance which is a long tunnel which I'll obsidianify as the first step. The dwarf would have to tunnel his way out.
21:11:57 <oren> I'm not sure it will flood the whole map, but if I switch on a waterfall of each substance at the same time, I assume it will come close.
21:14:19 <oren> The only other guess I have as to the effect, is that a wall of obsidian will separate a vast ocean of magma from a similar ocean of water.
21:16:01 <oren> Either way it will be epic
21:16:32 <b_jonas> will you be able to find out which happens?
21:17:16 <oren> Eventually, when the second pumptower is complete.
21:18:04 <oren> First I have to modify the first one to integrate its power.
21:19:30 <b_jonas> oren: but isn't there fog of war in that game?
21:20:53 <oren> There is clouds, but above ground I can see everything.
21:21:48 <oren> I think it's something like 128 by 128 tiles
21:21:54 <oren> I haven't counted
21:22:02 -!- Patashu has joined.
21:22:08 -!- TieSoul has changed nick to TieSoul_.
21:22:14 -!- TieSoul_ has changed nick to TieSoul.
21:22:20 <oren> each tile is the size of a dwarf
21:24:08 -!- Tritonio_ has joined.
21:24:13 <oren> Seems like it is 48*4 x 48*4
21:26:14 <oren> The bigger it is the begger the lag
21:26:56 -!- Tritonio has quit (Ping timeout: 252 seconds).
21:30:22 -!- Tritonio_ has changed nick to Tritonio.
21:36:48 <b_jonas> so how good is the support chamber? how long can the lone dwarf live in it?
21:37:09 <b_jonas> or will you then rebuild civilization starting from that chamber?
21:37:25 -!- Lymia has joined.
21:39:28 <oren> I *think* practically indefinitely.
21:39:57 <b_jonas> what does that chamber have to contain for that?
21:40:07 <oren> It contains a small farm, and a still.
21:41:29 -!- AnotherTest has quit (Remote host closed the connection).
21:42:30 -!- R40UL has joined.
21:42:47 <oren> And i whenI get around to using it, I'll dump everything usable in the fort into the chamber
21:45:53 <oren> Hmm... won't both of the fluids just flow off the edge.
21:46:12 <oren> They have to meet before they do
21:49:25 <oren> I need like 100 enormous iron corkscrews
21:49:45 -!- nycs has quit (Quit: This computer has gone to sleep).
21:50:33 -!- `^_^v has joined.
21:50:45 <oren> To reach to the top of the map
21:51:35 <oren> I need to build a tower almost 100 levels high (easy with obsidian blocks) and then build 100 magma-proof pumps
21:53:03 <b_jonas> you'll need 100 confused scrolls of enchant weapon to magma-proof that many pumps
21:54:42 <oren> For unexplained reasons, ordinary iron is magma-proof
21:56:57 <b_jonas> oren: probably because DF magma is of only 1500 K or colder temperature
21:57:13 <b_jonas> and the iron is old low tech one with a high melting point
22:04:09 -!- oren has quit (Ping timeout: 265 seconds).
22:10:39 -!- oren has joined.
22:13:56 -!- aretecode has quit (Quit: Toodaloo).
22:18:44 -!- CADD has quit (Remote host closed the connection).
22:21:46 -!- CADD has joined.
22:29:48 -!- aretecode has joined.
22:33:46 <oren> The method of a self-powering water pump is due to escher, of course.
22:35:39 <oren> See we pump the water up, where it falls and becomes water pressure for a waterwheel.
22:35:57 <oren> Which then powers the pumps.
22:59:20 -!- zzo38 has quit (Remote host closed the connection).
23:05:28 -!- CADD has quit (Remote host closed the connection).
23:09:34 -!- CADD has joined.
23:13:12 -!- MDude has quit (Ping timeout: 245 seconds).
23:15:13 -!- cpressey has joined.
23:26:11 -!- `^_^v has quit (Quit: This computer has gone to sleep).
23:27:28 -!- `^_^v has joined.
23:29:19 <cpressey> It's entirely possible that there's no complexity class corresponding to the primitive recursive functionals simply because no one gives a crap.
23:29:35 <cpressey> I should probably just give up.
23:29:39 -!- cpressey has quit (Quit: leaving).
23:36:22 -!- mihow has quit (Quit: mihow).
23:38:00 <myname> since you people know haskell pretty well: is there something that is purely functional, can store things (like lists do) and support O(1) concatenation? I was thinking about something like a double linked list, but i am quite unsure
23:38:12 -!- mihow has joined.
23:38:23 <elliott> (you pay the O(1) cost in observation, though)
23:39:12 -!- `^_^v has quit (Quit: This computer has gone to sleep).
23:39:45 <myname> isn't ++ O(n) with n being the length of the first list?
23:39:52 <elliott> you only use that for literals.
23:39:58 <elliott> you can write \xs -> 'f':'o':'o':xs if you want
23:40:06 <elliott> the point is that if you have dlists f and g you can append with (f . g)
23:40:25 <elliott> > let foo xs = 'f':'o':'o':xs; bar xs = 'b':'a':'r':xs in (foo . bar) []
23:40:38 <elliott> the Show class uses this trick as ShowS (specialised to Strings only)
23:40:44 <elliott> to avoid exponential build-up doing lots of appends
23:41:25 <myname> searching through it works like always, right?
23:42:03 <elliott> you can only observe it by passing a list to it
23:42:09 <elliott> so you pay all the append costs then
23:42:15 <elliott> but it's much better than ((xs ++ ys) ++ zs) type stuff
23:42:26 <elliott> it's good for doing lots of appends and then observing the result once
23:42:51 <myname> i think i'm actually okay with that
23:42:59 -!- oerjan has joined.
23:43:47 -!- GeekDude has quit (Quit: ZNC - http://znc.in).
23:43:49 <lambdabot> fizzie said 12h 26m 45s ago: Uh-oh, I think my esowiki SSH key is only on the laptop and the fungot server, both of which are currently in the house-with-no-internet.
23:47:04 -!- oerjan has set topic: To the finder of this bottle: I'm a fungot trapped in a house with no internet | ZFC is a ChuChu rocket. | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/.
23:49:37 <oerjan> Gregor: can you tell HackEgo to join the channel? it's on freenode but not here
23:50:01 -!- FreeFull has joined.
23:50:04 <myname> elliott: does this do the clever way of concatenation? i.e. right associative?
23:51:31 <myname> oh, it has to, if i don't ignore something obvious
23:57:14 <oerjan> elliott: did you point out to cpressey that you can do goodstein sequence in system F, and ackermann is much simpler than that.
23:57:46 <oerjan> (someone on this channel did that after we discussed that it should be possible)
23:58:17 <elliott> myname: in particular (f . g) . h and f . (g . h) both do right-associative appends.
23:58:51 <oerjan> which means that the answer to "what complexity class does that correspond to" is something at most System F / second order logic
23:59:20 <elliott> myname: you can use Endo [a], that comes with the right Monoid instance I think
23:59:38 <myname> elliott: mind explaining?
23:59:43 <elliott> or there's, like, http://hackage.haskell.org/package/dlist
23:59:47 <oerjan> (those are equivalent in some sense iirc from the discussion)
23:59:50 <elliott> Endo a is a wrapper for (a -> a)
23:59:55 <ais523> at least it's not like Ursala, where Β«(f)(g)(h)Β» means (f g) h and Β«(f) (g) (h)Β» means f (g h)
23:59:58 <elliott> which has a Monoid instance that does composition and an mempty that's id