Muutke küpsiste eelistusi

Models of Computation 1st ed. 2017 [Kõva köide]

3.00/5 (2 hinnangut Goodreads-ist)
,
  • Formaat: Hardback, 395 pages, kõrgus x laius: 235x155 mm, kaal: 7509 g, 1 Illustrations, color; 33 Illustrations, black and white; XXII, 395 p. 34 illus., 1 illus. in color., 1 Hardback
  • Sari: Texts in Theoretical Computer Science. An EATCS Series
  • Ilmumisaeg: 10-Apr-2017
  • Kirjastus: Springer International Publishing AG
  • ISBN-10: 3319428985
  • ISBN-13: 9783319428987
Teised raamatud teemal:
  • Kõva köide
  • Hind: 57,96 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Tavahind: 68,19 €
  • Säästad 15%
  • Raamatu kohalejõudmiseks kirjastusest kulub orienteeruvalt 2-4 nädalat
  • Kogus:
  • Lisa ostukorvi
  • Tasuta tarne
  • Tellimisaeg 2-4 nädalat
  • Lisa soovinimekirja
Models of Computation 1st ed. 2017Suurem pilt
  • Formaat: Hardback, 395 pages, kõrgus x laius: 235x155 mm, kaal: 7509 g, 1 Illustrations, color; 33 Illustrations, black and white; XXII, 395 p. 34 illus., 1 illus. in color., 1 Hardback
  • Sari: Texts in Theoretical Computer Science. An EATCS Series
  • Ilmumisaeg: 10-Apr-2017
  • Kirjastus: Springer International Publishing AG
  • ISBN-10: 3319428985
  • ISBN-13: 9783319428987
Teised raamatud teemal:
Püsilink: https://www.kriso.ee/db/9783319428987.html
Märksõnad:
This book presents in their basic form the most important models of computation, their programming paradigms, and their mathematical descriptions, both concrete and abstract. The authors also describe important techniques for reasoning on them and for proving some essential properties. After preliminary chapters that introduce the notions of structure and meaning, semantic methods, inference rules, and logic programming, the authors arrange their chapters into parts on IMP, a simple imperative language; HOFL, a higher-order functional language, concurrent systems, and probabilistic systems.The book will be useful for undergraduate and graduate courses on theoretical computer science.

Preliminaries.- Operational Semantics of IMP.- Induction and Recursion.- Partial Orders and Fixpoints.- Denotational Semantics of IMP.- Operational Semantics of HOFL.- Domain Theory.- HOFL Denotational Semantics.- Equivalence Between HOFL Denotational and Operational Semantics.- Calculus for Communicating Systems (CCS).- Temporal Logic and mu-Calculus.- Pi-Calculus.- Measure Theory and Markov Chains.- Markov Chains with Actions and Non-determinism.- Performance Evaluation Process Algebra (PEPA).
Part I Preliminaries
1 Introduction
3(30)
1.1 Structure and Meaning
3(6)
1.1.1 Syntax, Types and Pragmatics
4(1)
1.1.2 Semantics
4(2)
1.1.3 Mathematical Models of Computation
6(3)
1.2 A Taste of Semantic Methods: Numerical Expressions
9(8)
1.3 Applications of Semantics
17(3)
1.4 Key Topics and Techniques
20(6)
1.4.1 Induction and Recursion
20(2)
1.4.2 Semantic Domains
22(2)
1.4.3 Bisimulation
24(1)
1.4.4 Temporal and Modal Logics
25(1)
1.4.5 Probabilistic Systems
25(1)
1.5
Chapter Contents and Reading Guide
26(2)
1.6 Further Reading
28(5)
References
30(3)
2 Preliminaries
33(20)
2.1 Notation
33(4)
2.1.1 Basic Notation
33(1)
2.1.2 Signatures and Terms
34(1)
2.1.3 Substitutions
35(1)
2.1.4 Unification Problem
35(2)
2.2 Inference Rules and Logical Systems
37(8)
2.3 Logic Programming
45(8)
Problems
47(6)
Part II IMP: a Simple Imperative Language
3 Operational Semantics of IMP
53(24)
3.1 Syntax of IMP
53(3)
3.1.1 Arithmetic Expressions
54(1)
3.1.2 Boolean Expressions
54(1)
3.1.3 Commands
55(1)
3.1.4 Abstract Syntax
55(1)
3.2 Operational Semantics of IMP
56(10)
3.2.1 Memory State
56(1)
3.2.2 Inference Rules
57(4)
3.2.3 Examples
61(5)
3.3 Abstract Semantics: Equivalence of Expressions and Commands
66(11)
3.3.1 Examples: Simple Equivalence Proofs
67(1)
3.3.2 Examples: Parametric Equivalence Proofs
68(2)
3.3.3 Examples: Inequality Proofs
70(2)
3.3.4 Examples: Diverging Computations
72(3)
Problems
75(2)
4 Induction and Recursion
77(26)
4.1 Noether's Principle of Well-Founded Induction
77(16)
4.1.1 Well-Founded Relations
77(6)
4.1.2 Noetherian Induction
83(1)
4.1.3 Weak Mathematical Induction
84(1)
4.1.4 Strong Mathematical Induction
85(1)
4.1.5 Structural Induction
85(3)
4.1.6 Induction on Derivations
88(1)
4.1.7 Rule Induction
89(4)
4.2 Well-Founded Recursion
93(10)
Problems
98(5)
5 Partial Orders and Fixpoints
103(24)
5.1 Orders and Continuous Functions
103(11)
5.1.1 Orders
104(2)
5.1.2 Hasse Diagrams
106(4)
5.1.3 Chains
110(1)
5.1.4 Complete Partial Orders
111(3)
5.2 Continuity and Fixpoints
114(5)
5.2.1 Monotone and Continuous Functions
114(2)
5.2.2 Fixpoints
116(3)
5.3 Immediate Consequence Operator
119(8)
5.3.1 The Operator R
120(1)
5.3.2 Fixpoint of R
121(3)
Problems
124(3)
6 Denotational Semantics of IMP
127(30)
6.1 λ-Notation
127(7)
6.1.1 λ-Notation: Main Ideas
128(3)
6.1.2 Alpha-Conversion, Beta-Rule and Capture-Avoiding Substitution
131(3)
6.2 Denotational Semantics of IMP
134(7)
6.2.1 Denotational Semantics of Arithmetic Expressions: The Function A
134(1)
6.2.2 Denotational Semantics of Boolean Expressions: The Function B
135(1)
6.2.3 Denotational Semantics of Commands: The Function C
136(5)
6.3 Equivalence Between Operational and Denotational Semantics
141(8)
6.3.1 Equivalence Proofs for Expressions
141(1)
6.3.2 Equivalence Proof for Commands
142(7)
6.4 Computational Induction
149(8)
Problems
152(5)
Part III HOFL: a Higher-Order Functional Language
7 Operational Semantics of HOFL
157(18)
7.1 Syntax of HOFL
157(7)
7.1.1 Typed Terms
158(2)
7.1.2 Typability and Typechecking
160(4)
7.2 Operational Semantics of HOFL
164(11)
Problems
171(4)
8 Domain Theory
175(16)
8.1 The Flat Domain of Integer Numbers ZT
175(1)
8.2 Cartesian Product of Two Domains
176(2)
8.3 Functional Domains
178(3)
8.4 Lifting
181(2)
8.5 Continuity Theorems
183(3)
8.6 Apply, Curry and Fix
186(5)
Problems
189(2)
9 Denotational Semantics of HOFL
191(14)
9.1 HOFL Semantic Domains
191(1)
9.2 HOFL Interpretation Function
192(6)
9.2.1 Constants
192(1)
9.2.2 Variables
193(1)
9.2.3 Arithmetic Operators
193(1)
9.2.4 Conditional
193(1)
9.2.5 Pairing
194(1)
9.2.6 Projections
194(1)
9.2.7 Lambda Abstraction
195(1)
9.2.8 Function Application
195(1)
9.2.9 Recursion
196(1)
9.2.10 Eager Semantics
196(1)
9.2.11 Examples
197(1)
9.3 Continuity of Meta-language's Functions
198(2)
9.4 Substitution Lemma and Other Properties
200(5)
Problems
201(4)
10 Equivalence Between HOFL Denotational and Operational Semantics
205(16)
10.1 HOFL: Operational Semantics vs Denotational Semantics
205(1)
10.2 Correctness
206(3)
10.3 Agreement on Convergence
209(3)
10.4 Operational and Denotational Equivalences of Terms
212(1)
10.5 A Simpler Denotational Semantics
213(8)
Problems
214(7)
Part IV Concurrent Systems
11 CCS, the Calculus of Communicating Systems
221(50)
11.1 From Sequential to Concurrent Systems
221(6)
11.2 Syntax of CCS
227(1)
11.3 Operational Semantics of CCS
228(9)
11.3.1 Inactive Process
228(1)
11.3.2 Action Prefix
228(1)
11.3.3 Restriction
229(1)
11.3.4 Relabelling
229(1)
11.3.5 Choice
229(1)
11.3.6 Parallel Composition
230(1)
11.3.7 Recursion
231(4)
11.3.8 CCS with Value Passing
235(1)
11.3.9 Recursive Declarations and the Recursion Operator
235(2)
11.4 Abstract Semantics of CCS
237(15)
11.4.1 Graph Isomorphism
237(2)
11.4.2 Trace Equivalence
239(2)
11.4.3 Strong Bisimilarity
241(11)
11.5 Compositionality
252(3)
11.5.1 Strong Bisimilarity Is a Congruence
253(2)
11.6 A Logical View of Bisimilarity: Hennessy-Milner Logic
255(4)
11.7 Axioms for Strong Bisimilarity
259(2)
11.8 Weak Semantics of CCS
261(10)
11.8.1 Weak Bisimilarity
262(2)
11.8.2 Weak Observational Congruence
264(1)
11.8.3 Dynamic Bisimilarity
265(2)
Problems
267(4)
12 Temporal Logic and the jti-Calculus
271(16)
12.1 Specification and Verification
271(1)
12.2 Temporal Logic
272(6)
12.2.1 Linear Temporal Logic
273(2)
12.2.2 Computation Tree Logic
275(3)
12.3 μ-Calculus
278(4)
12.4 Model Checking
282(5)
Problems
284(3)
13 π-Calculus
287(22)
13.1 Name Mobility
287(4)
13.2 Syntax of the π-Calculus
291(1)
13.3 Operational Semantics of the π-Calculus
292(5)
13.3.1 Inactive Process
293(1)
13.3.2 Action Prefix
293(1)
13.3.3 Name Matching
294(1)
13.3.4 Choice
294(1)
13.3.5 Parallel Composition
295(1)
13.3.6 Restriction
295(1)
13.3.7 Scope Extrusion
296(1)
13.3.8 Replication
296(1)
13.3.9 A Sample Derivation
297(1)
13.4 Structural Equivalence in the π-Calculus
297(2)
13.4.1 Reduction Semantics
298(1)
13.5 Abstract Semantics of the π-Calculus
299(10)
13.5.1 Strong Early Ground Bisimulations
300(1)
13.5.2 Strong Late Ground Bisimulations
301(1)
13.5.3 Compositionality and Strong Full Bisimilarities
302(1)
13.5.4 Weak Early and Late Ground Bisimulations
303(1)
Problems
304(5)
Part V Probabilistic Systems
14 Measure Theory and Markov Chains
309(24)
14.1 Probabilistic and Stochastic Systems
309(1)
14.2 Probability Space
310(3)
14.2.1 Constructing a CT-Field
311(2)
14.3 Continuous Random Variables
313(6)
14.3.1 Stochastic Processes
318(1)
14.4 Markov Chains
319(14)
14.4.1 Discrete and Continuous Time Markov Chains
320(1)
14.4.2 DTMCs as LTSs
320(3)
14.4.3 DTMC Steady State Distribution
323(1)
14.4.4 CTMCs as LTSs
324(1)
14.4.5 Embedded DTMC of a CTMC
325(1)
14.4.6 CTMC Bisimilarity
326(2)
14.4.7 DTMC Bisimilarity
328(1)
Problems
329(4)
15 Discrete Time Markov Chains with Actions and Nondeterminism
333(10)
15.1 Reactive and Generative Models
333(1)
15.2 Reactive DTMC
334(3)
15.2.1 Larsen-Skou Logic
336(1)
15.3 DTMC with Nondeterminism
337(6)
15.3.1 Segala Automata
337(1)
15.3.2 Simple Segala Automata
338(1)
15.3.3 Nondeterminism, Probability and Actions
339(1)
Problems
340(3)
16 PEPA - Performance Evaluation Process Algebra
343(14)
16.1 From Qualitative to Quantitative Analysis
343(1)
16.2 CSP
344(3)
16.2.1 Syntax of CSP
344(1)
16.2.2 Operational Semantics of CSP
345(2)
16.3 PEPA
347(10)
16.3.1 Syntax of PEPA
347(2)
16.3.2 Operational Semantics of PEPA
349(5)
Problems
354(3)
Solutions 357
Roberto Bruni is an associate professor in the Dept. of Computer Science of the University of Pisa. His research interests include concurrency, operational semantics, Petri nets, Java programming, business process modelling, software composition, and fog computing, and he teaches related courses to computer science and business informatics graduate and undergraduate students. He has served the community with committee membership of conferences such as FACS, Coordination, CONCUR and WRLA. He was previously an international fellow of the SRI International Computer Science Laboratory, and a visiting scholar of the University of Illinois at Urbana-Champaign.

Ugo Montanari is an emeritus professor in the Dept. of Computer Science of the University of Pisa. He has published over 400 refereed articles or papers in theoretical computer science and artificial intelligence. His current research interests are the semantics of concurrency, process description languages, constraint programming, graph transformation systems, coordination models, algebraic and categorical models of concurrency, models and languages for open distributed systems, network-aware programming, service-oriented computing, and collective autonomic systems. He has served as a board member for key international scientific journals such as Fundamenta Informaticae, Theoretical Computer Science, Computer Science Review, Artificial Intelligence, the IEEE Transactions on Software Engineering, Logic Programming, Science of Computer Programming, Theory and Practice of Logic Programming, and New Generation Computing, and he has served the community as a chair or committee member, PC or steering, of major related conferences such as CONCUR, WRLA, CP, CALCO, CMCS, ICGT, and TGC. He was Vice-Director of the IMT School for Advanced Studies, Lucca. He is member of the Academia Europaea.