Abstract
For nondeterministic recursive equations over an arbitrary signature of function symbols including the nondeterministic choice operator "or" the interpretation is factorized. It is shown that one can either associate an infinite tree with the equations, then interprete the function symbol "or" as a nondeterministic choice operator and so mapping the tree onto a set of infinite trees and then interprete these trees. Or one can interprete the recursive equation directly yielding a set-valued function. Both possibilities lead to the same result, i.e. we obtain a commuting diagram. This explains and solves a problem posed in [Nivat 80]. Basically the construction gives a generalisation of the powerdomain approach applicable to arbitrary nonflat (nondiscrete) algebraic domains.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
M. Broy: Fixed point theory for communication and concurrency. In: D. Björner (ed): IF IP TC2 Working Conference on "Formal Description of Programming Concepts II". Garmisch, June 1982, Amsterdam-New York-Oxford: North Holland Publ. Company 1983, 125–147
M. Nivat: On the interpretation of recursive polyadic program schemes. Symposia Mathematica 15, 1975, 255–281
M. Nivat: Nondeterministic programs: an algebraic overview. S.H. Lavington (ed.): Information Processing 80, Proc. of the IFJP Congress 80, Amsterdam — New York — Oxford: North-Holland Publ. Comp. 1980, 17–28.
G. Plotkin: A powerdomain construction. SIAM J. on Computing 5, 1976, 452–486
M. B. Smyth: Power domains. J. CSS 16, 1978, 23–36
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Broy, M. (1984). On the Herbrand Kleene universe for nondeterministic computations. In: Chytil, M.P., Koubek, V. (eds) Mathematical Foundations of Computer Science 1984. MFCS 1984. Lecture Notes in Computer Science, vol 176. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030301
Download citation
DOI: https://doi.org/10.1007/BFb0030301
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-13372-8
Online ISBN: 978-3-540-38929-3
eBook Packages: Springer Book Archive