A Programming Paradigm for Spatiotemporal Composability. Cordis¶

Cikk: Yifan Shi, Wei Zhang (Peking University), Tianyi Cui (DeepSeek-AI): A Programming Paradigm for Spatiotemporal Composability — 88 oldalas formális tanulmány (Section 1–8, 124 hivatkozás) Dátum: 2026-08-17 (feldolgozás) Forrás: (efemer gyorsítótár; a feltöltött PDF a takarítás óta nincs meg) ⚠️ (~2.1 MB) Wiki raw:

Összegzés¶

A Cordis a DeepSeek-AI és a Peking University közös, 88 oldalas formális tanulmánya, amely egy új programozási paradigmát vezet be a dinamikus kompozíció problémájára. A paradigmát a klasszikus algebraic effects és coeffects fogalmak futásidejű mechanizmusokká emelésével építi fel: a revertible effects révén minden kontextus-mutációhoz automatikusan generálódik inverz, a reactive coeffects révén pedig minden függőség-deklaráció reaktívan újrafeloldódik, amikor a szolgáltatók betöltődnek vagy eltávolítódnak. A két mechanizmust a Γ∞ típusegyesítés és az observational equivalence fogalma kapcsolja össze egyetlen kontextus-paradigmává. A cikk formális kalkulust (komponensek, rostok, registry, 10 lifecycle szabály: Preservation Theorem 59, Recovery exactness Theorem 61, Ordering Theorem 63, Progress Theorem 66, Confluence Theorem 73) és gyakorlati implementációt (TypeScript meta-framework, deklaratív component loader HMR-rel, Koishi case study 4000+ pluginnal) is bemutat. A legfontosabb gyakorlati üzenet: a Cordis a DeepSeek-AI saját önfejlesztő agent harness-ének formális alapjaként szolgál — a temporal garancia (teljes recovery rapid komponens-csere alatt) és a spatial garancia (dependencia koordináció gyakori topológiai változás alatt) együttesen strukturális, nem konvenció-alapú Spatiotemporal Composability-t ad.

1. A cikk célja és kontextusa¶

A dinamikus kompozíció (azaz egy futó rendszer komponenseinek biztonságos betöltése, cseréje és eltávolítása) a modern szoftverarchitektúrák egyik legnehezebb problémája. A mai gyakorlatban ezt vagy durva granularitással oldják meg (a teljes folyamatot újraindítják, mint a Kubernetes, Borg, konténer-orchestráció), vagy fejlesztői fegyelemre bízzák (plugin lifecycle callback-ek, useEffect cleanup, OSGi unload metódusok), az utóbbi megközelítés empirikusan szivárog: elfelejtett cleanup csendben erőforrás-szivárgást okoz.

A cikk egy programozási paradigmát javasol, amely a határt a két véglet között húzza meg: az effektusok és ko-effektusok futásidejű nyomon követésével strukturális garanciát ad a komponens-eltávolítás teljes visszafordítására, anélkül, hogy a fejlesztőnek bármilyen cleanup-kódot kellene írnia.

A cikk szerzői között van Tianyi Cui a DeepSeek-AI-tól, ami jelzi, hogy a DeepSeek ezt a meta-frameworköt (Cordis) a gyakorlatban is alkalmazza, vélhetően az önfejlesztő agent harness-ek belső komponenskezelésére. A tanulmány 8. szakaszában explicit validációs terepként említi az "self-evolving agent harnesses" forgatókönyvet.

2. A két alapfogalom: revertible effects és reactive coeffects¶

A cikk a klasszikus számítástudományi fogalmakat (algebraic effects, coeffects. Plotkin & Power 2001, Petricek-Orchard-Mycroft 2013) emeli át futásidejű mechanizmusokká.

2.1 Revertible effects, időbeli komponálhatóság¶

Minden kontextus-mutációhoz a fejlesztő inverz függvényt szolgáltat (pl. set ↔ delete, open ↔ close, malloc ↔ free). A futásidő az inverzeket egy akkumulátorba komponálja LIFO sorrendben, és a komponens eltávolításakor automatikusan lejátssza őket, így a kontextus visszatér a komponens betöltése előtti állapotába (Theorem 7).

A kulcs: az inverz nem a rendszer kötelessége, hanem a fejlesztő szolgáltatja az atomikus hatáshoz, és a kompozit hatás inverze automatikusan következik kompozícióból. Ez a React useEffect cleanup-pal szemben az, hogy ott a hatás törzsében nem lehet aszinkron vagy iterátor, itt lehet. A Cordis hatás egy delimált continuation (James & Sabry 2011), a yield operátor formájában, ami natívan támogatott a modern nyelvekben.

A ctx.effect(callback) primitív az Algorithm 1-ben: a callback egy iterátor, minden lépésben szolgáltat inverzet, a futásidő egy execute függvényben hajtja végre, és az inverzeket egyetlen kompozit dispose függvénnyé foldolja. A dispose önmaga is ctx.effect hívás, ami rekurzív struktúrát ad, a gyerek-hatás inverze a szülő kontextusra hat.

2.2 Reactive coeffects, térbeli komponálhatóság¶

Egy komponens deklarálja a függőségeit (pl. "adatbázis kell", "logger kell"). A futásidő ezt a specifikációt (a d halmazt) a kontextus változásai ellenében folyamatosan kiértékeli: - activating transition (dependencia megjelent) → betölti a komponenst - deactivating transition (dependencia eltűnt) → eltávolítja (inverzeket futtatja) - neutral transition → nincs teendő

Ez a Dependency Inversion távoli rokona, de a különbség lényeges: míg a Spring/Angular DI egyszer a boot-oláskor köt, a Cordis futásidőben folyamatosan újraköt, ha kicseréled az adatbázis-szolgáltatót, csak az érintett komponensek aktiválódnak újra.

A notify mechanizmus (Algorithm 3) minden egyes kulcskötés-változásra végigmegy az aktív rostokon, és akinél a kulcs a fiber.inject-ben van, meghívja a refresh-et (Algorithm 5). A frissítés idempotens, így a neutrális változások ártalmatlanok.

2.3 Isolation és interception¶

A Σ_iso kontextus (Definition 28) egy két-rétegű feloldást vezet be: a 𝜌: K ⇀ R realm-tábla, és a 𝜎: R ⇀ Vᵣ realm-szerinti értéktábla. Ugyanaz a kulcs különböző realm-ekben más értékre oldódik fel, ez a multi-tenant rendszerek, teszt-sandboxok és komponens-sandboxok alapja.

A Σ_inter kontextus (Definition 30) interception-t ad: a kulcshoz monoid-metadátát lehet csatolni, és a lekéréskor a kontextus saját és a komponens deklarált metadátáját monoid-művelettel merge-eli. Ez a policy enforcement alapja: az adatbázis-szolgáltató maga nem tudja, hogy egy adott komponens csak olvashat, a kontextus interception mondja meg neki.

3. A kontextus-paradigma: Γ∞ és az egységes típus¶

A Section 3.3 a két részt egyesíti: Γ∞ ≔ μΓ. Γ × (Γ → Γ) × Σ, rekurzív típus, ahol Γ a hatás-kontextus, Γ → Γ az akkumulátor, Σ a ko-effektus kontextus. A komponensek ezen a típuson hatnak, és a Σ tetszőleges típusú lehet (𝒱ᵏ), tehát minden megosztott állapot kódolható ko-effektusként.

Az observational equivalence (Definition 33) a Σ ko-effektusokra épül: két állapot akkor ekvivalens, ha azonos kulcsokra azonos (a kulcs saját ≃ᵏ relációjában) értékeket kötnek. Ez az egyenlőség pótolja a fizikai állás (heap layout, generatív nevek) visszaállíthatatlanságát, és az egyenlőségeket ≃-re cserélve a Theorem 7 (recovery exactness) ≃-ben is igaz marad (Lemma 38).

Az independence (Definition 19): két hatás független, ha minden transzformációjuk kommutál, és egyikük inverze sem zavarja a másik által szolgáltatott inveret. Ez a kulcsa a globális temporális komponálhatóságnak (egy komponens inverze csak a saját hatását vonja vissza, még ha mások is közben léptek).

Theorem 42 kimondja: ha minden kulcs kommutatív (minden művelet független minden másiktól), akkor a ko-effektus-mediált hatásfüggvények függetlenek. Ez a kulcsa annak, hogy a kompozíció skálázódik: a komponensek száma nem befolyásolja a globális garanciát.

4. A dinamikus kompozíció kalkulusa¶

4.1 Komponensek és rostok (fiber)¶

Egy komponens hármas (d, p, e): a deklarált ko-effektus specifikáció (d), a szolgáltatott kulcsok halmaza (p), és a witnessed effect function (e). A rost (fiber) ennek egy pillanatfelvétele a futó rendszerben: a (d, p, e, π, σ, τ, θ) tuple, ahol π a szülő rost, σ a saját ko-effektus tábla, τ a retired flag, θ a lifecycle állapot.

A registry a rostok táblázata (Fγ : N ⇀ F), és a Σ ko-effektus kontextust levezetjük a registryből: σγ ≔ ⋃{σ� | m ∈ dom(Fγ), θₘ = Active} (Definition 45). Tehát nincs központi ko-effektus tábla, az aktív rostok egyesítése adja. Minden kulcsnak egy provider-e van (a p ∩ pₘ = ∅ single-source discipline miatt).

4.2 A kétállapotú alap¶

A lifecycle a 4.2 szakaszban: Inactive ↔ Active. Két szabály: - L-Reload: ha θ = Inactive és target(γ, n) ≠ ⊥ → futtatja e-t, felhalmozza az inverzeket, kommitálja a nézetet (ω = target) - L-Unload: ha θ = Active(g, ω) és target(γ, n) ≠ ω → alkalmazza g-t (LIFO inverz sorrendben), eldobja ω-t

A target view (Definition 46) egy leképezés dₙ → N, minden deklarált kulcshoz megadja a jelenlegi providert (vagy ⊥-t, ha nincs). A rendszer akkor quiescent (Definition 42), ha minden rost nézete megegyezik a target nézetével.

4.3 A kibővített lifecycle: in-progress tranzíciók¶

A valódi runtime-ok nem atomiak és nem szinkronok. A 4.3 szakasz három dolgot bocsát ki: 1. Withdrawal (4.3.1): A L-Unload guard-ja, ¬reliedₙ(γ), biztosítja, hogy a provider ne vonja vissza a kulcsot, amíg valamely fogyasztó még aktív (az L-Leave kétlépcsős teardown). Ez teremti meg azt az intervallumot, ami alatt a fogyasztó a saját teardownját futtathatja. 2. Iteration (4.3.2): Az effect iterator (Definition 51) rekurzív típus, Γ → Γ × (Γ → Γ) × Maybe(iter). A Maybe continuation jelzi a yield-határt; a host bármikor divertelhet (L-Divert), ha a target nézet eltolódott. 3. Asynchrony (4.3.3): Az iteráció Future-t ad vissza; az in-flight iteráció inerciális, landolnia kell, mielőtt a rendszer másra reagál. Ez adja a "kölcsönös láncolás" viselkedését. 4. Failure (4.3.4): Az iteráció Either(Ξ, Γ × (Γ → Γ) × Maybe(iter)), L-Raise kezeli a hibát, és az akkumulátor visszafordítja a részleges hatásokat.

4.4 A metaelmélet¶

Preservation (Theorem 59): a 10 szabály megőrzi a registry well-formednességét.
Recovery exactness (Theorem 61): egy rost akkumulátora ≃-ben visszaadja azt az állapotot, amit akkor kapnánk, ha a rost sosem futott volna, bármi történik közben.
Ordering (Theorem 63): a guard biztosítja, hogy egy komponens csak akkor aktiválódik, ha minden függősége elérhető, és egy provider csak azután vonja vissza a kulcsot, miután minden fogyasztó deaktiválódott.
Progress (Theorem 66): nincs deadlock (a � precedencia reláció aciklikussága mellett); a S(n) ≤ (K+4)(V(n)+1) komplexitású termináció.
Confluence (Theorem 73): a rendszer mindig ugyanoda quiescel, függetlenül attól, hogy a tranzíciók milyen sorrendben futottak, ez az, ami lehetővé teszi, hogy a Cordis alkalmazásról úgy gondolkodjunk, mintha statikusan lenne összerakva.

5. Implementáció: Cordis meta-framework¶

5.1 Core library¶

Három tier, lentről fölfelé: 1. Effect tracking (Algorithm 1): ctx.effect(callback) primitív, ami iterátorként hajtja végre a callbackot, és dispose függvényt ad vissza. 2. Coeffect operations (Algorithm 2): ctx.get(key), ctx.set(key, value), ctx.isolate(key, realm), ctx.intercept(key, metadata). A set egy ctx.effect, így automatikusan tracked. 3. Component lifecycle (Algorithm 4-5): ctx.use(component, config) egy rostot hoz létre. A refresh újraszámolja a target nézetet és elindítja a reload/unload taskot.

A Table 2 a 18 elméleti konstrukció és a runtime implementáció közötti megfeleltetés, ez adja a meta-framework státuszt: Cordis nem domain-specifikus (nem web routing, nem ORM), hanem univerzális dinamikus kompozíció.

5.2 Component loader és HMR¶

A loader egy deklaratív konfigurációs réteget ad: az orchestrátor egy perzisztens adatszerkezetben írja le a kívánt kompozíciót (Definition 74 entry-k: id, url, isolate, intercept, config, disabled), és a loader a változásokat imperatív rost-műveletekre fordítja. A reconciliation inkrementális: Theorem 73 miatt a quiescens állapot a végső konfiguráció függvénye, Corollary 62 miatt egy entry eltávolítása nem zavarja a többieket.

A Hot Module Replacement (Algorithm 8-10) három fázisban működik: 1. Module classification: a stashed fájlok dependency subgraph-ját accepted/declined halmazokra bontja (ciklikus függőség → declined). 2. Stale-entry detection: csak azokat az entry-ket jelöli meg, amelyeknek a függőségi fája érint accepted modult. 3. Transactional reload: eldobja a régi rostokat és újrainstantiálja az accepted modulokból; ha bármelyik import elbukik, a backupból rollbackel.

5.3 Koishi case study¶

A Koishi egy nyílt forráskódú chatbot keretrendszer, amely 4+ év alatt 4000+ közösségi plugint halmozott fel (IM adapterek, DB driverek, admin konzolok). A cikk négy érvényesítési pontot emel ki:

Expressiveness: a teljes gyártási rendszer kifejezhető Cordis primitívokkal, a Koishi csak a chatbot-domain szókincset adja hozzá.
Generality: ugyanaz a modell működik szerver-oldalon (chatbot) és a böngészőben (webkonzol), más domain, más futásidejű környezet, ugyanaz a Cordis.
Temporal composability overhead nélkül: a plugout a konzolról → azonnali, helybeni hatás-visszavonás. A HMR a save-re azonnal újratölti a plugint, megtartva a cache-állapotot és az élő kapcsolatokat.
Spatial composability nyílt ökoszisztémában: az IM adapterek biztosítják a messaging platformokat, a DB driverek a perzisztens tárolást, a feature pluginek ezeket deklarálják, a szerzők nem koordinálnak, csak a ko-effektus kulcsot egyeztetik.

A threats to validity: egy ökoszisztéma, egy hoszt nyelv, megfigyeléses (nem kontrollált összehasonlítás). Létezés- és adaptáció-validáció, nem kvantitatív.

6. Diskusszió: rendszerhatár, sandboxing, nyelvek¶

6.1 System boundary, acquisition vs emission¶

A határ lokáció-szintű, nem médium-szintű: egy memóriaregió a határon belül van, ha a rendszer kizárólagosan írja és vissza tudja állítani; kívül, ha más folyamatok is írják. A ko-effektus mozgatja a határt: ha egy lokációt ko-effektusként reifikálunk, a rendszer képes lesz visszaállítani.

Minden művelet két fázisban megy végbe: acquisition (a határon belül, revertálható) + emission (a határon kívül, nem revertálható). A visszaállítás két stratégiája: withhold (a kibocsátás késleltetése az output commit probléma) vagy compensation (kompenzáló akció, ami ≃-nál durvább ekvivalenciával állítja vissza az állapotot, pl. fájl törlése).

6.2 Service multiplexing, service broker¶

A ko-effektus modell natívan támogatja a service broker mintát: egy központi szolgáltatás, ami több providert is befogad, és a kéréseket policy (round-robin, least-loaded, latency-weighted) alapján osztja szét. Ez adja a load balancing-ot, rolling updates-et (új provider betöltése, forgalom-átirányítás, régi unload), és a cross-process invocation-t (RPC-n keresztül, async contract).

6.3 Capability-based access control + sandboxing¶

A dependency access mechanism már egy capability-based security forma: a komponens csak az általa deklarált ko-effektusokhoz fér. Az interception metaadat-policy-ként szolgál (pl. read-only DB hozzáférés egy közösségi pluginnak). A sandboxing (amikor a komponens kódja nem megbízható) a nyelv-szintű határokon túlmutat. WebAssembly, OS process, software fault isolation kell hozzá.

6.4 Language independence¶

A kontextus-paradigma nyelv-agnosztikus, de a host nyelvnek két dolgot kell tudnia: 1. Closure (az inverz first-class érték kell hogy legyen) 2. Dynamic module registry (a modulok betölthetők és eltávolíthatók futásidőben)

A 4. szinten a nyelvek: managed runtime (Node.js CommonJS/ESM cache) ↔ natív kód (dlopen/dlclose) ↔ WebAssembly (managed vagy natív embedder). A ko-effektus oldalon: typeclasses (Haskell), traits (Rust), TypeScript module augmentation a típus-szinten; Proxy (JS), descriptor protocol (Python), vagy metaprogramming (Rust proc macros, Scala macros, Zig comptime) a mediation-re.

6.5–6.7 Mutual dependencies, typing, OS co-design¶

A ciklikus függőségek a ⊲ reláció ciklussá válásával járnak, de a futásidő ezt jelenti (mindkét komponens örökre Inactive), szemben a concurrent deadlockkal, ami schedule-függő. A dekompozíció (kétirányú kölcsönhatás → két egyirányú integrációs komponens) mindig lehetséges, de a komponensek számát a négyzetével növeli.

A dependency typing a kulcs-azonosítás vs. strukturális kompatibilitás problémája: a kulcs-ütközés (két provider ugyanazt a kulcsot használja, de más interfészt) és az interface drift (verzióváltáskor a consumer nem veszi észre) ellen három megoldás: key namespacing, peer dependencies, structural compatibility, nyitott probléma.

Az OS co-design víziója: ha az OS a ko-effektust első osztályú állampolgárként kezeli (minden erőforrás ko-effektusként érhető el, a sandboxing natív, a reifikáció a kernel szintjén történik), akkor a komponensek deklaratív formában írhatják le, mit érnek el, és az OS garantálja, hogy nem érnek el mást.

A cikk a 124 hivatkozással 4 tengely mentén pozicionálja magát:

Effect systems. ZIO/Effect-TS/fp-ts monadic embedding vs. Cordis overlay; Effekt capability-based scope-based vs. Cordis runtime tracking; Heunen et al. reversible arrows denotációs vs. Cordis runtime inverzek; Orchard et al. graded modal types statikus vs. Cordis dinamikus.
Programming paradigms. COP (rétegek aktiválása) vs. Cordis (komponensek revertálható betöltése); AOP (oblique pointcut-ok) vs. Cordis (deklarált ko-effektusok).
Temporal composability. DSU/HMR (state forward migration, kézzel írt transzformációk) vs. Cordis (automatikus revertálás); STM (statikus scope rollback) vs. Cordis (dinamikus lifecycle); Nooks/shadow drivers (kernel-szintű reclamation) vs. Cordis (komponens-szintű, általános).
Spatial composability. Spring/DI/Angular (boot-time wiring) vs. Cordis (runtime reactive); OSGi Declarative Services/iPOJO (availability-reactive, kézzel írt cleanup) vs. Cordis (automatikus revert); FRP/signals (value-level reactivity) vs. Cordis (component-level, async lifecycle).

A kulcsszó: Cordis egyszerre kínál futásidejű revertálhatóságot és futásidejű resettelhetőséget, ez a kombináció hiányzik minden más rendszerből.

8. Következtetés és az agent harness validáció¶

A cikk a kontextus-paradigmát és a Cordis-t létező megoldásként mutatja be: a Koishi 4000+ pluginnal bizonyítja, hogy a dinamikus kompozíció skálázódik production környezetben.

A jövőbeli validáció iránya kifejezetten az önfejlesztő agent harness-ek: - Temporal garancia (teljes recovery rapid komponens-csere alatt), az agent harness másodpercenként cserélheti a komponenseit - Spatial garancia (dependencia koordináció gyakori topológiai változás alatt), a harness topológiája futásidőben alakul

A DeepSeek-AI szerzői tehát saját use-case-ük validációs anyagaként publikálják a Cordis-t: a Cordis az ő saját harness engineering-jük formális alapja. Ez összhangban van a Henky MEMORY-ban rögzített "deepseek harness audit" kontextussal.

A két kulcs-claim: 1. Teljes recovery invariáns, nem a fejlesztő fegyelmén múlik 2. Reaktív re-feloldás, nem a boot-time wiring-on múlik

Ezek együttesen jelentik a Spatiotemporal Composability garanciáját: a rendszer térben és időben is biztonságosan komponálható, és ez a garancia strukturális, nem konvenció.

Forrás és meta¶

Forrás: (efemer gyorsítótár; a feltöltött PDF a takarítás óta nincs meg) ⚠️ (~2.1 MB, 88 oldal, 2330 sor kinyert szöveg) Topic: ai-automation.md (DeepSeek engineering + AI policy convergence pont) Feldolgozás: saját kiolvasás (PDF szövegkinyerés a read_file eszközzel) → kézi magyar összefoglaló → tanulmanyok pipeline patch.