zbMATH — the first resource for mathematics

A theory for nondeterminism, parallelism, communication, and concurrency. (English) Zbl 0601.68022
An applicative language is introduced for representing concurrent programs and communicating systems in the form of mutually recursive systems of nondeterministic equations for functions and streams. Mathematical semantics is defined by associating particular fixed points with such systems. These fixed points are chosen using a combination of several complete partial orderings. Operational semantics is described in the form of term rewriting rules, consistent with the mathematical semantics. It represents data-driven reduction semantics for usual expressions and data-driven data flow semantics in the case of recursive stream equations. So the language allows to treat the basic semantic notions of nondeterminism, parallelism, communication, and concurrency for multiprogramming in a completely formal, applicative framework. In particular, it provides a semantic theory for networks of loosely coupled, nondeterministic, communicating, stream processing functions. Finally, the relationship of the presented language to partial recursive functions and nonconventional models such as data flow and reduction machines is shown.

68N25 Theory of operating systems
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Apt, K. R.; Plotkin, G., A Cook’s tour of countable nondeterminism, (Even, S.; Kariv, O., 8th Internat. Coll. on Automata, Languages and Programming, Haifa 1981, Lecture Notes in Computer Science, 115, (1981), Springer Berlin), 479-494 · Zbl 0465.68002
[2] Arnold, A., Operational and denotational semantics of nets of processes, Laboratoire Informatique Théoretique et Programmation, Université P. et M. Curie, Université Paris 7, Rept. No. 79-35, (June 1979)
[3] Arnold, A.; Nivat, M., Nondeterministic recursive program schemes, (Karpinski, M., Fundamentals of Computation Theory, Lecture Notes in Computer Science, 56, (1977), Springer Berlin), 12-21 · Zbl 0361.68020
[4] Arvind and K.P. Gostelow, Some relationships between asynchronous interpreters of a dataflow language, in: [72] 96-119. · Zbl 0374.68014
[5] Astesiano, E.; Costa, G., Sharing in nondeterminism, (Maurer, H. A., 6th Internat. Coll. on Algorithms, Languages and Programming, Lecture Notes in Computer Science, 71, (1979), Springer Berlin), 1-13
[6] Backus, J., Can programming be liberated from the von Neumann style? A functional style and its algebra of programs, Comm. ACM, 21, 8, 613-641, (1978) · Zbl 0383.68013
[7] de Bakker, J. W., Semantics and termination of nondeterministic recursive programs, (Michaelson, S.; Milner, R., Proc. 3rd Internat. Coll. on Automata, Languages and Programming, (1976), Edinburgh University Press Edinburgh), 435-477 · Zbl 0354.68021
[8] F.L. Bauer, Detailization and lazy evaluation, infinite objects and pointer representation, in: [9] 235-236. · Zbl 0408.68016
[9] Bauer, F. L.; Broy, M., Program construction, (Lecture Notes Internat. Summer School on Program Construction, Lecture Notes in Computer Science, 69, (1979), Springer Berlin), Marktoberdorf 1978 · Zbl 0396.00016
[10] Bauer, F. L.; Heinhold, J.; Samelson, K.; Sauer, R., Moderne rechenanlagen, (1965), Teubner Stuttgart · Zbl 0131.15605
[11] Bauer, F. L.; Wössner, H., Algorithmische sprache und programmentwicklung, (1981), Springer Berlin · Zbl 0466.68006
[12] Benson, D. B., Parameter passing in nondeterministic recursive programs, J. Comput. System Sci., 19, 50-62, (1979) · Zbl 0418.68011
[13] Berkling, K., Reduction machines for reduction languages, (Proc. 2nd Internat. Sym. on Computer Architecture, (1975)), 133-140
[14] Brock, J. D.; Ackermann, W. B., Scenarios: A model of non-determinate computation, (Diaz, J.; Ramos, I., Formalization of Programming Concepts, Lecture Notes in Computer Science, 107, (1981), Springer Berlin), 252-267, Peniscola 1981
[15] Broy, M., Transformation parallel ablaufender programme, (Dissertation, (February 1980), Fakultät für Mathematik, Technische Universität München) · Zbl 0461.68013
[16] Broy, M., Transformational semantics for concurrent programs, Inform. Process. Lett., 11, 2, 87-91, (1980) · Zbl 0444.68017
[17] Broy, M., Are fairness-assumptions fair?, (Proc. 2nd Internat. Conf. on Distributed Computing Systems, Paris 1981, (1981), IEEE), 116-125
[18] Broy, M., Prospects of new tools for software development, (Duijvestijn, A. J.W.; Lockemann, C. P., Trends in Information Processing Systems, Lecture Notes in Computer Science, 123, (1981), Springer Berlin), 106-121
[19] Broy, M., On language constructs for concurrent programming, (Händler, W., CONPAR ’81, Lecture Notes in Computer Science, 111, (1981), Springer Berlin), 141-154
[20] Broy, M., A fixed point approach to applicative multiprogramming, (Broy, M.; Schmidt, G., Theoretical Foundations of Programming Methodology, (1982), Reidel Boston/Dordrecht), 565-622 · Zbl 0508.68012
[21] Broy, M., Fixed point theory of communicating and concurrent processes, (IFIP TC 2 Working Conf. on Formal Description of Programming Concepts II, Garmisch-Patenkirchen, (1982)), 125-147
[22] Broy, M.; Bauer, F. L., A rational approach to language constructs for concurrent programs, Sci. Comput. Programm., 4, 2, 103-139, (1984) · Zbl 0536.68013
[23] Broy, M.; Wirsing, M., Initial versus terminal algebra semantics for partially defined abstract types, (1980), Institut für Informatik, Technische Universität München, TUM-I8018 · Zbl 0433.68014
[24] Broy, M.; Wirsing, M., On the algebraic specification of nondeterministic programming languages, (Astesiano, E.; Böhm, C., 6th Coll. on Trees in Algebra and Programming, Genua 1981, Lecture Notes in Computer Science, 112, (1981), Springer Berlin), 162-179 · Zbl 0462.68063
[25] Broy, M.; Wirsing, M., Unbounded nondeterminism—an exercise in abstract data types, (Langages et Traducteurs, Collection Seminaires, (1981), INRIA), 75-98
[26] M. Broy, R. Gnatz and M. Wirsing, Semantics of nondeterministic and noncontinuous constructs, in: [9] 553-592. · Zbl 0406.03059
[27] Broy, M.; Partsch, H.; Pepper, P.; Wirsing, M., Semantic relations in programming languages, (Lavington, S. H., Information Processing 80, Proc. IFIP 80, (1980), North-Holland Amsterdam), 101-106 · Zbl 0443.68005
[28] Burge, W. H., Stream processing functions, IBM J. Res. Develop., 19, 12-25, (1975) · Zbl 0295.68017
[29] Chandra, A. K., The power of parallelism and nondeterminism in programming, (Rosenfeld, J. L., Information Processing 74, Proc. IFIP Congress 74, (1974), North-Holland Amsterdam), 461-465
[30] Chandra, A. K., Computable nondeterministic functions, (Proc. 19th Ann. Symp. on Foundations of Computer Science, (1978)), 127-131
[31] Chandra, A. K.; Kozen, D. C.; Stockmeyer, L. J., Alternation, J. ACM, 28, 1, 114-133, (1981) · Zbl 0473.68043
[32] Dennis, J. B., First version of a data flow procedure language, (Robinet, B., Colloque sur la Programmation, Lecture Notes in Computer Science, 19, (1974), Springer Berlin), 362-367
[33] Dennis, J. B.; Weng, K. K.-S., An abstract implementation for concurrent computation with streams, (Proc. 1979 Internat. Conf. on Parallel Processing, (August 1979)), 35-45
[34] Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Comm. ACM, 22, 8, 465-476, (1979) · Zbl 0431.68016
[35] Dijkstra, E. W., A discipline of programming, (1976), Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013
[36] Egli, H., A mathematical model for nondeterministic computations, (1975), ETH Zürich, Unpublished report
[37] A.P. Ershov, On the essence of compilation, in: [72] 391-418. · Zbl 0373.68018
[38] Francez, N.; Rodeh, M., A distributed abstract data type implemented by a probabilistic communication scheme, (21st Ann. Symp. on Foundations of Computer Science, (October 1980))
[39] Friedmann, D. P.; Wise, D. S., CONS should not evaluate its arguments, (Michaelson, S.; Milner, R., Proc. 3rd Internat. Coll. on Automata, Languages and Programming, (1976), Edinburgh Univ. Press Edinburgh), 257-284 · Zbl 0461.68023
[40] Friedmann, D. P.; Wise, D. S., Applicative multiprogramming, (Techn. Rep., 72, (January 1978), Computer Science Dept., Indiana Univ), revised December 1978
[41] Friedmann, D. P.; Wise, D. S., A note on conditional expressions, Comm. ACM, 21, 11, 931-933, (1978) · Zbl 0386.68010
[42] Henderson, P., Functional programming: application and implementation, (1980), Prentice-Hall Englewood Cliffs, NJ · Zbl 0426.68059
[43] Henderson, P.; Morris, J. H., A lazy evaluator, (Techn. Rep. Series No. 85, (1976), Computing Laboratory, Univ. Newcastle upon Tyne)
[44] Hennessy, M. C.B., The semantics of call-by-value and call-by-name in a nondeterministic environment, SIAM J. Comput., 9, 1, 67-84, (1980) · Zbl 0437.68002
[45] Hennessy, M.; Ashcroft, E. A., The semantics of nondeterminism, (Michaelson, S.; Milner, R., Proc. 3rd Internat. Coll. on Automata, Languages and Programming, (1976), Edinburgh University Press Edinburgh), 479-493 · Zbl 0379.02015
[46] Hennessy, M.; Ashcroft, E. A., Parameter passing mechanisms and nondeterminism, (Proc. 9th ACM Symp. on Theory of Computing, (1977)), 306-311
[47] Hennessy, M.; Ashcroft, E. A., A mathematical semantics for typed λ-calculus, Theoret. Comput. Sci., 11, 227-245, (1980) · Zbl 0462.68006
[48] C. Hewitt and H. Baker, Actors and continuous functionals, in:[72] 367-390. · Zbl 0391.68046
[49] Hoare, C. A.R., Communicating sequential processes, Comm. ACM, 21, 8, 666-677, (1978) · Zbl 0383.68028
[50] Preliminary report on study and research on fifth-generation-computers, (October 1981), Japan
[51] Kahn, G., The semantics of a simple language for parallel processing, (Rosenfeld, J. L., Information Processing 74, Proc. of the IFIP Congress 74, (1974), North-Holland Amsterdam), 471-475
[52] Kahn, G.; MacQueen, D., Coroutines and networks of parallel processes, (Gilchrist, B., Information Processing 77, Proc. of the IFIP Congress 77, (1977), North-Holland Amsterdam), 994-998
[53] R.M. Keller, Denotational models for parallel programs with indeterminate operators, in: [72] 33-366.
[54] Keller, R. M., Semantics and applications of function graphs, (Techn. Rept. UUCS-80-112, (October 1980), Dept. of Computer Science, Univ. of Utah)
[55] Kennaway, J. R.; Hoare, C. A.R., A theory of nondeterminism, (de Bakker, J.; Leeuwen, J.v.d., Proc. 7th Internat. Coll. on Algorithms, Languages and Programming, Lecture Notes in Computer Science, 85, (1980), Springer Berlin), 338-350 · Zbl 0444.68027
[56] Kleene, S. C., Introduction to metamathematics, (1952), Van Nostrand New York · Zbl 0047.00703
[57] König, D., Theorie der endlicher und unedlicher graphen, (1950), Chelsea Publishing Company New York
[58] Kosinski, P. R., A data flow language for operating systems programming, SIGPLAN Notices, 8, 9, 89-94, (1973)
[59] Kosinski, P. R., A straightforward denotational semantics for nondeterminate data flow programs, (Proc. 5th Ann. Symp. on Principles of Programming Languages, (1977))
[60] Kosinski, P. R., Denotational semantics of determinate and nondeterminate data flow programs, (TR-220, (May 1979), MIT, Lab. for Computer Science)
[61] Landin, P. J., A correspondence between ALGOL 60 and Church’s lambda-notation: part I, Comm. ACM, 8, 2, 89-101, (1965) · Zbl 0134.33403
[62] Lehmann, D. J., Categories for fixpoint-semantics, (Proc. 17th Ann. Symp. on Foundations of Computer Science, (1976)), 122-126
[63] MacQueen, D. B., Models for distributed computing, IRIA Rapport de Recherche No. 351, (April 1979)
[64] Mago, G. A.; Mago, G. A., A network of r microprocessors to execute reduction languages, Internat. J. Comput. and Inform. Sci., Internat. J. Comput. and Inform. Sci., 8, 6, 435-471, (1979) · Zbl 0427.68029
[65] Manna, Z., The correctness of nondeterministic programs, Artificial Intelligence, 1, 1-26, (1970) · Zbl 0203.49402
[66] Manna, Z.; Ness, S.; Vuillemin, J., Inductive methods for providing properties of programs, Comm. ACM, 16, 8, 491-502, (1973) · Zbl 0278.68019
[67] McCarthy, J., A basis for a mathematical theory of computation, (Braffort, P.; Hirschberg, D., Computer Programming and Formal Systems, (1963), North-Holland Amsterdam), 33-70
[68] Milne, G.; Milner, R., Concurrent processes and their syntax, (Rept. CSR-2-77, (1977), Univ. of Edinburgh, Dept. of Computer Science)
[69] Milner, R., Processes: A mathematical model of computing agents, (Proc. Logic Colloquim, Bristol, (1973), North-Holland Amsterdam), 157-173
[70] Milner, R., A calculus of communicating systems, (Lecture Notes in Computer Science, 92, (1980), Springer Berlin) · Zbl 0452.68027
[71] Milner, R., On relating synchrony and asynchrony, (Intern. Rep. CSR-75-80, (1980), Dept. of Computer Science, Univ. of Edinburgh)
[72] (Neuhold, E. J., Formal Descriptions of Programming Concepts, (1978), North-Holland Amsterdam) · Zbl 0367.00022
[73] Nivat, M., Nondeterministic programs: an algebraic overview, (Lavington, S. H., Information Processing 80, Proc. of the IFIP Congress 80, (1980), North-Holland Amsterdam), 17-28
[74] Park, D., On the semantics of fair parallelism, (Björner, D., Abstract Software Specification, Lecture Notes in Computer Science, 86, (1980), Springer Berlin), 504-526
[75] Plotkin, G., A powerdomain construction, SIAM J. Comput., 5, 452-486, (1976) · Zbl 0355.68015
[76] Plotkin, G., LCF considered as a programming language, Theoret. Comput. Sci., 5, 3, 223-256, (1977) · Zbl 0369.68006
[77] Scott, D., Lambda-calculus: some models, some philosophy, (Barwise, J.; Keisler, H. J.; Kunen, K., The Kleene Symposium, (1980), North-Holland Amsterdam), 223-265
[78] Scott, D., Lectures on a mathematical theory of computation, (November 1980), Mathematical Institute, University of Oxford, preliminary version, completed
[79] Smyth, M. B., Power domains, J. Comput. System Sci., 16, 23-36, (1978) · Zbl 0391.68011
[80] Tesler, L. G.; Enea, H. J., A language design for concurrent processes, (Spring Joint Computer Conference, (1968)), 403-408
[81] Treleaven, P. C.; Brownbridge, D. R.; Hopkins, R. P., Data driven and demand driven computer architecture, (Techn. Rept. Series 168, (June 1981), Univ. of Newcastle upon Tyne)
[82] Turner, D. A., A new implementation technique for applicative languages, Software-Practice and Experience, 9, 31-49, (1979) · Zbl 0386.68009
[83] Vuillemin, J., Correct and optimal implementation of recursion in a simple programming language, J. Comput. Sci., 9, 3, 332-354, (1974)
[84] Vuillemin, J., Syntaxe, semantique et axiomatique d’un langage de programmation simple, (Interdisciplinary Systems Research, 12, (1975), Birkhauser Basel/Stuttgart) · Zbl 0327.68006
[85] Wadsworth, C., Semantics and pragmatics of lambda-calculus, Ph.D. Dissertation, (1971), Oxford
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.