[with mostly up-to-date semantics, but this year I gave up on approximating (≲), which is \refines in the suite, in the language itself; the following seems to be more productive (for technical reasons related to using an implementation-specific total order):
FNull <= f && f <= f NB. <= is discrete
where equality of closures is pessimistic, based on lexical source and equality of the captured environments, so:
f <= g ==> f \refines g
f \refines g <=> f`x ~ g`x
using (`) as application]
it may help to read chapter 2 of https://www.cs.utoronto.ca/~hehner/aPToP/ for the basic data structure inspiration; another alternate syntax would be to stick with his (for data; this all grew out of wishing to treat functions very differently)
I've also been inspired by the Boom Hierarchy (in terms of trying to put laws, especially distributive/module laws, first) but as my areas of interest don't run to commercial proggys, I haven't found a use for the bag level. [Lamport stuttering, otoh, suggests that ordered but absorbing would be a useful abstraction — and I think that'd easily be buildable on top of this basis]
if I can remember out my creds for oortcloud, and it would help, I can make available a browser-based precedence tool that translates expressions in the JUNK syntax into their abstract trees.
Sorry, waiting for w.a.o to debug themselves, using it as an us-heirs-approved (or rather judgement-mostly-withheld) pro-bono to the su-heirs-approved alternative (which has a largely orthogonal feature set)
It does smell like there is something here*, but judging by your scleras (shall we say, sclera-pupillary boundaries) we should focus on the GR-QM convo, just a tad more..
(Where tad = some kind of dot product with this convo)
Percival: Arithmetical properties of strongly chaotic motion ?
TIL Scwhinger was on the Bonaparte counter-clockual programme...
Any chance you could sketch to me why SM works with SR but not GR? Curvature?
[squinting hard enough, is the Wick Theorem related to how algebraically, given pairs (2-things, and hence rel'ns) one automatically gets all finite n-things?]
[another squint: separated at birth: space-ordered vs normal-ordered, and all the sign gymnastics* in computer graphics geometry, where re-ordering matters and vertices are connected by digons of two half-edges?]
is there anything related to the notion that one might have a bunch of geodesic paths connecting events, but that we might apply creation and annihilation to these as well, so fewer geodesics would lead to positive curvatures and more to negative?
* what I like about my algebraic CS model is that I often skim systems papers, and think, "oh, this is just exploiting this particular instance of distributivity..."
