00:14:47 -!- deltaepsilon23 has changed nick to delta23.
00:16:26 <HackEso> The password of the month is Algol Waterloo Athens aftermath quadrant hydraulic tissue exodus stormy decadence egghead resistor flatfoot escapade newborn recipe
00:17:18 <b_jonas> yeah, I grabbed it at the start of this month
00:39:26 -!- sftp has quit (Ping timeout: 258 seconds).
00:40:13 -!- sftp has joined.
00:52:56 -!- Lord_of_Life has quit (Ping timeout: 240 seconds).
00:52:59 -!- Lord_of_Life_ has joined.
00:54:46 -!- arseniiv has quit (Ping timeout: 246 seconds).
01:45:05 -!- sftp has quit (Ping timeout: 240 seconds).
02:30:41 -!- sftp has joined.
04:07:43 -!- dcristofani has joined.
04:26:01 -!- dcristofani has quit (Ping timeout: 264 seconds).
04:50:47 -!- adu has joined.
05:02:05 -!- dcristofani has joined.
05:32:38 -!- dcristofani has quit (Ping timeout: 260 seconds).
06:07:26 -!- Bowserinator has quit (Ping timeout: 256 seconds).
06:08:12 -!- moony has quit (Ping timeout: 260 seconds).
06:08:13 -!- ATMunn has quit (Ping timeout: 260 seconds).
06:08:21 -!- iovoid has quit (Ping timeout: 272 seconds).
06:32:26 -!- aaaaaa has quit (Quit: leaving).
07:16:48 -!- tromp has quit (Remote host closed the connection).
07:25:32 -!- dcristofani has joined.
07:30:50 -!- Sgeo has quit (Read error: Connection reset by peer).
07:34:51 -!- dcristofani has quit (Ping timeout: 256 seconds).
07:37:18 -!- adu has quit (Quit: adu).
07:37:53 -!- ATMunn has joined.
07:38:29 -!- Bowserinator has joined.
07:42:53 -!- iovoid has joined.
07:43:21 -!- moony has joined.
07:53:12 -!- tromp has joined.
07:54:49 -!- wesleyac has quit (Quit: ZNC 1.8.2 - https://znc.in).
07:54:58 -!- wesleyac has joined.
07:58:28 -!- tromp has quit (Ping timeout: 260 seconds).
07:59:25 -!- tromp has joined.
08:07:55 -!- hendursa1 has joined.
08:09:52 -!- sprocklem has quit (Ping timeout: 260 seconds).
08:10:23 -!- hendursaga has quit (Ping timeout: 240 seconds).
08:49:15 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
09:27:10 -!- dcristofani has joined.
09:33:06 <esowiki> [[5D Brainfuck With Multiverse Time Travel]] M https://esolangs.org/w/index.php?diff=78175&oldid=78149 * RocketRace * (+140) Recommended race condition strategies
09:33:51 -!- imode has quit (Ping timeout: 260 seconds).
10:00:38 -!- arseniiv has joined.
10:05:20 -!- dcristofani has quit (Ping timeout: 272 seconds).
10:19:03 -!- t20kdc has joined.
10:24:13 <Taneb> There's an awful lot of maths out there
10:24:32 -!- delta23 has quit (Quit: Leaving).
10:26:45 -!- dcristofani has joined.
11:37:01 <int-e> Pfft, tfw you work half an hour building a stack of boxes to reach an area that turns out to be supposedly unreachable :)
11:38:16 <Taneb> int-e: ...context?
11:42:24 <int-e> Amnesia: The Dark Descent. I guess my reward is a closeup of this https://int-e.eu/~bf3/tmp/halla.jpg ... stack of boxes from above: https://int-e.eu/~bf3/tmp/outofbounds.jpg
11:43:02 <int-e> the latter also has a few wooden boards whose backside face is missing.
11:44:01 <int-e> which is a strong indication that the designers didn't think the area could be reached.
11:45:08 <int-e> Yeah you can get a glimpse of that from a comparatively small stack of boxes.
11:45:21 <int-e> And one that actually looks climbable ;)
11:45:47 <FireFly> is swedish like, a thing in the settnig of amnesia, or is the sign/message just an easter egg?
11:46:25 <int-e> language is english
11:46:27 <FireFly> I played a tiny, tiny bit of penumbra but it was too terrifying fro me
11:46:34 <FireFly> why am I so typoful today..
11:49:12 <FireFly> I don't think horror is my thing
11:49:15 <int-e> https://en.wikipedia.org/wiki/Frictional_Games is a swedish company though
11:49:46 <int-e> (Which is what I thought, but I wasn't sure.)
11:50:00 <int-e> I'm not sure it's for me either.
11:50:33 <int-e> This is before it gets really scary though.
11:53:44 <int-e> Just for completeness, this is the same stack from below https://int-e.eu/~bf3/tmp/boxes.jpg
11:54:23 <int-e> and initially those boxes were distributed over about 3 rooms.
11:55:08 <int-e> Oh well. I kind of hoped for a proper secret area, so this is a bit disapppointing :)
12:05:25 -!- arseniiv has quit (Quit: gone too far).
12:05:36 <fizzie> I've been looking at this "reMarkable 2" device. Cons: a bit expensive, tips of the pens apparently wear out over time. Pros: seems quite hackable, all members of the GitHub org of the company that makes it have photos of cats as their profile pictures on GitHub.
12:05:54 <fizzie> Especially that last bit's pretty compelling.
12:06:39 <myname> i baught a likebook with a pen for about half the price
12:06:52 <myname> it runs on an older version of android, pretty hackable
12:07:31 <fizzie> Does the screen feel like glass or like paper? I've got a ChromeOS tablet with a pen on it, and it just doesn't do it for me.
12:08:14 <myname> it's not as smooth as glass, but i wouldn't call it paper
12:15:30 -!- arseniiv has joined.
12:40:58 <myname> i am a bit angry that the noteslate pretty much never really came to be
12:42:57 <myname> i heard about it like 6 or 7 years ago and got excited. now you can "pre-order" on the web page with shipping expected in august 2016
12:45:23 <esowiki> [[5D Brainfuck With Multiverse Time Travel]] https://esolangs.org/w/index.php?diff=78176&oldid=78175 * RocketRace * (+141) Yeet pointers into the void
13:02:10 -!- hendursa1 has quit (Quit: hendursa1).
13:02:29 -!- hendursaga has joined.
13:04:13 -!- hendursaga has quit (Client Quit).
13:04:25 -!- hendursaga has joined.
13:12:29 <esowiki> [[Eternity]] https://esolangs.org/w/index.php?diff=78177&oldid=72746 * Jabutosama * (+17) added year category
13:15:26 -!- tromp has quit (Remote host closed the connection).
13:16:26 <esowiki> [[5D Brainfuck With Multiverse Time Travel]] https://esolangs.org/w/index.php?diff=78178&oldid=78176 * RocketRace * (+105) Interpreter
13:33:01 -!- tromp has joined.
14:00:08 -!- rain1 has quit (Quit: Leaving).
14:09:48 -!- rain1 has joined.
14:13:45 <esowiki> [[AAEEEEEEEEEI]] https://esolangs.org/w/index.php?diff=78179&oldid=65118 * Jabutosama * (-2504)
14:14:13 <esowiki> [[AAEEEEEEEEEI]] https://esolangs.org/w/index.php?diff=78180&oldid=78179 * Jabutosama * (-211)
14:19:07 -!- Frater_EST has joined.
14:20:20 -!- Frater_EST has quit (Read error: Connection reset by peer).
14:29:43 -!- FreeFull has joined.
14:31:26 -!- Arcorann_ has quit (Read error: Connection reset by peer).
14:47:15 -!- t20kdc has quit (Ping timeout: 265 seconds).
14:55:10 -!- t20kdc has joined.
15:52:42 -!- Frankenlime has quit (Quit: quit).
15:52:54 -!- also_uplime has joined.
16:03:26 -!- tromp has quit (Remote host closed the connection).
16:05:35 -!- imode has joined.
16:05:36 <esowiki> [[Talk:Modulous]] M https://esolangs.org/w/index.php?diff=78181&oldid=78019 * Abyxlrz * (+21)
16:07:58 -!- FreeFull has quit (Remote host closed the connection).
16:09:12 -!- FreeFull has joined.
16:12:41 -!- Sgeo has joined.
16:24:18 -!- tromp has joined.
16:36:13 <esowiki> [[Special:Log/newusers]] create * Mantita223 * New user account
16:39:17 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=78182&oldid=78137 * Mantita223 * (+128) /* Introductions */
16:39:39 <esowiki> [[User:Mantita223]] N https://esolangs.org/w/index.php?oldid=78183 * Mantita223 * (+2) Created page with "hi"
16:40:28 <imode> joy seems to have a lot of combinators that it comes packed with.
16:40:38 <imode> without a concrete explanation of what those combinators are.
16:43:04 -!- dcristofani has quit (Ping timeout: 272 seconds).
17:04:52 -!- imode has quit (Quit: WeeChat 2.9).
17:23:08 -!- LKoen has joined.
17:52:41 -!- aaaaaa has joined.
18:03:35 -!- orbitaldecay has joined.
18:08:41 <orbitaldecay> I'm trying to wrap my head around the feasibility of developing an automatic SKI programmer (i.e. you feed the program constraints and it generates a SKI program that satisfies those constraints). If you think of SKI calculus as a term rewriting system, then there are E unification algorithms that do this for *convergent* term rewrite systems. Do
18:08:41 <orbitaldecay> any of you know if there are any semidecidable unification algorithms that would meet my needs or am I barking up the wrong tree for this?
18:09:11 -!- ais523 has joined.
18:09:19 <ais523> what sort of constraints are you thinking of?
18:09:29 <orbitaldecay> It's hard to find places to ask these kind of questions, so forgive me for being a little off topic.
18:09:34 <ais523> automated lambda calculus → SKI translation exists (and vice versa), but I'm not sure I understand the problem
18:09:52 -!- arseniiv has quit (Ping timeout: 256 seconds).
18:11:21 <orbitaldecay> ais523: For example, if there were a unification algorithm that worked for this, then it would be possible to provide the equation (c) (b) (a) apply apply = (b) and the unification algorithm would solve for (a) (b) (c), ideally finding the most general unifier, which would be (a) = K, (b) = (b), (c) = (c)
18:12:17 <orbitaldecay> Equality here would represent beta equality, as can be deduced from rewrite rules
18:13:03 <orbitaldecay> I suspect that there is no decidable algorithm that does this, but I'd settle for semidecidable
18:13:26 -!- sprocklem has joined.
18:13:42 <ais523> it's probably decidable if the hardcoded parts of the program are simple enough
18:13:58 <rain1> you can write a computer program that will try to produce SKI terms that do certain things, and it can often succeed
18:14:01 <ais523> my reaction is that the only thing that would make it undecidable would be if the hardcoded parts of the program somehow ended up Turing-complete
18:15:01 <orbitaldecay> yeah, it get's tricky, because E unification is *in general* undecidable, but for specific equational theories it's either semidecidable, or completely decidable
18:15:27 <rain1> what's the exact problem in terms of input and output
18:16:18 -!- ais523 has quit (Read error: Connection reset by peer).
18:16:30 <orbitaldecay> E unification is decidable modulo a convergent term rewrite system for an equational theory, but SKI as a term rewrite system is not convergent
18:17:29 -!- ais523 has joined.
18:17:31 <ais523> I guess our language is ` s k i (Unlambda-style, not Underload-style)
18:17:52 <orbitaldecay> Either language would be interesting to look at, but I've been thinking in unlambda style so far
18:18:05 <ais523> and we have an expression made of ` and some unknowns (not sure about if s k i themselves are needed)
18:18:06 <orbitaldecay> in theory, the same idea applies to both as we're just thinking of them as term rewrite systems
18:18:15 <ais523> and need to make them equal
18:18:36 <orbitaldecay> I *think* this is best thought of as a unification problem
18:19:06 <rain1> i dont understand the specifics of "automatic SKI programmer"
18:19:08 <ais523> expressions of the form ````…`AB…X = (insert arbitrary data structure which doesn't contain A here) are equivalent to the lambda→unlambda compilation
18:19:21 <rain1> is the input a list of equations like X a b c = b(cbb)
18:19:26 <ais523> so that's one fairly useful class that can be solved
18:19:37 <rain1> this problem is trivial
18:20:10 <ais523> say you have ```Xabc = `b``cbb
18:20:31 <ais523> you can move the applys through the equals, to get X = \a.\b.\c.`b``cbb
18:20:51 <ais523> then the conversion of the nested lambda to SKI has known, entirely mechanical techniques
18:21:01 <orbitaldecay> That was more directed at rain1, but thank you for clarifying ais523
18:21:12 <ais523> I thought it might be, but decided to clarify anyway
18:21:19 -!- arseniiv has joined.
18:21:25 <ais523> especially as rain1 may be thinking only of this class of equations when saying "this problem is trivial"
18:21:37 <orbitaldecay> I suspect where we'll likely run into issues is with programs that necessarily require fixed point combinators in their solution
18:22:01 <ais523> right, say if X appears on both sides
18:22:13 <ais523> you can still mechanically generate a solution *but* it may correspond to an infinite loop, not the answer you want
18:22:16 <b_jonas> wait, that's usually backwards
18:22:23 <ais523> just like fixed point combinators in other languages
18:22:35 <ais523> oh, should be \c.\b.\a, right
18:22:50 <b_jonas> X = \a.someexpr implies the equation Xa = someexpr
18:23:08 <b_jonas> but if you go backwards, you need equality up to something
18:23:24 -!- ais523 has quit (Remote host closed the connection).
18:23:30 <b_jonas> what semantics do you even assign to your original eqution system
18:23:36 -!- ais523 has joined.
18:24:01 <orbitaldecay> b_jonas: I'm approaching SKI as a term rewrite system in this instance, so it's equality modulo beta reduction
18:24:02 <ais523> b_jonas: I'm using observational equality here, e.g. same inputs produce same outputs
18:24:56 <orbitaldecay> I was really only worried about equality modulo beta reduction, as I figured that'd be a lot simpler
18:25:36 -!- tromp has quit (Remote host closed the connection).
18:25:36 <ais523> >> let x a = 4/a in fix x
18:25:39 <ais523> > let x a = 4/a in fix x
18:25:47 <rain1> the difficult problem is to find X when given equations like X S K = K
18:25:55 <ais523> the problem with fixed point combinators is
18:26:08 <ais523> ideally you would want that to output 2, rather than getting stuck in an infinite loop
18:26:28 <ais523> rain1: there are clearly an infinite number of unequal such X
18:26:53 <ais523> -2 is also a valid fixed point
18:27:45 <orbitaldecay> Yeah, certain unification theories have proof of the existence of a "most general unifier" which would be, in your case rain1, an X such that all other X's can be derived from it, but E unification does not generally have this
18:28:00 <b_jonas> a quadratic equation! we have a solver for that
18:28:26 -!- rain1 has quit (Quit: Leaving).
18:29:01 <ais523> sage: x=var("x"); (x == 4/x).solve(x)
18:29:12 <ais523> if I go to all this trouble to install a CAS, may as well use it for this sort of thing
18:29:31 <ais523> it wouldn't be hard to rejig that into a fixed-point operator, although I don't know what sorts of function it would work on
18:30:08 -!- imode has joined.
18:31:46 <orbitaldecay> I'm thinking in the space between SKI and prolog and it's very strange territory
18:31:55 <ais523> simplest polynomial on which it fails appears to be x⁵ - x == 1, that makes sense
18:31:59 <b_jonas> sage is like a meta-CAS, it is bundled with a bunch of other CASes and can also use multiple commercial ones
18:32:07 <ais523> (this is the simplest polynomial with provably no solution in radicals)
18:32:18 <ais523> b_jonas: right, I think of it like glue for CASes
18:32:30 <ais523> you just write the problem you want and it figures out which CAS to use to solve it
18:32:32 <b_jonas> the sort of glue like bash is
18:32:59 <ais523> although, this means it probably isn't very good at complex problems that go through multiple domains because I wouldn't expect it to port your data structure from one CAS to another
18:35:22 <ais523> sage: x=var("x"); find_root(x**5 - x == 1,1,2)
18:35:36 <ais523> it can find it numerically even if it can't find it symbolically
18:37:15 -!- Lord_of_Life has quit (Changing host).
18:37:15 -!- Lord_of_Life has joined.
18:38:16 -!- rain1 has joined.
18:42:44 -!- tromp has joined.
18:48:59 <orbitaldecay> My final thoughts on this are the following: If we think about the naive algorithm of unifyiing an expression like X Y Z ` ` = Y in SKI calculus (i.e. iterating through all programs until we find one that works), it's clear to see why convergent rewrite rules are required because as we're iterating through those programs we might find one that
18:48:59 <orbitaldecay> doesn't terminate (in term rewriting language, doesn't converge). So I'm thinking that unifying a TC term rewriting system is always going to be undecidable.
18:51:02 <orbitaldecay> So this might be a project for a sub Turing language
18:54:17 <b_jonas> ais523: anyway, that doesn't mean that the case that orbital asked about is hopeless, because such an equation is not pure combinator calculus, and you can't encode it to pure combinator calculus. you don't have a way to force (fix x) to be a number (whatever kind) with equations.
18:56:30 <b_jonas> it can just give you (fix ) where fix is a fixed point combinator and so (fix x)
18:56:44 <b_jonas> give you (fix \a -> 4/a) where fix is a fixed point combinator and so (fix x) diverges
18:58:07 <b_jonas> but there also won't always be a solution, because you can write some contradictory equations like X = k; X = `ki
18:59:08 <rain1> minikanren can discover a quine, can it discover a y combinator?
19:14:50 <ais523> I just realised that a quine is basically just a fixed point of an interpreter
19:15:50 <shachaf> This reminds me, one time I thought quines are related to Lawvere's fixed point theorem (and are constructed the same way), but then I wasn't sure the details worked out.
19:16:45 <shachaf> I should figure out the details.
19:18:57 <rain1> is kleenes fixed point theorem related to lawveres?
19:19:17 -!- deltaepsilon23 has joined.
19:19:36 -!- deltaepsilon23 has changed nick to delta23.
19:20:12 <shachaf> Hmm, it looks more like Tarski's to me.
19:26:54 <esowiki> [[Special:Log/newusers]] create * Dregni * New user account
19:29:17 <esowiki> [[Special:Log/move]] move * SunnyMoon * moved [[99]] to [[99 (Joke language)]]: There is another language called 99.
19:29:17 <esowiki> [[Special:Log/move]] move * SunnyMoon * moved [[Talk:99]] to [[Talk:99 (Joke language)]]: There is another language called 99.
19:29:49 <esowiki> [[99]] https://esolangs.org/w/index.php?diff=78188&oldid=78185 * SunnyMoon * (-32) This is left for something else now...
19:32:29 <esowiki> [[99 (disambiguation)]] N https://esolangs.org/w/index.php?oldid=78189 * SunnyMoon * (+102) Disambiguation page created!
19:34:11 <esowiki> [[99]] https://esolangs.org/w/index.php?diff=78190&oldid=78188 * SunnyMoon * (+33) To the disambiguation page we go!
19:34:53 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=78191&oldid=78182 * Dregni * (+206) /* Introductions */
19:36:03 <esowiki> [[99 (disambiguation)]] M https://esolangs.org/w/index.php?diff=78192&oldid=78189 * SunnyMoon * (+4) Oh, it is italic...
19:38:40 <esowiki> [[99 (disambiguation)]] M https://esolangs.org/w/index.php?diff=78193&oldid=78192 * SunnyMoon * (+13) Finally!
19:40:47 <esowiki> [[User:Dregni]] N https://esolangs.org/w/index.php?oldid=78194 * Dregni * (+378) Dregni BrainFuckFart dev
19:45:33 <esowiki> [[User talk:Dregni]] N https://esolangs.org/w/index.php?oldid=78195 * Dregni * (+34) Created page with "I don't know what I'm doing tbh..."
20:17:41 <esowiki> [[99 (Esolang)]] N https://esolangs.org/w/index.php?oldid=78196 * SunnyMoon * (+239) Will finish this. I need to go to sleep :(
20:21:57 <esowiki> [[User talk:Dregni]] https://esolangs.org/w/index.php?diff=78197&oldid=78195 * Dregni * (+1049) /* BrainFuckFart */ new section
20:22:15 <esowiki> [[User talk:Dregni]] https://esolangs.org/w/index.php?diff=78198&oldid=78197 * Dregni * (-2) /* BrainFuckFart */
20:23:16 <esowiki> [[User talk:Dregni]] https://esolangs.org/w/index.php?diff=78199&oldid=78198 * Dregni * (+10) /* Open to */
20:37:30 <esowiki> [[BrainFuckFart]] N https://esolangs.org/w/index.php?oldid=78200 * Dregni * (+1055) Created page with "= BrainFuckFart = == BrainFuckFart a surprisingly fun language == === Concept === I started creating BrainFuckFart as a simple C++ interpreter for BrainFuck. As I went and..."
20:37:50 <esowiki> [[Language list]] https://esolangs.org/w/index.php?diff=78201&oldid=78166 * Dregni * (+20) /* B */
20:40:16 -!- shikhin has quit (Quit: Quittin'.).
20:40:39 -!- shikhin has joined.
20:58:41 -!- ^[_ has quit (*.net *.split).
20:58:41 -!- dog_star has quit (*.net *.split).
20:58:41 -!- ocharles has quit (*.net *.split).
20:58:41 -!- paul2520 has quit (*.net *.split).
20:58:51 -!- dog_star has joined.
20:58:54 -!- ocharles has joined.
20:58:56 -!- paul2520 has joined.
20:58:56 -!- paul2520 has quit (Changing host).
20:58:56 -!- paul2520 has joined.
20:59:08 -!- ^[_ has joined.
21:11:18 -!- deltaepsilon23 has joined.
21:13:26 -!- delta23 has quit (Ping timeout: 265 seconds).
21:13:42 -!- deltaepsilon23 has changed nick to delta23.
21:17:27 -!- orbitaldecay has quit (Remote host closed the connection).
22:26:00 -!- arseniiv has quit (Ping timeout: 256 seconds).
22:33:16 -!- ineiros has quit (Ping timeout: 246 seconds).
22:35:00 -!- ineiros has joined.
23:03:23 -!- hendursaga has quit (Ping timeout: 240 seconds).
23:05:10 -!- hendursaga has joined.
23:08:27 -!- Arcorann_ has joined.
23:13:14 <esowiki> [[Talk:BrainFuckFart]] N https://esolangs.org/w/index.php?oldid=78202 * Pipythonmc * (+269) Why is this in first person, and who even is the author? Needs fixing
23:15:06 <esowiki> [[BrainFuckFart]] https://esolangs.org/w/index.php?diff=78203&oldid=78200 * Pipythonmc * (+10) Add stub template
23:18:50 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”).
23:41:24 <esowiki> [[BrainFuckFart]] https://esolangs.org/w/index.php?diff=78204&oldid=78203 * Pipythonmc * (+2155) Add command table from github with some grammar fixes
23:45:18 <esowiki> [[Talk:BrainFuckFart]] https://esolangs.org/w/index.php?diff=78205&oldid=78202 * Pipythonmc * (+352) Add talk page entry
23:46:57 <user3456> wow, adding the table of commands tripled the character count