Halting and Equivalence of Program Schemes in Models of Arbitrary Theories

In this note we consider the following decision problems. Let be a fixed first-order signature. (i) Given a first-order theory or ground theory T over of Turing degree , a program scheme p over , and input values specified by ground terms t1, . . . , tn, does p halt on input t1, . . . , tn in all models of T? (ii) Given a first-order theory or ground theory T over of Turing degree and two program schemes p and q over , are p and q equivalent in all models of T? When T is empty, these two problems are the classical halting and equivalence problems for program schemes, respectively. We show that problem (i) is 1 -complete and problem (ii) is 2 -complete. Both problems remain hard for their respective complexity classes even if is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate. It follows from (ii) that there can exist no relatively complete deductive system for scheme equivalence over models of theories of any Turing degree...

• Type: Conference
• Year: 2010
• Where: BIRTHDAY
• Authors: Dexter Kozen
• Keywords: Applied Computing, BIRTHDAY 2010, First-order Theory, Program Schemes, Turing Degree