JavaScript is disabled for your browser. Some features of this site may not work without it.
Halting and Equivalence of Program Schemes in Models of Arbitrary Theories
dc.contributor.author | Kozen, Dexter | |
dc.date.accessioned | 2010-05-19T16:04:59Z | |
dc.date.available | 2010-05-19T16:04:59Z | |
dc.date.issued | 2010-05-19T16:04:59Z | |
dc.identifier.uri | https://hdl.handle.net/1813/14998 | |
dc.description.abstract | In this note we consider the following decision problems. Let S be a fixed first-order signature. (i) Given a first-order theory or ground theory T over S of Turing degree A, a program scheme p over S, 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 S of Turing degree A and two program schemes p and q over S, 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 Sigma^A_1-complete and problem (ii) is Pi^A_2-complete. Both problems remain hard for their respective complexity classes even if S 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. | en_US |
dc.description.sponsorship | NSF CCF-0635028 | en_US |
dc.language.iso | en_US | en_US |
dc.subject | dynamic model theory | en_US |
dc.subject | program scheme | en_US |
dc.subject | scheme equivalence | en_US |
dc.title | Halting and Equivalence of Program Schemes in Models of Arbitrary Theories | en_US |
dc.type | technical report | en_US |