Head-Order Techniques and Other Pragmatics of Lambda Calculus Graph Reduction

Front Cover
Universal-Publishers, 2011 - Computers - 250 pages
Available in Paperback Available in eBook editions (PDF format) Institution: Syracuse University (Syracuse, NY, USA) Advisor(s): Prof. Klaus J. Berkling Degree: Ph.D. in Computer and Information Science Year: 1993 Book Information: 248 pages Publisher: Dissertation.com ISBN-10: 1612337570 ISBN-13: 9781612337579 View First 25 pages: (free download) Abstract The operational aspects of Lambda Calculus are studied as a fundamental basis for high-order functional computation. We consider systems having full reduction semantics, i.e., equivalence-preserving transformations of functions. The historic lineage from Eval-Apply to SECD to RTNF/RTLF culminates in the techniques of normal-order graph Head Order Reduction (HOR). By using a scalar mechanism to artificially bind relatively free variables, HOR makes it relatively effortless to reduce expressions beyond weak normal form and to allow expression-level results while exhibiting a well-behaved linear self-modifying code structure. Several variations of HOR are presented and compared to other efficient reducers, with and without sharing, including a conservative breadth-first one which mechanically takes advantage of the inherent, fine-grained parallelism of the head normal form. We include abstract machine and concrete implementations of all the reducers in pure functional code. Benchmarking comparisons are made through a combined time-space efficiency metric. The original results indicate that circa 2010 reduction rates of 10-100 million reductions per second can be achieved in software interpreters and a billion reductions per second can be achieved by a state-of-the art custom VLSI implementation.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

LAMBDA CALCULUS AND REDUCTION COMPUTING
1
List of Tables
6
6 Classification of reduction algorithmssystems and historical summary
20
SYNTAX NOTATION AND REPRESENTATIONS
25
List of Figures
33
2 Lambda expressions in classic de Bruijn and BTF notation
37
1 Combinator reduction contrasted to direct lambda reduction Figure 1 2 Contributions to the theory and the practice of Lambda Calculus Reduction
39
GRAPH REDUCTION ALGORITHMS
47
5 Cost and reduction ratios of APSH vs HORSH for the all test suite
138
7 Reduction counts for pred116
143
9 Ratios of APSHHORSH for the pred test suite
144
13 BETAR3 reduction counts for the tfac test suite
151
10 Definition of the fsa expression family
154
14 Family with infinitely increasing µβµπ of Frandsen Sturtivant
156
TOWARDS PRACTICAL REDUCTION SYSTEMS
163
1 Organization of memory in an active instruction implementation of HOR
165

2 Eager reduction of 2 1 12 1 01 0
50
5 The translation function r2b from REPstyle graph representations to BTF Figure 3 1 Result graph of EVAP reduction with pointer variables v1 v2 f...
57
6 Partial copying of the operator subgraph Figure 3 7 Compact RTNFRTLF normal order reducer with a force flag
63
5 Example of transforming an expression via the inthelarge rules
67
FACETS OF HEAD ORDER REDUCTION
77
2 Additional rules of early VA lookup for WHOR
83
5 Tree form of tw10 2 1 1 0 0 11 2 0 11 0 2
87
9 Quantumcontrolled HORSH reduction of 1 0 02 1 11 01 0
91
7 Memory and time for the all suite under four pure normalorder reducers
95
RELATED THEORIES
97
1 Substitution operators of the calculus
101
6 Nondeterministic reduction rules for Head Order Reduction
107
SHARING STRATEGIES
109
2 WHORSH reduction of 2 1 12 1 01 0
114
1 Shared open subterm in different abstraction contexts
119
7 Reduction of wads34 2 1 0 2 0 1 0 1 0 1 under HORSHVA
120
COMPARATIVE ANALYSIS AND EVALUATION
127
1 Results of whnf reduction for pred7
129
1 Memory vs time plots of three abstract reducers all tests
131
1 Description of the registers of the µRED machine
170
3 The µRED lowlevel pure HOR machine with linearmemory
171
5 Tree and linear graph of fact n if n 0 1 n fact n 1
176
4 Process queues under BFHOR for five test expressions
179
A PPENDICES
185
Figure A 7 APHOR Reducer with RTNFRTLF strategy and dBUVC machinery
189
B Reduction TracesGraphs
195
9 Left Spine tagged with a count of binding levels Figure 3 10 Symbolic depiction of the rules of HOR inthelarge Figure 3 11 Picture of a Head Nor...
199
Table B 8 Graph EVAP reduction of 2 1 12 1 01 0
201
The BTRD Experimentation System
205
1 Dialog for selecting a BTRD reducer and its applicable options
206
1 Runtime statistics fields of the B3 simulator of BTRD
207
4 Reduction Unit Display for the B3B3SH simulatorreducer
214
3 Possible entries in the B3 environment arrays E1 and E2
215
Test Expressions and Runtime Statistics
219
2 HORSHVA reduction of the all test set
221
79
223
Index
227
Copyright

Common terms and phrases

Bibliographic information