This thesis was written while I was employed half be the Mathematical Institute and half by the 'Centrale Interfaculteit' of the University of Utrecht, from 1975 to 1979. It was a privilege to be a promovendus in the Logic department of Professor Dirk van Dalen, and those years will remain a dear memory because of the enjoyable and stimulating working conditions he created there. Apart from that, it is my pleasure to express my deep gratitude to him for the general guidance of my work and for the numerous detailed improvements that he suggested in an earlier draft of the text.
Author(s): Jan Willem Klop
Publisher: Mathematisch Centrum
Year: 1980
Language: English
Commentary: Scanned by author; DjVu'ed, OCR'ed by Envoy
Pages: 341
City: Amsterdam
INTRODUCTION AND SUMMARY V
INTERDEPENDENCE OF THE SECTIONS xiii
CHAPTER I. XB-CALCULUS AND DEFINABLE EXTENSIONS 1
1. Lambda terms 1
2. Combinators 11
3. Labels and descendants 17
4. Finite Developments 30
5. Abstract Reduction Systems 44
6. The Church-Rosser Theorem 57
7. Church's Theorem 72
8. Strong Normalization of labeled X-calculi (via Al-calculus) 75
9. Standardization 84
10. Standardization and equivalence of reductions 93
11. Normalization 113
12. Cofinal reductions 115
CHAPTER II. REGULAR COMBINATORY REDUCTION SYSTEMS 119
1. Combinatory Reduction Systems 120
2. Descendants and labels for combinatory reductions 137
3. The Church-Rosser Theorem for regular combinatory reductions 141
4. Reductions with memory 151
5. Non-erasing reductions 164
6. Decreasing labelings and Strong Normalization 175
CHAPTER III. IRREGULAR COMBINATORY REDUCTION SYSTEMS 195
1. Counterexamples to the Church-Rosser property 195
2. Intermezzo. An intuitive explanation via Bohm trees 216
3. Additional properties of A(CL) 220
4. Some positive CR-results for non-left-linear CRS's 232
5. The 'black box' lemma 240
CHAPTER IV. XBn-CALCULUS 249
1. The Church-Rosser Theorem for XBri-calculus 249
2. Residuals 252
3. Tracing in diagrams 257
4. Standardization of Bn-reductions 263
5. The Normalization Theorem for X3r-calculus 279
6. Cofinal 3ri-reductions 293
REFERENCES 298
