Abstract
We present a small step reduction semantics for the untyped lazy lambda calculus plus a non-deterministic choice. The addition of a fair scheduler enables the choice operator to avoid divergence, and so the semantics implements locally bottom-avoiding choice and not erratic choice. A big step semantics that is sound and complete with respect to the small step semantics is also presented. It includes inference rules for both convergent and divergent behaviour. The operational equivalence that is derived from the big step semantics is much more discriminating than that arising in current denotational models. The semantics is suitable as a basis for reasoning about non-deterministic functional programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming. Addison Wesley, 1990.
P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739–782. Elsevier, 1977.
P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In POPL ’91, Albuquerque, New Mexico, USA, January 1991.
U. de’Liguoro and A. Piperno. Must preorder in non-deterministic untyped λ-calculus. In CAAP ’92, volume 581 of LNCS, pages 203–220, February 1992.
C. A. Gunter. Relating total and partial correctness interpretations of non-deterministic programs. In POPL ’90, San Francisco, California, USA, January 17 – 19 1990.
M. A. B. Hennessy and E. A. Ashcroft. A mathematical semantics for a nondeterministic typed λ-calculus. Theoretical Computer Science, 11: 227 – 245, 1980.
R.Heckmann. Set domains. InESOP ’90volume 432 ofLNCSpages 177–196, May 1990.
J. McCarthy. A basis for a mathematical theory of computations. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, pages 33–70. North-Holland, 1963.
G.D. Plotkin. A powerdomain construction.SIAM Journal of Computing5(3):452–487, 1976.
G.D. Plotkin. LCF considered as a programming language.Theoretical Computer Science5:223–255, 1977.
G. D. Plotkin. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Aarhus University, 1981.
M.B. Smyth. Power domains.Journal of Computer and System Sciences,16(23–26):23–35, 1978.
M. B. Smyth. Power domains and predicate transformers: A topological view. In ICALP ’83, volume 154 of LNCS, pages 662 – 676, 1983.
D.Turner. An approach to functional operating systems. In D.Turner, editor, Research Topics in Functional Programming. Addison Wesley, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 British Computer Society
About this paper
Cite this paper
Hughes, J., Moran, A. (1993). A Semantics for Locally Bottom-Avoiding Choice. In: Launchbury, J., Sansom, P. (eds) Functional Programming, Glasgow 1992. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3215-8_9
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3215-8_9
Publisher Name: Springer, London
Print ISBN: 978-3-540-19820-8
Online ISBN: 978-1-4471-3215-8
eBook Packages: Springer Book Archive