Functional behavior of nondeterministic programs

  • Michael G. Main
  • David B. Benson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 158)


The functional behavior of a deterministic program is a function f:D→D, where D is some set of states for the computation. This notion of functional behaviors can be extended to nondeterministic programs using techniques from linear algebra. In particular, the functional behavior of a nondeterministic program is a linear transformation f:A→A, where A is a free semiring module. Other notions from linear algebra carry over into this setting. For example, weakest preconditions and predicate transformers correspond to well-studied concepts in linear algebra. Finally, we consider multiple-input and multiple-output programs. The functional behavior of a nondeterministic program with multiple inputs and outputs is a linear transformation f:⊗ m A→⊗ n A, where ⊗ x A is an iterated tensor product of the semiring module A. This is in contrast to the deterministic case, where such a program is a function f:D m →D n , using the Cartesian products D m and D n .


Tensor Product Linear Transformation Functional Behavior Deterministic State Commutative Monoid 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. (1).
    D.B. Benson. Counting paths: nondeterminism as linear algebra, to appear in IEEE Trans. Software Engineering.Google Scholar
  2. (2).
    D.B. Benson. Studies in fork-join parallelism, Washington State University Technical Report CS-82-101, Pullman, WA 99164 (1982).Google Scholar
  3. (3).
    E.W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs, CACM 18 (1975), 453–457.Google Scholar
  4. (4).
    E.W. Dijkstra. A Discipline of Programming, (Prentice-Hall, 1976).Google Scholar
  5. (5).
    P.A. Grillet. The tensor product of semi-groups, Trans. Amer. Math. Soc. 138 (1969), 267–280.Google Scholar
  6. (6).
    P.A. Grillet. The tensor product of commutative semi-groups, Trans. Amer. Math. Soc. 138 (1969), 281–293.Google Scholar
  7. (7).
    M.C.B. Hennessy and G.D. Plotkin. Full abstraction for a simple parallel programming language, in: Mathematical Foundations of Computer Science 79, LNCS 74, (Springer-Verlag, 1979), 108–120.Google Scholar
  8. (8).
    D. Kozen. Semantics of probabilistic programs, JCSS 22 (1981), 328–350.Google Scholar
  9. (9).
    S. MacLane and G. Birkhoff. Algebra, (MacMillan Publishing Co., 1979).Google Scholar
  10. (10).
    M.G. Main and D.B. Benson. An algebra for nondeterministic distributed processes, Washington State University Technical Report CS-82-087, Pullman, WA 99164 (1982).Google Scholar
  11. (11).
    E.G. Manes. A Class of Fuzzy Theories, J. Math. Analysis and Applications 85 (1982), 409–451.Google Scholar
  12. (12).
    G.D. Plotkin. A powerdomain construction, SIAM J. Computing 5 (1976), 452–487.Google Scholar
  13. (13).
    A. Poigné. Using least fixed points to characterize formal computations of non-determinate equations, in: Formalizations of Programming Concepts (J. Diaz and I. Ramos, Eds.), LNCS 107, (Springer-Verlag, 1981), 447–459.Google Scholar
  14. (14).
    A. Poigné. On effective computations of nondeterministic schemes, in: 5th International Symposium on Programming, LNCS 137, (Springer-Verlag, 1982), 323–336.Google Scholar
  15. (15).
    N. Saheb-Djahromi. CPO's of measures for nondeterminism, TCS 12 (1980), 19–37.Google Scholar
  16. (16).
    M. Smyth. Powerdomains, JCSS 16 (1978)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Michael G. Main
    • 1
  • David B. Benson
    • 2
  1. 1.Department of Computer ScienceUniversity of ColoradoBoulderUSA
  2. 2.Department of Computer ScienceWashington State UniversityPullman

Personalised recommendations