In computability theory, Bekić's theorem or Bekić's lemma is a theorem about fixed-points which allows splitting a mutual recursion into recursions on one variable at a time.[1][2][3] It was created by Austrian Hans Bekić (1936-1982) in 1969,[4] and published posthumously in a book by Cliff Jones in 1984.[5]

The theorem is set up as follows.[1][4] Consider two operators and on pointed directed-complete partial orders and , continuous in each component. Then define the operator . This is monotone with respect to the product order (componentwise order). By the Kleene fixed-point theorem, it has a least fixed point , a pair in such that and .

Bekić's theorem (called the "bisection lemma" in his notes)[4] is that the simultaneous least fixed point can be separated into a series of least fixed points on and , in particular:

In this presentation is defined in terms of . It can instead be defined in a symmetric presentation:[1][6][7]

Proof (Bekić):

since it is the fixed point. Similarly . Hence is a fixed point of . Conversely, if there is a pre-fixed point with , then and ; hence and is the minimal fixed point.

Variants

In a complete lattice

A variant of the theorem strengthens the conditions on and to be that they are complete lattices, and finds the least fixed point using the Knaster–Tarski theorem. The requirement for continuity of and can then be weakened to only requiring them to be monotonic functions.[1][3]

Categorical formulation

Bekić's lemma has been generalized to fix-points of endofunctors of categories (initial -algebras).[8]

Given two functors and such that all and exist, the fix-point is carried by the pair:

Usage

Bekić's theorem can be applied repeatedly to find the least fixed point of a tuple in terms of least fixed points of single variables. Although the resulting expression might become rather complex, it can be easier to reason about fixed points of single variables when designing an automated theorem prover.[9]

References

  1. 1 2 3 4 Winskel, Glynn (5 February 1993). The Formal Semantics of Programming Languages: An Introduction. MIT Press. p. 163. ISBN 978-0-262-73103-4.
  2. Díaz-Caro, Alejandro; Martínez López, Pablo E. (2015). "Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an implementation of λ +". Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages - IFL '15: 8. arXiv:1511.09324. doi:10.1145/2897336.2897346. S2CID 10413161.
  3. 1 2 Harper, Robert (Spring 2020). "Tarski's Fixed Point Theorem for Power Sets" (PDF). 15-819 Computational Type Theory Notes. Retrieved 7 March 2022.
  4. 1 2 3 Bekić, Hans (1984). "Definable operations in general algebras, and the theory of automata and flowcharts". Programming Languages and Their Definition. Lecture Notes in Computer Science. Vol. 177. pp. 30–55. doi:10.1007/BFb0048939. ISBN 3-540-13378-X.
  5. Jones, Cliff B. (1984). "Front matter" (PDF). In Jones, C. B (ed.). Programming Languages and Their Definition. Lecture Notes in Computer Science. Vol. 177. doi:10.1007/BFb0048933. ISBN 3-540-13378-X. S2CID 7488558.
  6. Leiss, Hans (2016). "The Matrix Ring of a mu-Continuous Chomsky Algebra is mu-Continuous" (PDF). 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs). 62: 6:1–6:15. doi:10.4230/LIPIcs.CSL.2016.6. ISBN 9783959770224.
  7. Arnold, A.; Niwinski, D. (7 February 2001). Rudiments of Calculus. Elsevier. p. 27. ISBN 978-0-08-051645-5.
  8. Lehmann, Daniel J.; Smyth, Michael B. (1981-12-01). "Algebraic specification of data types: A synthetic approach". Mathematical Systems Theory. 14 (1): 97–139. doi:10.1007/BF01752392. ISSN 1433-0490. S2CID 23076697.
  9. Andersen, Henrik Reif; Winskel, Glynn (1992). "Compositional checking of satisfaction". Computer Aided Verification. Lecture Notes in Computer Science. Vol. 575. pp. 24–36. doi:10.1007/3-540-55179-4_4. ISBN 978-3-540-55179-9.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.