Types for Grassroots Logic Programs
This work addresses the challenge of ensuring correctness in complex communication modalities for logic programming, particularly when using AI for code generation, by introducing a type system that can handle deadlocks, failures, and non-termination, though it is incremental as it builds on prior type definitions for logic programs.
The paper tackles the problem of typing interactive partial computations in Grassroots Logic Programs (GLP), a concurrent logic programming language, by defining types as regular sets of moded paths to capture communication directionality, and proves that well-typing corresponds to covariance and contravariance conditions in the semantics. It also implements the type system in Dart using AI, advocating for a joint human-AI development process to improve programming reliability.
Grassroots Logic Programs (GLP) is a concurrent logic programming language in which logic variables are partitioned into paired readers and writers. An assignment is produced at most once via a writer and consumed at most once via its paired reader, and may contain additional readers and/or writers. This enables the concise expression of rich multidirectional communication modalities. ``Logic Programs as Types for Logic Programs'' (LICS'91) defined types as regular sets of paths over derivable ground atoms. Here, we define types to be regular sets of moded paths, where a mode captures directionality of communication -- whether a subterm is consumed from or produced to the environment -- enabling the typing of interactive partial computations including those that eventually deadlock or fail, or never terminate. We provide a syntactic definition of well-typing and prove that a program is well-typed iff the path abstraction of its moded-atom semantics satisfies covariance and contravariance conditions with respect to its type. The GLP type system was implemented in Dart by AI, starting from a mathematical specification of Typed GLP (this paper), deriving from it an English spec (written by AI), and from the spec deriving Dart code (by AI). While GLP is naturally untyped, the motivation for Typed GLP comes from programming with AI: Asking AI to program complex communication modalities in GLP (and in general) and hoping for the best is a tenuous strategy. The emerging discipline we advocate and employ is for the human designer and AI to jointly develop and agree upon (1)~GLP types; (2)~GLP procedure type declarations; (3)~informal (English) descriptions of the procedures; and only then let AI attempt to write (4)~GLP code based on those.