On backtracking and greatest fixpoints

  • Willem P. de Roever
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 52)


Descriptions and correctness proofs are discussed of three algorithms involved with iterative processing of tree-structured computations: iterative traversal of a binary tree, a backtracking algorithm, and a marking algorithm of a binary directed graph which constructs a spanning tree of that graph (the Deutsch-Schorr-Waite marking algorithm). The backtracking algorithm is believed to be novel. Intuitively these proofs are complicated by the fact that one does not know beforehand whether the processed space of computations is finite or infinite (; in the finite case a proof is simple). The complication due to the possibility of an infinite (search) space is dealt with by introducing an induction principle which asserts that a given computation is necessarily infinite, and therefore yields an undefined result. This principle, greatest fixpoint induction, is both in its actual mechanics and in spirit complementary to Burstall's structural induction.


Span Tree Binary Tree Correctness Proof Structural Induction Induction Principle 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [1]
    De Bakker, Termination of nondeterministic programs, in 3rd colloquium on automata, languages & programming, Michelson & Milner (eds.), Edinburgh University Press, 1976.Google Scholar
  2. [2]
    Hitchcock & Park, Induction rules and proofs of termination, in Proc. IRIA symp. on automata, formal languages, and programming, M. Nivat (ed.), North-H., 1972.Google Scholar
  3. [3]
    Milne, Private communication.Google Scholar
  4. [4]
    Park, Fixpoint induction and proof of program semantics, in Machine Intelligence V, pp 59–78, Edinb. Univ. Press, 1970.Google Scholar
  5. [5]
    de Roever, On proofs about backtracking: a tutorial, report no.51, Dép. d'Informatique, Univ. de Rennes, France, 1976.Google Scholar
  6. [6]
    De Roever, Lecture notes for “Introduction to programme correctness” unpublished notes, Univ. of Oxford, 1975.Google Scholar
  7. [7]
    de Roever, Maximal fixpoints solve some of the problems with Scott induction, Université de Rennes, France, 1976.Google Scholar
  8. [8]
    Topor, Correctness of the Schorr-Waite list marking algorithm, Memo MIP — R-104, School of Artificial Intelligence, Univ. of Edinburgh, 1974.Google Scholar
  9. [9]
    Manna & McCarthy, Properties of programs and partial function logic, in M.I.V., Meltzer & Michie (eds.), Edinb. Univ. Press, 1970.Google Scholar
  10. [10]
    Burstall, Program proving as hand simulation with a little induction, IFIP 74, North-Holland.Google Scholar
  11. [11]
    De Roever, Recursion and parameter mechanisms: an axiomatic approach, Proc. 2nd coll. on Automata, Languages, and Programming, Springer C. Sc. 14 (1974).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1977

Authors and Affiliations

  • Willem P. de Roever
    • 1
  1. 1.Queen's University at Belfast/Mathematisch CentrumAmsterdam

Personalised recommendations