A Programming Language for the Inductive Sets, and Applications

Abstract

We introduce a programming language IND that generalizes alternating Turing machines to arbitrary first-order structures. We show that IND programs (respectively, everywhere-halting IND programs, loop-free IND programs) accept precisely the inductively definable (respectively, hyperelementary, elementary) relations. We give several examples showing how the language provides a robust and computational approach to the theory of first-order inductive definability. We then show: (1) on all acceptable structures (in the sense of Moschovakis), r.e. Dynamic Logic is more expressive than finite-test Dynamic Logic. This refines a separation result of Meyer and Parikh; (2) IND provides a natural query language for the set of fixpoint queries over a relational database, answering a question of Chandra and Harel.