eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/14998
Title:  Halting and Equivalence of Program Schemes in Models of Arbitrary Theories 
Authors:  Kozen, Dexter 
Keywords:  dynamic model theory program scheme scheme equivalence 
Issue Date:  19May2010 
Abstract:  In this note we consider the following decision problems. Let S be a fixed firstorder signature.
(i) Given a firstorder 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 firstorder 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_1complete and problem (ii) is Pi^A_2complete. 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. 
URI:  http://hdl.handle.net/1813/14998 
Appears in Collections:  Computing and Information Science Technical Reports

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
