Traducción de ingeniería de los teoremas formales
El artículo §4.4 da 6 teoremas metateóricos centrales. Aquí no listamos las pruebas; solo traducimos cada teorema a "qué significa para un Agent Runtime real". Entender Confluence es la clave para entender el valor de todo el artículo.
Tabla de traducción de ingeniería de los seis teoremas
[Conclusión original del artículo §4.4]
| Teorema | Sección | Traducción de ingeniería |
|---|---|---|
| Preservation (Thm 59) | §4.4.1 | Tras cualquier aplicación de regla, el registry sigue siendo well-formed: los punteros parent caen dentro del registry, los provisions de distintos fibers son disjuntos, y el committed view solo apunta a fibers installed. Significado: el runtime nunca se encuentra en un estado con "referencias a fiber colgantes" o "dos plugins afirmando ambos proveer 'database'". |
| Recovery Exactness (Thm 61) | §4.4.2 | Bajo el supuesto de pairwise independence, para un episode [b, u] del fiber n, aplicar su accumulator equivale al estado "n nunca se cargó" (salvo campos de control). Significado: tras descargar un plugin, el estado del entorno equivale a que nunca hubiera existido — crucial para HMR y reemplazo en caliente de plugins. |
| Ordering (Thm 63) | §4.4.3 | Los Providers deben activarse antes que los Consumers y descargarse después; la resolución de dependencias (committed view) que un Consumer lee a lo largo de un episode es invariante. Significado: los pools de conexiones no se cierran hasta que se devuelven todas las conexiones; las bases de datos no se cierran hasta que todas las transacciones se comprometen; no hay "race condition donde el consumer lee un provider medio cerrado". |
| Resolution Coherence (Thm 64) | §4.4.3 | Todas las iterations de una transición se ejecutan bajo el mismo committed view; si target cambia a mitad, o se completa hacia Active, o se entra en Unloading vía L-Divert/L-Raise y se revierte por completo. Significado: al cargar componentes de forma asíncrona no se llega a "medio viejo, medio nuevo" — parte de los effects no pueden usar dependencias viejas mientras otra parte usa dependencias nuevas. |
| Progress (Thm 66) | §4.4.4 | Bajo los supuestos de ≺ acíclico, len(e_n) ≤ K, y nombres de fiber finitos, un estado non-quiescent siempre tiene una regla aplicable, y el número de steps por fiber es acotado. Significado: el sistema no puede entrar en deadlock (los guards siempre se liberan); cada cambio de configuración alcanza eventualmente un estado estable. |
| Confluence (Thm 73) | §4.4.5 | Bajo los supuestos de pairwise independence, component total on provision y no failure, por muchas cargas/descargas/reemplazos que ocurran, siempre que la configuración final sea la misma, el estado estable equivale a un arranque limpio desde esa configuración final. Significado: la historia dinámica no deja rastro — tras un Agente haber reemplazado repetidamente sus propios componentes, equivale a un arranque único con la configuración final. Es la piedra angular teórica del "Agente auto-evolutivo". |
Confluence: la historia dinámica no deja rastro
Confluence es el clímax de esta teoría y merece una exposición aparte.
Enunciado intuitivo: después de que el sistema pase por cualquier número de cargas, descargas y reemplazos dinámicos, siempre que la configuración final sea la misma, su estado estable debería ser equivalente al obtenido arrancando limpio desde la configuración final.
Para un Agente auto-evolutivo, esto significa: supongamos que el Agente reemplaza la herramienta A tres veces seguidas, descarga y reinstala el Skill B dos veces, y ajusta el isolation realm del sub-Agente C; mientras su configuración final de componentes sea la misma que la de "algún arranque limpio", entonces el estado estable del runtime (qué componentes están activos, sus committed views, el estado del entorno acumulado) es equivalente al de ese arranque limpio. La historia dinámica no deja ningún rastro.
Esta es una garantía que otros frameworks DI/HMR no ofrecen:
- La DI tradicional no soporta reemplazo en runtime, así que no hay Confluence que hablar;
- HMR exige a los desarrolladores escribir a mano funciones de migración de estado, sin garantía formal de que la migración sea correcta;
- La orquestación de contenedores "reiniciar = limpio" descarta todo el estado de forma gruesa, no es una equivalencia de la misma granularidad.
[Conclusión original del artículo §4.4.5] Nótese las precondiciones de Confluence:
- pairwise independence: los effects son independientes entre sí o conmutan (Def 19);
- component total on provision: todo component instala realmente todas las keys que declara (Def 69);
- no failure: se excluyen los escenarios de failure.
[Conclusión original del artículo §4.4.5] Confluence excluye los escenarios de failure (L-Raise en §4.3.4) — porque los failures son una fuente real de divergencia: un schedule puede fallar mientras otro puede tener éxito, pero Cor 62 garantiza que la contribución de un fiber failed al state es 0 (los efectos secundarios del componente fallido se revierten por completo y no afectan a otros fibers). Así que "failure" no rompe la consistencia del estado, pero sí provoca que dos caminos dinámicos diverjan (uno con failure, otro sin él).
Lo que esta prueba no garantiza
[Conclusión original del artículo §6.1, §6.3] Las pruebas formales solo cubren los efectos secundarios gestionados a través del Context. No garantizan que:
- Los inverses escritos por los desarrolladores sean necesariamente correctos (la condición witness
g(δ)=γes una obligación, no verificada); - Efectos secundarios fuera del Context (modificar directamente variables globales, ficheros, bases de datos, sistemas externos) puedan revertirse;
- Emisiones externas (peticiones de red, mensajes, correos, pagos) puedan revertirse automáticamente — una vez emitidas, cruzan la frontera del sistema;
- La seguridad de plugins no fiables — el control de acceso a nivel de Context no puede sustituir a un sandbox de proceso/contenedor/WASM;
- Confluence bajo escenarios de failure (explícitamente excluido);
- Compatibilidad de versiones y estructural de las claves de dependencia (§6.6 open problem).
Para Preconditions y límites detallados ver Límites y evaluación general. Para cómo aterriza esta teoría en DeepSeek Harness ver La relación con DeepSeek Harness.