+612 9045 4394
 
CHECKOUT
Compiling Natural Semantics : Lecture Notes in Computer Science - Mikael Pettersson

Compiling Natural Semantics

Lecture Notes in Computer Science

By: Mikael Pettersson (Editor)

Paperback

Published: 5th May 1999
Ships: 5 to 9 business days
5 to 9 business days
$125.05
or 4 easy payments of $31.26 with Learn more
if ordered within

Natural Semantics has become a popular tool among programming language researchers for specifying many aspects of programming languages. However, due to the lack of practical tools for implementation, the natural semantics formalism has so far largely been limited to theoretical applications.
This book introduces the rational meta-language RML as a practical language for natural semantics specifications. The main part of the work is devoted to the problem of compiling natural semantics, actually RML, into highly efficient code. For this purpose, an effective compilation strategy for RML is developed and implemented in the rml2c compiler. This compiler ultimately produces low-level C code. Benchmarking results show that rml2c-produced code is much faster than code resulting from compilers based on alternative implementation approaches.

Introductionp. 1
The Problemp. 1
Our Solutionp. 2
Overview of this Thesisp. 2
Relation to our Previous Workp. 3
Preliminariesp. 5
Use of Formal Specificationsp. 5
Why Generate Compilers?p. 6
Ways to Specify Semanticsp. 6
Interpretersp. 6
Abstract Machinesp. 7
Attribute Grammarsp. 7
Donotational Semanticsp. 8
Action Semanticsp. 9
Evolving Algebrasp. 10
Structural Operational Semanticsp. 10
Natural Semanticsp. 11
Natural Deductionp. 11
Relation to Programming Languagesp. 12
Examplep. 12
Meaningp. 13
Pragmaticsp. 14
Recent Extensionsp. 15
The Design of RMLp. 17
Syntaxp. 18
Static Semanticsp. 20
Bindings and Unknownsp. 21
Technicalitiesp. 21
Modelling Backtrackingp. 22
Intuitionp. 22
Originsp. 24
Denotational Semantics of Backtrackingp. 25
Deter minacyp. 30
Historyp. 31
Static Semanticsp. 31
Dynamic Semanticsp. 32
Differences from SMLp. 32
Examplesp. 35
A Small Examplep. 35
Abstract Syntaxp. 35
Inference Rulesp. 36
Operational Interpretationp. 36
Mini-Frejap. 37
Abstract Syntaxp. 37
Valuesp. 38
Environmentsp. 38
Evaluationp. 39
Modularityp. 41
Adding Recursionp. 42
Summaryp. 44
Dieselp. 44
Static Elaborationp. 44
Flatteningp. 45
Emitting Codep. 46
C Gluep. 46
Summaryp. 46
Petrolp. 47
Summaryp. 47
Mini-MLp. 47
Rémy-Style let-Polymorphismp. 48
Equality Typesp. 50
Wright's Simple Imperative Polymorphismp. 50
Overloadingp. 51
Specification Fragmentsp. 53
Summaryp. 55
Problematic Issuesp. 55
Environmentsp. 55
Default Rulesp. 55
Summaryp. 56
Implementation Overviewp. 57
Compilation Strategyp. 57
Developmentp. 58
Alternativesp. 59
Prologp. 59
Warren's Abstract Machinep. 59
Attribute Grammarsp. 60
SMLp. 60
Implementation Statusp. 60
Reducing Nondeterminismp. 63
Backgroundp. 64
Grammarsp. 64
FOL Representationp. 65
The Front-Endp. 66
The FOL-TRS Rewriting Systemp. 67
Propertiesp. 70
Terminationp. 70
Confluencep. 73
Alternatives for Rewriting Negationsp. 74
Examplesp. 75
appendp. 75
lookupp. 76
Missed Conditionalsp. 78
Implementation Notesp. 81
Implementation Complexityp. 82
Limitationsp. 83
Related Workp. 84
Compiling Pattern Matchingp. 85
Introductionp. 85
What is Matching?p. 85
Compiling Term Matchingp. 86
Troublesome Examplesp. 87
Copied Expressionsp. 88
Repeated and Sub-Optimal Testsp. 89
Intuitive Operationp. 89
Preliminariesp. 91
Objectsp. 92
Operationsp. 93
The Algorithmp. 95
Step 1: Preprocessingp. 95
Step 2: Generating the DFAp. 96
Step 3: Merging of Equivalent Statesp. 97
Step 4: Generating Intermediate Codep. 97
The Examples Revisitedp. 98
The demo Functionp. 98
The unwieldy Functionp. 100
State Mergingp. 102
Implementation Notesp. 105
Data Representationp. 105
Compile-Time Warningsp. 105
Matching Exceptionsp. 106
Guarded Patternsp. 106
Related Workp. 107
Modifications for RMLp. 108
Experiences and Conclusionsp. 109
Compiling Continuationsp. 111
Properties of CPSp. 111
Translating RML to CPSp. 113
Data Representationp. 113
Local Optimizations on CPSp. 116
Translating CPS to Codep. 116
Controlp. 116
Copy Propagationp. 120
Memory Allocationp. 120
Datap. 121
Translating Code to Cp. 121
Data Representationp. 122
Memory Managementp. 122
A Code Generation Examplep. 123
Simulating Tailcalls in Cp. 127
The Problemp. 127
Overviewp. 128
Why is C not Tail-Recursive?p. 129
Why do not Prototypes Help?p. 130
ANDFp. 130
Preliminariesp. 130
Tailcall Classificationp. 133
Plain Dispatching Labelsp. 133
Alternative Access Methods for Globalsp. 135
The Monster Switchp. 136
Dispatching Switchesp. 138
Step 1: Fast Known Intramodule Callsp. 138
Step 2: Recognizing Unknown Intramodule Callsp. 139
Step 3: Fast Unknown Intramodule Callsp. 140
Additional Benefitsp. 144
Pushy Labelsp. 144
Pushy Labels and Register Windowsp. 147
The `Warped Gotos' Techniquep. 148
The wamcc Approachp. 150
Non-Solutionsp. 151
Experimental Resultsp. 152
Conclusionsp. 152
Performance Evaluationp. 153
Target Systemsp. 153
Overviewp. 154
Allocation Arena Sizep. 155
State Access Methodsp. 163
Compiler Optimizationsp. 163
Facing the Oppositionp. 166
Mini-Frejap. 166
Petrolp. 167
Conclusionsp. 168
Concluding Remarksp. 169
Summaryp. 169
Future Workp. 170
Default Rulesp. 170
Programming Sub-Languagep. 171
Taming Side-Effectsp. 171
Moded Typesp. 171
Linear Typesp. 171
Compile to SMLp. 172
Tuning the Runtime Systemsp. 172
User-Friendlinessp. 172
The Definition of RMLp. 173
Introductionp. 173
Differences to SMLp. 173
Notation for Natural Semanticsp. 175
Lexical Definitionsp. 175
Syntax Definitionsp. 175
Setsp. 176
Tuplesp. 176
Finite Sequencesp. 176
Finite Mapsp. 176
Substitutionsp. 177
Disjoint Unionsp. 177
Relationsp. 177
Examplep. 178
Lexical Structurep. 180
Reserved Wordsp. 180
Integer Constantsp. 180
Real Constantsp. 180
Character Constantsp. 180
String Constantsp. 180
Identifiersp. 181
Type Variablesp. 181
Whitespace and Commentsp. 181
Lexical Analysisp. 181
Syntactic Structurep. 183
Derived Forms, Full and Core Grammarp. 183
Ambiguityp. 183
Static Semanticsp. 190
Simple Objectsp. 190
Compound Objectsp. 190
Initial Static Environmentsp. 191
Inference Rulesp. 191
Dynamic Semanticsp. 201
Simple Objectsp. 201
Compound Objectsp. 201
Initial Dynamic Objectsp. 202
Inference Ridesp. 202
Initial Objectsp. 211
Initial Static Objectsp. 211
Initial Dynamic Objectsp. 211
Bibliographyp. 223
Indexp. 239
Table of Contents provided by Publisher. All Rights Reserved.

ISBN: 9783540659686
ISBN-10: 3540659684
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 246
Published: 5th May 1999
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 1.4
Weight (kg): 0.37