+612 9045 4394
 
CHECKOUT
Call-By-Push-Value : A Functional/Imperative Synthesis - Paul Blain Levy

Call-By-Push-Value

A Functional/Imperative Synthesis

Hardcover

Published: 30th November 2003
Ships: 7 to 10 business days
7 to 10 business days
RRP $574.99
$397.75
31%
OFF
or 4 easy payments of $99.44 with Learn more

Other Available Formats (Hide)

  • Paperback View Product Published: 27th September 2012
    $317.00

This monograph, written for graduate students and researchers, exposes the call-by-push-value structure underlying a remarkable range of semantics, including operational semantics, domains, possible worlds, continuations and games. Incorporating recent simplifications, this is a key text for anyone interested in Ylambda"-calculus, programming language foundations or applications of category theory.

List of Figuresp. xvii
Prefacep. xxi
Acknowledgmentsp. xxv
Introductionp. xxvii
Computational Effectsp. xxviii
Reconciling CBN and CBVp. xxix
The Problem Of Two Paradigmsp. xxix
A Single Languagep. xxix
"Hasn't This Been Done By ...?"p. xxxi
The Case For Call-By-Push-Valuep. xxxii
Conventionsp. xxxii
Notation and Terminologyp. xxxii
Weakeningp. xxxiii
A CBPV Primerp. xxxiii
Basic Featuresp. xxxiii
Example Programp. xxxiv
CBPV Makes Control Flow Explicitp. xxxvi
Value Types and Computation Typesp. xxxvi
Structure of Thesisp. xxxvii
Goalsp. xxxvii
Chapter Outlinep. xxxviii
Chapter Dependencep. xl
Proofsp. xl
Language
Call-By-Value and Call-By-Namep. 3
Introductionp. 3
The Main Point Of The Chapterp. 3
A Simply Typed [lambda]-Calculusp. 4
The Languagep. 4
Product Typesp. 4
Equationsp. 6
Reversible Derivationsp. 7
Adding Effectsp. 8
The Principles Of Call-By-Value and Call-By-Namep. 8
Call-By-Valuep. 10
Operational Semanticsp. 10
Denotational Semantics for printp. 11
Scott Semanticsp. 13
The Monad Approachp. 14
Observational Equivalencep. 17
Coarse-Grain CBV vs. Fine-Grain CBVp. 17
Call-By-Namep. 18
Operational Semanticsp. 18
Observational Equivalencep. 18
CBN vs. Lazyp. 20
Denotational Semantics for printp. 21
Scott Semanticsp. 22
Algebras and Plain Mapsp. 23
Comparing CBV and CBNp. 25
Call-By-Push-Value: a Subsuming Paradigmp. 27
Introductionp. 27
Aims Of Chapterp. 27
CBV And CBN Lead To CBPVp. 28
Syntaxp. 28
Operational Semantics Without Effectsp. 30
Big-Step Semanticsp. 30
CK-Machinep. 32
CK-Machine For Non-Closed Computationsp. 33
Typing the CK-Machinep. 33
Operations On Stacksp. 36
Agreement Of Big-Step and CK-Machine Semanticsp. 37
Operational Semantics for printp. 37
Big-Step Semantics for printp. 37
CK-Machine For printp. 38
Observational Equivalencep. 39
Denotational Semanticsp. 39
Values and Computationsp. 39
Denotational Semantics Of Stacksp. 41
Monads and Algebrasp. 41
Subsuming CBV and CBNp. 42
From CBV to CBPVp. 42
From CBN to CBPVp. 43
CBPV As A Metalanguagep. 45
Useful Syntactic Sugarp. 45
Pattern-Matchingp. 45
Commandsp. 46
Computations Matter Mostp. 47
Complex Values and Equational Theoryp. 49
Introductionp. 49
Complex Valuesp. 50
Equationsp. 51
CK-Machine Illuminates to Equationsp. 52
Adding Complex Values is Computation-Unaffectingp. 54
The Problem With the CBPV Equational Theoryp. 56
Complex Stacksp. 57
Equational Theory For CBPV With Stacksp. 58
Reversible Derivationsp. 60
Example Isomorphisms Of Typesp. 61
Trivializationp. 61
Recursion and Infinitely Deep CBPVp. 65
Introductionp. 65
Divergence and Recursionp. 66
Divergent and Recursive Termsp. 66
Type Recursionp. 68
Denotational Semantics Of Type Recursionp. 69
Bilimit-Compact Categoriesp. 69
Sub-Bilimit-Compact Categoriesp. 72
Minimal Invariantsp. 73
Interpreting Recursive Typesp. 75
Infinitely Deep Termsp. 77
Syntaxp. 77
Partial Terms and Scott Semanticsp. 78
Infinitely Deep Typesp. 79
Syntaxp. 79
Partial Types and Scott Semanticsp. 79
The Inductive/Coinductive Formulation of Infinitely Deep Syntaxp. 80
Relationship Between Recursion and Infinitely Deep Syntaxp. 82
Predomain Semantics For CBPVp. 83
Domains and Predomainsp. 83
Interpreting Type Recursion In Predomains and Domainsp. 84
Concrete Semantics
Simple Models of CBPVp. 89
Introductionp. 89
Semantics of Valuesp. 90
Global Storep. 91
The Languagep. 91
Denotational Semanticsp. 92
Combining Global Store With Other Effectsp. 94
Control Effectsp. 95
letstk and changestkp. 95
Typing Control Effectsp. 96
Regarding nil As A Free Identifierp. 98
Observational Equivalencep. 100
Denotational Semanticsp. 101
Combining Control Effects With Other Effectsp. 105
Erratic Choicep. 107
The Languagep. 107
Denotational Semanticsp. 107
Finite Choicep. 109
New Model For May Testingp. 109
Errorsp. 111
The Languagep. 111
Denotational Semanticsp. 113
Summaryp. 114
Possible World Model for Cell Generationp. 117
Cell Generationp. 117
The Languagep. 118
Operational Semanticsp. 119
Worldsp. 119
Storesp. 120
Operational Rulesp. 121
Observational Equivalencep. 122
Cell Types As Atomic Typesp. 122
Excluding Thunk Storagep. 123
Introductionp. 124
What Is A Possible World Semantics?p. 124
Contribution Of Chapterp. 125
Storesp. 125
Possible Worlds Via CBPV Decompositionp. 126
Denotational Semanticsp. 127
Semantics of Valuesp. 127
Semantics of Computationsp. 128
A Computation Type Denotes A Contravariant Functorp. 128
Semantics of Stacksp. 129
Summaryp. 130
Combining Cell Generation With Other Effectsp. 131
Introductionp. 131
Cell Generation + Printingp. 132
Cell Generation + Divergencep. 133
Related Models and Parametricityp. 135
Modelling Thunk Storage And Infinitely Deep Typesp. 137
Jump-With-Argumentp. 141
Introductionp. 141
The Languagep. 142
Jumpingp. 143
Intuitive Reading of Jump-With-Argumentp. 143
Graphical Syntax For JWAp. 144
Executionp. 145
The StkPS Transformp. 148
StkPS Transform As Jumping Implementationp. 148
Related Transformsp. 149
C-Machinep. 151
C-Machine for Effect-Free JWAp. 151
Adapting the C-Machine for printp. 153
Relating Operational Semanticsp. 154
Observational Equivalencep. 155
Equationsp. 155
Equational Theoryp. 155
Example Isomorphismsp. 156
JWA As A Type Theory For Classical Logicp. 157
The StkPS Transform Is An Equivalencep. 160
The Main Resultp. 160
Complex Valuesp. 161
Equational Theory For CBPV+Controlp. 162
Representing CBPV+Stacks In CBPV+Controlp. 163
Stacks and Complex Values Are Computation-Unaffectingp. 164
The StkPS Transform Between Equational Theoriesp. 166
Pointer Gamesp. 169
Introductionp. 169
Pointer Games And Their Problemsp. 169
Contribution Of This Chapterp. 170
More Is Simplerp. 171
Cells As Objectsp. 171
Related Work On Abstract Machinesp. 173
Structure Of Chapterp. 174
Arenas In The Literaturep. 174
Player/Opponent Labellingp. 174
Tokens Of An Arenap. 174
Arenas Versus Arena Familiesp. 175
Forests Versus Graphsp. 176
Pointer Game Semantics For Infinitary JWA + Storagep. 176
Typesp. 176
Termsp. 180
[eta]-Expansion And Copycat Behaviourp. 188
Semantics Of Termsp. 189
Categorical Structurep. 190
Cell Generationp. 192
Claimsp. 193
Pointer Game For Infinitary CBPV + Control + Storagep. 194
Pointer Game Via StkPSp. 194
Introducing Questions and Answersp. 195
Answer-Move Pointing To Answer-Movep. 197
Removing Controlp. 198
Categorical Semantics
Semantics in Element Stylep. 207
Countable vs. Finitep. 207
Introductionp. 207
Categorical Preliminariesp. 208
Modulesp. 208
Homset Functorsp. 209
Some Notationp. 210
Locally Indexed Categoriesp. 210
OpGrothendieck Construction And Homset Functorsp. 213
Locally Indexed Modulesp. 215
Locally Indexed Natural Transformationsp. 216
Modelling Effect-Free Languagesp. 216
Cartesian Categories and Substitution Lemmap. 216
Products, Exponentials and Distributive Coproductsp. 217
Categorical Structures For Judgements Of JWA And CBPVp. 220
Introductionp. 220
Judgement Model of JWAp. 220
Stacks In CBPVp. 221
Computations In CBPVp. 222
Enrichmentp. 223
Connectivesp. 225
Right Adjunctives--Interpreting Up. 225
Jumpwiths--Interpreting [not sign]p. 226
Left Adjunctives--Interpreting Fp. 226
Products--Interpreting [Pi]p. 227
Exponentials--Interpreting top. 229
Distributive Coproducts--Interpreting [Sigma]p. 231
Tying It All Togetherp. 234
Adjunctionsp. 235
Examplesp. 236
Trivial Models Of CBPVp. 236
Eilenberg-Moore Models Of CBPVp. 236
Between JWA and CBPVp. 237
Erratic Choicep. 239
Global Storep. 240
Possible Worlds: Part 1p. 241
Familiesp. 243
Composite Connectivesp. 243
Families Construction For JWAp. 246
Families Construction For CBPVp. 247
All Models are Categorical Modelsp. 249
Introductionp. 249
All Models Of x-Calculus Are Cartesian Categoriesp. 249
The Theorem, Vaguely Statedp. 249
Fixing The Object Structurep. 250
What Is A Model Of x-Calculus?p. 251
The Theorem, Precisely Statedp. 253
All Models Of CBPV Are CBPV Adjunction Modelsp. 254
All Models Of JWA Are JWA Module Modelsp. 259
Enrichmentp. 260
Representing Objectsp. 261
Introductionp. 261
Categorical Structuresp. 262
Joint vs. Separate Naturalityp. 262
Context Extension Functorsp. 263
Representable Functorsp. 264
Ordinary Categoryp. 264
Locally Indexed Categoryp. 266
Cartesian Categoryp. 267
Category With Right Modulesp. 269
Cartesian Category With Left Modulesp. 271
Parametrized Representabilityp. 273
Possible Worlds: Part 2p. 277
Adjunctions and Monadsp. 278
Definitions of Adjunctionp. 278
Terminality of Eilenberg-Moorep. 283
Kleisli and Co-Kleisli Adjunctionsp. 284
CBV Is Kleisli, CBN Is Co-Kleislip. 287
Conclusions
Conclusions, Comparisons and Further Workp. 293
Summary of Achievements and Drawbacksp. 293
Simplifying Algebra Semanticsp. 294
Advantages Of CBPV Over Monad And Linear Logic Decompositionsp. 294
Beyond Simple Typesp. 296
Dependent Typesp. 296
Polymorphismp. 297
Further Workp. 297
Appendicesp. 298
Technical Treatment of CBV and CBNp. 299
The Jumbo [lambda]-Calculusp. 300
Introductionp. 300
Tuple Typesp. 300
Function Typesp. 301
Languages and Translationsp. 302
Call-By-Valuep. 304
Coarse-Grain Call-By-Valuep. 304
Fine-Grain Call-By-Valuep. 305
From CG-CBV To FG-CBVp. 308
Call-By-Namep. 311
The Lazy Paradigmp. 312
Subsuming FG-CBV and CBNp. 314
From FG-CBV to CBPVp. 314
From CBPV Back To FG-CBVp. 314
From CBN to CBPVp. 319
From CBPV Back To CBNp. 320
Models In The Style Of Power-Robinsonp. 327
Introductionp. 328
Actions of Monoidal Categoriesp. 328
Freyd Categoriesp. 329
Judgement Modelp. 330
Enrichmentp. 331
Connectivesp. 331
Modelling CBPVp. 332
The Full Reflectionp. 333
Theoriesp. 334
Conservativityp. 336
Referencesp. 337
Indexp. 345
Table of Contents provided by Rittenhouse. All Rights Reserved.

ISBN: 9781402017308
ISBN-10: 1402017308
Series: Semantics Structures in Computation
Audience: Professional
Format: Hardcover
Language: English
Number Of Pages: 352
Published: 30th November 2003
Publisher: Springer-Verlag New York Inc.
Country of Publication: US
Dimensions (cm): 23.5 x 15.5  x 2.54
Weight (kg): 0.77