Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog
Gianluca Amato, Mary DeMarco, James Lipton
TL;DR
The paper addresses the challenge of giving sound and complete semantics to resolution in Higher Order Hereditarily Harrop formulas ($HOHH$) underlying $ ext{λProlog}$, which is impeded by impredicativity in Church's type theory. It develops Uniform Algebras, an indexed, intuitionistic semantic framework built on a typed applicative structure and an $oldsymbol{ m ext{Ω}}$-valued valuation, and proves soundness of resolution within this model. Completeness is achieved through both a constructive Lindenbaum-algebra approach and a fixed-point construction $I^ullet$, along with an enriched-resolution variant that preserves conservativity over uniform proofs. The work yields multiple semantic characterizations (term-models, substitution semantics, Lindenbaum algebras, ideals) and demonstrates a tight correspondence between operational HOHH proof procedures and semantic truth, with broad implications for the theoretical foundations and potential automation of $ ext{λProlog}$-style logic programming. Overall, the results establish a robust, intuitionistic, model-theoretic basis for resolution in HOHH and its constructive completeness, highlighting the interplay between higher-order logic, type theory, and logic programming semantics.
Abstract
This paper introduces a model theory for resolution on Higher Order Hereditarily Harrop formulae (HOHH), the logic underlying the Lambda-Prolog programming language, and proves soundness and completeness of resolution. The semantics and the proof of completeness of the formal system is shown in several ways, suitably adapted to deal with the impredicativity of higher-order logic, which rules out definitions of truth based on induction on formula structure. First, we use the least fixed point of a certain operator on interpretations, in the style of Apt and Van Emden, Then a constructive completeness theorem is given using a proof theoretic variant of the Lindenbaum algebra, which also contains a new approach to establishing cut-elimination.