Backward through Time, Algebraically

# Backward through Time, Algebraically
Source: [https://arxiv.org/html/2608.17087](https://arxiv.org/html/2608.17087)
© none

###### Abstract\.

Linear temporal logic is a modal extension of propositional logic that allows one to state how a system should behave over time\. Its canonical domain is the booleans, but discretely\-valued judgements are of little use in steering softly\-valued systems \(neural policies, adaptive controllers, sequence models,etc\.\)\. In such cases, the goal formula’s \(dis\)satisfaction becomes a training signal, and differentiability becomes a prime concern\. Candidate differentiable semantics abound, but navigating them is tricky\. Implementations, where available, are shallow embeddings, demanding an upfront commitment to a single semantic algebra and its \(usually implicit\) conduct\. The paper casts the reader as a functional programmer asked to come to terms with this predicament, and refusing\. Out of that refusal comes an evaluation engine that is algebra\-generic and amenable to differentiation, together with an executable specification of the algebras it can accept\. Various algebras are implemented and audited for their behavior, both forward and backward\. Each algebra turns out to be a choice of which direction to disappoint, and how\. Everything described \(and more\) is part of the PyTorch librarytelos, to be found at[https://github\.com/konstantinosKokos/telos](https://github.com/konstantinosKokos/telos)\.

## 1\.Syntax

You stumble upon a logical formula, and a mostly innocuous one at that; it contains only familiar propositional connectives, plus a few funny symbols\. Some vague but undeniable authority tasks you with evaluating the formula as it wades throughtime\. You do not flinch\. The funny symbols attain their denotation as the problem makes its way into your memory\. It is old, and all but solved\. You dust off the authoritative scriptures of old\([22](https://arxiv.org/html/2608.17087#bib.bib1)\)and recall the syntax oflinear temporal logic:

ϕ,ψ:=⊤\|⊥\|α​\|¬ϕ\|​ϕ∧ψ\|​ϕ∨ψ\|​ϕ→ψ​\|𝒳​ϕ\|​ϕ​𝒰​ψ\\phi,\\psi:=\\top\\ \|\\ \\bot\\ \|\\ \\alpha\\ \|\\ \\neg\\phi\\ \|\\ \\phi\\wedge\\psi\\ \|\\ \\phi\\vee\\psi\\ \|\\ \\phi\\to\\psi\\ \|\\ \\mathcal\{X\}\\phi\\ \|\\ \\phi\\mathcal\{U\}\\psiOf the two non\-classical operators, one makesinstantsense;𝒳​ϕ\\mathcal\{X\}\\phi\(read:nextϕ\\phi\) is justϕ\\phi, one tick ahead of whenevernowis\. The other takes a few momentslonger;ϕ​𝒰​ψ\\phi\\mathcal\{U\}\\psi\(read:ϕ\\phiuntilψ\\psi\) turns out to be two promises uttered at once: that a moment favorable toψ\\psiexists, and thatϕ\\phicarries the burden of truth every tick of the way, arrival included\. One symbol isa step; the other isa search, within a search\. Two more symbols sometimes travel in the same circles:ℱ​ϕ\\mathcal\{F\}\\phi\(read:finallyϕ\\phi\), and𝒢​ϕ\\mathcal\{G\}\\phi\(read:globallyϕ\\phi\)\. Both are just𝒰\\mathcal\{U\}in disguise\. The former is the search relieved of its side condition,ℱ​ϕ:=⊤𝒰​ϕ\\mathcal\{F\}\\phi:=\\top\\mathcal\{U\}\\phi; the latter denies a future whereϕ\\philapses,𝒢​ϕ:=¬ℱ​¬ϕ\\mathcal\{G\}\\phi:=\\neg\\mathcal\{F\}\\neg\\phi\. The two find use in specifying temporal conduct:safety, demanding that nothing bad ever happens, andliveness, that something good eventually does\([12](https://arxiv.org/html/2608.17087#bib.bib2)\)\.

On its own, the formula is only half an instruction\. The other half is atraceτ\\tau, the world the formula speaks of\. The trace is a two\-dimensional assignment; it says what the value of each atomα\\alphais at each ticktt, over a finite time window ofTTticks\. You pair the two together and get the full instruction, ajudgementτ⊧ϕ\\tau\\models\\phi\. You roll up your sleeves and, honestly, it doesn’t seem like much of a task; pattern match onϕ\\phi, step the trace to the right on𝒳⋅\\mathcal\{X\}\\cdot, sweep from the far end for⋅𝒰⋅\\cdot\\mathcal\{U\}\\cdot,etc\.

Just as you announce your compute\-readiness, the data comes in\. It is not what you expected\. For starters, the trace matrix is not boolean\. It contains numbers of somedtype=float32, and carries a flag that readsrequires\_grad=True; a PyTorch\([21](https://arxiv.org/html/2608.17087#bib.bib3)\)Tensor\. You flinch\. The numbers, you learn, are freshly squeezed out of a neural network, and that flag is the umbilical cord that keeps them attached to the machinery that produced them\. Whoever sent them your way does not much care what the formula’s verdict is right now; they intend tomakeit favorable by repeatedly nudging the trace’s producer, for as long as that takes\. You relent; you are picky and precious about your instruments, but concessions are sometimes necessary\. The grammar ports in an hour’s work, sugar included, your ADTs now emulated via abstract class inheritance\. Your first semantic instinct is to round: call anything above one halfTrue, and the scriptures are back in business\. The rounding restores your truth\-values, and it costs only everything\. The step function’s derivative flickers between zero and infinity; whatever loss is built downstream of your verdict cannot find its way through the rounding and back into the network\. Your mistake was brandishing a verdict \(whetherthe formula is satisfied\) when you were asked for feedback \(howsatisfied it is\); feedback that must additionally bedifferentiablein every number the trace contains\. The voice did not speak of bools; it spoke ofvalues, writ large\. You do your due diligence perusing the bazaar of fuzzy logics\([10](https://arxiv.org/html/2608.17087#bib.bib4)\)\. You get dizzy; there’s a few options too many, and you’re not invested enough to make the call yourself\. You shrug;“I’ll just make this algebra\-generic and let the user pick, I guess”\.

## 2\.Semantics, Abstract

You gather and superimpose the go\-to algebras and blank out the places where they diverge\. The impression left underneath is a blueprint of their shared abstraction: acarrierwith twodistinguished elements, standing in for⊤\\topand⊥\\bot, and a pointwise operation over that carrier for each logical connective\. You don’t let backprop obligations dissuade you from purity and peace of mind; PyTorch can deal with the effectful book\-keeping on its own\. You start writing111ReadFnas shorthand for the unutterableCallableannotation\. ReadTas shorthand fortorch\.Tensor\. Consider syntax errors a deliberate attempt at condensation \(most of them are\)\.:

classAlgebra\(abc\.ABC,torch\.nn\.Module\):

top:T;bot:T

defmeet\(self,x:T,y:T\)\-\>T:\.\.\.

defjoin\(self,x:T,y:T\)\-\>T:\.\.\.

defimpl\(self,x:T,y:T\)\-\>T:\.\.\.

defneg\(self,x:T\)\-\>T:\.\.\.

The names are borrowed from lattice theory on credit; whether an algebra earns them is a question momentarily deferred\. But what oftime? The funny symbols are still semantically adrift\. Anchoring them takes little effort; you know well that the “temporal” part is just first\-order quantification \(i\.e\., iteration\) in disguise\. Time enters the play as the last tensor axis, and every temporal need reduces to sweeping some operation along it:

defscan\(fn:Fn\[\[T,T\],T\]\)\-\>Fn\[\[T\],T\]:

deff\(x:T\)\-\>T:

returntorch\.stack\(list\(accumulate\(x\.unbind\(\-1\),func=fn\)\),dim=\-1\)

returnf

deffold\(fn:Fn\[\[T,T\],T\],initial:T\)\-\>Fn\[\[T\],T\]:

deff\(x:T\)\-\>T:

returnreduce\(fn,x\.unbind\(\-1\),initial\)

returnf

defspan\(fn:Fn\[\[T\],T\],neutral:T,bot:T\)\-\>Fn\[\[T\],T\]:

deff\(x:T\)\-\>T:

n=x\.size\(\-1\)

mask=torch\.triu\(torch\.ones\(n,n,device=x\.device\)\)\.bool\(\)

rows=torch\.where\(mask,x\.unsqueeze\(\-2\),neutral\)

returntorch\.where\(mask,fn\(rows\),bot\)

returnf

Armed with these, your algebra\-concocting recipe is finally complete:

classAlgebra\(abc\.ABC,torch\.nn\.Module\):

\.\.\.

defrunning\_meet\(self,x:T\)\-\>T:returnscan\(self\.meet\)\(x\)

defrunning\_join\(self,x:T\)\-\>T:returnscan\(self\.join\)\(x\)

defforall\(self,x:T\)\-\>T:returnfold\(self\.meet,self\.top\)\(x\)

defexists\(self,x:T\)\-\>T:returnfold\(self\.join,self\.bot\)\(x\)

defspan\_meet\(self,x:T\)\-\>T:returnspan\(self\.running\_meet,self\.top,self\.bot\)\(x\)

Note what has quietly transpired: the derived operations are spelled out once, in terms of the four abstract primitives and not much else\. You will lean on this harder than it may now appear; the definitions above are less of a default implementation and more of aspecificationthat just so happens to be runnable\.

## 3\.Interface

The sleeves, rolled up for a while now, finally meet their pattern match\. Evaluation is structural recursion over the formula, each case deferring to the algebra:

classModel\(torch\.nn\.Module\):

defforward\(self,A:Algebra,judgement:Judgement\)\-\>T:

\(trace,phi\)=judgement

defgo\(phi:Formula\)\-\>T:

matchphi:

caseVariable\(x\):

returntrace\[x\]

caseNegation\(Until\(AbstractTop\(\),Negation\(x\)\)\):

returnA\.running\_meet\(go\(x\)\.flip\(\-1\)\)\.flip\(\-1\)

caseNegation\(x\):

returnA\.neg\(go\(x\)\)

caseConjunction\(l,r\):

returnA\.meet\(go\(l\),go\(r\)\)

\.\.\.

caseNext\(x\):

returntorch\.nn\.functional\.pad\(go\(x\)\[\.\.\.,1:\],\(0,1\),value=A\.bot\)

caseUntil\(AbstractTop\(\),r\):

returnA\.running\_join\(go\(r\)\.flip\(\-1\)\)\.flip\(\-1\)

caseUntil\(l,r\):

returnA\.exists\(A\.meet\(A\.span\_meet\(go\(l\)\),go\(r\)\.unsqueeze\(\-2\)\)\)

returngo\(phi\)\[\.\.\.,0\]

Writing⟦⋅⟧\\llbracket\\cdot\\rrbracketto denote the evaluatorgounder some algebra and trace,𝒳⋅\\mathcal\{X\}\\cdotpads its unoccupied final tick with⟦⊥⟧\\llbracket\\bot\\rrbracket; a certain pessimism about the end of time that youelectto own\. The two aliases of𝒰\\mathcal\{U\}are amenable to compute\-friendly searches over suffixes,i\.e\., running reductions over reversed time;finallyandgloballythen sit only a primitive apart\. The more general⋅𝒰⋅\\cdot\\mathcal\{U\}\\cdotreads exactly as promised: every window ofϕ\\phiis pitted against its witnessψ\\psi, and the best outcome is kept\. The evaluator is thus complete, blissfully oblivious of algebra peculiarities anddtypecommitments; it shall interpret every formula under every algebra ever written \(including the ones yet to be\)\.

## 4\.Semantics, Concrete

Before celebrating generality, you reconcile with the scriptures through a quick regression test\. To no one’s surprise, boolean semantics are trivial to recover:

classBoolean\(Algebra\):

top,bot=torch\.tensor\(True\),torch\.tensor\(False\)

defmeet\(self,x,y\):returnx&y

defjoin\(self,x,y\):returnx\|y

defimpl\(self,x,y\):return~x\|y

defneg\(self,x\):return~x

Instantiate, evaluate and the answers come back as promised\. Whatever the abstraction may end up costing, it won’t be correctness; the scriptures have just been demoted to a special case of the blueprint\. Confident, you return to the fuzzy bazaar, freshly relieved of the burden of choice\. You begin transcribing; first a helper:

classFuzzyBase\(Algebra,abc\.ABC\):

top,bot=torch\.tensor\(1\.\),torch\.tensor\(0\.\)

defneg\(self,x\):returnself\.top\-x

Then, the probabilist’s default:

classProduct\(FuzzyBase\):

defmeet\(self,x,y\):returnx\*y

defjoin\(self,x,y\):returnx\+y\-x\*y

defimpl\(self,x,y\):returntorch\.where\(x==self\.bot,self\.top,\(y/x\)\.clamp\(max=1\)\)

The evaluator obliges; every judgement now returns a number that quacks like a probability\.

Back to the deferred credit check; the namesmeetandjoincame with lattice\-theoretic obligations\. Associativity, commutativity and monotonicity you wave through, and involution and the De Morgan dualities with them; all hold universally in this corner of the world, a fact audited and asserted\. The other properties of interest are recited below:

idempotenceabsorptiondistributivitycomplementation⟦ϕ∧ϕ⟧=⟦ϕ⟧\\llbracket\\phi\\wedge\\phi\\rrbracket=\\llbracket\\phi\\rrbracket⟦ϕ∧\(ϕ∨ψ\)⟧=⟦ϕ⟧\\llbracket\\phi\\wedge\(\\phi\\vee\\psi\)\\rrbracket=\\llbracket\\phi\\rrbracket⟦ϕ∧\(ψ∨ξ\)⟧=⟦\(ϕ∧ψ\)∨\(ϕ∧ξ\)⟧\\llbracket\\phi\\wedge\(\\psi\\vee\\xi\)\\rrbracket=\\llbracket\(\\phi\\wedge\\psi\)\\vee\(\\phi\\wedge\\xi\)\\rrbracket⟦ϕ∧¬ϕ⟧=⟦⊥⟧\\llbracket\\phi\\wedge\\neg\\phi\\rrbracket=\\llbracket\\bot\\rrbracket⟦ϕ∨ϕ⟧=⟦ϕ⟧\\llbracket\\phi\\vee\\phi\\rrbracket=\\llbracket\\phi\\rrbracket⟦ϕ∨\(ϕ∧ψ\)⟧=⟦ϕ⟧\\llbracket\\phi\\vee\(\\phi\\wedge\\psi\)\\rrbracket=\\llbracket\\phi\\rrbracket⟦ϕ∨\(ψ∧ξ\)⟧=⟦\(ϕ∨ψ\)∧\(ϕ∨ξ\)⟧\\llbracket\\phi\\vee\(\\psi\\wedge\\xi\)\\rrbracket=\\llbracket\(\\phi\\vee\\psi\)\\wedge\(\\phi\\vee\\xi\)\\rrbracket⟦ϕ∨¬ϕ⟧=⟦⊤⟧\\llbracket\\phi\\vee\\neg\\phi\\rrbracket=\\llbracket\\top\\rrbracket
Product’s audit is brief, and unflattering\. Idempotence immediately bounces back:x∗xx\*xagrees withxxnowhere but at the domain’s edges\. A formulaϕ\\phipinned atxxgets⟦𝒢​ϕ⟧=xT\\llbracket\\mathcal\{G\}\\phi\\rrbracket=x^\{T\}; the value ofalwaysis now tied to its duration\. Absorption and distributivity fail on the same grounds, with more bureaucracy and no insights to show for it\. Complementation fares no better:x∗\(1−x\)x\*\(1\-x\)hovers consistently above⟦⊥⟧\\llbracket\\bot\\rrbracket, while the middle, supposedly excluded, is in fact perfectly included\. Product, in short, has earned almost none of its borrowed names\. No matter; in assuming no law, the evaluator couldn’t have broken any\. You record the audit all the same, and give in to your propensity for automation\. Each law is a function of the function\(s\) it constrains:

defidempotent\(op:Fn\[\[T,T\],T\]\)\-\>Fn\[\[T\],bool\]:

deff\(x:T\)\-\>bool:returntorch\.allclose\(op\(x,x\),x\)

returnf

defabsorption\(meet:Fn\[\[T,T\],T\],join:Fn\[\[T,T\],T\]\)\-\>Fn\[\[T,T\],bool\]:

deff\(x:T,y:T\)\-\>bool:

returntorch\.allclose\(meet\(x,join\(x,y\)\),x\)&torch\.allclose\(join\(x,meet\(x,y\)\),x\)

returnf

Strict equality makes way for lax negotiation, an artifact of finite precision arithmetic\. Auditing becomes a guided search for counter\-examples: a loop of every law against every algebra, over a batch of \(initially\) random tensors\([3](https://arxiv.org/html/2608.17087#bib.bib5);[15](https://arxiv.org/html/2608.17087#bib.bib6)\)\.

Tests in place, the rest of the wares transcribe just as quickly, and audit just as unevenly \(Table[1](https://arxiv.org/html/2608.17087#S4.T1)\)\.

Table 1\.Common algebras, audited\.Diff\.marks algebras differentiable in their inputs;Train\.marks parametric families whose parameter is itself a learnable tensor\. Lettered entries hold only as indicated by the corresponding note\. Law entries are checked mechanically\.aimplis not differentiable in its first argument\.basp→0p\\to 0\.casp→∞p\\to\\infty\.datp=1p=1\.eforp≥1p\\geq 1\.

Booleansits at the top; the only lattice proper\. Its descendants below trade lawfulness for the spoils of differentiability\. On \{0, 1\}\-valued traces, the boundary conditions leave zero freedom: every algebra on the unit interval agrees withBooleanexactly \(modulo the necessary type coercion\)\. It is in the interior where variation lives\.RobustnessandLSEstand apart from the rest, having wandered off the unit interval altogether\. These are imported fromsignal temporal logic\([16](https://arxiv.org/html/2608.17087#bib.bib7);[6](https://arxiv.org/html/2608.17087#bib.bib8);[13](https://arxiv.org/html/2608.17087#bib.bib22)\); their carrier is the extended real line and their negation plain arithmetic:⟦¬ϕ⟧=−⟦ϕ⟧\\llbracket\\neg\{\\phi\}\\rrbracket=\-\\llbracket\\phi\\rrbracket\. The lower half of the table hosts the generalized, parametric families\([10](https://arxiv.org/html/2608.17087#bib.bib4)\): each carries a parameterppdeclared as a learnable tensor, so that the algebras themselves \(not just the traces they judge\) can be subject to numerical optimization\. Varyingppsmoothly deforms an algebra, up to the limit where it meets a law\-abiding neighbor: Frank, Aczél\-Alsina, Dombi and Yager all harden to Gödel, and LSE to Robustness\. Looking back, you gleefully note how the abstract machinery has been doing double duty as a reference manual, and its instantiations now serve as literature review\.

## 5\.Semantics, Faster

Alas, utility stands in opposition to generality\. As traces outgrow politely\-sized examples, the evaluator buckles under unfavorable asymptotes: spans quadratic in memory, folds and scans linear in depth, each tick a round\-trip through the interpreter\. Correct and general, sure\. But also heavy and slow\.

The memory footprint seems impossible to tackle\. But what of time? The offense committed needs some clarifying; it’s not theworkthat’s at fault\. Each of theTTticks has to be read once, and each is indeed read exactly once\. The culprit is the serial nature ofdepthiteration: not the number of steps taken, but the number of steps spent in wait\. Each fold treads like a procession, single file across a device built millions of lanes wide\. Mid\-diagnosis, you pause and instinctively shift your attention towards the audit table and the laws unceremoniously inscribed therein\. Your mind’s eye rests on a column loudly absent:associativity\. For the logician, a license to re\-bracket; for the engineer, a license to start tomorrow’s work today\([2](https://arxiv.org/html/2608.17087#bib.bib21)\)\. A fold free to regroup needs not proceed one tick at a time\. What it regroupsinto, though, is not for associativity to decide; the closed form, when one exists, depends on the rest of the algebra’s properties\.

Goedel, for instance, is idempotent; its meet is an extremum, and running extrema are long canonized builtins:

classGoedel\(FuzzyBase\):

\.\.\.

defrunning\_meet\(self,x\):returntorch\.cummin\(x,dim=\-1\)\.values

defrunning\_join\(self,x\):returntorch\.cummax\(x,dim=\-1\)\.values

The override here is less of an over\-rule and more of a claim of agreement with the fold it displaces\. Ordinarily one would owe a proof; here, the displaced fold could \(and stillcan\) run, so the claim simply joins the audit as one more law, searched for counter\-examples alongside the rest\. The two sides of overriding appeal to different sensibilities: one is optimization; the other is stating tiny little theorems that also happen to execute\.

Product, despite holding no special law, draws the same luck; its running meet is a cumulative product; kernel enough to also be found on the shelf\. The shelf stocks nothing for the running join, but doesn’t really need to; De Morgan’s law transforms a join into a negated meet over negated parts:

classProduct\(FuzzyBase\):

\.\.\.

defrunning\_meet\(self,x\):returntorch\.cumprod\(x,dim=\-1\)

defrunning\_join\(self,x\):returnself\.neg\(self\.running\_meet\(self\.neg\(x\)\)\)

Suspiciously,LSEfinds its kernel waiting on the same shelf, almost as if commissioned\([20](https://arxiv.org/html/2608.17087#bib.bib9);[7](https://arxiv.org/html/2608.17087#bib.bib24)\):

classLSE\(Algebra\):

\.\.\.

defrunning\_join\(self,x\):returntorch\.logcumsumexp\(self\.p\*x,dim=\-1\)/self\.p

The parametric families hold no idempotence, and no kernel awaits them by name\. Their meets, though, look eerily alike:

\.\.\.returntorch\.clamp\(1\-\(\(1\-x\)\*\*p\+\(1\-y\)\*\*p\)\*\*\(1/p\),min=0\.\)

\.\.\.returntorch\.exp\(\-\(\(\-torch\.log\(x\)\)\*\*p\+\(\-torch\.log\(y\)\)\*\*p\)\*\*\(1/p\)\)

\.\.\.return1/\(1\+\(\(\(1\-x\)/x\)\*\*p\+\(\(1\-y\)/y\)\*\*p\)\*\*\(1/p\)\)

You squint a bit, and the nested complexity begins to look less like variety and more like camouflage\. You reprise the opening trick: superimpose them, blank out the places where they diverge:

\.\.\.returng\_inv\(g\(x\)\+g\(y\)\)

What is left behind this time isaddition, albeit in different coordinates\. Each meet factors asg−1​\(g⁡\(x\)\+g⁡\(y\)\)g^\{\-1\}\(g\(x\)\+g\(y\)\)for some strictly decreasinggeneratorggwithg⁡\(1\)=0g\(1\)=0\([14](https://arxiv.org/html/2608.17087#bib.bib10)\); where a family’s meet saturates at00, its pseudo\-inverse clamps to match\. In generator coordinates the fold is a running sum;torch\.cumsumhas been there for you all along:

classArchimedean\(Algebra,ABC\):

defg\(self,x:T\)\-\>T:\.\.\.

defg\_inv\(self,x:T\)\-\>T:\.\.\.

defmeet\(self,x,y\):returnself\.g\_inv\(self\.g\(x\)\+self\.g\(y\)\)

defimpl\(self,x,y\):returntorch\.where\(x<=y,self\.top,self\.g\_inv\(self\.g\(y\)\-self\.g\(x\)\)\)

defrunning\_meet\(self,x\):returnself\.g\_inv\(torch\.cumsum\(self\.g\(x\),dim=\-1\)\)

defforall\(self,x\):returnself\.g\_inv\(self\.g\(x\)\.sum\(dim=\-1\)\)

The joins mirror through negation, courtesy of De Morgan duality, and the whole parametric wing gets to exercise its re\-bracketing license\. In hindsight, the move retroactively explains the shelf’s earlier generosity: a cumulative product is acumsumin−log\-\\logcoordinates, andlogcumsumexpcarries its generator loudly in its name\.Productnow quietly re\-parents, surrendering its hand\-written joins to the family it secretly belonged to all along\. One line of the listing was not asked for:implcomputes theresiduum, the largest value whose meet withxxstays at or belowyy; it fell out of the coordinates unbidden, and it retires a hand\-written implication in every family it touches\. Instantiating is now embarrassingly brief:

classLukasiewicz\(Archimedean,FuzzyBase\):

defg\(self,x\):return1\-x

defg\_inv\(self,s\):returntorch\.clamp\(1\-s,min=0\.\)

That is really the entire algebra; two lines of coordinates, everything else derived\.

The licenses reach⋅𝒰⋅\\cdot\\mathcal\{U\}\\cdotas well\. The general case wants a meet over every windowxt\.\.t′x\_\{t\.\.t^\{\\prime\}\}; there areT2T^\{2\}of those, and computing each on its own is how one arrives, honestly and carefully, at a cubic algorithm\. But windows sharing a start differ only in their end; each is a prefix of the next, and a single running sweep along a row delivers the whole family at once\. This is the triangular constructionspanhas been performing all along, for which no special license is needed\. What associativity buys is the sweep itself: handed a closed\-formrunning\_meet,span\_meetcollapses into one kernel launch over oneT×TT\\times Ttensor\.

Who, then, still keeps the fold? In the current catalogue, no one\. It now stands only where it first appeared: as a specification and a fallback, held in reserve for the algebras the evaluator promised to interpret, the ones yet to be written\. With time tamed, it is tempting to call the matter closed\.

## 6\.Semantics, Backward?

You yield to the temptation\. The setup is the minimal workable one: a formula encoding some preference, a sweep over algebras, an optimizable trace with the appropriate carrier\. The goal is simple: evaluate the formula, turn the value into a loss term, backprop to the trace, update it towards satisfaction\. Nothing breaks; the loss even descends… at a geological timescale\. Suspicious, you put a single backward pass under the loupe\. The feedback is differentiable, as requested; it is also rather empty\.

Emptiness takes three forms\. The first isselection\.GoedelandRobustnessrely on extrema, and their derivatives are indicator functions\([24](https://arxiv.org/html/2608.17087#bib.bib23)\)\. However long the trace or involved the formula, the backward pass singles out one tick of one atom, which then bears the computation’s entire credit; every other entry receives an exact zero\. The second issaturation\.Lukasiewiczrelies on repeated clamping: on traces of any serious length, outputs plateau and gradients are erased\. The third isdecay\.Productdistributes feedback credit among participants, across both time and \(syntactic\) space\. Regrettably, distribution does not counteract scarcity\. Chains of multiplications in the unit interval push values towards⟦⊥⟧\\llbracket\\bot\\rrbracket, and collapsing values beget collapsing gradients\. This suspiciously tidy taxonomy happens to be a theorem\([18](https://arxiv.org/html/2608.17087#bib.bib11);[14](https://arxiv.org/html/2608.17087#bib.bib10)\)\. Loosely, it claims that every continuous t\-norm is anordinal sum, glued together from two archetypes, anilpotentone and astrictone, with anidempotentone at the seams; saturation, decay, and selection, in that order\. The classification is exhaustive; there is no fourth alternative to look for\.

Two problems compound\. One you have just witnessed: standard fuzzy operators make for notoriously bad neural networks in their own right\([23](https://arxiv.org/html/2608.17087#bib.bib12)\)\. The other is that naively unrolling a contracting operator yields a gateless and parameterless recurrent neural network, invariably condemned to vanishing gradients \(even for well\-behaved operators\)\([9](https://arxiv.org/html/2608.17087#bib.bib13)\)\. The moment time was declared quantification in disguise, both problems were committed to at once, and their effects seem to now be putting this enterprise to an unrewarding end\. The realization stings, then condemns: were all the concessions made in vain?

## 7\.Semantics, Lifted

You anxiously search the wreckage for survivors\. On reread, the theorem’s domain is continuous t\-norms, which neitherRobustnessnorLSEare \(their carrier being the extended real line\)\. Its selective behavior has burned the former; the latter was condemned by association alone, and without proper trial\. You put its backward pass under the same loupe, and find it… dense with gradients\! The per\-tick shares of credit are softmax weights: they sum to one, and none of them is a zero\. Aϕ\\phipinned to almost truth forTTticks sees its feedback thinning as1/T1/T\(i\.e\., harmonically rather than exponentially\); duration may dilute the credit, but it never extinguishes it\. Read against the taxonomy, the profile appears a threefold antidote: it is dense, so nothing is selected out; it is smooth, so nothing saturates; and it is normalized, so nothing decays\. A panacea, however, it is not: the audit’s old complaint stands, and the verdict ofalwaysis still tied to its duration\. Holdϕ\\phito finite truth, and every confirming tick drags⟦𝒢​ϕ⟧\\llbracket\\mathcal\{G\}\\phi\\rrbracketlower; enough ticks, and the verdict\-carrying sign flips to unsafety\. Conversely,⟦ℱ​ϕ⟧\\llbracket\\mathcal\{F\}\\phi\\rrbracketclimbs up with each tick spent not findingϕ\\phi, eventually reporting liveness where there is none\. The catalogue thus splits clean in two: sound verdicts with dead credit, or live credit with unsound verdicts; no algebra presently holds both halves\.

But what makesLSEso special? You return to the theorem and give it another read, this time looking for hypotheses rather than verdicts: continuity, associativity, and the unit interval\.LSEkept the first two and broke the third\. But then again, as the generator already confessed,LSEis justProductunder bent coordinates\. The theorem has not been escaped; transported across the algebra isomorphism, it still classifies the survivor as strict\. And then it clicks: the theorem is indifferent to coordinate bending, but the backward pass is not; it’s the unit interval doing the extinguishing all along\! The click resolves the dead credit question, but the unsound verdict problem still stands\. What’s missing is idempotence: the sum nested withinLSEgrows with its duration, and no coordinate bending can make it forget its length\.

The two problems translate into two demands\. The credit must keep the only profile to have survived inspection: the shares must be the softmax\. The verdict must forget its duration: the sum must be normalized like a mean, since a mean of equals is an equal, indifferent to how many steps it averages over\. For once, credit assignment can be prescribed rather than discovered\. Both demands seemingly point at the same object: the first names the softmax outright, and the softmax is itself a normalized weighting scheme, so averaging under it is a mean by construction\. The emerging candidate is actually folklore: theBoltzmannaverage, a mean whose weights are the softmax of its inputs\.

But the demands exceed the spec, and transcription stalls at the first reduction\. The spec assumed no law, so that it could not break any\. Yet it did assume a shape: it derived quantification as the fold of a binary operator, native to the algebra’s carrier\. The newcomer holds neither of the licenses that shape has been spending\. Its bracketings disagree: an average of averages is not the average of the whole, so a binary fold is a silent commitment to one of many bracketings\([4](https://arxiv.org/html/2608.17087#bib.bib17)\)\. The fallback would still run it, only to correctly compute the wrong thing\. Furthermore, it has no mute member: every finite value carries weight in a weighted average, leaving nothing to fillspan’s blanks with\. For the first time, it is not an algebra that fails an audit, but the spec that fails an algebra\.

How does one binarize an irreducibly variadic operator? The usual trick of superimposing no longer applies; there are no two items to compare\. Then again, the trick’s last run left a residue: theArchimedeanfamily\. It prescribes the recipeg−1∘cumsum∘gg^\{\-1\}\\circ\\mathrm\{cumsum\}\\circ\\,g; a fold flanked by coordinate transformations\. You squint again, harder this time, and realize your perspective may have been somewhat myopic\. The fold never ran in the carrier; it ran in another space, picked exactly so that the fold behaves\. Reducibility is not a property of the operator alone; it is granted to the operator by the space it folds in\. The misattribution is excusable; the target space has so far been hiding under two independent coincidences\. One, the crossing cost nothing semantically,ggbeing invertible\. And two, it cost nothing syntactically,ggmappingTtoT\. Breaking away from both, you consider the minimum workable properties of the target space: associativity \(to license speed\), identity \(to license padding\), and… that’s it\. You lift the operator to amonoidalstate that just so happens to contain tensors in some shape or form:

classState\(ABC\):

duration:int;device:torch\.device

defcombine\(self,other:Self\)\-\>Self:\.\.\.

defneutral\(self\)\-\>Self:\.\.\.

defzip\_with\(self,other:Self,fn:Fn\[\[Tensor,Tensor\],Tensor\]\)\-\>Self:\.\.\.

The licenses are spent immediately, on what will soon becomescan’s faster replacement\([8](https://arxiv.org/html/2608.17087#bib.bib20)\)inState\-space:

defsweep\[S:State\]\(states:S\)\-\>S:

defshifted\(acc:S,k:int\)\-\>S:

defdelay\(s:Tensor,n:Tensor\)\-\>Tensor:

returntorch\.cat\(\[n\.expand\(\*s\.shape\[:\-1\],k\),s\[\.\.\.,:\-k\]\],dim=\-1\)

returnacc\.zip\_with\(states\.neutral\(\),delay\)

ks=takewhile\(lambdak:k<states\.duration,\(1<<jforjincount\(\)\)\)

returnreduce\(lambdaacc,k:shifted\(acc,k\)\.combine\(acc\),ks,states\)

Read temporally, aStateis asummaryof an interval;combinemerges adjacent intervals without revisiting their ticks: a monitor’s memory that splices as readily as it extends\.sweepis that monitor run over every prefix at once\. The same licenses admit the triangular tiling ofspan, its blanks this time filled by the monoid’s unit:

defwindows\[S:State\]\(states:S\)\-\>S:

n=states\.duration

mask=torch\.triu\(torch\.ones\(n,n,device=states\.device\)\)\.bool\(\)

deftile\(s:Tensor,i:Tensor\)\-\>Tensor:

returntorch\.where\(mask,s\[\.\.\.,None,:\],i\)

returnsweep\(states\.zip\_with\(states\.neutral\(\),tile\)\)

The abstraction meets its first inhabitant, whose state is shaped nothing like its value:

classBoltzmannState\(State\):

max:Tensor;weight:Tensor;wsum:Tensor

defcombine\(self,other:BoltzmannState\)\-\>BoltzmannState:

m=torch\.maximum\(self\.max,other\.max\)

wa=torch\.exp\(self\.max\-m\)

wb=torch\.exp\(other\.max\-m\)

returnBoltzmannState\(

max=m,

weight=wa\*self\.weight\+wb\*other\.weight,

wsum=wa\*self\.wsum\+wb\*other\.wsum,

\)

defneutral\(self\)\-\>BoltzmannState:

returnBoltzmannState\(

max=self\.max\.new\_tensor\(float\(’\-inf’\)\),

weight=self\.weight\.new\_tensor\(0\.\),

wsum=self\.wsum\.new\_tensor\(0\.\),

\)

The state carries the weighted mean in three pieces: a numerator, a denominator, and a running maximum\([17](https://arxiv.org/html/2608.17087#bib.bib15);[5](https://arxiv.org/html/2608.17087#bib.bib16)\)\.

The blueprint, in its current form, is not ready to consume the new arrivals\. The upside is thatStates are transient and internal; they never escape the confines of a computation, so they can be tucked away by anAlgebrathat only ever deals withTensors\. The downside is thatAlgebraspelled out reductions as folds of binary primitives, folds which subclasses inherit as both a fallback and a specification; this now becomes a liability\. The solution is a retroactive split:Algebrakeeps the signatures and surrenders the bodies; the runnable spec relocates, virtually identical, intoFolded\(Algebra,ABC\), and the entire catalogue reparents to it\. A new sibling then emerges:

classLifted\[S:State\]\(Algebra,ABC\):

defembed\(self,x:T\)\-\>S:\.\.\.

defreadout\(self,s:S\)\-\>T:\.\.\.

defmeet\(self,x,y\):returnself\.readout\(self\.embed\(x\)\.combine\(self\.embed\(y\)\)\)

defjoin\(self,x,y\):returnself\.neg\(self\.meet\(self\.neg\(x\),self\.neg\(y\)\)\)

defimpl\(self,x,y\):returnself\.join\(self\.neg\(x\),y\)

defrunning\_meet\(self,x\):returnself\.readout\(sweep\(self\.embed\(x\)\)\)

defrunning\_join\(self,x\):returnself\.neg\(self\.running\_meet\(self\.neg\(x\)\)\)

defforall\(self,x\):returnself\.running\_meet\(x\)\[\.\.\.,\-1\]

defexists\(self,x\):returnself\.running\_join\(x\)\[\.\.\.,\-1\]

defspan\_meet\(self,x:T\)\-\>T:

n=x\.size\(\-1\)

mask=torch\.triu\(torch\.ones\(n,n,device=x\.device\)\)\.bool\(\)

returntorch\.where\(mask,self\.readout\(windows\(self\.embed\(x\)\)\),self\.bot\)

Each running reduction factors asreadout∘sweep∘embed\\mathrm\{readout\}\\circ\\mathrm\{sweep\}\\circ\\mathrm\{embed\}, withsweep\\mathrm\{sweep\}determined bycombinealone; the crossing is the factorization’s only free parameter\. The span is the old triangular construction transported across the crossing\. Meet and join are distinct aggregations over a shared monoid, so they could only ever differ in their crossings; rather than implement a second pair, the abstraction assumes involutive negation so that join can mirror the meet through negation, just like theArchimedeanfamily\. The second implicit assumption is that each embed is a section of the readout,readout∘embed=id\\mathrm\{readout\}\\circ\\mathrm\{embed\}=\\mathrm\{id\}so that each value sent can come back unharmed \(the mean of one thing is the thing\)\. The converse is not true; the readout is free to forget, and what is forgotten is forever lost\. And that is what the imprint of non\-associativity really is: two different brackets forget different things, at different places\. Both assumptions then turn to laws, and join the audit alongside the rest\. The newcomer gets a name and a listing, made of one crossing pair and a negation:

classBoltzmann\(Lifted\[BoltzmannState\]\):

b:T

defembed\(self,x\):returnBoltzmannState\(\-self\.b\*x,torch\.ones\_like\(x\),x\)

defneg\(self,x\):return\-x

defreadout\(self,s\):returns\.wsum/s\.weight

Boltzmannruns at the catalogue’s full speed, its credit dense by construction, but its laws still owed\. Once more, it is tempting to call the matter closed\.

## 8\.Semantics, Backward\!

This time around you know better, and jump straight to the loupe\. Initially, the backward pass invites optimism; the feedback is differentiable, as requested, and this time it is anything but empty: dense, smooth, and normalized, not a tick uncredited\. The audit interrupts:monotonicity, previously universal, now fails\. The disproving exhibit is compact and unquestionable: a two\-tick judgement ofℱ​ϕ\\mathcal\{F\}\\phi, one strong peak and one faint tick;raisethe faint tick and the verdictdrops\. It takes a second, but the cause becomes obvious in hindsight: the weights are elected by the very values under judgement, so a straggler promoted gains weight \(while still testifying low\!\), and the average obliges, downward\.

The mistake is a rehash of your very first one, except this time in reverse: the softmax belonged to the feedback, but was spent instead on the verdict\. The demands said where the softmax must show, not where to install it; the shares reside in the backward pass, and the survivor had been holding them there all along\. The repair has to be “backwards”\-engineered from the survivor: keep its aggregation, and let its sum too become a mean\. The constraints converge: at fixed duration, division becomes subtraction by a constant, and constants are invisible to the backward pass; the survivor’s shares carry over verbatim\. The resulting operator already has a name,mellowmax, and a reputation as a better\-behaved alternative to the Boltzmann average\([1](https://arxiv.org/html/2608.17087#bib.bib14)\)\. It is also a quasi\-arithmetic mean,i\.e\., the averaging sibling of theArchimedeanfamily, its exponential tilting a generator in disguise\([11](https://arxiv.org/html/2608.17087#bib.bib18);[19](https://arxiv.org/html/2608.17087#bib.bib19)\)\. InState\-space,Boltzmann’s successor requires a single substitution: the weighted sum retires, and in its place sits acounter, given a field of its own\.

classMellowmaxState\(State\):

max:Tensor;weight:Tensor;count:Tensor

defcombine\(self,other:MellowmaxState\)\-\>MellowmaxState:

m=torch\.maximum\(self\.max,other\.max\)

wa=torch\.exp\(self\.max\-m\)

wb=torch\.exp\(other\.max\-m\)

returnMellowmaxState\(

max=m,

weight=wa\*self\.weight\+wb\*other\.weight,

count=self\.count\+other\.count,

\)

defneutral\(self\)\-\>MellowmaxState:

returnMellowmaxState\(

max=self\.max\.new\_tensor\(float\(’\-inf’\)\),

weight=self\.weight\.new\_tensor\(0\.\),

count=self\.count\.new\_tensor\(0\.\),

\)

The algebra follows suit:

classMellowmax\(Lifted\[MellowmaxState\]\):

b:T

defembed\(self,x\):returnMellowmaxState\(\-self\.b\*x,torch\.ones\_like\(x\),torch\.ones\_like\(x\)\)

defneg\(self,x\):return\-x

defreadout\(self,s\):return\(s\.max\+torch\.log\(s\.weight\)\-torch\.log\(s\.count\)\)/\-self\.b

Almost mechanically, you reach for another backward pass\. Not unlike before, the feedback is dense, smooth and normalized\. Unlike before, it is also non\-negative, exactly matchingLSE’s profile: the softmax, verbatim\. As designed, the verdict does forget its duration; the mean is idempotent, soϕ\\phipinned atxxreads⟦𝒢​ϕ⟧=x\\llbracket\\mathcal\{G\}\\phi\\rrbracket=x, at anyTT\. No more selection, no more saturation, and no more decay222At finiteβ\\beta\. Asβ\\betagrows, the shares collapse towards one\-hotness and mellowmax hardens intoRobustness\. Selection was never banished, only pushed to a boundary, and the distance to the boundary is the parameter\.\. As is customary, the audit interrupts, on a debt thought settled: theunit\. A mean has no mute member; for any⊤\\toplarge enough to approximate infinity, conjunction with truth pushes the conjunct further towards truthhood\. The unit’s loss is unavoidable; a mean divides by the count of its voters, and a unit is an abstainer, a value not to be counted\. The loss is not, however, insurmountable; with⊤\\topread as a distinguished boundary value, a numerical inequality suffices to map it to the monoid’s unit:

classMellowmax\(Lifted\[MellowmaxState\]\):

\.\.\.

defembed\(self,x\):

member=x<self\.top

returnMellowmaxState\(

max=torch\.where\(member,\-self\.b\*x,\-torch\.inf\),

weight=member\.float\(\),count=member\.float\(\)

\)

defreadout\(self,s\):

vote=\(s\.max\+torch\.log\(s\.weight\)\-torch\.log\(s\.count\)\)/\-self\.b

returntorch\.where\(s\.count\>0,vote,self\.top\)

Despite the algebra not being unital in the carrier, the unit can be emulated inState\-space, which is where computation happens anyway; a half\-win\. The audit concludes without further surprises\. Monotonicity, involution, De Morgan duality, and the section law all pass, as expected\. Also as expected, associativity, the residuum and the lattice honorifics \(absorption, distributivity, complementation\) all fail, and implication retracts to its material form\. The search concludes: duration\-invariant verdicts and live credit, at last held by a single algebra\.

## 9\.Semantics, in Hindsight

The matter can finally be called closed\. The concessions were indeed worth it; more than that, every concession can now be understood as a structural trespass, a property broken in the verdict world for a behavior gained in the feedback world\. None of the ruckus was perceived by the evaluator, which has kept its promise throughout: every formula, under every algebra\. The result is a bunch of algebras for the user to pick, in varying grades of well\-behavedness, properly qualified, and with at least one of them working; they all get to meet one another under Table[2](https://arxiv.org/html/2608.17087#S9.T2)\. You walked into the bazaar a dizzy customer; you walk out its keeper; the dizziness has been cured by careful appraisal rather than choice\. Satisfied with the artifact, you start recounting your turmoils into a somewhat exaggerated second\-person narrative, which you reckon could make for a good enough functional pearl\. In time, you will get both feedback and a verdict; this time around, neither will be of your own design\.

Table 2\.Table[1](https://arxiv.org/html/2608.17087#S4.T1)revisited: the extended catalogue and audit suite\.Greyedcells are carried over unchanged from Table[1](https://arxiv.org/html/2608.17087#S4.T1); black cells are new here\. Law entries are still checked mechanically\.Creditis not a law but a classification, forward\-determined and backward\-observed\.\[2\]

aimplis not differentiable in its first argument\.basp→0p\\to 0\.casp→∞p\\to\\infty\.datp=1p=1\.eforp≥1p\\geq 1\. finState\-space, up to readout; not in the carrier\.

## References

- Asadi and Littman \(2017\)K\. Asadi and M\. L\. LittmanAn alternative softmax operator for reinforcement learning\.InProceedings of the 34th International Conference on Machine Learning, ICML 2017,Proceedings of Machine Learning Research, Vol\.70,pp\. 243–252\.External Links:[Link](https://proceedings.mlr.press/v70/asadi17a.html)Cited by:[§8](https://arxiv.org/html/2608.17087#S8.p2.1)\.
- Blelloch \(1989\)G\. E\. BlellochScans as primitive parallel operations\.IEEE Transactions on Computers38\(11\),pp\. 1526–1538\.External Links:[Document](https://dx.doi.org/10.1109/12.42122)Cited by:[§5](https://arxiv.org/html/2608.17087#S5.p2.1)\.
- Claessen and Hughes \(2000\)K\. Claessen and J\. HughesQuickCheck: a lightweight tool for random testing of haskell programs\.InProceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming \(ICFP ’00\), Montreal, Canada, September 18\-21, 2000,pp\. 268–279\.External Links:[Document](https://dx.doi.org/10.1145/351240.351266)Cited by:[§4](https://arxiv.org/html/2608.17087#S4.p7.2)\.
- Czogała and Drewniak \(1984\)E\. Czogała and J\. DrewniakAssociative monotonic operations in fuzzy set theory\.Fuzzy Sets and Systems12\(3\),pp\. 249–269\.External Links:[Document](https://dx.doi.org/10.1016/0165-0114%2884%2990072-1)Cited by:[§7](https://arxiv.org/html/2608.17087#S7.p4.1)\.
- Daoet al\.\(2022\)T\. Dao, D\. Y\. Fu, S\. Ermon, A\. Rudra, and C\. RéFlashAttention: fast and memory\-efficient exact attention with io\-awareness\.InAdvances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022,pp\. 16344–16359\.External Links:[Document](https://dx.doi.org/10.52202/068431-1189),[Link](http://papers.nips.cc/paper_files/paper/2022/hash/67d57c32e20fd0a7a302cb81d36e40d5-Abstract-Conference.html)Cited by:[§7](https://arxiv.org/html/2608.17087#S7.p10.2)\.
- Fainekos and Pappas \(2009\)G\. E\. Fainekos and G\. J\. PappasRobustness of temporal logic specifications for continuous\-time signals\.Theoretical Computer Science410\(42\),pp\. 4262–4291\.External Links:[Document](https://dx.doi.org/10.1016/j.tcs.2009.06.021)Cited by:[§4](https://arxiv.org/html/2608.17087#S4.p9.1)\.
- Gilpinet al\.\(2021\)Y\. Gilpin, V\. Kurtz, and H\. LinA smooth robustness measure of signal temporal logic for symbolic control\.IEEE Control Systems Letters5\(1\),pp\. 241–246\.External Links:[Document](https://dx.doi.org/10.1109/LCSYS.2020.3001875)Cited by:[§5](https://arxiv.org/html/2608.17087#S5.p6.2)\.
- Hillis and Steele Jr\. \(1986\)W\. D\. Hillis and G\. L\. Steele Jr\.Data parallel algorithms\.Communications of the ACM29\(12\),pp\. 1170–1183\.External Links:[Document](https://dx.doi.org/10.1145/7902.7903)Cited by:[§7](https://arxiv.org/html/2608.17087#S7.p6.2)\.
- Hochreiter \(1998\)S\. HochreiterThe vanishing gradient problem during learning recurrent neural nets and problem solutions\.International Journal of Uncertainty, Fuzziness and Knowledge\-Based Systems6\(2\),pp\. 107–116\.External Links:[Document](https://dx.doi.org/10.1142/S0218488598000094)Cited by:[§6](https://arxiv.org/html/2608.17087#S6.p3.1)\.
- Klementet al\.\(2000\)E\. P\. Klement, R\. Mesiar, and E\. PapTriangular norms\.Trends in Logic,Springer Netherlands\.External Links:ISBN 9789401595407,[Document](https://dx.doi.org/10.1007/978-94-015-9540-7)Cited by:[§1](https://arxiv.org/html/2608.17087#S1.p3.1),[§4](https://arxiv.org/html/2608.17087#S4.p9.1)\.
- Kolmogoroff \(1930\)A\. KolmogoroffSur la notion de la moyenne\.Atti della Accademia Nazionale dei Lincei, Rendiconti, VI\. Serie12,pp\. 388–391\.Cited by:[§8](https://arxiv.org/html/2608.17087#S8.p2.1)\.
- Lamport \(1977\)L\. LamportProving the correctness of multiprocess programs\.IEEE Transactions on Software EngineeringSE\-3\(2\),pp\. 125–143\.External Links:[Document](https://dx.doi.org/10.1109/TSE.1977.229904)Cited by:[§1](https://arxiv.org/html/2608.17087#S1.p1.2)\.
- Leunget al\.\(2023\)K\. Leung, N\. Aréchiga, and M\. PavoneBackpropagation through signal temporal logic specifications: infusing logical structure into gradient\-based methods\.International Journal of Robotics Research42\(6\),pp\. 356–370\.External Links:[Document](https://dx.doi.org/10.1177/02783649221082115)Cited by:[§4](https://arxiv.org/html/2608.17087#S4.p9.1)\.
- Ling \(1965\)C\. LingRepresentation of associative functions\.Publicationes Mathematicae Debrecen12\(1\-4\),pp\. 189–212\.External Links:[Document](https://dx.doi.org/10.5486/pmd.1965.12.1-4.19)Cited by:[§5](https://arxiv.org/html/2608.17087#S5.p9.2),[§6](https://arxiv.org/html/2608.17087#S6.p2.1)\.
- MacIveret al\.\(2019\)D\. R\. MacIver, Z\. Hatfield\-Dodds, and Many Other ContributorsHypothesis: a new approach to property\-based testing\.Journal of Open Source Software4\(43\),pp\. 1891\.External Links:[Document](https://dx.doi.org/10.21105/joss.01891)Cited by:[§4](https://arxiv.org/html/2608.17087#S4.p7.2)\.
- Maler and Nickovic \(2004\)O\. Maler and D\. NickovicMonitoring temporal properties of continuous signals\.InFormal Techniques, Modelling and Analysis of Timed and Fault\-Tolerant Systems, FORMATS/FTRTFT 2004,Lecture Notes in Computer Science, Vol\.3253,pp\. 152–166\.External Links:[Document](https://dx.doi.org/10.1007/978-3-540-30206-3%5F12)Cited by:[§4](https://arxiv.org/html/2608.17087#S4.p9.1)\.
- Milakov and Gimelshein \(2018\)M\. Milakov and N\. GimelsheinOnline normalizer calculation for softmax\.CoRRabs/1805\.02867\.External Links:1805\.02867,[Link](http://arxiv.org/abs/1805.02867)Cited by:[§7](https://arxiv.org/html/2608.17087#S7.p10.2)\.
- Mostert and Shields \(1957\)P\. S\. Mostert and A\. L\. ShieldsOn the structure of semigroups on a compact manifold with boundary\.Annals of Mathematics65\(1\),pp\. 117–143\.External Links:[Document](https://dx.doi.org/10.2307/1969668)Cited by:[§6](https://arxiv.org/html/2608.17087#S6.p2.1)\.
- Nagumo \(1930\)M\. NagumoÜber eine klasse der mittelwerte\.Japanese Journal of Mathematics7,pp\. 71–79\.External Links:[Document](https://dx.doi.org/10.4099/jjm1924.7.0%5F71)Cited by:[§8](https://arxiv.org/html/2608.17087#S8.p2.1)\.
- Pantet al\.\(2017\)Y\. V\. Pant, H\. Abbas, and R\. MangharamSmooth operator: control using the smooth robustness of temporal logic\.InIEEE Conference on Control Technology and Applications, CCTA 2017,pp\. 1235–1240\.External Links:[Document](https://dx.doi.org/10.1109/CCTA.2017.8062628)Cited by:[§5](https://arxiv.org/html/2608.17087#S5.p6.2)\.
- Paszkeet al\.\(2019\)A\. Paszke, S\. Gross, F\. Massa, A\. Lerer, J\. Bradbury, G\. Chanan, T\. Killeen, Z\. Lin, N\. Gimelshein, L\. Antiga, A\. Desmaison, A\. Köpf, E\. Z\. Yang, Z\. DeVito, M\. Raison, A\. Tejani, S\. Chilamkurthy, B\. Steiner, L\. Fang, J\. Bai, and S\. ChintalaPyTorch: an imperative style, high\-performance deep learning library\.InAdvances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8\-14, 2019, Vancouver, BC, Canada,pp\. 8024–8035\.External Links:[Link](https://proceedings.neurips.cc/paper/2019/hash/bdbca288fee7f92f2bfa9f7012727740-Abstract.html)Cited by:[§1](https://arxiv.org/html/2608.17087#S1.p3.1)\.
- Pnueli \(1977\)A\. PnueliThe temporal logic of programs\.In18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October \- 1 November 1977,pp\. 46–57\.External Links:[Document](https://dx.doi.org/10.1109/SFCS.1977.32)Cited by:[§1](https://arxiv.org/html/2608.17087#S1.p1.1)\.
- van Kriekenet al\.\(2022\)E\. van Krieken, E\. Acar, and F\. van HarmelenAnalyzing differentiable fuzzy logic operators\.Artificial Intelligence302,pp\. 103602\.External Links:[Document](https://dx.doi.org/10.1016/j.artint.2021.103602)Cited by:[§6](https://arxiv.org/html/2608.17087#S6.p3.1)\.
- Várnai and Dimarogonas \(2020\)P\. Várnai and D\. V\. DimarogonasOn robustness metrics for learning STL tasks\.InAmerican Control Conference, ACC 2020,pp\. 5394–5399\.External Links:[Document](https://dx.doi.org/10.23919/ACC45564.2020.9147692)Cited by:[§6](https://arxiv.org/html/2608.17087#S6.p2.1)\.