Loop variant (original) (raw)
In computer science, a loop variant is a mathematical function defined on the state space of a computer program whose value is monotonically decreased with respect to a (strict) well-founded relation by the iteration of a while loop under some invariant conditions, thereby ensuring its termination. A loop variant whose range is restricted to the non-negative integers is also known as a bound function, because in this case it provides a trivial upper bound on the number of iterations of a loop before it terminates. However, a loop variant may be transfinite, and thus is not necessarily restricted to integer values.
| Property | Value |
|---|---|
| dbo:abstract | In computer science, a loop variant is a mathematical function defined on the state space of a computer program whose value is monotonically decreased with respect to a (strict) well-founded relation by the iteration of a while loop under some invariant conditions, thereby ensuring its termination. A loop variant whose range is restricted to the non-negative integers is also known as a bound function, because in this case it provides a trivial upper bound on the number of iterations of a loop before it terminates. However, a loop variant may be transfinite, and thus is not necessarily restricted to integer values. A well-founded relation is characterized by the existence of a minimal element of every non-empty subset of its domain. The existence of a variant proves the termination of a while loop in a computer program by well-founded descent. A basic property of a well-founded relation is that it has no infinite descending chains. Therefore a loop possessing a variant will terminate after a finite number of iterations, as long as its body terminates each time. A while loop, or, more generally, a computer program that may contain while loops, is said to be totally correct if it is partially correct and it terminates. (en) |
| dbo:wikiPageID | 19024734 (xsd:integer) |
| dbo:wikiPageLength | 10501 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1040388185 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Primitive_recursive_function dbr:Partial_correctness dbr:Universal_quantification dbr:Μ-recursive_function dbr:Infinite_descending_chain dbr:Loop_invariant dbr:Transfinite_induction dbr:Predicate_transformer_semantics dbr:Order_type dbr:Μ_operator dbr:Function_(mathematics) dbr:Correctness_(computer_science) dbr:Computational_complexity_theory dbr:Computer_science dbr:State_(computer_science) dbr:C_(programming_language) dbr:Well-founded_relation dbr:Well-order dbr:Large_countable_ordinal dbr:For_loop dbr:Gödel's_incompleteness_theorems dbr:Halting_problem dbc:Control_flow dbc:Formal_methods dbr:Termination_analysis dbr:Tractable_problem dbr:Transfinite_number dbr:While_loop dbr:Axiom_of_choice dbr:Integer dbr:Kurt_Gödel dbr:Recursion_(computer_science) dbr:Turing_machine dbr:First_uncountable_ordinal dbr:Pseudocode dbr:Partial_order dbr:Floyd–Hoare_logic dbr:Ackermann's_function dbr:Descending_chain_condition |
| dbp:wikiPageUsesTemplate | dbt:Math dbt:Mvar dbt:Reflist dbt:Tmath dbt:Var |
| dct:subject | dbc:Control_flow dbc:Formal_methods |
| gold:hypernym | dbr:Function |
| rdf:type | yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Know-how105616786 yago:Method105660268 yago:PsychologicalFeature100023100 dbo:Disease yago:WikicatFormalMethods |
| rdfs:comment | In computer science, a loop variant is a mathematical function defined on the state space of a computer program whose value is monotonically decreased with respect to a (strict) well-founded relation by the iteration of a while loop under some invariant conditions, thereby ensuring its termination. A loop variant whose range is restricted to the non-negative integers is also known as a bound function, because in this case it provides a trivial upper bound on the number of iterations of a loop before it terminates. However, a loop variant may be transfinite, and thus is not necessarily restricted to integer values. (en) |
| rdfs:label | Loop variant (en) |
| owl:sameAs | freebase:Loop variant yago-res:Loop variant wikidata:Loop variant https://global.dbpedia.org/id/4rBAS |
| prov:wasDerivedFrom | wikipedia-en:Loop_variant?oldid=1040388185&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Loop_variant |
| is dbo:wikiPageRedirects of | dbr:Bound_function |
| is dbo:wikiPageWikiLink of | dbr:Loop_invariant dbr:Minkowski's_question-mark_function dbr:Control_flow dbr:Microsoft_and_open_source dbr:Dafny dbr:For_loop dbr:Hoare_logic dbr:Termination_analysis dbr:Recursion_(computer_science) dbr:Bound_function |
| is foaf:primaryTopic of | wikipedia-en:Loop_variant |