00:14:47 -!- deltaepsilon23 has changed nick to delta23. 00:16:03 `? compass 00:16:07 compass? ¯\(°​_o)/¯ 00:16:11 `? pass 00:16:13 pass? ¯\(°​_o)/¯ 00:16:25 `? password 00:16:26 The password of the month is Algol Waterloo Athens aftermath quadrant hydraulic tissue exodus stormy decadence egghead resistor flatfoot escapade newborn recipe 00:16:44 eh 00:17:18 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 [[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 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 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 int-e: ...context? 11:42:24 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:42:54 Ahaha 11:43:02 the latter also has a few wooden boards whose backside face is missing. 11:44:01 which is a strong indication that the designers didn't think the area could be reached. 11:44:12 heh 11:44:20 'hallå!', cute 11:44:23 lit. 'hi!' 11:45:08 Yeah you can get a glimpse of that from a comparatively small stack of boxes. 11:45:21 And one that actually looks climbable ;) 11:45:47 is swedish like, a thing in the settnig of amnesia, or is the sign/message just an easter egg? 11:45:57 setting* 11:46:09 the latter 11:46:13 makes sense 11:46:25 language is english 11:46:27 I played a tiny, tiny bit of penumbra but it was too terrifying fro me 11:46:29 for* 11:46:34 why am I so typoful today.. 11:49:12 I don't think horror is my thing 11:49:15 https://en.wikipedia.org/wiki/Frictional_Games is a swedish company though 11:49:46 (Which is what I thought, but I wasn't sure.) 11:50:00 I'm not sure it's for me either. 11:50:33 This is before it gets really scary though. 11:53:44 Just for completeness, this is the same stack from below https://int-e.eu/~bf3/tmp/boxes.jpg 11:54:23 and initially those boxes were distributed over about 3 rooms. 11:55:08 Oh well. I kind of hoped for a proper secret area, so this is a bit disapppointing :) 12:05:23 hello bye! 12:05:25 -!- arseniiv has quit (Quit: gone too far). 12:05:36 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 Especially that last bit's pretty compelling. 12:06:39 i baught a likebook with a pen for about half the price 12:06:52 it runs on an older version of android, pretty hackable 12:07:31 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 it's not as smooth as glass, but i wouldn't call it paper 12:15:30 -!- arseniiv has joined. 12:40:58 i am a bit angry that the noteslate pretty much never really came to be 12:42:57 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 [[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 [[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 [[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 [[AAEEEEEEEEEI]] https://esolangs.org/w/index.php?diff=78179&oldid=65118 * Jabutosama * (-2504) 14:14:13 [[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 [[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 [[Special:Log/newusers]] create * Mantita223 * New user account 16:39:17 [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=78182&oldid=78137 * Mantita223 * (+128) /* Introductions */ 16:39:39 [[User:Mantita223]] N https://esolangs.org/w/index.php?oldid=78183 * Mantita223 * (+2) Created page with "hi" 16:40:28 joy seems to have a lot of combinators that it comes packed with. 16:40:38 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:03:53 Greetings all 18:08:41 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 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 what sort of constraints are you thinking of? 18:09:29 It's hard to find places to ask these kind of questions, so forgive me for being a little off topic. 18:09:34 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 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:11:34 (postfix) 18:12:17 Equality here would represent beta equality, as can be deduced from rewrite rules 18:13:03 I suspect that there is no decidable algorithm that does this, but I'd settle for semidecidable 18:13:16 or rather, that this problem is not decidabe 18:13:17 hi 18:13:18 *decidable 18:13:20 hi rain 18:13:26 -!- sprocklem has joined. 18:13:42 it's probably decidable if the hardcoded parts of the program are simple enough 18:13:58 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 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 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 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 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:16:39 and any TC rewrite system won't be convergent 18:17:29 -!- ais523 has joined. 18:17:31 I guess our language is ` s k i (Unlambda-style, not Underload-style) 18:17:52 Either language would be interesting to look at, but I've been thinking in unlambda style so far 18:18:05 and we have an expression made of ` and some unknowns (not sure about if s k i themselves are needed) 18:18:06 in theory, the same idea applies to both as we're just thinking of them as term rewrite systems 18:18:12 two such expressions 18:18:15 and need to make them equal 18:18:19 yep 18:18:36 I *think* this is best thought of as a unification problem 18:18:42 but there are other ways of thinking about it 18:19:06 i dont understand the specifics of "automatic SKI programmer" 18:19:08 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 is the input a list of equations like X a b c = b(cbb) 18:19:23 and it finds X 18:19:26 so that's one fairly useful class that can be solved 18:19:30 rain1: yes 18:19:37 this problem is trivial 18:19:47 How so? 18:20:10 say you have ```Xabc = `b``cbb 18:20:31 you can move the applys through the equals, to get X = \a.\b.\c.`b``cbb 18:20:51 then the conversion of the nested lambda to SKI has known, entirely mechanical techniques 18:21:01 That was more directed at rain1, but thank you for clarifying ais523 18:21:12 I thought it might be, but decided to clarify anyway 18:21:19 -!- arseniiv has joined. 18:21:25 especially as rain1 may be thinking only of this class of equations when saying "this problem is trivial" 18:21:37 I suspect where we'll likely run into issues is with programs that necessarily require fixed point combinators in their solution 18:22:01 right, say if X appears on both sides 18:22:08 exactly 18:22:13 you can still mechanically generate a solution *but* it may correspond to an infinite loop, not the answer you want 18:22:16 wait, that's usually backwards 18:22:22 the lambda form X = 18:22:23 just like fixed point combinators in other languages 18:22:35 oh, should be \c.\b.\a, right 18:22:50 X = \a.someexpr implies the equation Xa = someexpr 18:23:08 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 what semantics do you even assign to your original eqution system 18:23:36 -!- ais523 has joined. 18:24:01 b_jonas: I'm approaching SKI as a term rewrite system in this instance, so it's equality modulo beta reduction 18:24:02 b_jonas: I'm using observational equality here, e.g. same inputs produce same outputs 18:24:14 Ah, got it 18:24:56 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 >> let x a = 4/a in fix x 18:25:39 > let x a = 4/a in fix x 18:25:42 *Exception: <> 18:25:47 the difficult problem is to find X when given equations like X S K = K 18:25:55 the problem with fixed point combinators is 18:26:08 ideally you would want that to output 2, rather than getting stuck in an infinite loop 18:26:28 rain1: there are clearly an infinite number of unequal such X 18:26:53 -2 is also a valid fixed point 18:27:45 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 a quadratic equation! we have a solver for that 18:28:12 yes 18:28:26 -!- rain1 has quit (Quit: Leaving). 18:29:01 sage: x=var("x"); (x == 4/x).solve(x) 18:29:02 [x == -2, x == 2] 18:29:12 if I go to all this trouble to install a CAS, may as well use it for this sort of thing 18:29:29 (y) 18:29:31 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 I'm thinking in the space between SKI and prolog and it's very strange territory 18:31:55 simplest polynomial on which it fails appears to be x⁵ - x == 1, that makes sense 18:31:59 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 (this is the simplest polynomial with provably no solution in radicals) 18:32:18 b_jonas: right, I think of it like glue for CASes 18:32:30 you just write the problem you want and it figures out which CAS to use to solve it 18:32:32 the sort of glue like bash is 18:32:44 ugly but usable 18:32:59 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 sage: x=var("x"); find_root(x**5 - x == 1,1,2) 18:35:23 1.1673039782615173 18:35:36 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 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 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 So this might be a project for a sub Turing language 18:54:17 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:55:42 b_jonas: indeed 18:56:30 it can just give you (fix ) where fix is a fixed point combinator and so (fix x) 18:56:44 give you (fix \a -> 4/a) where fix is a fixed point combinator and so (fix x) diverges 18:58:07 but there also won't always be a solution, because you can write some contradictory equations like X = k; X = `ki 18:59:08 minikanren can discover a quine, can it discover a y combinator? 19:14:50 I just realised that a quine is basically just a fixed point of an interpreter 19:15:50 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 I should figure out the details. 19:18:57 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 Hmm, it looks more like Tarski's to me. 19:26:54 [[Special:Log/newusers]] create * Dregni * New user account 19:29:17 [[Special:Log/move]] move * SunnyMoon * moved [[99]] to [[99 (Joke language)]]: There is another language called 99. 19:29:17 [[Special:Log/move]] move * SunnyMoon * moved [[Talk:99]] to [[Talk:99 (Joke language)]]: There is another language called 99. 19:29:49 [[99]] https://esolangs.org/w/index.php?diff=78188&oldid=78185 * SunnyMoon * (-32) This is left for something else now... 19:32:29 [[99 (disambiguation)]] N https://esolangs.org/w/index.php?oldid=78189 * SunnyMoon * (+102) Disambiguation page created! 19:34:11 [[99]] https://esolangs.org/w/index.php?diff=78190&oldid=78188 * SunnyMoon * (+33) To the disambiguation page we go! 19:34:53 [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=78191&oldid=78182 * Dregni * (+206) /* Introductions */ 19:36:03 [[99 (disambiguation)]] M https://esolangs.org/w/index.php?diff=78192&oldid=78189 * SunnyMoon * (+4) Oh, it is italic... 19:38:40 [[99 (disambiguation)]] M https://esolangs.org/w/index.php?diff=78193&oldid=78192 * SunnyMoon * (+13) Finally! 19:40:47 [[User:Dregni]] N https://esolangs.org/w/index.php?oldid=78194 * Dregni * (+378) Dregni BrainFuckFart dev 19:45:33 [[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 [[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 [[User talk:Dregni]] https://esolangs.org/w/index.php?diff=78197&oldid=78195 * Dregni * (+1049) /* BrainFuckFart */ new section 20:22:15 [[User talk:Dregni]] https://esolangs.org/w/index.php?diff=78198&oldid=78197 * Dregni * (-2) /* BrainFuckFart */ 20:23:16 [[User talk:Dregni]] https://esolangs.org/w/index.php?diff=78199&oldid=78198 * Dregni * (+10) /* Open to */ 20:37:30 [[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 [[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 [[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 [[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 [[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 [[Talk:BrainFuckFart]] https://esolangs.org/w/index.php?diff=78205&oldid=78202 * Pipythonmc * (+352) Add talk page entry 23:46:57 wow, adding the table of commands tripled the character count