Algebra and Coalgebra in Computer Science: Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009, Proceedings

3642037402......Page 1
Lecture Notes in Computer Science 5728......Page 2
Algebra and Coalgebrain Computer Science......Page 4
Preface......Page 5
Organization......Page 6
Table of Contents......Page 8
Adequacy for Infinitary Algebraic Effects (Abstract)......Page 11
Introduction......Page 13
Parameterised Monads......Page 14
Algebraic Theories with Parameters......Page 17
Beck's Theorem......Page 19
Structured Parameterisation......Page 22
Semantics for Type and Effect Systems......Page 23
Conclusions......Page 27
Introduction......Page 28
Preliminaries: Monads and Generic Imperative Programs......Page 31
Kleene Monads......Page 33
Continuity......Page 38
Worked Example: Stack Reverse in the MCE......Page 41
References......Page 42
Introduction......Page 44
Background—Distributive Laws for Set-Functors......Page 45
Iterative Algebras with Effects......Page 48
Free $\lambda$-cias......Page 54
Characterisation of $\lambda$-cias......Page 56
Conclusions......Page 57
Introduction......Page 59
Presheaves as Algebras......Page 61
Presheaves as Monoids......Page 65
Higher-Order Recursion Schemes......Page 68
Interpreted Solutions......Page 70
Conclusions......Page 72
References......Page 73
Introduction......Page 74
Leading Example: Sequential Composition......Page 75
Presenting Algebraic Structure as a Category......Page 77
The FP-Theory PLTh......Page 78
Outer Model: L-Category......Page 80
Categorical Compositionality......Page 82
Taxonomy of FP-Theories for Component Calculi......Page 83
The FP-Theories ArrTh, MArrTh......Page 84
Set-Theoretic Models: Arrows, Freyd Categories......Page 85
PLTh, ArrTh and MArrTh as Component Calculi......Page 86
Conclusions and Future Work......Page 89
Introduction......Page 91
Preliminaries......Page 94
One-Step Complementation......Page 95
Game Bisimulations......Page 97
Complementation of Alternating Coalgebra Automata......Page 101
Transalternating Automata......Page 102
Complementation of Transalternating Automata......Page 103
Transalternating and Alternating Automata......Page 104
Size Matters......Page 105
Introduction......Page 107
Behaviour and Final Coalgebras (Preliminaries)......Page 108
Abstract Coalgebraic Languages......Page 109
An Elementary Construction of Final Coalgebras......Page 111
Simple Coalgebras......Page 115
Logical Congruences......Page 116
Different Faces of the Hennessy-Milner Property......Page 118
Generalization to Other Categories......Page 119
Conclusions......Page 121
Introduction......Page 123
The Problem......Page 124
Type Equality versus Reduction......Page 127
Weakly Final Coalgebras: A Principled Retreat......Page 128
O for an Observational Propositional Equality!......Page 129
Observational Equality......Page 130
Interaction Structures Closed under Bisimulation......Page 132
Epilogue......Page 134
Introduction......Page 137
Preliminaries......Page 142
Behavioral Specification and Satisfaction......Page 143
Behavioral Equivalence and Coinduction......Page 145
Circular Coinduction......Page 148
Conclusion......Page 153
Introduction......Page 155
Labelled Markov Processes......Page 158
Bisimulation and Logic......Page 159
Approximation by Unfolding......Page 160
Bisimulation......Page 162
Approximation Revisited......Page 164
Conclusions......Page 165
Introduction......Page 167
Semantic Domain for Weak Bisimilarity......Page 169
Denotational Semantics for CCS......Page 173
Conclusions and Related Work......Page 181
Introduction......Page 183
Saturated Semantics......Page 185
Running Example: Open Petri Nets......Page 187
Symbolic Semantics......Page 188
(Structured) Coalgebras......Page 191
Coalgebraic Saturated Semantics......Page 192
Saturated Coalgebras......Page 193
Normalized Coalgebras......Page 194
Isomorphism Theorem......Page 196
From Normalized Coalgebras to Symbolic Minimization......Page 197
Conclusions and Related Works......Page 198
Introduction......Page 201
Coalgebras: Definition and Examples......Page 203
Four Definitions of Bisimulation......Page 204
The Congruences of Aczel and Mendler......Page 205
Conditions on Endofunctors......Page 206
Relating Notions of Bisimulation......Page 207
Bisimilarity through Transfinite Constructions......Page 208
Models of Name-Passing Process Calculi......Page 209
Coalgebras and Notions of Non-determinism......Page 210
Bisimulation for Name-Passing Calculi......Page 212
Remarks on Functor Categories and Other Models of Name-Passing......Page 213
Introduction......Page 216
A Motivating Example: Binary Trees with Output......Page 217
Final Coalgebras in Kleisli Categories......Page 220
Fat Traces and Executions......Page 221
Splitting Up Functors......Page 222
Thin Traces and Executions for Non-determinism......Page 224
Scheduling......Page 226
Conclusions and Future Work......Page 230
Introduction......Page 231
Preliminaries on Duality......Page 232
Algebras as Relational Frames......Page 235
The Algebra of Recognisable Subsets of an Algebra......Page 236
Profinite Completions as Dual Spaces......Page 237
Syntactic Monoids and Profinite Terms......Page 241
Duality for Subalgebras and Eilenberg-Reiterman Theorems......Page 242
Introduction......Page 246
Discrete Duality for Distributive Lattices......Page 247
Freely Adding Weak Implications......Page 249
Free Weak Heyting Algebras......Page 253
Freely Adding Heyting Implications......Page 255
Free Heyting Algebras......Page 256
Conclusions and Future Work......Page 259
Introduction......Page 262
Ontological Frameworks and Knowledge Bases......Page 264
Duality for Distributive Lattices......Page 268
The Terminal Solution of a Knowledge Base......Page 269
Description of $F_{DLA}(C)$ and Its Dual Frame......Page 270
The Attribute-Free Case......Page 272
The General Case......Page 274
Related and Future Work......Page 277
Introduction......Page 279
Commutative Real $C*$ Algebras......Page 280
Proximity Lattices and Skew Frames with Negation......Page 281
From $C*$ Algebras to Skew Frames with Negation......Page 284
From Skew Frames with Negation to $C*$ Algebras......Page 287
The Equivalence Theorem......Page 292
Conclusions and Further Work......Page 293
Introduction......Page 295
The Theory of Conway Games......Page 297
The Theory of Hypergames......Page 299
Characterization Theorem for Non-losing Strategies......Page 302
Sum and Negation of Hypergames......Page 304
The Theory of Impartial Hypergames......Page 305
The Grundy-Sprague Theory......Page 306
The Smith Theory in the Hypergame Setting......Page 307
Comparison with Related Work and Directions for Future Work......Page 310
Introduction......Page 312
Program Semantics......Page 314
Processes and Controls......Page 315
Games as Processes......Page 316
Designing and Refining Relational Strategies......Page 317
Playing Out the Strategies: Computing the Equilibria......Page 319
Strategies as Randomized Programs......Page 321
Position and Memory......Page 324
Conclusions and Future Work......Page 326
Appendix: Fixed Points in { f FRel}......Page 328
Appendix: Fixed Points in { f SRel}......Page 329
Van Kampen Colimits as Bicolimits in Span......Page 330
Preliminaries......Page 331
Van Kampen Cocones......Page 334
Van Kampen Cocones in a Span Bicategory......Page 335
Span Bicolimits......Page 336
Van Kampen Cocones as Span Bicolimits......Page 341
Conclusion, Related Work and Future Work......Page 342
Introduction......Page 345
Adhesive Categories for SPO Rewriting......Page 348
Grammars and Grammar Morphisms as Simulations......Page 350
Unfolding Grammars into Occurrence Grammars......Page 353
Occurrence Grammars......Page 354
The Unfolding Construction......Page 355
$\omega$-Adhesive Categories and the Coreflection Result......Page 357
Related Work and Conclusion......Page 359
Introduction......Page 362
Behaviour Protocols......Page 364
Implementation Semantics of Protocols......Page 367
User Semantics of Protocols......Page 369
Interaction Semantics of Protocols and Compositionality......Page 371
Protocol Refinement......Page 374
Conclusions......Page 376
Introduction......Page 378
Preliminaries......Page 379
Pattern-Based Model-to-Model Transformation......Page 381
Correctness, Completeness, and Termination of Transformations......Page 383
Related Work......Page 390
Conclusions and Future Work......Page 391
Introduction......Page 393
Institutions......Page 394
Universal Institutions......Page 400
Borrowing Completeness......Page 403
Conclusions and Future Work......Page 406
Introduction......Page 408
DBL, the Directed Bigraphical Language......Page 409
Graphical Visualization......Page 410
Matching......Page 411
RPO and IPO......Page 413
Related and Future Work......Page 417
Introduction......Page 418
Music Therapy for Autistic Children......Page 419
Monoidal Soft Constraints......Page 420
Constraint-Based Music Creation......Page 421
User Interaction......Page 422
Conclusions and Further Work......Page 425
Introduction......Page 428
Behavioral Specifications and CIRC......Page 429
CIRC at Work......Page 431
Conclusions......Page 437
Introduction......Page 438
Specification and Analysis in Priced-Timed Maude......Page 439
Example: A Multiset of Simple Thermostats......Page 440
Comparison with { c Uppaal Cora}......Page 441
Future Work......Page 442
Introduction......Page 444
Definitions and Theory......Page 445
The Tool......Page 447
Examples......Page 448
Conclusions, Related Work......Page 450
Author Index......Page 452