Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Halting and Equivalence of Schemes over Recursive Theories

Halting and Equivalence of Schemes over Recursive Theories

File(s)
2002-1881.ps (113.81 KB)
Permanent Link(s)
https://hdl.handle.net/1813/5857
Collections
Computer Science Technical Reports
Author
Kozen, Dexter
Abstract

Let S be a fixed first-order signature. In this note we consider the following decision problems. (i) Given a recursive ground theory T over S, 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 recursive ground theory T over S 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 r.e.-complete and problem (ii) is Pi-0-2-complete. Both these problems remain hard for their respective complexity classes even if T is empty and 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.

Date Issued
2002-10-28
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2002-1881
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance