00:06:52 <shachaf> kmc: are you into sat solvers yet
00:12:01 <kmc> not really
00:12:09 <kmc> i've been into them for brief periods in the past
00:12:18 <kmc> i wanted to use sat solvers to run Game of Life backwards
00:12:21 <kmc> but couldn't get it working
00:15:12 <shachaf> I was reading Knuth's fancy thing that does that.
00:20:15 -!- imode has joined.
00:27:25 -!- atslash has quit (Quit: This computer has gone to sleep).
00:34:50 -!- arseniiv has quit (Ping timeout: 240 seconds).
00:48:25 <shachaf> It's in TAOCP volume 4 fascicle 6.
00:49:11 <shachaf> Also there's a program at http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/knuth/pdf/sat-life.pdf ?
01:27:57 -!- imode has quit (Ping timeout: 240 seconds).
01:51:29 -!- imode has joined.
02:31:47 -!- atslash has joined.
03:20:27 -!- tromp has joined.
03:24:44 -!- tromp has quit (Ping timeout: 246 seconds).
03:47:26 -!- Lord_of_Life_ has joined.
03:48:02 -!- Lord_of_Life has quit (Ping timeout: 240 seconds).
03:48:51 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
04:18:03 -!- imode has quit (Quit: WeeChat 2.6).
04:43:06 -!- nfd9001 has joined.
04:50:39 -!- tromp has joined.
04:54:41 -!- tromp has quit (Ping timeout: 246 seconds).
05:04:32 <shachaf> Under what conditions does a programming language have quines?
05:15:25 -!- aloril has quit (Ping timeout: 265 seconds).
05:27:35 <shachaf> I wanted to figure out whether the existence of quines was a direct consequence of Lawvere's fixed point theorem.
05:27:49 <shachaf> It's surely related, but the construction is usually somewhat different.
05:44:41 -!- tromp has joined.
05:48:57 -!- tromp has quit (Ping timeout: 246 seconds).
06:18:13 -!- aloril has joined.
06:47:39 -!- tromp has joined.
07:28:57 -!- cpressey has joined.
07:31:53 <cpressey> shachaf: I'm pretty sure any Turing-complete language whose programs can be enumerated has a quine, by the s-n-m theorem.
07:32:11 <cpressey> s-m-n theorem. whetevr. it's early.
07:33:51 <cpressey> I guess "running a program" in the language has to considered to be able to produce an integer, or whatever the programs are enumerated with.
07:34:19 -!- MDead has joined.
07:37:37 -!- MDude has quit (Ping timeout: 268 seconds).
07:37:45 -!- MDead has changed nick to MDude.
07:43:16 <int-e> @teill arseniiv "we should just wait for arriving of a good AI photo sorter" <-- I'm waiting for the AI that will create the photos that I should have taken
07:47:54 -!- b_jonas has quit (Remote host closed the connection).
07:50:31 <cpressey> On the subject of quines, I was reading about Richard's paradox last night, and if I'm not mistaken, a Richardian number is basically the same as a https://esolangs.org/wiki/Narcissist
07:51:03 <shachaf> cpressey: I think maybe https://en.wikipedia.org/wiki/Kleene%27s_recursion_theorem has an answer to my question.
07:55:53 <shachaf> cpressey: Hmm, what's interesting about this paradox as opposed to all the other well-known paradoxes that seem identical to it?
07:58:02 -!- nfd9001 has quit (Ping timeout: 240 seconds).
07:59:44 <cpressey> I found it when trying to research why lambda calculus and combinatory logic are not used as deductive systems, even though they were invented as deductive systems. The Kleene-Rosser paradox that shows that ^c is inconsistent, is apparently more or less a version of Richard's paradox.
07:59:44 <int-e> cpressey: Oh I didn't know of that paradox. Of course on a formal level it'll be resolved by Tarski's theorem
08:00:14 <shachaf> I also don't particularly see narcissists as very interestingly different from quines, though it's possible I'm missing something there.
08:01:20 <int-e> (Tarski's theorem = undefinablility of truth. The sentence whose truth is of interest here is "F defines a unique real number")
08:01:21 <shachaf> I'd have to imagine that every Turing-complete language admits a quine. How could it not?
08:01:46 <shachaf> (Unless you're playing games with encoding, which don't seem that interesting to me.)
08:02:27 -!- nfd9001 has joined.
08:02:33 <int-e> TC-ness doesn't require any output capability (beyond one bit).
08:03:13 <shachaf> Yes, that's true. One semibit.
08:03:36 <int-e> I mean a mathematical truth value.
08:03:49 <shachaf> But I guess I don't care about that too much. I'm looking for interesting ways in which languages can fail to have quines.
08:04:09 <int-e> Not a weird three-state bit.
08:04:30 <shachaf> Which truth value are you talking about in particular? Halts/doesn't halt?
08:05:21 <int-e> accept/doesn't accept
08:05:53 <int-e> We have some wild cases that never halt.
08:06:09 <shachaf> Oh, here's a different question.
08:06:16 <shachaf> Hmm, I'm actually not sure how to phrase this question.
08:06:57 <shachaf> Lawvere's theorem is along the lines of, say you a function : A -> (A -> B) which is surjective. Then every function : B -> B must have a fixed point.
08:07:13 <shachaf> (For appropriate values of "function" and "surjective" and "(A -> B)".)
08:07:27 <esowiki> [[Wagon]] https://esolangs.org/w/index.php?diff=66655&oldid=65529 * Chris Pressey * (+332) Expand lead a little bit
08:07:50 <int-e> shachaf: any TC formalism will allow the kind of circularity that Kleene's fixed point theorem embodies. I.E. a program can contain a full description of itself, suitable for simulation or other analysis.
08:08:03 <shachaf> int-e: Yes, that's what I was getting at.
08:08:23 <int-e> And I agree that it's really hard to capture this more rigorously.
08:08:36 <shachaf> That seems more interesting than insisting on quines which gets into a bunch of nonsense.
08:08:48 <shachaf> I guess that question was about sub-TC systems.
08:09:15 <int-e> For the most part, Quines are just cute programming puzzles of no real importance.
08:09:20 <shachaf> Clearly some of those can still create quines (and use the same techniques that you'd normally use, not something one-off).
08:09:41 <cpressey> Also on the subject of quines: https://github.com/dpiponi/infinite-quine
08:09:44 <shachaf> Yes, I'm certainly not concerned with the quine itself.
08:10:42 <int-e> We have a notion of I/O-completeness on the wiki. An O-complete TC language has quines.
08:10:42 <shachaf> Anyway, on Lawvere's theorem.
08:11:15 <shachaf> What should I call A and B? I'm tempted to call A "Name", where A names an element of A -> B
08:11:37 <shachaf> (And with that element in turn an A names a B.)
08:11:48 <shachaf> Surjectivity means that everything has a name.
08:12:11 <shachaf> One concrete example is A as any set, and B as 2, which gives you Cantor's theorem.
08:12:51 <shachaf> If you can map elements of A to subsets of A such that every subset can be named by an element, then ¬ : 2 -> 2 has a fixed point.
08:14:20 <shachaf> Why is (A -> B) the right codomain here in general?
08:15:55 <shachaf> That's clearly not the question I want to be asking.
08:18:03 <shachaf> Maybe instead of B=2 I should take an example with an arbitrary B.
08:18:24 <shachaf> The Y combinator gives you fixed points for any function : B -> B this way.
08:23:56 -!- nfd9001 has quit (Ping timeout: 240 seconds).
08:24:50 <shachaf> OK, I guess you can say that eval : A -> (A -> B) is a two-argument function doing the same sort of thing Q(x, y) is?
08:26:14 <shachaf> How would you phrase "eval : A -> (A -> B) is surjective" on an uncurried function eval : A×A -> B?
08:27:56 -!- nfd9001 has joined.
08:38:41 -!- nfd has joined.
08:40:02 -!- nfd9001 has quit (Ping timeout: 240 seconds).
08:45:36 -!- nfd has quit (Ping timeout: 240 seconds).
08:51:25 -!- nfd9001 has joined.
08:52:22 <cpressey> Is SK-calculus known to be confluent? I mean it *must* be, right? I've just never seen anyone say anything about it one way or the other.
08:53:38 <cpressey> You can probably show it just by showing that the translation to lambda calculus preserves confluence.
08:53:38 <shachaf> Do you mean something other than the confluence you get if you expand every S and K to lambdas?
08:58:48 <Taneb> Confluence as a rewriting system?
08:59:23 <shachaf> Hmm, I guess that makes more sense.
08:59:59 <shachaf> Speaking of SK, I still don't understand why BCKW is a good system.
09:00:14 <shachaf> I already like it but I'd like to like it for a good reason.
09:00:37 <Taneb> shachaf: I found it easier to understand the translation between lambda calculus and BCKW than lambda calculus and SK
09:01:12 <shachaf> What I'd like is a connection to reordering, weakening, and contraction.
09:01:50 <shachaf> What's the lambda calculus translation?
09:02:25 <int-e> cpressey: SK and SKI are confluent
09:02:45 <Taneb> I can't remember, this was about 8 years ago I did this
09:02:52 <Taneb> Near when I was first in here
09:03:22 <shachaf> you're still in the top ten in here hth
09:03:38 -!- nfd9001 has quit (Ping timeout: 240 seconds).
09:03:47 <int-e> cpressey: They are orthogonal first-order term rewriting systems. This is usually shown by introducing a parallel reduction relation and something called a "parallel moves lemma" that shows that that relation has the diamond property (ensuring confluence); the terminology is similar to that used for the lambda calculus but the proofs are actually quite a bit simpler.
09:04:13 <int-e> cpressey: I forgot, did you mention having looked at Baader/Nipkow's book on term rewriting?
09:04:53 <int-e> (because that stuff is all covered in that book)
09:05:13 -!- nfd9001 has joined.
09:05:20 <int-e> Except maybe the concrete case of combinatory logic
09:07:23 <int-e> Btw, orthogonal = left-linear (no duplicate variables in left-hand sides of rules) + absence of critical pairs (which you might know from Knuth/Bendix completion or the corresponding confluence criterion for terminating systems).
09:08:29 <int-e> Taneb: do you also approach these systems from a point of view of abstraction elimination?
09:08:52 <int-e> (BCKW(I) and SK(I))
09:09:15 <int-e> Actually, hrm. I want SBCKI, I don't like W at all.
09:10:03 <shachaf> W is supposed to replace S presumably, as the only combinator that does duplication.
09:10:07 -!- nfd9001 has quit (Ping timeout: 268 seconds).
09:10:12 <int-e> myname: you missed the oppertunity there: BSICK (be sick)
09:10:34 <int-e> shachaf: because it has no immediate use for abstraction elimination
09:11:08 <int-e> \x. M[x] N[x] -> S (\x.M[x]) (\x.N[x])
09:11:43 <int-e> but with BCKW you artificially (to my mind) deduplicate the x first, ... -> W (\x1 x2. M[x1] N[x2]) x.
09:12:37 <shachaf> Well, you might be interested in talking about substructural logic.
09:12:59 <shachaf> So I could be interested in what you get with BCK without W, for instance.
09:13:14 <int-e> Sure, but I also get that from SBCKI by dropping the S.
09:14:09 <int-e> I don't like the flavour of duplication offered by W; I prefer the flavor offered by S.
09:14:15 <int-e> That's it in a nutshell.
09:14:16 <shachaf> The S is serving multiple purposes, I guess.
09:14:39 <shachaf> I like S but I'm curious whether a simpler basis will let you pick out parts you like better.
09:15:02 <shachaf> Hmm, is there a standard combinatory basis for some kind of linear lambda calculus?
09:15:03 <int-e> But I'm definitely not approaching this from a logical perspective. My first encounter of combinatory logic was as a model of computation.
09:15:06 -!- wib_jonas has joined.
09:15:41 <int-e> shachaf: Sure, BCI is the standard basis for that, add K if you allow deletion.
09:15:57 <wib_jonas> "<shachaf> I'd have to imagine that every Turing-complete language admits a quine. How could it not?" => only if they can do universal IO
09:16:08 <int-e> I do like B and C precisely because they capture linearity.
09:16:19 <int-e> Something that SK hides.
09:16:19 <shachaf> wib_jonas: Yes, see the discussion below.
09:16:32 <shachaf> How do you turn a lambda term into BCKW?
09:16:52 <wib_jonas> BCKW => we just had a discussion about that
09:17:08 <wib_jonas> http://www.cs.ox.ac.uk/people/samson.abramsky/pcpt.pdf
09:17:33 <int-e> you have \x. M[x] N -> X (\x.M[x]) N, \x. M N[x] -> Y M (\x.N[x]), where X,Y \in {B,C}.
09:17:39 <int-e> I can never remember which is which.
09:17:55 <shachaf> OK, that PDF indeed makes the connection I wanted.
09:18:21 <Taneb> int-e: I don't quite know what you mean by abstraction elimination (my brain isn't fully awake yet)
09:18:25 <int-e> (So these look like specializations of \x. M[x] N[x] -> S (\x.M[x]) (\x.N[x]) when x does not occur freely in N or M)
09:18:33 <Taneb> SBCKI would be better, I think
09:18:44 <wib_jonas> in particular, there are no non-empty quines in geo because it can only output decimal integers (followed by a newline), but the source has to have "print" in it to output anything
09:19:07 <int-e> Taneb: the process of starting from a lambda term (which has lambda-abstractions) and turning it into an equivalent (in some sense) abstraction-free term using your combinator basis
09:19:22 <wib_jonas> but this probably isn't an interesting reason
09:19:32 <shachaf> wib_jonas: OK, but I already said that that's an encoding detail that I don't find interesting.
09:20:21 <Taneb> int-e: yeah, I think that's what I do
09:20:50 <wib_jonas> "<int-e> For the most part, Quines are just cute programming puzzles of no real importance." => Smullyan and Hofstadter would disagree
09:22:08 <int-e> wib_jonas: "quine" is just a surface phenomenon (a program that prints its own source code)... you need much more to make it computationally interesting
09:22:59 <wib_jonas> int-e: right, that's why Golf SE tried to qualify interesting quines with a rule, so that non-cheating quines are ones that are useful for building self-referential programs
09:23:05 <cpressey> int-e: Right, yes. I've read Baader and Nipkow, also some other texts on term rewriting. Didn't remember about orthogonality of term rewrite systems. Didn't really occur to me at the time to look at SK-calculus as a rewrite system. And I guess lots of other ppl don't usually look at it that way either.
09:23:30 <wib_jonas> and, in particular, empty quines, or quines that are just a numeral in languages that echo a numeral, are considered cheating for them
09:25:01 <int-e> ``` dc <<<6581840dnP
09:25:40 <shachaf> Oh, I like this connection to polynomial time.
09:25:55 <shachaf> I don't really know good ways of talking about computational complexity for lambda calculus at all.
09:26:10 <int-e> That's a quine, but hardly interesting from a logical perspective... there's no real quoting (quining) going on here.
09:26:55 <int-e> cpressey: That's fair. Happy to help with connecting dots :)
09:27:04 <shachaf> I imagine lambda calculus is just bad at talking about things like time and space constraints.
09:27:18 <wib_jonas> int-e, KBCSI => yeah, that could work
09:27:29 <shachaf> Since reduction is so unrealistic.
09:28:18 <wib_jonas> but my problem is sort of that all of these get weird if you try to abstraction-eliminate multiple variables
09:28:50 <wib_jonas> so could I instead advocate Amicus, which deals with functions of multiple variables naturally?
09:30:37 <shachaf> «It was always hard for many to comprehend how Cantor’s mathematical theorem could be re-christened as a ”paradox“ by Russell and how Gödel’s theorem could be so often declared to be the most significant result of the 20th century. There was always the suspicion among scientists that such extra-mathematical publicity movements concealed an agenda for re-establishing belief as a substitute for s
09:30:43 <shachaf> cience. Now, one hundred years after ...
09:30:46 <shachaf> ... Gödel’s birth, the organized attempts to harness his great mathematical work to such an agenda have become explicit.»
09:31:45 <int-e> wib_jonas: The other thing that makes writing quine more of a puzzle is that ultimately the quining process is very automatic (one cute trick: take a description of a program P(x) that takes a description of a program Q and produces Q([Q]) by whatever notation) but you have a lot of leeway in choosing the encoding for Q, so that's what the focus tends to be on.
09:33:20 <int-e> In the end 6581840dnP doesn't depart from the core idea at all... but the encoding is chosen such that both priting [Q] and printing Q is done by a single dc instruction.
09:34:58 <wib_jonas> int-e: no no, the argument Q is printed by [n] instruction, the program Q is pritned by the [P] instruction
09:35:17 <int-e> wib_jonas: You may have mis-parsed what I wrote.
09:36:10 <int-e> wib_jonas: I KNOW HOW IT WORKS DAMNIT
09:36:20 <wib_jonas> yeah, sorry, but I wasn't sure how it worked
09:36:34 <wib_jonas> because I don't write dc stuff and the instructions are weird
09:37:57 <int-e> (I came up with that quine myself some years ago. But it's obvious enough that I would be surprised if I was the first.)
09:39:28 <wib_jonas> yeah. the perl quine that starts with print<< x2,$/ is also like that, multiple people come up with it independently by simply trying to write a very short quine
09:39:53 <wib_jonas> whereas some of the other perl quines that I wrote are much less canonical
09:40:47 <int-e> > text$ap(++)show"text$ap(++)show"
09:40:56 <wib_jonas> https://www.perlmonks.com/?node_id=835076 these for example
09:41:48 <wib_jonas> `perl -eprint+("`perl -eprint+(","\"",",","\\",")[g1012131121212133121414=~/./g]")[g1012131121212133121414=~/./g]
09:41:49 <HackEso> `perl -eprint+("`perl -eprint+(","\"",",","\\",")[g1012131121212133121414=~/./g]")[g1012131121212133121414=~/./g]
09:42:01 <wib_jonas> where the order of the strings in the list is totally arbitrary
09:42:22 <wib_jonas> `perl -eprint+("\\","\"",",","`perl -eprint+(",")[3,1,0,0,1,2,1,0,1,1,2,1,2,1,2,1,3,1,2,1,4,1,4]")[3,1,0,0,1,2,1,0,1,1,2,1,2,1,2,1,3,1,2,1,4,1,4]
09:42:22 <shachaf> So does this pattern fit into the Lawvere theorem form?
09:42:23 <HackEso> `perl -eprint+("\\","\"",",","`perl -eprint+(",")[3,1,0,0,1,2,1,0,1,1,2,1,2,1,2,1,3,1,2,1,4,1,4]")[3,1,0,0,1,2,1,0,1,1,2,1,2,1,2,1,3,1,2,1,4,1,4]
09:46:37 <wib_jonas> ais523: here's a perl quine by mtve that has only ascii punctuation and spaces. I don't know how it works, but perhaps it also helps with your string eval question: https://www.perlmonks.com/?node_id=836752
10:01:55 <int-e> woah, really... 'In late 2011, Intel [35]introduced a performance enhancement to its line of server processors that allowed network cards and other peripherals to connect directly to a CPU's last-level cache'
10:02:24 <int-e> [35] is https://www.intel.com/content/www/us/en/io/data-direct-i-o-technology.html
10:03:41 <int-e> context is https://www.schneier.com/blog/archives/2019/09/another_side_ch.html (I'm reading the october CRYPTO-GRAM)
10:03:55 <wib_jonas> int-e: yeah, that's what spawned all the rumors about NSA backdoors
10:04:40 <int-e> I'm a bit surprised I missed this.
10:05:18 <int-e> I didn't miss the ME stuff (which is a backdoor by design, if you look at it cynically enough)
10:05:27 <wib_jonas> well, it's one of the things that spawned the rumors at least
10:05:39 <int-e> (I mean ME = management engine)
10:06:18 <int-e> I think IME is the official abbreviation.
10:06:23 <wib_jonas> int-e: how about the enclave thing, that lets you create encrypted parts of the memory that can run code but where the rest of the programs that the cpu runs can't read that code and its state?
10:07:07 <int-e> I didn't miss that either... I see it as related really.
10:07:38 <int-e> (It's also a bit of the extension of the decades old system manangement mode.)
10:08:26 <shachaf> OK, when you have f.g = id, what should you call f and g?
10:08:37 <shachaf> "left inverse" and "right inverse" is too confusing, I think.
10:08:44 <int-e> I mean, SMM is almost as invasive, also based on hiding a region of memory, just not /designed/ to be secure.
10:09:03 <wib_jonas> you should consider the other side though. rather than keeping all the technology that they use for the backdoors a secret that nobody will find unless they spend a man-decade of studying electron-microscope scans, they benevolently document all the backdoor capabilities of the cpu so that you can write high performance backdoors too
10:09:04 <int-e> shachaf: left inverse of g; right inverse of f.
10:09:14 <shachaf> I've been going with "retraction" and "section" but I'm suspecting that's not so great either.
10:09:15 <wib_jonas> it's not exclusive to the NSA, you can backdoor the bios too
10:09:33 <shachaf> int-e: The problem is that if you say "f is a right inverse", I have to write down the thing to see what's going on.
10:10:58 <shachaf> Maybe the intuition I want is "object" and "name": Every object has at least one name, and you can pick out a canonical name (at least if you have choice).
10:11:29 <wib_jonas> why would every object have at least one name? no way
10:11:36 <int-e> wib_jonas: It's not even necessary to involve the NSA as a driver here... SMM was introduced to simulate legacy hardware capabilities. Secure enclaves can be perfectly explained by the desire to enforce copyright. Data direct I/O addresses a genuine (if very high-end) performance problem.
10:11:43 <wib_jonas> especially not when the names come from a countable set and the objects come from a bigger one
10:11:49 <shachaf> Well, it does in this case, because you have a surjection.
10:12:27 <shachaf> What's a better terminology where I can easily remember which set is the bigger one and which function goes in which direction?
10:12:32 <int-e> wib_jonas: I mean I would be surprised if the NSA were not involved in this at all... they are too big. But I don't think they have to do anything beyond subtle nudging here.
10:12:38 <int-e> wib_jonas: System Management Mode
10:13:07 <int-e> wib_jonas: Not sure when that was introduced, i386 or i486 maybe? Around that time I think.
10:13:08 <wib_jonas> int-e: I don't mean that it has to be the NSA specifically, that's just the name that people use in rumors
10:13:52 <wib_jonas> int-e: but in reality it's usually the big secret agencies of all other countries that puts the backdoors there, rather than the secret agency of your country
10:14:15 <wib_jonas> int-e: system management mode, how does that differ from ME?
10:14:16 <int-e> SMM can be used for things like simulating the AT keyboard interface (port 60h/61h) for USB hardware.
10:14:36 <int-e> wib_jonas: It runs on the same processor.
10:15:04 <int-e> It's just that certain I/O operations can trigger a software emulation layer. Nothing really deep.
10:15:32 <int-e> 'It was first released with the Intel 386SL.'
10:17:01 <wib_jonas> int-e: ah, so five years after the 386
10:17:07 <esowiki> [[Wagon]] https://esolangs.org/w/index.php?diff=66656&oldid=66655 * Chris Pressey * (+599) More describing language overview
10:17:14 <int-e> The ME is a full (but less powerful) separate core... that's a fairly recent thing.
10:18:39 <int-e> But even there its existence can be explained in a perfectly innocent way.
10:20:21 <int-e> Initializing a processor (memory subsystem (training DRAM, probably other I/O lines as well)) has become so complex that it's better to do it in software than in pure hardware. As a bonus, you get the ability to work around some hardware bugs in software. Now if you're Intel, which hardware platform are you likely to use for this?
10:21:12 <jix> intel did use a 3rd party architecture (ARC) for the ME for a long time until they switched to a x86 core AFAIK
10:21:20 <int-e> So now you have a separate processor on your die... and it's dormant for most of the system's operation. That's stupid maybe you can find a use for it? ... and suddenly you end up with an ME-like device.
10:22:21 <jix> (which I found quite funny, given the origin of ARC as the superfx chip used in starfox on the super nintendo)
10:22:23 <int-e> (Of course the architecture is secondary. If it's a universal machine... it can be used for arbitrary purposes.)
10:22:57 <wib_jonas> "Now if you're Intel, which hardware platform are you likely to use for this?" => I'm not familiar with the licensing situation of cpus really
10:23:44 <int-e> Intel tried to make a GPU out of X86.
10:24:39 <int-e> Or are trying to make... according to https://en.wikipedia.org/wiki/Larrabee_(microarchitecture) they've revived that project.
10:25:29 <shachaf> Intel is back at it with Larrabee?
10:25:35 <jix> The only reason I can think of why they didn't went with x86 in the first place is that an ARC core is smaller than what intel had at that time
10:26:23 <int-e> (The timing makes sense actually... now that we want to do raytracing with (I suspect) hardly predictable memory access patterns, the SIMT model will run into severe problems.)
10:26:51 <shachaf> int-e: That page is very ambiguous about it.
10:26:52 <int-e> wib_jonas: The ones with the 0x8086 vendor id.
10:27:06 <shachaf> Or rather it's not ambiguous enough. Is there any definite connection to Larrabee?
10:31:11 <int-e> I don't find any tangible evidence of that connection either.
10:31:18 <int-e> Still, it's Intel ;-)
10:33:32 <int-e> And anyway, it definitely *tried*, which was my main point.
11:01:28 -!- anima has joined.
11:01:36 -!- anima has quit (Client Quit).
11:08:00 <cpressey> <int-e> But I'm definitely not approaching this from a logical perspective. My first encounter of combinatory logic was as a model of computation. <-- That would seem to be the dominant paradigm for it these days. But I'm interested in the logical perspective of it atm. I guess you can write proofs in SKI by treating it like the Hilbert system it was derived from. But you can't use the deduction theorem
11:08:02 <cpressey> for brevity, you have to write it all out in full.
11:08:38 <cpressey> It sounds awful, but it also sound like you could "compile" a sentence in first-order logic, into it.
11:09:50 <wib_jonas> my first encounter of combinatory logic was unlambda
11:09:56 <cpressey> Rather I think I mean, "compile" a proof written in natural deduction style in FOL, into it.
11:12:19 <cpressey> "Under the Curry–Howard correspondence, the above conversion process for the deduction meta-theorem is analogous to the conversion process from lambda calculus terms to terms of combinatory logic" oh. Well. Okay then
11:12:24 <int-e> cpressey: W makes perfect sense if you have an explicit rule for duplicating premises in a sequent
11:13:13 <int-e> the C f x = f x x one
11:13:51 <wib_jonas> cpressey: see https://esolangs.org/wiki/Combinatory_logic
11:13:54 <int-e> (is there another?)
11:15:15 -!- arseniiv has joined.
11:15:39 <cpressey> I was just hoping you weren't referring to some System W that I'd never heard of. Anyway yes. W is dup and C is swap and this is Forth
11:19:52 <cpressey> So if the answer to my (unspoken) question "What's one of the simplest languages in which a proof can be stated and mechanically checked?" is "SK-calculus" then I guess my question becomes "How complex would a compiler from a tolerable proof language, to SK-terms, be?"
11:20:21 <myname> that depends on what you'd call tolerable
11:20:28 <myname> haskell to SK should be pretty easy
11:20:59 <myname> like, we do that manually in first semester here
11:21:20 <cpressey> You convert proofs written in Haskell into proofs written in SKI-calculus?
11:22:08 <myname> not proofs as such but small programms to lambda calculus and lambda calculus to SKI
11:22:19 <myname> removing I should be fairly easy
11:29:45 <wib_jonas> I only remember the bird name of two combinators really: S is seregély and K is vércse
11:30:16 <wib_jonas> also, do we have a link from the wiki to the crocodile family interpretation of lambda calculus_
11:31:32 <myname> aren't those alligators?
11:32:09 <myname> K is clearly for cancel
11:34:05 <Taneb> wib_jonas: what is that?
11:35:13 <esowiki> [[Lambda calculus]] https://esolangs.org/w/index.php?diff=66657&oldid=58720 * B jonas * (+732) Alligator eggs
11:35:54 <myname> I don't really like them that much
11:37:55 <int-e> Birdlife: Kestrels compete with starlings for nest cavities
11:38:08 <int-e> I didn't know that there was so much competition in the SK world.
11:41:03 <esowiki> [[Lambda calculus]] https://esolangs.org/w/index.php?diff=66658&oldid=66657 * B jonas * (+16) /* External resources */
12:22:43 <esowiki> [[Deadfish~]] M https://esolangs.org/w/index.php?diff=66659&oldid=66653 * A * (-9) /* Implementation */
12:49:42 <esowiki> [[Wagon]] https://esolangs.org/w/index.php?diff=66660&oldid=66656 * Chris Pressey * (+1032) Create partially-filled-out table of primitive Wagon macros.
12:58:59 <esowiki> [[Wagon]] https://esolangs.org/w/index.php?diff=66661&oldid=66660 * Chris Pressey * (+1074) Finish the primitives stable. No longer a stub, I think.
14:19:38 <esowiki> [[User:Camto]] M https://esolangs.org/w/index.php?diff=66662&oldid=60398 * Camto * (+19) Lmao
14:20:56 <esowiki> [[User:Camto]] M https://esolangs.org/w/index.php?diff=66663&oldid=66662 * Camto * (+6) Rewording
14:24:02 <esowiki> [[User:Camto]] https://esolangs.org/w/index.php?diff=66664&oldid=66663 * Camto * (-70) Friendship ended with OOT Now Thue is my best friend
14:24:32 <esowiki> [[User:Camto]] M https://esolangs.org/w/index.php?diff=66665&oldid=66664 * Camto * (+6) Aha
14:26:14 <esowiki> [[User:Camto]] M https://esolangs.org/w/index.php?diff=66666&oldid=66665 * Camto * (+7) BF dialecs
14:57:44 -!- cpressey has quit (Quit: ...).
15:25:21 -!- imode has joined.
15:47:59 -!- Lord_of_Life_ has joined.
15:49:45 -!- Lord_of_Life has quit (Ping timeout: 250 seconds).
15:49:46 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
16:26:05 -!- wib_jonas has quit (Remote host closed the connection).
17:02:03 -!- LKoen has joined.
17:09:41 -!- Vorpal has joined.
17:09:41 -!- Vorpal has quit (Changing host).
17:09:41 -!- Vorpal has joined.
17:16:54 -!- Vorpal has quit (Quit: ZNC - http://znc.sourceforge.net).
17:28:38 -!- LKoen has quit (Remote host closed the connection).
17:35:03 -!- FreeFull has joined.
17:38:58 -!- LKoen has joined.
17:45:52 <arseniiv> I had a thought to take from J its part-of-speech terminolody and strange rules (which I don’t know) and from Lojban its puristic non-european-centric approach to terminology and that to result in an obfuscation-first language but it would need more good ideas
17:46:07 -!- b_jonas has joined.
17:52:55 <b_jonas> épelung: a spelling reform for the English language where you spell words the same as the most corresponding etymologically related word in modern German or modern French
17:53:37 <b_jonas> this sounds like it probably has a canonical execution somewhere on the internet, but searching for "épelung" or "épeleung" shows that those words are quasi-nonexistent, and what else would you call this system?
17:56:01 <imode> https://repl.it/repls/ShadowyBumpyLinkedlist
17:59:01 <zzo38> I don't know what it is call, perhaps, is English without English.
18:10:16 <b_jonas> also, yesterday's SMBC http://www.smbc-comics.com/comic/mathematicians about matrix multiplication algorithm asymptotics is fun
18:25:51 -!- hppavilion[1] has joined.
18:57:49 -!- sprocklem has quit (Ping timeout: 250 seconds).
19:24:02 -!- arseniiv has quit (Ping timeout: 240 seconds).
19:26:08 -!- hppavilion[1] has quit (Ping timeout: 245 seconds).
19:55:11 -!- arseniiv has joined.
19:56:30 <arseniiv> oh int-e I’ve just read what you @told that time
20:24:30 <zzo38> Do you know how to make text formatting in PostScript? To implement printer output in the implementation of Z-machine in PostScript, I should know how to do that.
20:36:31 -!- LKoen has quit (Remote host closed the connection).
20:41:08 -!- LKoen has joined.
20:41:21 -!- LKoen has quit (Remote host closed the connection).
20:55:44 <Cale> .oO(A legendary land that enters untapped and taps for one mana of any colour that could not be produced by your other mana in play.)
20:56:28 <Cale> other lands* in play
20:56:37 <zzo38> OK, that might do.
20:56:42 <zzo38> Is there such a card?
20:56:54 <Cale> Would be kind of interesting
20:57:28 <shachaf> Any lands on the battlefield or any lands you control?
20:58:01 <Cale> lands you control, probably?
20:58:01 <shachaf> Can it also be tapped for colorless?
20:59:16 <Cale> Any lands on the battlefield (including your opponents') might make it unusable
20:59:51 <Cale> I don't think it'd be able to tap for colourless, but obviously that could be a variation on the idea
21:07:08 <zzo38> If you have more than one land with that ability, then what? Rule 106.7 doesn't seem to mention if they interfere with each other in this way.
21:07:18 <zzo38> (Although, rule 106.7 could be fixed so that it does work.)
21:08:11 <shachaf> zzo38: Well, it's a legendary land anyway.
21:08:19 <zzo38> Yes, but there are still ways to work around that.
21:08:45 <zzo38> (e.g. Mirror Gallery)
21:10:48 <Cale> Probably it should be considered a land that could produce mana of any colour, so that it shuts off any other copies of itself entirely.
21:11:14 <Cale> (but yeah, there's a funny paradox there)
21:11:34 <shachaf> I don't think it's much of a paradox.
21:11:50 <shachaf> It is a bit different from other mana abilities.
21:12:12 <Cale> It's almost exactly Russell's paradox :D
21:12:58 <shachaf> Sure, but I meant that answers to this kind of question are established.
21:13:34 <zzo38> Note that rule 106.7 does not say only mana abilities or only activated abilities.
21:15:33 <Cale> Or how about a land that can produce 2 mana of any colour that you have no devotion to?
21:15:56 <zzo38> Yes, that is another possibility, I think.
21:16:00 <Cale> That might be too good for activated abilities...
21:16:10 <zzo38> O, yes, I suppose so
21:16:23 <zzo38> Maybe base it on color identity
21:18:45 <b_jonas> Cale: how does that behave if you have such a land and a Forest in play and the opponent has a Plains and an Exotic Orchard in play?
21:18:45 <zzo38> In RDF format, "add one mana of any color that no other land you control could produce" might be something like: [:add-mana [:choose [:and :color, [:not [:any-could-produce [:and :land, [:controller :you], [:not :this]]]]]]]]
21:20:32 <Cale> b_jonas: I'm not sure, does Exotic Orchard usually care about predicates that restrict mana abilities?
21:21:21 <Cale> b_jonas: "Exotic Orchard doesn’t care about any restrictions or riders your opponents’ lands (such as Ancient Ziggurat or Hall of the Bandit Lord) put on the mana they produce. It just cares about colors of mana."
21:21:22 <zzo38> Yes, that is another case. Rule 106.7 mentions Exotic Orchard as an example.
21:21:55 <b_jonas> Cale: or more simply, how does it work if you have that land and a Forest and Reflecting Pool in play, and the opponent has four Plains?
21:22:02 <zzo38> But that what you quoted is clear enough from the rules I think, but it is not relevant to the case you have here
21:23:38 <Cale> ah, right, it does actually care about the state of the cards in play
21:23:56 <Cale> Lands that produce mana based only on what other lands “could produce” won’t help each other unless some other land allows one of them to actually produce some type of mana. For example, if you control an Exotic Orchard and your opponent controls an Exotic Orchard and a Reflecting Pool, none of those lands would produce mana if their mana abilities were activated. On the other hand, if you control a Forest and an Exotic Orc
21:23:57 <Cale> hard, and your opponent controls an Exotic Orchard and a Reflecting Pool, then each of those lands can be tapped to produce Green. Your opponent’s Exotic Orchard can produce Green because you control a Forest. Your Exotic Orchard and your opponent’s Reflecting Pool can each produce Green because your opponent’s Exotic Orchard can produce Green.
21:25:24 <Cale> But yeah, it's an additional weird twist when it's "can't produce"
21:26:30 <zzo38> Yes, all of that you mentioned is what would be done by rule 106.7. But, yes, the "can't produce" can result in no stable result, it seem like.
21:29:54 <zzo38> (I would think that the RDF code I mentioned probably wouldn't compile (if a compiler for it were implemented), or if it does compile, result in an infinite loop or stack overflow.)
21:31:50 <Cale> There are a few sensible ways that one could clarify what happens, like explicitly disallowing cycles in the determination of whether an ability can produce mana of a given type.
21:32:25 <zzo38> Yes, that was also my idea about how to amend rule 106.7
21:32:59 -!- sprocklem has joined.
21:34:15 <b_jonas> I was thinking that if you put this effect into the triggered ability of a Growth-like enchantment, maybe it becomes impossible to make a cycle, but I'm not really sure
21:37:03 <zzo38> Since that triggered ability is not an ability of a land, then it might work. Still, I think the rule should be amended in case
21:38:02 <esowiki> [[Unlambda]] https://esolangs.org/w/index.php?diff=66667&oldid=51370 * B jonas * (+312) /* External resources */ IOCCC winner interpreter
21:39:17 <b_jonas> zzo38: right, but it's hard to know whether there is a way to turn it into a land, or have an ability that cares about what mana some non-land permanents could produce, now or in future cards
21:39:46 <zzo38> Yes, I thought of that, which is why the rule should be amended anyways in case
21:40:01 <b_jonas> Imprisoned in the Moon can turn an existing permanent into a land
21:40:54 <zzo38> Although it deletes that permanent's abilities, too.
21:41:52 <b_jonas> yes, that's why I think that doesn't help
21:45:33 <zzo38> (My own opinion is the rules ought to support combinations that do not currently exist.)
21:46:10 <zzo38> I also made up this land card (based on the story of the GURPS I have played): Sun Town {-} Legendary World Land ;; Vehicles cannot enter the battlefield. ;; At the beginning of each end combat step, end the turn. ;; {T}: Add {C}. ;; {1}, {T}: Add {W}.
21:47:11 <b_jonas> Song of the Dryads is another such card
21:48:28 <zzo38> Yes, but rule 305.7 causes its abilities to be deleted.
21:49:51 <zzo38> Still, if something else can grant it an ability, then it can be kept and rule 305.7 only deletes the abilities due to its own text.
21:52:44 <Cale> Wow, vehicle hate
22:52:33 -!- imode has quit (Quit: WeeChat 2.6).
22:57:54 -!- imode has joined.
23:00:13 -!- tromp has quit (Remote host closed the connection).
23:11:12 -!- FreeFull has quit.
23:24:53 -!- arseniiv has quit (Ping timeout: 246 seconds).
23:35:58 -!- Sgeo_ has joined.
23:39:37 -!- Sgeo__ has quit (Ping timeout: 268 seconds).
23:52:08 -!- tromp has joined.
23:56:26 -!- tromp has quit (Ping timeout: 240 seconds).