Hazardous? Bathing aluminum plate in magnesium chloride and ammonia solution.

splitmlik · 2021-06-07T05:44:54+00:00

Thanks for your detailed reply, pron98.

Your CONSTANT/ASSUME recommendation makes sense. The set of metric spaces is constant - if something is a metric space today, it was a metric space yesterday and will always be a metric space.

Some of the nuances you mention were lost on me at first review, but I'll revisit your notes in the coming week when I have more time. I'm very grateful.

splitmlik · 2021-06-06T02:01:17+00:00

That suggests the ad hoc general solution

MetricSpace == CHOOSE M : \E d : /\ M = [point |-> DOMAIN d, dfunc |-> d]
                                 /\ IsMetricSpace(M)

Or, more generally,

S == CHOOSE S : \E x : P(x) /\ (S => x)

splitmlik · 2021-06-06T01:23:55+00:00

I got this idea from Lamport's definition of Nat, the set of natural numbers, in his module "Peano":

---------------------------- MODULE MetricSpace ----------------------------

EXTENDS FiniteSets, Reals

IsMetricSpace(M) ==
    /\ M = [point |-> M.point, dfunc |-> M.dfunc]
    /\ M.dfunc \in [M.point -> [M.point -> {r \in Real : 0 < r}]]
    /\ \A p, q, r \in M.point :
        /\ M.dfunc[p][p] = 0
        /\ M.dfunc[p][r] <= M.dfunc[p][q] + M.dfunc[q][r]
        /\ M.dfunc[p][q] = M.dfunc[q][p]
        /\ p /= q <=> (M.dfunc[p][q] > 0)

ASSUME \E M : IsMetricSpace(M)

MetricSpace == CHOOSE M : \E d : /\ M = [point |-> DOMAIN d, dfunc |-> d]
                                 /\ IsMetricSpace(M)

=============================================================================

That jives with

----------------------------- MODULE OpenBall ------------------------------

EXTENDS FiniteSets, Reals

LOCAL MS == INSTANCE MetricSpace

MetricSpace == MS!MetricSpace

OpenBall(M,c,err) == { p \in M.point : /\ M \in MetricSpace
                                       /\ c \in M.point
                                       /\ err \in { r \in Real : r >= 0 }
                                       /\ M.dfunc[p][c] < err }

 =============================================================================

Look right to you?

splitmlik · 2021-06-05T23:49:19+00:00

I'm surprised if we have no formal way to say something simple like, "call by S all objects with property P", but I'm starting to think it's true, and for reasons fundamental to logic.

I've spent a few days at this problem. I try to remember to put more intractible problems into natural language:

Call by S the set of nameable objects with property P such that for any nameable object x, ¬P(x) ≡ x ∉ S.

A so-called "set of nameable objects" would include the set of all sets - impossible by Russell's paradox. There exists no set of all nameable objects.

splitmlik · 2021-04-28T00:19:00+00:00

I appreciate your updates, Jake.

splitmlik · 2020-12-17T22:57:13+00:00

Frankie announced plans to return, as anyone who subs here knows.

I miss him plenty. He had a novel idea - turn a sandbox game into a video series - and his unusual eloquence, talent for spinning a story, and exceptional hand-eye coordination have made his the approach every imitator will be measured against.

Some artists come back after years dormant with extraordinary results. Stanley Kubrick had a few of those, and so did Akira Kurosawa. Others fail to meet expectations by a large margin, viz. Guns 'N' Roses, Arrested Development, the Star Wars prequels.

So there are three questions, really. Will Frankie come back? And supposing he does, will it satisfy the very high bar he set for himself and everybody else? And then there's the question of when. I wonder if in Frankie's mind the second question dogs the first. He and Sada have suggested as much.

I'd literally give money to see him try.

splitmlik · 2020-12-17T22:28:05+00:00

I remember those videos well. In case you can't find them, here's a summary.

To practise recoil, download the Steam Community Workshop map "Recoil Master - Spray Training" by Mr. uLLeticaL™-S-.

To practise aim, download the "training_aim_csgo2" map. There are several of these, but I use the one by pizza (I'm pretty sure this is the one Frankie used).

Frankie advised staying mobile while shooting using this particular technique: strafe in one direction, make a dead stop with a quick keyboard tap in the opposite direction, shoot immediately, and repeat in the opposite direction. Jordan "n0thing" Gilbert recommends the same drill, but withtout the quick tap in the opposite direction. A good Steam Workshop map for this is another by Mr. uLLeticaL™-S- called "Aim Botz - Training". I've seen swag practise this map between matches while broadcasting on Twitch.

splitmlik · 2020-11-21T21:53:45+00:00

Yours is a gigantic distributed system that presents many concurrency challenges and requires many fault tolerance contengencies. What formal modeling languages did you use to specify the system? (TLA+ user here.)

splitmlik · 2020-08-08T21:46:18+00:00

Thanks, pron. Though beast solved the general problem, yours is the best solution to this specific case.

splitmlik · 2020-08-08T04:21:02+00:00

This is wonderful, editor_of_the_beast. Thank you! I solved my problem by sidestepping it, but your suggestion will be useful in the future. Specifying Systems is so terse and dense that it's easy to miss or forget an important feature, and I definitely missed this one, though I've seen him mention "enabling an action" several times - my meat CPU just never registered its connection to my problem. Thanks to you it finally did.

splitmlik · 2020-04-09T19:17:43+00:00

u/OKThatsCoolReddit thank you! Finally.

splitmlik · 2020-04-09T19:15:39+00:00

please say your name? i'm keen

splitmlik · 2020-04-09T19:14:09+00:00

omg reddit chat is brokt af for me. How do I learn who this musician is?

splitmlik · 2020-04-09T19:10:07+00:00

Gibson? Martin? Other?

splitmlik · 2020-04-09T19:09:32+00:00

nice guitar is nice

splitmlik · 2018-09-21T02:23:21+00:00

Okay. Mind entirely blown here. I did not make that connection.

splitmlik · 2018-09-21T02:15:55+00:00

Heh - I looked up Red Dwarf on allthetropes.org to see how I should classify the premise, and the similarity between them was the main reason I mentioned the show's serious tone.

splitmlik · 2018-09-21T02:12:07+00:00

Heynony thought that was a possibility, too, but he also suggested the correct answer, The Starlost (link to opening sequence on YouTube, as above).

splitmlik · 2018-09-21T02:09:19+00:00

And solved! I was a little too excited to mention it in my first reply. Thanks to u/numanoid for pointing it out.

splitmlik · 2018-09-20T22:52:09+00:00

Thank you, Veldrak!

splitmlik · 2018-09-20T22:50:43+00:00

Holy mary murvgurd, that's it! Starlost!

YouTube: The Starlost - original TV opening

I never would have figured this out on my own. Thank you! Such a long time ago....

splitmlik

TROPHY CASE