Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-28T17:11:24.506Z Has data issue: false hasContentIssue false
  • English
  • Français

Non-deterministic structures of computation

Published online by Cambridge University Press:  10 November 2014

YUXI FU
YUXI FU*
Affiliation:
BASICS, Department of Computer Science, and MOE-MS Key Laboratory for Intelligent Computing and Intelligent Systems, Shanghai Jiaotong University, Shanghai 200240, China Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Divergence and non-determinism play a fundamental role in the theory of computation, and their combined effect on computational equality deserves further study. By looking at the issue from the point of view of both computation and interaction, we are led to a canonical equality for non-deterministic computation, revealing its rich algebraic structure. We study this structure in three ways. First, we construct a complete equational system for finite-state non-deterministic computation. The challenge with such a system is to find an equational alternative to fixpoint induction à la Milner. We establish a negative result in the form of the non-existence of a finite equational system for the canonical equality of non-deterministic computation to support our approach. We then investigate infinite-state non-deterministic computation in the light of definability and show that every recursively enumerable set is generated by an unobservable process. Finally, we prove that, as far as computation is concerned, the effect produced jointly by divergence and non-determinism is model independent for a large class of process models.

We use C-graphs, which are interesting in their own right, as abstract representations of the computational objects throughout the paper.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 25 , Issue 6 , September 2015 , pp. 1295 - 1338
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S. (1988) The Lazy Lambda Calculus. In: Turner, D. (ed.) Declarative Programming, Addison-Wesley 65–116.Google Scholar
Aceto, L. and Hennessy, M. (1992) Termination, Deadlock, and Divergence. Journal of the ACM 39 147–187.CrossRefGoogle Scholar
Baeten, J. and Weijland, W. (1990) Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press.CrossRefGoogle Scholar
Baeten, J., Bergstra, J. and Klop, J. (1987) On the Consistency of Koomen's Fair Abstraction Rule. Theoretical Computer Science 51 129–176.CrossRefGoogle Scholar
Barendregt, H. (1994) The Lambda Calculus: Its Syntax and Semantics, North-Holland.Google Scholar
Bloom, S. and Ésik, Z. (1994) Iteration Algebras of Finite State Process Behaviors. Unpublished paper.CrossRefGoogle Scholar
Bloom, B., Istrail, S. and Meyer, A. (1995) Bisimulation Can't be Traced. Journal of the ACM 42 232–268.CrossRefGoogle Scholar
Busi, N., Gabbrielli, M. and Zavattaro, G. (2003) Replication vs Recursive Definitions in Channel Based Calculi. In: Proceedings ICALP'03. Springer-Verlag Lecture Notes in Computer Science 2719 133–144.CrossRefGoogle Scholar
Busi, N., Gabbrielli, M. and Zavattaro, G. (2004) Comparing Recursion, Replication and Iteration in Process Calculi. In: Proceedings ICALP'04. Springer-Verlag Lecture Notes in Computer Science 3142 307–319.CrossRefGoogle Scholar
Cai, X. and Fu, Y. (2011) The λ-Calculus in the π-Calculus. Mathematical Structure in Computer Science 21 943–996.CrossRefGoogle Scholar
Cardone, F. and Hindley, J. (2009) Lambda Calculus and Combinators in the 20th Century. In: Gabbay, D. and Woods, J. (eds.) Handbook of the History of Logic, Volume 5: Logic from Russell to Church, Elsevier 723–817.CrossRefGoogle Scholar
Church, A. (1936) An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics 58 345–363.CrossRefGoogle Scholar
Cook, S. and Reckhow, R. (1973) Time Bounded Random Access Machines. Journal of Computer and System Science 7 354–375.CrossRefGoogle Scholar
Darondeau, P. (1990) Concurrency and Computability. In: Semantics of Systems of Concurrent Processes: Proceedings LITP Spring School on Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science 469 223–238.CrossRefGoogle Scholar
Davis, M. (1965) The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Raven Press.Google Scholar
van Emde Boas, P. (1990) Machine Models and Simulations. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: Algorithm and Complexity, volume A, Elsevier, 65–116.Google Scholar
Fu, Y. (2012) Theory of Interaction. Unpublished paper.Google Scholar
Fu, Y. (2013) The Value-Passing Calculus. In: Theories of Programming and Formal Methods. Springer-Verlag Lecture Notes in Computer Science 8051 166–195.CrossRefGoogle Scholar
Fu, Y. and Lu, H. (2010) On the Expressiveness of Interaction. Theoretical Computer Science 411 1387–1451.CrossRefGoogle Scholar
Giambiagi, P., Schneider, G. and Valencia, F. (2004) On the Expressiveness of Infinite Behavior and Name Scoping in Process Calculi. In: FOSSACS 2004. Springer-Verlag Lecture Notes in Computer Science 2987 226–240.CrossRefGoogle Scholar
van Glabbeek, R, Luttik, B. and Trčka, N. (2009) Branching Bisimilarity with Explicit Divergence. Fundamenta Informaticae 93 371–392.CrossRefGoogle Scholar
van Glabbeek, R. and Weijland, W. (1989) Branching Time and Abstraction in Bisimulation Semantics. In: Information Processing'89, North-Holland 613–618.Google Scholar
Gödel, K. (1931) Über Formal Unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme. Monatshefte für Mathematik und Verwandter Systeme I 38 173–198.CrossRefGoogle Scholar
Hennessy, M. (1981) A Term Model for Synchronous Processes. Computation and Control 51 58–75.CrossRefGoogle Scholar
Hennessy, M. (1988) An Algebraic Theory of Processes, MIT Press.Google Scholar
Hennessy, M. and Ingólfsdóttir, A. (1993) A Theory of Communicating Processes with Value-Passing. Information and Computation 107 202–236.CrossRefGoogle Scholar
Hennessy, M. and Lin, H. (1995) Symbolic Bisimulations. Theoretical Computer Science 138 353–369.CrossRefGoogle Scholar
Kleene, S. (1936a) General Recursive Functions of Natural Numbers. Mathematicsche Annalen 112 727–742.CrossRefGoogle Scholar
Kleene, S. (1936b) λ-Definablity and Recursiveness. Duke Mathematical Journal 2 340–353.CrossRefGoogle Scholar
Kleene, S. (1938) On Notation for Ordinal Numbers. Journal of Symbolic Logic 3 150–155.CrossRefGoogle Scholar
Kleene, S. (1952) Introduction to Metamathematics, Van Nostrand.Google Scholar
Kleene, S. (1981) Origin of Recursive Function Theory. Annals of the History of Computing 3 52–67.CrossRefGoogle Scholar
Lohrey, M., D'Argenio, P. and Hermanns, H. (2002) Axiomatising Divergence. In: Proceedings ICALP 2002. Springer-Verlag Lecture Notes in Computer Science 2380 585–596.CrossRefGoogle Scholar
Lohrey, M., D'Argenio, P. and Hermanns, H. (2005) Axiomatising Divergence. Information and Computation 203 115–144.CrossRefGoogle Scholar
Markov, A. (1960) The Theory of Algorithms. American Mathematical Society Translations, series 2 15 1–14.CrossRefGoogle Scholar
Mendler, M. and Lüttgen, G. (2010) Is Observational Congruence on μ-Expressions Axiomatisable in Equational Horn Logic? Information and Computation 208 634–651.CrossRefGoogle Scholar
Milner, R. (1980) A Calculus of Communicating Systems. Springer-Verlag Lecture Notes in Computer Science 92.CrossRefGoogle Scholar
Milner, R. (1983) Calculi for Synchrony and Asynchrony. Theoretical Computer Science 25 267–310.CrossRefGoogle Scholar
Milner, R. (1984) A Complete Inference System for a Class of Regular Behaviours. Journal of Computer and System Science 28 439–466.CrossRefGoogle Scholar
Milner, R. (1989a) Communication and Concurrency, Prentice Hall.Google Scholar
Milner, R. (1989b) A Complete Axiomatization System for Observational Congruence of Finite State Behaviours. Information and Computation 81 227–247.CrossRefGoogle Scholar
Milner, R. (1992) Functions as Processes. Mathematical Structures in Computer Science 2 119–146.CrossRefGoogle Scholar
Milner, R. (1993) Elements of Interaction. Communications of the ACM 36 78–89.CrossRefGoogle Scholar
Milner, R., Parrow, J. and Walker, D. (1992a) A Calculus of Mobile Processes: Part I. Information and Computation 100 1–40.CrossRefGoogle Scholar
Milner, R., Parrow, J. and Walker, D. (1992b) A Calculus of Mobile Processes: Part II. Information and Computation 100 41–77.CrossRefGoogle Scholar
Milner, R and Sangiorgi, D. (1992) Barbed Bisimulation. In: Proceedings ICALP'92. Springer-Verlag Lecture Notes in Computer Science 623 685–695.CrossRefGoogle Scholar
Minsky, M. (1967) Computation: Finite and Infinite Machines, Prentice-Hall.Google Scholar
Park, D. (1981) Concurrency and Automata on Infinite Sequences. In: Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science 104 167–183.CrossRefGoogle Scholar
Post, E. (1943) Formal Reduction of the General Combinatorial Decision Problem. American Journal of Mathematics 65 197–215.CrossRefGoogle Scholar
Priese, L. (1978) On the Concept of Simulation in Asynchronous, Concurrent Systems. Progress in Cybernetics and Systems Research 7 85–92.Google Scholar
Rogers, H. (1987) Theory of Recursive Functions and Effective Computability, MIT Press.Google Scholar
Sangiorgi, D. (2009) On the Origin of Bisimulation and Coinduction. Transactions on Programming Languages and Systems 31 (4).CrossRefGoogle Scholar
Sangiorgi, D. and Walker, D. (2001) The π Calculus: A Theory of Mobile Processes, Cambridge University Press.Google Scholar
Sewell, P. (1994) Bisimulation is not Finitely (First Order) Equationally Axiomatisable. In: Proceedings LICS'94, IEEE 62–70.CrossRefGoogle Scholar
Sewell, P. Nonaxiomatisability of Equivalence Over Finite State Processes. Annals of Pure and Applied Logic 90 163–191.CrossRefGoogle Scholar
Shepherdson, J. and Sturgis, H. (1965) Computability and Recursive Functions. Journal of Symbolic Logic 32 1–63.Google Scholar
de Simone, R. (1984) On Meije and SCCS: Infinite Sum Operators vs. Non-Guarded Definitions. Theoretical Computer Science 30 133–138.CrossRefGoogle Scholar
de Simone, R. (1985) Higher-Level Synchronising Devices in Meije-SCCS. Theoretical Computer Science 37 245–267.CrossRefGoogle Scholar
Srba, J. (2004a) Completeness Results for Undecidable Bisimilarity Problems. Electronic Notes in Theoretical Computer Science 98 5–19.CrossRefGoogle Scholar
Srba, J. (2004b) Roadmap of Infinite Results. In: Formal Models and Semantics: II, World Scientific.CrossRefGoogle Scholar
Turing, A. (1936) On Computable Numbers, with an Application to the Entsheidungsproblem. Proceedings of the London Mathematical Society 42 230–265.Google Scholar
Turing, A. (1937a) Computability and λ-Definability. Journal of Symbolic Logic 2 153–163.CrossRefGoogle Scholar
Turing, A. (1937b) On Computable Numbers, with an Application to the Entsheidungsproblem: a Correction. Proceedings of the London Mathematical Society 43 544–546.Google Scholar
Vaandrager, F. (1993) Expressiveness Results for Process Algebras. In: Proceedings REX Workshop on Semantics: Foundations and Applications. Springer-Verlag Lecture Notes in Computer Science 666 609–638.CrossRefGoogle Scholar
Walker, D. (1990) Bisimulation and Divergence. Information and Computation 85 202–241.CrossRefGoogle Scholar
Wegener, I. (2005) Complexity Theory, Springer-Verlag.Google Scholar