Modelling Visualisation Using Formal Algebra

Matthew Alexander Hutchins

A thesis submitted for the degree of Doctor of Philosophy of The Australian National University.

March 1999

• Download my thesis as a PDF (4,190 KB): Thesis.pdf

Abstract

This thesis is an investigation into the development of a formal model of visualisation. It combines traditional visualisation modelling approaches with algebraic specification techniques from formal software engineering.

A visualisation presents a data set as a perceptual scene that can be interpreted by a human observer to perform some task. There are several different kinds of visualisation, including statistical and mathematical graphics, cartography, software diagrams, scientific visualisation, information visualisation and some human-computer interfaces. In the more mature areas, best-practice approaches to designing displays have been recognised, but there is good reason to explore the field more systematically. In particular, increasing complexity of data sets, advances in display technology, and the diversity of display problems indicate a need for a more generic, theoretical, extensible approach to understanding visualisation.

This thesis presents a framework for modelling visualisation as a series of mappings between mathematically structured spaces. The key contributions of the framework are: modelling at a conceptual rather than a computational level; modelling visualisation spaces as algebras and mappings as morphisms; an indirect display model that includes an explicit task space, and focuses on the essential structure of spaces; and two high-level context models and a design process model. The modelling framework is supported by “Axiomaniac” — a computer-readable algebraic language for describing structured spaces and mappings.

Elements of the modelling framework and the use of the Axiomaniac language are illustrated by a survey and discussion of commonly used perceptual and data structures, a catalogue of mathematical theories expressed in Axiomaniac, and three visualisation design case studies in the fields of software maintenance, rule induction for data mining and airspace conflict modelling. The thesis demonstrates that a formal and systematic approach to modelling visualisation is both practical and beneficial.

Table of Contents

Declaration

Abstract

Acknowledgements

Table of Contents

Colour Pages

Chapter 1: Introduction

This chapter introduces visualisation through definitions and examples, states the aims, contributions and structure of the thesis, and provides the motivation for modelling visualisation using formal algebra.
1 Visualisation 55
2 The Gamut 57
3 Modelling Visualisation Using Formal Algebra 64
3.1 Thesis 64
3.2 Contributions 65
3.3 Context 66
3.4 Thesis Outline 66
4 Terminology 68
5 Why Make Models? 71
5.1 Bedtime Story 71
5.2 Motivators 71
5.3 Potential Benefits 73
6 Summary 76

Chapter 2: Inspiration

This chapter reviews the literature relating to models of visualisation, looking for inspiration in the form of ideas about data, ideas about scenes, ideas about tasks and ideas about the visualisation design process. It concludes with an analysis of the strengths and weaknesses of existing approaches.
1 Introduction 77
2 Foundations of Quantitative Graphics 79
2.1 Collections of Graphical Techniques 79
2.2 Experimental Classification of Images 80
2.3 Semiology of Graphics 80
2.4 Theory of Graphical Perception 84
3 Automated Design of Graphics 86
3.1 Automated Design of Presentations (APT) 86
3.2 Task Analytic Approach (BOZ) 89
3.3 Extended Data Characterisation (SAGE) 90
4 Scientific Visualisation Concepts 91
4.1 Visualisation Idioms 91
4.2 Problem-oriented Matrix of Techniques 93
4.3 Fibre Bundle Data Model 94
5 Assisted Visualisation Design Systems 97
5.1 Compositional Synthesis (VISTA) 98
5.2 Natural Scene Paradigm 99
5.3 Cooperative Computer Aided Design 100
5.4 Rule-based, Multivariate Design (AutoVisual) 102
5.5 Cooperative Rule-based Visualisation 103
5.6 Intelligent Visualisation Planner 104
5.7 Task-specific Visualisation Assistant 104
6 More Graphics and UI Design 106
6.1 Model-based Design of Interfaces and Dialogues 106
6.2 Visual Metaphors for Schema Display 107
6.3 Generative Theory of Diagram Design 109
7 More Visualisation Design 112
7.1 Scalar Mapping and Lattice Model 112
7.2 Interacting With Colour Gamuts 115
7.3 Auditory Information Design 116
7.4 Category Theoretic Model 120
8 Discussion 121
9 Summary 125

Chapter 3: A Framework for Modelling Visualisation

This chapter introduces a framework for modelling visualisation at a conceptual rather than a computational level. The central proposal of the chapter is that visualisation spaces are algebras, and the mappings between them are morphisms. Several models and a general design process are proposed based on the algebraic concept. Key contributions are the introduction of an explicit change of space in an indirect display model, and the use of algebras to model metaspaces.
1 Introduction 127
2 Conceptual Model 129
2.1 A Computational Visualisation Model 129
2.2 A Conceptual Visualisation Model 131
3 Spaces and Algebras 134
3.1 Motivating Examples 134
3.2 The Space of Spaces 135
3.3 Visualisation Spaces Are Algebras 136
3.4 Mappings Are Morphisms 138
4 Direct Display Model 139
4.1 The Model 139
4.2 Example: Values and Widgets 140
4.3 Example: Tuples and Marks 143
5 Indirect Display Model 147
5.1 Limitations of the Direct Model 147
5.2 Indirect Display Model 148
5.3 Example: Box Plots 152
5.4 Example: ThemeScapes 154
6 Visualisation Supermodel 157
6.1 The Model 157
6.2 General Questions 158
7 Visualisation Paradigm Model 159
7.1 Issues 159
7.2 The Paradigm Model 159
7.3 The Paradigm Context Model 161
7.4 Example: APT 162
7.5 Example: VIS-AD 164
7.6 Example: NSP 165
7.7 Discussion 166
8 Design Process Model 168
8.1 A Process Model 168
8.2 Phases of the Process 169
8.3 Examples 173
9 Summary 174

Chapter 4: “Axiomaniac”: A Formal Theory Language

This chapter introduces “Axiomaniac”, a formal algebraic theory language for describing spaces and mappings.
1 Introduction 175
2 A Theory Language 177
3 Exploring Languages 179
3.1 Language Possibilities 179
3.2 Algebraic Specification Languages 180
4 The Development of Axiomaniac 182
4.1 Syntactic Changes from LSL 182
4.2 Semantic Changes from LSL 183
4.3 Theory Mapping and Satisfaction 184
4.4 Relations and General First Order Logic 186
4.5 Meta-Algebraic Extensions 186
5 Axiomaniac Theory Language 188
5.1 Signatures 188
5.2 Assertions 189
5.3 Imports, Satisfaction, and Mapping 191
5.4 Morphism Theories 195
5.5 Generated By and Partitioned By 195
5.6 Implications and Conversions 197
5.7 Classes 199
6 Axiomaniac Logic 204
6.1 About Logic 204
6.2 Axiomaniac Sentences 204
6.3 Rules of Inference 205
7 Software Support 206
8 Summary 208

Chapter 5: Theoretical and Perceptual Foundations

This chapter illustrates and formalises an assortment of commonly encountered data, task and scene structures.
1 Introduction 209
2 Measurement Spaces 211
2.1 Data and Measurement 211
2.2 A Family of Measurement Spaces 211
2.3 The Basics 212
2.4 Orders 212
2.5 Addition and Norms 214
2.6 Measurement Morphisms 216
3 Graphical Spaces 217
3.1 Graphical Spaces and Measurement 217
3.2 Object Spaces 217
3.3 Positional Spaces 218
3.4 Size Spaces 223
3.5 Shape Spaces 225
3.6 Pattern and Shading Spaces 226
3.7 Colour Spaces 230
3.8 Direction and Angular Spaces 231
4 Topological Spaces 234
4.1 Topology, Shape and Dimension 234
4.2 Zero Dimensional Spaces 235
4.3 One Dimensional Spaces 236
4.4 Higher Dimensional Spaces 237
4.5 Continuous Morphisms 238
5 Projected Spaces 239
5.1 Objects and Attributes 239
5.2 Marks and Attributes 239
6 Spaces With Edges 241
6.1 Graphs and Binary Relations 241
6.2 Perceptual Relations 241
7 Some Special Cases 243
7.1 Cyclic Spaces 243
7.2 Proportions and Part/Wholes 243
7.3 Class and Magnitude 244
7.4 Comment 246
8 Sets, Relations and Functions 247
8.1 Set Spaces 247
8.2 Relations 248
8.3 Functions 249
9 Multivariate Relation Spaces 250
10 Summary 253

Chapter 6: Case Studies

This chapter illustrates the use of the modelling framework, the design process, and the Axiomaniac theory language through three visualisation case studies.
1 Introduction 255
2 About the Case Studies 256
2.1 The Role of Domain and Visualisation Experts 256
2.2 Visualisation Technology 257
2.3 Implementation Languages 257
3 Visualising Program Slices 258
3.1 Background 258
3.2 The Display Problem 259
3.3 Initial Data Analysis 261
3.4 Initial Task Analysis 263
3.5 Initial Scene Analysis 264
3.6 More Task Analysis 265
3.7 Scene Synthesis 268
3.8 Task Analysis Again 273
3.9 Scene Synthesis Again 278
3.10 Comment 285
4 Visualising Rules 287
4.1 Background 287
4.2 The Display Problem 287
4.3 Initial Data Analysis 289
4.4 Initial Task Analysis 290
4.5 Scene Synthesis 294
4.6 The Second Pass 300
4.7 Comment 304
5 Visualising Airspace Conflict 305
5.1 Background 305
5.2 The Display Problem 307
5.3 Data Analysis 309
5.4 Task Analysis 313
5.5 Scene Synthesis 317
5.6 Comment 324
6 Summary 325

Chapter 7: Coda

This chapter concludes the thesis, and looks at unsolved issues and directions for future work.
1 Thesis Summary 327
1.1 Motivation 327
1.2 Inspiration 328
1.3 Approach 329
1.4 Axiomaniac 331
1.5 Foundations 332
1.6 Case Studies 332
2 Directions for Future Work 335
2.1 Putting the Theory to Work 335
2.2 Modelling Scenes 336
2.3 Interaction 337
2.4 Algebra for Everyone 337
3 Conclusion 338

References

Appendix A: Definition of Axiomaniac

This appendix provides some technical details about the Axiomaniac theory language.
1 Concrete Syntax 351
1.1 Notation 351
1.2 Lexical Details 351
1.3 Names 353
1.4 Signatures 354
1.5 Expressions, Terms and Propositions 355
1.6 Signature Maps 357
1.7 Statements and Conversions 357
1.8 Theories 358
1.9 Sentences and Theorems 359
2 Abstract Syntax 360
2.1 Notation 360
2.2 Names 361
2.3 Signatures 361
2.4 Expressions, Terms and Propositions 364
2.5 Signature Maps 367
2.6 Statements and Conversions 371
2.7 Theories 377
2.8 Sentences and Theorems 377
3 Further Details 379
3.1 Parsing 379
3.2 Rules of Inference 380
3.3 Semantics 385

Appendix B: Background Theories

This appendix is a collection of mathematical theories expressed in the Axiomaniac language.
1 Introduction 389
2 Morphisms 390
2.1 Signature 390
2.2 Properties 390
2.3 Inverse, Identity and Composite 391
2.4 Two-Sorted Morphisms 392
2.5 Morphism Spaces 392
3 Orders 393
3.1 Signatures 393
3.2 Properties 394
3.3 Spaces 396
3.4 Homomorphisms 398
4 Groupoids 400
4.1 Signatures 400
4.2 Properties 400
4.3 Spaces 403
4.4 Abelian Spaces 405
4.5 Homomorphisms 405
5 Double Groupoids 406
5.1 Signatures 406
5.2 Properties 407
5.3 Spaces 408
5.4 Homomorphisms 409
6 Lattices 410
6.1 Semilattices and Lattices 410
6.2 Special Lattices 411
6.3 Homomorphisms 412
7 Set Spaces 413
7.1 Signature 413
7.2 Partial Order 413
7.3 Meet and Join 414
7.4 Boolean Operations 414
7.5 Complete Set Spaces 415
7.6 Finite Sets 415
7.7 Lists 417
7.8 Predicate Spaces 418
7.9 Injected Set Spaces 418
7.10 Homomorphisms 419
8 Posets 420
8.1 Posets and Chains 420
8.2 Lattices and Posets 423
9 Number Theories 425
9.1 Natural Numbers 425
9.2 Natural Exponentiation 427
9.3 Cardinality of Sets 427
9.4 Integers 428
9.5 Integer Exponentiation 429
9.6 Rational Numbers 430
9.7 Real Numbers 432
9.8 Complex Numbers 434
10 Modules and Vector Spaces 436
10.1 Spaces 436
10.2 Homomorphisms 437
11 Sequences and Enumerations 438
11.1 Sequences 438
11.2 Homomorphisms 438
11.3 Sequence Spaces 439
11.4 Field and Vector Space of Sequences 439
11.5 Homomorphisms 440
11.6 Enumerations 441
11.7 Homomorphisms 442
11.8 Enumeration Spaces 443
11.9 Homomorphisms 443
12 Arrays and Matrices 444
12.1 Arrays 444
12.2 Array Spaces 445
12.3 Fixed Array Vector Spaces 446
12.4 Matrices 447
12.5 Matrix Spaces 447
12.6 Fixed Matrix Vector Spaces 449
13 Topological Spaces and Continuity 450
13.1 Topological Spaces 450
13.2 Morphisms 452
13.3 Separation Axioms 454
13.4 Convergent Sequence Spaces 457
14 Metric Spaces 458
14.1 Metric Spaces 458
14.2 Examples 459
14.3 Morphisms 460
14.4 Cauchy Sequence Spaces 461
15 Graphs 462
15.1 Hypergraphs 462
15.2 Graphs 464
15.3 Homomorphisms 466
15.4 Directed and Labelled Graphs 466
16 Products, Unions and Tuples 469
16.1 Pointed, Projected and Injected Sets 469
16.2 Simple Products 469
16.3 Simple Unions 470
16.4 Union Spaces 471
16.5 Tuple Spaces 472
17 Relation and Function Spaces 473
17.1 Binary Relation Spaces 473
17.2 Constrained Binary Relation Spaces 474
17.3 Function Spaces 475
17.4 Set-Of-Product Relation Spaces 475
17.5 Fixed Tuple Relation Spaces 476
17.6 Free Tuple Relation Spaces 477
18 Vector Bundles 478
18.1 Coordinate Spaces 478
18.2 Manifolds 478
18.3 Bundles 479
18.4 Sections 480
19 Categories 481
19.1 Abstract Categories 481
19.2 Concrete Categories 482
19.3 Examples of Concrete Categories 484