We study positive–negative guarded systems of language equations over a fixed finite alphabet. The ambient space is the complete ultrametric space of all formal languages equipped with a length-based distance, where two languages are close whenever they agree on all words up to a sufficiently large length. The systems considered here contain both positive recursive dependencies and negative dependencies expressed through language complements. To handle this mixed structure, we introduce a suitable product order on pairs of languages and prove that the associated system operator has the weak monotone property. We show that the complement is an isometry for the length-based ultrametric and establish a signed wrapping estimate for guarded positive and negative language terms. These estimates lead to an ordered contraction principle for comparable pairs. As a consequence, the canonical lower and upper Picard iterations converge to the same limit, which is the unique fixed pair of the system. We also derive an explicit convergence rate and a finite-depth certification result: after a prescribed number of iterations, the approximants agree with the fixed-point semantics on all words below a given length. Additional symmetry assumptions are shown to force the unique fixed pair to be diagonal, reducing the system to a single language equation. Finally, we discuss an application to trace-based policies for tool-using AI agents. In this interpretation, finite executions of an agent are represented as words over an alphabet of observable tool-events, and the two components of the fixed point provide a stable semantics for policy-defined admissible and risky trace classes. The resulting framework gives a mathematically certified method for finite-depth analysis of recursive trace-based policies based on ultrametric fixed-point techniques.
Ajeti et al. (Sat,) studied this question.