Size-change termination principle

Last updated

The size-change termination principle (SCT) guarantees termination for a computer program by proving that infinite computations always trigger infinite descent in data values that are well-founded. [1] Size-change termination analysis utilizes this principle in order to solve the universal halting problem for a certain class of programs. When applied to general programs, the principle is intended to be used conservatively, which means that if the analysis determines that a program is terminating, the answer is sound, but a negative answer means "don't know". The decision problem for SCT is PSPACE-complete; however, there exists an algorithm that computes an approximation of the decision problem in polynomial time. [2] Size-change analysis is applicable to both first-order [1] and higher-order functional programs, [3] as well as imperative programs [4] and logic programs. [5] The latter application preceded by four years the general formulation of the principle by Lee et al.

Contents

Overview

The size-change termination principle was introduced by Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram in 2001. [1] It relies on intermediary objects called size-change graphs that describe the relationship between source and destination parameters in a given function call (for a functional program). The method analyzes these graphs to make conclusions about the existence of monotonically decreasing sequences of parameters throughout the execution of a program. The size-change termination principle is stated as such:

If every infinite computation would give rise to an infinitely decreasing value sequence (according to the size-change graphs), then no infinite computation is possible. [1]

Size-change graphs express both the possible presence of a function call as well as whether parameters within function call decrease or do not increase. In order to derive termination from size-change graphs, Lee at al. formulate a sufficient condition in terms of the graphs (with no reference to the underlying program). This condition is decidable by an algorithm that operates solely on the graphs.

Size-change termination analysis is related to abstract interpretation, in particular to a technique called predicate abstraction. [6]

Relationship to the halting problem

The halting problem for Turing-complete computational models states that the decision problem of whether a program will halt on a particular input, or on all inputs, is undecidable. Therefore, a general algorithm for proving any program to halt does not exist. Size-change termination is decidable because it only asks whether termination is provable from given size-change graphs.

Related Research Articles

<span class="mw-page-title-main">Algorithm</span> Sequence of operations for a task

In mathematics and computer science, an algorithm is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing calculations and data processing. More advanced algorithms can use conditionals to divert the code execution through various routes and deduce valid inferences, achieving automation eventually. Using human characteristics as descriptors of machines in metaphorical ways was already practiced by Alan Turing with terms such as "memory", "search" and "stimulus".

In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved by a computer. A computation problem is solvable by mechanical application of mathematical steps, such as an algorithm.

<span class="mw-page-title-main">Discrete mathematics</span> Study of discrete mathematical structures

Discrete mathematics is the study of mathematical structures that can be considered "discrete" rather than "continuous". Objects studied in discrete mathematics include integers, graphs, and statements in logic. By contrast, discrete mathematics excludes topics in "continuous mathematics" such as real numbers, calculus or Euclidean geometry. Discrete objects can often be enumerated by integers; more formally, discrete mathematics has been characterized as the branch of mathematics dealing with countable sets. However, there is no exact definition of the term "discrete mathematics".

In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.

<span class="mw-page-title-main">Clique problem</span> Task of computing complete subgraphs

In computer science, the clique problem is the computational problem of finding cliques in a graph. It has several different formulations depending on which cliques, and what information about the cliques, should be found. Common formulations of the clique problem include finding a maximum clique, finding a maximum weight clique in a weighted graph, listing all maximal cliques, and solving the decision problem of testing whether a graph contains a clique larger than a given size.

In graph theory, the Robertson–Seymour theorem states that the undirected graphs, partially ordered by the graph minor relationship, form a well-quasi-ordering. Equivalently, every family of graphs that is closed under minors can be defined by a finite set of forbidden minors, in the same way that Wagner's theorem characterizes the planar graphs as being the graphs that do not have the complete graph K5 or the complete bipartite graph K3,3 as minors.

In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is functional correctness, which refers to the input-output behavior of the algorithm.

<span class="mw-page-title-main">Clique (graph theory)</span> Subset of the vertices of a node-link graph that are all adjacent to each other

In the mathematical area of graph theory, a clique is a subset of vertices of an undirected graph such that every two distinct vertices in the clique are adjacent. That is, a clique of a graph is an induced subgraph of that is complete. Cliques are one of the basic concepts of graph theory and are used in many other mathematical problems and constructions on graphs. Cliques have also been studied in computer science: the task of finding whether there is a clique of a given size in a graph is NP-complete, but despite this hardness result, many algorithms for finding cliques have been studied.

In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. Unlike other compressed representations, operations are performed directly on the compressed representation, i.e. without decompression.

In graph theory, the treewidth of an undirected graph is an integer number which specifies, informally, how far the graph is from being a tree. The smallest treewidth is 1; the graphs with treewidth 1 are exactly the trees and the forests. The graphs with treewidth at most 2 are the series–parallel graphs. The maximal graphs with treewidth exactly k are called k-trees, and the graphs with treewidth at most k are called partial k-trees. Many other well-studied graph families also have bounded treewidth.

In theoretical computer science, a pointer machine is an atomistic abstract computational machine model akin to the random-access machine. A pointer algorithm could also be an algorithm restricted to the pointer machine model.

In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function.

In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi-Elgot-Trakhtenbrot theorem gives a logical characterization of the regular languages.

In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. The halting problem is an example: it can be proven that there is no algorithm that correctly determines whether arbitrary programs eventually halt when run.

In the study of graph algorithms, Courcelle's theorem is the statement that every graph property definable in the monadic second-order logic of graphs can be decided in linear time on graphs of bounded treewidth. The result was first proved by Bruno Courcelle in 1990 and independently rediscovered by Borie, Parker & Tovey (1992). It is considered the archetype of algorithmic meta-theorems.

<span class="mw-page-title-main">Reachability problem</span> Problem in math and computer science

Reachability is a fundamental problem that appears in several different contexts: finite- and infinite-state concurrent systems, computational models like cellular automata and Petri nets, program analysis, discrete and continuous systems, time critical systems, hybrid systems, rewriting systems, probabilistic and parametric systems, and open systems modelled as games.

<span class="mw-page-title-main">Neil D. Jones</span>

Neil D. Jones was an American computer scientist. He was a Professor Emeritus in computer science at University of Copenhagen.

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that can be used in these sentences. The first-order logic of graphs concerns sentences in which the variables and predicates concern individual vertices and edges of a graph, while monadic second-order graph logic allows quantification over sets of vertices or edges. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power.

<span class="mw-page-title-main">Glossary of artificial intelligence</span> List of definitions of terms and concepts commonly used in the study of artificial intelligence

This glossary of artificial intelligence is a list of definitions of terms and concepts relevant to the study of artificial intelligence, its sub-disciplines, and related fields. Related glossaries include Glossary of computer science, Glossary of robotics, and Glossary of machine vision.

References

  1. 1 2 3 4 Lee, Chin Soon; Jones, Neil D.; Ben-Amram, Amir M.; Lee, Chin Soon; Jones, Neil D.; Ben-Amram, Amir M. (2001-01-01). "The size-change principle for program termination, The size-change principle for program termination". ACM SIGPLAN Notices. 36 (3): 81–92. doi:10.1145/360204.360210. ISSN   0362-1340. S2CID   12721873.
  2. ↑ Ben-Amram, Amir M.; Lee, Chin Soon (2007-01-01). "Program termination analysis in polynomial time". ACM Transactions on Programming Languages and Systems. 29 (1): 5. doi:10.1145/1180475.1180480. ISSN   0164-0925. S2CID   9093670.
  3. ↑ Sereni, Damien; Jones, Neil D. (2005). "Termination Analysis of Higher-Order Functional Programs". Programming Languages and Systems. Lecture Notes in Computer Science. Vol. 3780. pp. 281–297. CiteSeerX   10.1.1.102.4934 . doi:10.1007/11575467_19. ISBN   978-3-540-29735-2.
  4. ↑ Avery, James (2006). "Size-Change Termination and Bound Analysis". Functional and Logic Programming. Lecture Notes in Computer Science. Vol. 3945. pp. 192–207. doi:10.1007/11737414_14. ISBN   978-3-540-33438-5.
  5. ↑ Lindenstrauss, Naomi and Sagiv, Yehoshua. Automatic Termination Analysis of Prolog Programs. Proceedings of the Fourteenth International Conference on Logic Programming. MIT Press, 1997.
  6. ↑ Heizmann, Matthias; Jones, Neil D.; Podelski, Andreas (2010). "Size-Change Termination and Transition Invariants". Static Analysis. Lecture Notes in Computer Science. Vol. 6337. pp. 22–50. CiteSeerX   10.1.1.167.8500 . doi:10.1007/978-3-642-15769-1_4. ISBN   978-3-642-15768-4.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.