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 θ*(P) and an explicit time bound Tmax(P) such that the iterated sequence \emph{exactly} reproduces TPinf(F0) for every initial fact set F0 throughout the window [D(P, F0), Tmax(P)], where D(P, F0) ≤ M is the derivation depth. The window Tmax is large in practice (≥ 105 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 σmax scales precisely as the union bound RM · Φ(−10/ση) predicts.
Related
- Constructive Bounds for the Topological Expressivity of Neural Networks
- Fractional Laplace Neural Operators: Exact Architectures, an Expressivity Frontier at Criticality, and Certified Stability for Memory-Driven Network Dynamics
- Constructive equivalence between Brouwer's fixed-point theorem and weak König's lemma
- Polynomial Spectral Gap Estimates for Finitely Differentiable Quasi-Periodic Schrödinger Operators
- On the convolution theorem for directionally pathwise differentiable functionals
BibTeX
@misc{mejri2026differentiable,
title = {{Differentiable Horn Programs: A Constructive Expressivity Theorem for Latent Rule Operators}},
author = {Aymen Mejri},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.06235},
eprint = {2609.06235},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.06235},
}
RIS
TY - UNPB
TI - Differentiable Horn Programs: A Constructive Expressivity Theorem for Latent Rule Operators
AU - Aymen Mejri
PY - 2026
DA - 2026/09/05
PB - arXiv
DO - 10.48550/arxiv.2609.06235
UR - https://arxiv.org/abs/2609.06235
AB - 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 θ^*(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) ≤ M is the derivation depth. The window T_max is large in practice (≥ 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 σ_max scales precisely as the union bound RM · Φ(−10/σ_η) predicts.
ER -