Differentiable Horn Programs: A Constructive Expressivity Theorem for Latent Rule Operators

Abstract

We introduce \textsc{LatentGamma}, a differentiable operator on the unit cube $[0,1{]}^M$ designed as a smooth surrogate of Tarski's immediate consequence operator $\TP$ associated with a definite Horn program $P$ on $M$ atoms. The operator is built as a five-stage composition combining sigmoidal gating, softmax routing, and a residual update that enforces monotonicity by construction. We establish four theoretical results. First, the iterated sequence is coordinate-wise non-decreasing and bounded by $\ind$, hence converges to a fixed point of \textsc{LatentGamma}; the operator itself is lattice-monotone on $[0,1{]}^M$. Second, our \emph{constructive expressivity theorem} shows that for every definite Horn program $P$ there exists a closed-form parameter assignment ${\theta }^{\ast }(P)$ and an explicit time bound $T_{\max }(P)$ such that the iterated sequence \emph{exactly} reproduces $\TPinf(F_0)$ for every initial fact set $F_0$ throughout the window $[D(P,F_0),T_{\max }(P)]$, where $D(P,F_0)\le M$ is the derivation depth. The window $T_{\max }$ is large in practice ($\ge 10^5$ for sparse programs) and reflects the finite-time nature of computation by smooth sigmoidal gates. Third, the oracle is robust to Gaussian noise on its body and head logits, with explicit non-asymptotic bounds. Fourth, we prove a matching information-theoretic lower bound on the parameter count. We provide a complete numerical validation on programs ranging from $M=33$ to $M=504$ atoms: oracle accuracy reaches $1.0000$ on $2000$ test cases with zero false-positive and false-negative rates, and the empirical noise tolerance ${\sigma }_{\max }$ scales precisely as the union bound $RM\cdot \Phi (-10/{\sigma }_{\eta })$ predicts.