00:15:37 -!- MDead has joined.
00:17:25 -!- MDude has quit (Ping timeout: 256 seconds).
00:17:32 -!- MDead has changed nick to MDude.
00:58:15 <esowiki> [[Talk:Flurry]] https://esolangs.org/w/index.php?diff=70547&oldid=70530 * Challenger5 * (+270)
01:16:21 -!- arseniiv has quit (Ping timeout: 256 seconds).
01:17:25 -!- divergence has joined.
01:17:37 -!- diverger has quit (Ping timeout: 264 seconds).
01:34:51 -!- zzo38 has joined.
02:12:39 -!- divergence has quit (Ping timeout: 260 seconds).
02:14:02 -!- diverger has joined.
03:22:40 -!- xkapastel has quit (Quit: Connection closed for inactivity).
03:59:05 -!- ArthurStrong has quit (Quit: leaving).
04:05:14 -!- spruit11 has quit (Ping timeout: 256 seconds).
05:33:53 -!- Lord_of_Life has quit (Read error: Connection reset by peer).
05:34:08 -!- MDude has quit (Quit: Going offline, see ya! (www.adiirc.com)).
05:35:48 -!- Lord_of_Life has joined.
06:06:02 -!- Cale has quit (Ping timeout: 256 seconds).
06:25:46 -!- Cale has joined.
07:12:38 -!- user24 has joined.
07:23:10 -!- spruit11 has joined.
07:32:31 <Hooloovo0> have any of you played robo rally? it's basically a game about programming
07:32:58 <Hooloovo0> it has sort of an befunge feel, but the board modifies your actions
07:35:13 <Hooloovo0> also, made by the creator of MTG before he did that
07:52:06 -!- Phantom_Hoover has joined.
08:14:17 -!- imode has quit (Ping timeout: 258 seconds).
08:26:27 <esowiki> [[Talk:Flurry]] https://esolangs.org/w/index.php?diff=70548&oldid=70547 * Yul3n * (+123)
08:26:46 <esowiki> [[Talk:Flurry]] https://esolangs.org/w/index.php?diff=70549&oldid=70548 * Yul3n * (+75)
08:31:00 <esowiki> [[Talk:Z]] https://esolangs.org/w/index.php?diff=70550&oldid=62307 * Yul3n * (+191)
08:44:35 <fizzie> We (as in the channel collectively) played a bunch of that one web puzzle game that's a little like that, except single-player and much simpler.
08:51:55 <Hooloovo0> very nice, going to link to it since it seems like the beta/js(ugh, but whatever) version is much more usable http://www.robozzle.com/beta/
08:53:50 <Hooloovo0> hmm it doesn't seem like quite the same thing
08:55:12 <Hooloovo0> maybe if I play past the tutorials it will become more similar?
09:03:03 <Hooloovo0> anyway, we have *ALL* the expansions... I'd be interested in making an online version, if I knew how to do that at all
09:04:21 <Hooloovo0> as a board game, the weapons upgrades seem like they're overpowered... but also some are as programmable as the players...
09:04:56 <Taneb> Hooloovo0: ooh, I think I played that once?
09:07:47 <Hooloovo0> (implicit once-plague-is-over invitation) if any if any of you visit urbana
09:11:55 -!- rain1 has joined.
09:14:19 <Taneb> Unless you're in a village in Italy, that's slightly the wrong continent for me :(
09:19:34 <Hooloovo0> no, we're basically in the middle of NA :(
09:22:44 -!- Lord_of_Life_ has joined.
09:23:03 <int-e> tromp: BB(30)=160, BB(31)=267
09:23:27 <int-e> tromp: I added a BB.txt
09:23:41 -!- Lord_of_Life has quit (Ping timeout: 256 seconds).
09:24:02 <tromp> you must have some way better divergence detection than me:)
09:24:02 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
09:24:27 <Taneb> \exists c, n. \forall i, i >= n. \forall j, j >= i + c. BB(j) > BB(i)?
09:24:30 <int-e> it's not fully automatic... I have 2 manual proofs (as indicated in the file)
09:24:45 <tromp> i had 3 manual proofs at 29
09:24:52 <int-e> Taneb: that one is certainly true
09:25:23 <int-e> Taneb: I should figure out what the concrete c for which I can prove this is though... 20ish, maybe?
09:25:46 <tromp> probably true for c = 2
09:26:04 <rain1> which terms require manual proof?
09:26:16 <int-e> rain1: https://github.com/tromp/AIT/blob/master/BB.txt
09:26:58 <int-e> tromp: plausible, yes, but... :)
09:27:14 <tromp> i know, i wldn't bet my life on it:)
09:28:40 <int-e> Taneb: c=9 should work; one can prefix terms with lambda 2 bits, or with (\x\y.x) (7 bits, plus 2 for the apply).
09:28:58 <int-e> err, I meant to put parentheses around (2 bits).
09:31:06 <int-e> tromp: now how does one automate such inductive arguements... eww.
09:31:10 <tromp> isn't prefixing with lambda enough to get BB(n+2) >= BB(n) + 2 ?
09:31:36 <int-e> tromp: But Taneb's statement has j >= i+c
09:31:41 <rain1> how hard would it be to write a program that can prove those TODO ones halt?
09:31:54 <int-e> tromp: so we need an odd offset as well
09:31:58 <rain1> it seems kind of tricky i'm not sure how it would be done
09:33:08 <int-e> rain1: well, there's a certain pattern to these proofs, terms that grow in a very regular fashion.
09:33:16 -!- b_jonas has quit (Quit: leaving).
09:33:55 <int-e> So that could probably be captured somehow but it's highly unpleasant, and obviously once you do that you'll find terms with more complicated patterns, all up to the point where termination becomes unprovable.
09:33:57 <rain1> maybe hash each subterm, perform some reductions and then use the hash to look for repeating subterms?
09:34:33 <tromp> you don't get exact repetition though
09:34:36 <int-e> rain1: That's what we're doing already.
09:34:58 <int-e> rain1: It doesn't apply to those manual proofs (well the 3 I actually looked at)
09:37:02 <rain1> T (\1^k (T 1)) is kind of 'flat', it could basically be expressed as a string T \^k T 1 rather than a tree
09:37:50 <rain1> maybe when terms are flat it could be a simpler case
09:46:02 <int-e> Anyway, I'll leave BB(32) for a rainy day (there are few enough cases to be hopeful that they can be sorted out). But I think beyond that point it will very soon become a research grade problem (i.e., take a lot of effort and creativity). Obviously I have no clue where the unprovability territory starts.
09:49:41 <int-e> rain1: For reference, there are 978447 closed terms of size 32, so narrowing that down to 10 problematic cases is quite significant.
09:50:18 <rain1> that's really interesting, so that's where the real work was. how was that done?
09:51:24 <int-e> enumerate, reduce (with simplification along the way), try to detect loops and one relatively common class of non-terminating terms that does not have simple loops.
09:52:39 <int-e> Which, incidentally, only covers 2 terms of size 32. It can probably be generalized somewhat to cover a couple more.
09:54:37 <int-e> Taneb: actually I should've written c=8. But c=6 should also work: pick any variable n and replace it by \(n+1) 1 (which eta-reduces to n).
09:55:08 <int-e> Taneb: Which adds an abstraction, an application, and one extra bit for changing n to n+1, so that's 7 bits.
09:55:45 <int-e> Hmm, unfortunately though that only shows BB(n+7) >= BB(n).
09:56:09 <int-e> (Wheras BB(n+2) > BB(n) is strict.)
10:42:55 -!- kspalaiologos has joined.
12:20:04 -!- rain1 has quit (Quit: Lost terminal).
12:21:01 -!- xkapastel has joined.
12:52:25 -!- zzo38 has quit (Ping timeout: 264 seconds).
12:58:55 -!- wib_jonas has joined.
13:03:02 <esowiki> [[Talk:Alphaprint]] https://esolangs.org/w/index.php?diff=70551&oldid=70399 * Rerednaw * (+867) Edit in my JS code, following the addition of the "Hello, World!" example
13:17:37 -!- arseniiv has joined.
13:20:37 <esowiki> [[Talk:Flurry]] https://esolangs.org/w/index.php?diff=70552&oldid=70549 * Yul3n * (+169)
13:24:05 <tromp> int-e: how did you automate the proof of divergence for the 29-bit terms (\1 1) (\1 (\\3 2)), (\1 1) (\1 (\1 (2 1))), and (\1 1) (\1 (\2 1 1)) ?
13:26:16 <tromp> ignore the muddle one; i see you did that manually
13:35:19 -!- user24 has quit (Quit: Leaving).
13:36:43 <wib_jonas> how does this lambda thing work? can you effectively do lazy evaluation, as in, if there's a non-terminating term inside but it's never called, it isn't a problem?
13:39:09 <int-e> tromp: I want to sleep on what I did and document it properly, please remind me tomorrow
13:40:24 <tromp> wib_jonas: for BB you take consider the normal form so any non terminating part is a problem
13:41:02 <int-e> tromp: but the idea is to generalize the (\1 1) (\1 1) thing, noting in particular that you can have additional contexts (\1 1) (\C[1 1]) (C may have lambdas and that shifts the variables) and also some additional abstractions (\1 1) (\1 (\1 1)).
13:41:08 <wib_jonas> tromp: but don't those non-terminating parts get discarded as you evaluate to the normal form?
13:41:08 <tromp> i.e. BB is not specific to any normalization strategy
13:41:47 <tromp> so you do need to use one that guarantees nf if one exists
13:42:06 <int-e> wib_jonas: left-most outermost is strongly normalizing (even hypernormalizing--that's a fun concept) for the untyped lambda calculus.
13:42:39 <wib_jonas> int-e: right, that is lazy evaluation. and I assume you take this into account when you prove non-termination of a term.
13:43:25 <int-e> (normalizing = finds a normal form if it exists. strongly normalizing = that + termination. hypernormalizing: if you interleave the strategy and arbitrary reduction, you still reach the normal form if you don't starve the strategy)
13:44:35 <int-e> (such arbitrary reduction steps are highly useful for simplification, but also for program transformations)
13:44:37 <wib_jonas> int-e: I don't understand the distinction between the first two
13:45:08 <int-e> wib_jonas: strong normalization entails that normal forms always exist
13:47:38 <int-e> (And the term is usually used in contexts where the strategy doesn't matter, like simply typed lambda calculus, where unrestricted beta (or beta+eta) reduction is strongly normalizing)
13:48:03 <wib_jonas> er what? this is lambda calculus and you consider all terms, so a normal form doesn't always exist. how can "strong normalization entail" that and be meaningful?
13:48:14 <int-e> wib_jonas: it isn't
13:48:21 <int-e> wib_jonas: That's why I corrected to "normalizing"
13:49:32 <esowiki> [[Procedure]] M https://esolangs.org/w/index.php?diff=70553&oldid=70538 * PythonshellDebugwindow * (+169) /* Define/Call Function */
13:56:45 <wib_jonas> http://sigbovik.org/2020/ says SIGBOVIK 2020 is a conference that isn't on-site but works by audio talks through the internet. it also says that it's "on April 1 at 5pm". what timezone?
13:57:03 <wib_jonas> probably the New York timezone, yes
13:57:08 <Taneb> (the time zone of the usual venue)
14:01:47 -!- Phantom_Hoover has quit (Ping timeout: 256 seconds).
14:44:56 -!- MDude has joined.
14:48:01 <tromp> int-e: in your (\1 1) (\C[1 1]), you check that context C is strict in the hole?
15:14:57 <esowiki> [[DINAC]] M https://esolangs.org/w/index.php?diff=70554&oldid=70260 * PythonshellDebugwindow * (+18) /* Comments */
15:27:21 <int-e> tromp: Actually I demand that the hole is in a head position...
15:27:42 <tromp> that would do it...
15:45:36 -!- wib_jonas has quit (Remote host closed the connection).
15:47:50 -!- b_jonas has joined.
15:49:36 -!- b_jonas has quit (Client Quit).
15:52:35 -!- b_jonas has joined.
16:01:01 <arseniiv> how many prominent SIGBOVIK entries have #esoteric made? (for all time)
16:02:31 <b_jonas> some of #esoteric are actually in the U.S., we Europeans aren't in a clear majority
16:03:09 <arseniiv> when I read (too late) the presentations are audio-only, I thought I may have lost a chance to push my luck and submit something, though anyway I had no ideas at all and I have very little experience in spoken English, and in writing papers too :D
16:03:52 <arseniiv> <b_jonas> some of #esoteric are actually in the U.S., we Europeans aren't in a clear majority => yeah I thought the distribution is more or less diverse between many countries
16:04:51 -!- rain1 has joined.
16:05:05 <arseniiv> that said, I’m not against a joint paper, SIGBOVIK or not. Though the lack of interesting ideas on my part still stands :(
16:17:00 <b_jonas> arseniiv: they also say that you can submit just a paper, without a presentation, I think
16:18:21 <arseniiv> b_jonas: yeah though I’d be glad to be involved in random picking of answers to audience; and I still don’t have any interesting things to write
16:29:34 -!- imode has joined.
16:47:41 -!- mniip has quit (Remote host closed the connection).
16:51:02 -!- mniip has joined.
17:01:12 -!- zzo38 has joined.
17:05:56 -!- zzo38 has quit (Quit: zzo38).
17:25:40 -!- zzo38 has joined.
18:17:39 <tromp> int-e: does (\1 1) (\1 (\\3 2)) fall under your (\1 1) (\C[1 1]) detection?
18:27:32 <zzo38> Why does my internet connection tend to not work so well on the last day of a month?
18:29:14 -!- zzo38 has quit (Disconnected by services).
18:29:24 -!- zzo38 has joined.
19:21:49 -!- kspalaiologos has quit (Quit: Leaving).
19:31:17 -!- rain1 has quit (Quit: Lost terminal).
19:35:24 -!- imode has quit (Ping timeout: 265 seconds).
19:41:50 -!- ArthurStrong has joined.
20:20:57 <esowiki> [[+-]] https://esolangs.org/w/index.php?diff=70555&oldid=66723 * Voltage2007 * (+1744)
20:36:47 -!- imode has joined.
21:23:18 -!- cpressey has joined.
21:24:37 -!- Lord_of_Life_ has joined.
21:25:04 -!- Lord_of_Life has quit (Ping timeout: 256 seconds).
21:25:58 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
21:38:15 <cpressey> I saw a strange sight in the night sky tonight - a line of lights moving eastward, all the same velocity and trajectory. Turns out it was, most likely, a group of experimental SpaceX satellites.
21:39:39 -!- arseniiv_ has joined.
21:42:44 -!- arseniiv has quit (Ping timeout: 258 seconds).
21:44:07 -!- cpressey has quit (Quit: WeeChat 1.9.1).
22:40:12 -!- arseniiv_ has quit (Ping timeout: 256 seconds).
23:37:23 -!- xelxebar has quit (Ping timeout: 240 seconds).