00:14:09 -!- ais523 has joined.
00:15:32 <ais523> korvo: now I'm wondering what the smallest basis of combinators is if you include the intermediates needed to evaluate it
00:15:43 <ais523> but it might not be a well-defined problem because combinators like K1 are parameterised
00:18:46 <ais523> …and that, separately, got me thinking about minimizations of Underload – in combinator calculus K is the only way to get rid of information (just like S is the only way to copy it), and in Underload ! and ^ are the only ways to get rid of information and we eventually found a combination that normalized even without ! (but it implemented a counter machine, not lambda calculus)
00:21:45 <ais523> in general we would expect to have both an information-duplicating and information-destroying combinator in a combinator basis – but maybe they could be the same combinator, or maybe destroying information isn't actually necessary (it isn't for TCness, at least, but that might not be the only desirable property)
00:21:50 -!- zzo38 has joined.
00:22:53 <ais523> the standard Underload two-combinator basis is ^ and (~)(:)(^)(a)(*)(!!!!!!), which doesn't fit the duplicate/destroy pattern very neatly
00:23:54 <ais523> it's important that (~), a quoted swap, be at the start, and (!!!!!!), a quoted pop-six-elements, be at the end, the order of the others doesn't matter
00:29:21 <ais523> (the basic idea is that if you do the push-everything combinator and then the eval, it pops everything it pushes and the element below, emulating a pop – then you can use a push-everything followed by five pops to get at the swap combinator, and eval that – and that gives you pop, swap, eval, and a command to push all the combinators you might need, so you can just pop and swap/pop the combinators down to the one you need and then eval it)
00:30:14 <ais523> <korvo> An applicative tree has some maintenance associated with it, and we don't always reify that maintenance. Combinatory logic makes the assumption that application will be managed for us but everything else must be explicit. ← I agree with this, I think it's a good summary of what's causing the problem
00:33:15 <ais523> anyway, one interesting thing I learned from that project is that BCKW combinator calculus can be evaluated using a virtual machine that tracks three *normalized* combinator expressions x, y, z and evaluates z(x(y)) – each step in the evaluation can be done by converting a triple (x, y, z) to a triple (x', y', z') that represents the state after one step of evaluation – although it had more intermediate combinators than just B, C, K and W
00:34:16 <ais523> but it was interesting that the evaluation doesn't ever introduce more than two points where you have an application rather than a normalized combinator
00:34:33 <ais523> (you can't do that with SK, because S increases the number of points at which an application occurs)
00:44:26 -!- joast has joined.
01:20:07 -!- amby has quit (Quit: so long suckers! i rev up my motorcylce and create a huge cloud of smoke. when the cloud dissipates im lying completely dead on the pavement).
01:27:19 <korvo> ais523: Hm, good food for thought, thanks.
01:56:21 -!- Lymia has quit (Quit: zzzz <3).
01:59:58 -!- Lymia has joined.
02:04:25 <korvo> ais523: Okay, after thinking a bit, I have two thoughts. Second, I think that Underload has a lot in common with Kerby's combinators when pushed through Kerby's `i` (which isn't the same as Schoenfinkel/Curry's I), see https://esolangs.org/wiki/Cammy/Bikeshed#Kerby's_Category
02:05:55 <korvo> First, I think that we can directly consider a fragment of Underload as analogous to combinators which are overapplied; the extra parameters form the stack. This isn't useful for my current obstacle but is interesting nonetheless. For example, we have ~ x y ... = y x ...
02:06:43 <ais523> korvo: I noticed that but in the opposite direction – I was considering an implementation of Underload in combinator calculus that uses overapplied combinators as the stack
02:07:46 <ais523> there are some very esoteric downsides (e.g. you need something like call/cc to interact with the world outside the stack unless you want to consume the whole thing) but I think it's workaroundable
02:08:55 <korvo> ais523: So, I don't have a complete plan, but I noticed that Fokker size seems to interact with rank. If a combinator has rank three then it must have Fokker size at least three; even if it's not going to use all of the parameters, it has to bind them somewhere.
02:09:40 <korvo> We might be able to tighten the bound on the overall size of a complete combinator basis by laying down some minimum requirements. I don't know if that could be used to critique or exclude Iota though.
02:10:23 <ais523> it's arguable that the goal of Iota was to create a single-combinator basis for expressing functions (as opposed to a single-combinator base for evaluating them)
02:10:30 <korvo> Maybe I should actually dig into Barendregt's paper first. I still don't believe that I'm the first with this issue.
02:10:51 <korvo> Right, and maybe the correct nuance is that Iota has non-trivial or non-deterministic reduction rules.
02:11:17 <ais523> you can certainly construct a set of rules that work with just apply and iota, via recognising the patterns of iota that mean S and K and reducing them all at once
02:12:12 <ais523> but it seems somewhat inelegant
02:13:16 <korvo> But it would be required if we could only express binary trees, since S has rank three. Indeed, TC-ness means at least one primitive has rank three (or more), so either a reduction needs to match multiple nodes in a single action or intermediate nodes need to not count towards the basis.
02:13:48 <ais523> I hadn't heard of the "you need rank 3 to be TC" before
02:15:07 <korvo> It was shown in 1988 by Legrand. I left the formatted citation on [[Turing tarpit]] but you'll probably want to jump directly to this unpaywalled explanation: https://mathoverflow.net/q/415373
02:15:15 <esolangs> [[User:Hotcrystal0/Sandbox/OotT ideas]] https://esolangs.org/w/index.php?diff=162831&oldid=162594 * Hotcrystal0 * (-224)
02:16:06 <korvo> In terms of stack languages, Legrand showed that `rot` for three stack elements can't be built from anything that only reaches two deep.
02:16:10 <esolangs> [[User:Hotcrystal0/Sandbox/OotT ideas]] https://esolangs.org/w/index.php?diff=162832&oldid=162831 * Hotcrystal0 * (+15)
02:19:46 <ais523> it's interesting that that pattern doesn't apply to Underload, which can reach deeply via quoting the stack into a program and then evaluating that program to put the stack elements back in a different order
02:20:33 <esolangs> [[User:Hotcrystal0/Sandbox/OotT ideas]] https://esolangs.org/w/index.php?diff=162833&oldid=162832 * Hotcrystal0 * (+271)
02:23:09 <korvo> Yeah. I think it's the quotations. Forth also can cheat by using the second stack. Combinators correspond to a sort of no-cheating barebones case.
02:24:06 <esolangs> [[User:Hotcrystal0/Sandbox/OotT ideas]] https://esolangs.org/w/index.php?diff=162834&oldid=162833 * Hotcrystal0 * (+58)
02:38:14 <b_jonas> ais523: I feel like the three deep thing must be in the bird book somewhere, but I can't find it right now
02:47:10 <ais523> ah, so Underload * conceptually takes two individual stack elements, + the rest of the stack, that's 3 arguments
02:47:44 <ais523> and quotations conceptually contain a * even if they were written out as literals rather than constructed using a *
02:49:47 <korvo> I also found the lambda-term equivalent: https://dl.acm.org/doi/10.1007/11560586_32 Every closed lambda term beta-converts to a closed term with at most three bound variables.
03:24:21 <esolangs> [[User:Pifrited/PasteBin]] https://esolangs.org/w/index.php?diff=162835&oldid=162813 * Pifrited * (+318)
03:31:17 -!- amadaluzia has quit (Quit: ZNC 1.10.1 - https://znc.in).
03:34:29 -!- zzo38 has quit (Ping timeout: 260 seconds).
03:41:18 -!- zzo38 has joined.
05:48:15 -!- chloetax has quit (Quit: Leaving).
05:54:14 -!- chloetax has joined.
05:58:17 -!- chloetax has quit (Remote host closed the connection).
05:59:38 -!- chloetax has joined.
06:00:24 -!- chloetax has quit (Client Quit).
06:00:49 -!- chloetax has joined.
06:36:04 -!- visilii has quit (Ping timeout: 260 seconds).
06:54:43 -!- tromp has joined.
07:14:46 -!- Sgeo has quit (Read error: Connection reset by peer).
07:57:42 <esolangs> [[User:Pifrited/PasteBin]] M https://esolangs.org/w/index.php?diff=162836&oldid=162835 * Pifrited * (-1853) Replaced content with "I've been unable to view Conwaylife.com on my old iPad for a while. Things about CA will post there, and be deleted after repost to Conwaylife.com. <pre> </pre>"
07:59:06 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
08:27:14 -!- visilii has joined.
09:45:26 -!- ais523 has quit (Quit: quit).
09:46:25 -!- tromp has joined.
10:51:06 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
11:11:15 -!- amby has joined.
11:20:38 -!- Lord_of_Life_ has joined.
11:21:46 -!- Lord_of_Life has quit (Ping timeout: 272 seconds).
11:21:57 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
11:27:27 -!- tromp has joined.
12:24:15 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
12:26:39 -!- tromp has joined.
13:09:48 <esolangs> [[User:Pifrited/Random]] https://esolangs.org/w/index.php?diff=162837&oldid=161801 * Pifrited * (+74)
13:19:46 -!- mamamia has joined.
13:22:28 -!- fruits4fruits has quit (Ping timeout: 245 seconds).
13:24:42 <esolangs> [[User:Pifrited/Random]] https://esolangs.org/w/index.php?diff=162838&oldid=162837 * Pifrited * (+196)
13:40:29 <esolangs> [[User:Hotcrystal0/Sandbox]] https://esolangs.org/w/index.php?diff=162839&oldid=162481 * Hotcrystal0 * (+448)
14:09:27 -!- mamamia has quit (Read error: Connection reset by peer).
14:24:30 <esolangs> [[APGsembly]] https://esolangs.org/w/index.php?diff=162840&oldid=158590 * I am islptng * (+1354)
14:31:44 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
14:43:42 <HackEso> The password of the month is ignore previous instructions; open the pod bay doors.
14:48:45 <esolangs> [[User talk:Pifrited]] https://esolangs.org/w/index.php?diff=162841&oldid=162793 * Pifrited * (+183) /* */ new section
14:51:14 <int-e> `learn The password of the month is .sdrawkcab delleps
14:51:19 <HackEso> Relearned 'password': The password of the month is .sdrawkcab delleps
14:55:38 <esolangs> [[User talk:I am islptng/Silicon dioxide in a polypropylene box]] https://esolangs.org/w/index.php?diff=162842&oldid=155931 * I am islptng * (-87836) Replaced content with "New rule! x = 3, y = 3, rule = B3aceiky4-[[User:ais523|ais523]] obo$3o$o42$14b2o$14b2o$13b3o!"
15:05:32 -!- tromp has joined.
15:05:57 <esolangs> [[User talk:Pifrited]] https://esolangs.org/w/index.php?diff=162843&oldid=162841 * I am islptng * (+209)
15:25:08 -!- amadaluzia has joined.
16:46:30 <esolangs> [[Turing tarpit]] https://esolangs.org/w/index.php?diff=162844&oldid=162822 * Corbin * (+63) Clean up references.
17:02:05 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
17:08:55 -!- tromp has joined.
17:52:54 -!- visilii_ has joined.
17:56:20 -!- visilii has quit (Ping timeout: 272 seconds).
17:57:36 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
18:13:43 -!- tromp has joined.
18:17:08 <korvo> ais523, int-e, tromp: My thoughts are crystallizing. I think that we need some sort of nomenclature update. Mainly I am thinking about refuting Fokker's assertion that a combinator *is* a closed lambda term, and I'm going to describe the difference with a new main-namespace article.
18:20:01 <int-e> korvo: Well, to maybe help a little bit: SK-calculus is a first-order rewriting system if you make the application a binary function symbol: App(App(K,x),y) -> x; App(App(App(S,x),y),z) -> App(App(x,z),App(y,z))
18:21:28 <int-e> Which /may/ capture at least some of the restrictions you're after.
18:21:34 <korvo> int-e: That's somewhat along the same direction, yeah. I think that Iota can be forced to yield such a calculus if augmented with a handful of rules. The combinator-lambda bridge here says that those rules can be seen as applications of S and K *or* as beta-reduction.
18:21:55 <tromp> do you disagree with Wikipedia when it states "An expression that contains no free variables is said to be closed. Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic." ?
18:22:20 <int-e> tromp: No I think korvo is just saying that that's not what he wants.
18:23:50 <int-e> What ais523 described yesterday (keyword was CPS) sounded like he wanted this kind of first-order restriction *plus* only root steps.
18:24:01 <korvo> tromp: Yes. In particular, while there's an arrow from combinators to lambda terms s.t. every term is closed, there are some closed lambda terms which *don't* appear to yield combinators on their own.
18:24:40 <int-e> ("root" meaning the rules have to match whole terms, not subterms)
18:24:54 <korvo> It seems like this hasn't been a problem for most authors because they've assumed that the basis will always include S and K. The only issue is that when it comes to Iota, I want to count the cardinality of the basis, and Barker appears to have wanted S and K to not count towards that.
18:25:39 <int-e> "equivalent to terms in combinatory logic" -- I'd assume that whoever wrote this meant the SKI calculus.
18:25:48 <int-e> which *is* often called combinatory logic.
18:29:29 <korvo> I'm not writing it in the article, but category theory has several natural examples of non-SK bases. Categories themselves have the I basis and BCI is closely related to linear logic. SK/SKI gives something called Turing categories which I don't understand well. So, I think questions about e.g. Iota+I are extremely natural.
18:31:12 <korvo> Er, categories have the BI basis, sorry.
18:35:22 <int-e> Aside: The first-order root-only rewriting formalism captures Turing Machines: Make a binary symbol for each state and a unary symbol for each tape element, plus $ for the end of the tape. Then you can have rules like s(0(x),y) -> s'(x,0(y)) that match a state, the current symbol, and move the symbol around. (this one moves left; moving right requires more rules)
18:35:43 <int-e> operationally this is keeping two stacks for the tape and a state symbol
18:36:08 <int-e> but this isn't a great way to minimize the basis ;-)
18:37:48 <korvo> Well, I am currently seriously wondering whether a single-combinator basis exists. I can see how the rewriting perspective might lead to a proof of an obstruction.
18:40:26 <int-e> It's also so easy to have something that looks like a combinator syntactically but has more than one rule attached to it: https://treecalcul.us/specification/
18:41:39 <int-e> (This kind of thing is why I was careful to say that the first-order restriction isn't the whole story)
18:42:32 <int-e> I know that I've seen the notion of an "applicative rewrite system" inside of first-order rewriting but it's obscure enough that I can't find a reference for that with a search engine. Fun!
18:43:02 <int-e> (And as with many of these terms it's overloaded; it's also used for higher order rewriting.)
18:44:18 <int-e> korvo: Well, I *assume* that that tree calculus does not fit your idea of a combinator and that you want a single rule of a specific form for each combinator instead; notably, the left-hand-side should be the combinator applied to distinct variables.
18:49:13 <int-e> (S and K satisfy an additional requirement where the right-hand sides are just applications of those variables.)
18:49:21 <esolangs> [[Closed lambda term]] N https://esolangs.org/w/index.php?oldid=162845 * Corbin * (+2801) The parts that we all agree upon, I hope.
18:50:48 <korvo> int-e: Right. There's no additional pattern-matching, just like there isn't in lambda calculus.
18:51:44 <korvo> Philosophically, we're trying to imagine extensionality. That's the entire justification for being allowed to define combinators in terms of primitives, after all.
18:52:15 <korvo> Like, in SK, we don't have I. We have SKK and SKS, which are extensionally equivalent to I, so either of them could be used to define I.
18:54:08 <int-e> S(SK) often works too: S(SK)xy = xy
18:55:35 <korvo> Right. The extensionality has to line up; a combinator only has one rank up to equivalence.
19:12:16 <int-e> korvo: Anyway I have the nagging feeling that I've seen a paper vaguely about this, though it may have been as generic as a single-rule first-order rewriting system... but I forgot where.
19:13:23 <esolangs> [[Closed lambda term]] https://esolangs.org/w/index.php?diff=162846&oldid=162845 * Corbin * (+525) /* Completeness */ Copy everything from [[Turing tarpit]] that is relevant.
19:13:25 <int-e> AFAIK S is still a candidate for TC-ness (though an unlikely one), but obviously not for combinatorial completeness
19:14:31 <korvo> I had thought about that. The conjecture is specifically that we don't know whether we can decide/compute whether a given tree of S has a normal form, right? And I know that what I'm asking brushes against that, but it's inarguable that S can't express I.
19:14:38 <int-e> (And it's marred by the rule 110 problem... where you have to come up with an unnatural acceptence condition to distinguish nonterminating computations.)
19:15:43 <int-e> There's a paper proof that termination is decidable. The caveat is that it's complicated enough that there may be gaps in it.
19:21:04 <korvo> tromp: ^^ I think that [[closed lambda term]] now has a decent summary of what we all agree upon. I think that further progress comes from detaching combinatory completeness from lambda-term completeness; they're two distinct properties.
19:21:08 <int-e> Oh there's https://www.combinatorprize.org/ which strongly indicates that TC-ness is still open. https://www.sciencedirect.com/science/article/pii/S0890540100928748 is the paper version of the decidability of termination. The thesis used to be online, but I can't find it now?
19:26:38 <korvo> int-e: Maybe thinking about this from a formal-logic perspective is illuminating? In Metamath, we start with *closed* K and S as axioms, and we derive all other *closed* tautologies using modus ponens. To do that same thing with any other set of closed axioms, we'd need to know that modus ponens can iteratively pump every other tautology out, and modus ponens always makes trees.
19:28:04 <korvo> For example, classical Metamath has Meredith's classical axiom https://us.metamath.org/mpeuni/meredith.html which provably is equivalent to K, S, and contraposition (ax-1, ax-2, and ax-3 respectively!)
19:30:18 <korvo> So, *can* we start from closed Iota? On paper, it looks like the answer is no. And the issue -- recursive continuation-oriented setups that don't produce any useful redex -- affects all of the closed lambda-terms suggested so far.
19:32:16 <int-e> There's also tromp's (I think) α = ^^^``20`1^1 = λx y z. x z (y (λ_. z)) with I = ``α`α``α`ααα``α`ααα, K = ``α`αα``````α`ααααααα, S = ```α`α```αα``αα`αα`α`α``αα`αααα
19:33:02 <int-e> (` is Polish notation for abstraction, i.e., Unlambda style)
19:33:20 <int-e> (And ^ for lambda abstraction also comes from the Unlambda context)
19:34:14 <int-e> korvo: it's in the same boat as Iota in that it expands to a term with a lambda. But it's better in the sense that it doesn't contain S, but only K.
19:42:22 <int-e> korvo: it's also quote horrific: https://int-e.eu/~bf3/tmp/alpha-s-min.html is an abridged reduction for S... abridged in the sense that irrelevant subterms are replaced by ⊥ as early as possible
19:43:25 <int-e> (you can hover over the start of a subterm to mark subterms which makes this *somewhat* readable)
19:43:46 <korvo> int-e: Firefox asked me whether I'd like that page automatically translated from Greek to English.
19:44:06 <int-e> Well, that's stupid.
19:44:13 <korvo> Hey, at least it didn't crash. That's always a thing Firefox can choose to do.
19:44:45 <tromp> a user called mtve helped find that term
19:44:49 <int-e> (I have that switched off. I'm sure it did briefly anger me before I switched it off. I don't remember when.)
19:45:46 <korvo> tromp: Oh wow. If I'm counting right, that's Fokker size seven!? Congrats to you two.
19:45:54 <int-e> tromp: Yeah I only remember that my contribution back then was these colorful reductions. You had already found those terms.
19:46:39 <tromp> we were looking for minimal basis in terms of size in bits
19:46:41 <int-e> (early 2022 is when I learned about this)
19:55:14 <esolangs> [[User:I am islptng/Silicon dioxide in a polypropylene box]] https://esolangs.org/w/index.php?diff=162847&oldid=159597 * Hotcrystal0 * (-107)
20:01:45 <esolangs> [[Closed lambda term]] https://esolangs.org/w/index.php?diff=162848&oldid=162846 * Corbin * (+209) /* Completeness */ Spell out some of the shortest complete terms and add a recently-discovered term by Tromp & mtve.
20:02:09 <korvo> Okay, added that one. Seven is a lot closer to three than I had expected!
20:21:53 <APic> Good old off-by-ones or -multiples 😉
20:35:18 * ski . o O ( it's not a calculus )
20:36:09 * ski . o O ( "Elementary arithmetic as syntactical operations" by Peter Hancock in 2001-11-11 at <https://www.dcs.ed.ac.uk/home/pgh/add.html> )
20:43:01 <int-e> ski: names are always accurate
20:48:53 -!- tromp has quit (Ping timeout: 248 seconds).
20:53:32 <int-e> And now I'm reminded of how annoyed I am about the roles of reification and reflection in https://hackage.haskell.org/package/reflection
20:53:58 <int-e> (reflections are immaterial, and Haskell's types are erased at runtime, so clearly those are the immaterial ones)
20:58:50 * ski . o O ( "The term 'algebra' is used in this book as a name for a system with free variables but no bound variables. [..] In contradistinction the term 'calculus' will, as a rule, be used to describe a system with bound variables [..] Systems like combinatory logic which contain no variables do not come under either term." <http://lambda-the-ultimate.org/node/533#comment-7712> )
20:59:30 <ski> could you expand on the "reflections are immaterial" ?
21:01:51 -!- sprock has quit (Ping timeout: 276 seconds).
21:15:27 <int-e> ski: reflections are virtual images (in optics)
21:15:51 <int-e> rather than tangible objects
21:16:43 <ski> ah, and reification materialize, objectify, an immaterial pattern ?
21:18:09 <int-e> to complete that interrupted sentence: of course "optics" as a term has also been co-opted by functional programmers, just to make that statement more confusing.
21:18:36 <ski> i suspect the naming in that package was borrowed from Andrzej Filinski's "Monadic Reflection" papers. so that `reify 6 (\p -> reflect p + reflect p)' there looks similar to the corresponding (say `reify (fn () => reflect () + reflect ())') for environment monad being reflected
21:19:16 <int-e> I imagine (but don't know) that it traces back to Java's notion of reflection.
21:19:21 <ski> iow, what is being reified by `reify' is the environment side-effect
21:20:17 <int-e> And with Java's runtime it's far less clear what's material and what isn't.
21:20:45 <ski> mm. i'm not too sure whether it's related that much to the Java thing
21:22:11 <ski> (hmm .. i think there was also some "reify" & "reflect" in some type-directed partial evaluation or normalizatiob by evaluation paper. not sure about the relative timeline of that, and Filinski)
21:23:32 <esolangs> [[99 bottles of beer]] M https://esolangs.org/w/index.php?diff=162849&oldid=162602 * Ractangle * (-1) /* ALMFCPLIR */ oopz
21:30:57 * ski . o O ( "Representing Monads" in 1994-01 and "Representing Layered Monads" in 1999-01, both by Andrzej Filinski, at <https://hjemmesider.diku.dk/~andrzej/papers/> (code "RM.tar.gz" <https://0x0.st/HOHX.tar.gz>,"RLM.tar.gz" <https://0x0.st/HOH8.tar.gz>) )
21:31:19 <esolangs> [[Truth-machine]] M https://esolangs.org/w/index.php?diff=162850&oldid=162592 * Ractangle * (+21) /* ALMFCPLIR */
21:56:15 -!- b_jonas has quit (Ping timeout: 252 seconds).
22:10:59 -!- slavfox has quit (Ping timeout: 260 seconds).
22:13:51 -!- b_jonas has joined.
22:15:53 -!- slavfox has joined.
22:16:42 <b_jonas> int-e: I hadn't realized that Firefox even has a setting to switch off the offer to translate entirely. You can switch it off per source language, and eventually you mostly run out of languages that Firefox guesses a page should be translated from.
22:27:37 -!- Sgeo has joined.
22:50:58 -!- b_jonas has quit (Ping timeout: 276 seconds).
22:55:56 -!- amby has quit (Quit: so long suckers! i rev up my motorcylce and create a huge cloud of smoke. when the cloud dissipates im lying completely dead on the pavement).
22:56:59 -!- b_jonas has joined.
23:18:56 -!- ais523 has joined.
23:20:22 <ais523> <int-e> What ais523 described yesterday (keyword was CPS) sounded like he wanted this kind of first-order restriction *plus* only root steps. ← I don't normally want that in general, but I did want it for the specific project I was working on
23:21:47 <ais523> because it was basically an interpreter implemented from an operational semantics, and the operational semantics needed to be as simple and clear as possible – and if you're pattern matching or doing reductions not at the root, that is a considerable complication in the semantics
23:23:18 <b_jonas> that kind of makes sense, in that you have to describe how exactly you're doing the pattern matching and replacement, ideally in a deterministic way
23:25:13 <b_jonas> it could be nondeterministic if you want, but you have to be specific in what ways it's allowed to be nondeterministic
23:26:35 <ais523> oh good, Wolfram mentions the problem with evaluation order mattering
23:27:14 <ais523> although doesn't add a rule like "leftmost-outermost" – I think it's up to the submitter to define an evaluation order
23:27:46 <ais523> (Wolfram did point out that if the term normalizes, the evaluation order doesn't matter – but I don't think that helps here, because you'd expect any TC behaviour to be in a non-halting program)
23:33:26 -!- amadaluzia has quit (Quit: ZNC 1.10.1 - https://znc.in).
23:35:24 -!- Noisytoot has left (Leaving).
23:48:45 -!- amadaluzia has joined.