Relaxed Residuation Theory

Inversion is the ideal form of backward reasoning: given an output value, one recovers the input that produced it. Classical residuation weakens this picture order-theoretically, replacing exact inversion by an adjoint backward trans- former. In many semantic and abstract-interpretation settings, however, both exact inverses and classical residuals are unavailable, while sound backward abstraction or selection is still needed. We develop a theory of relaxed residuation by systematically weakening inver- sion. Starting from the two equations defining an inverse, we relax different combinations of exactness, optimality, and monotonicity, obtaining notions that lie between ordinary inversion and classical adjunction. The resulting backward selectors preserve residual-like soundness constraints, but need not be monotone. We characterize their existence through structural properties of the forward map, capturing when fibers, principal ideals, and principal filters admit suitable greatest or least elements. We then show that these relaxed residuals induce relaxed Galois connections, relaxed Galois insertions, and relaxed closure operators, thereby providing an abstract-interpretation framework beyond classical adjunctions. The framework applies to settings where a concretization or representation map has sound abstract representatives but no classical best abstraction, as in automata-based abstractions of language semantics. Finally, we reinterpret local completeness and abstract- domain repair through the Pareto frontiers induced by the relaxed framework.