## Head-Order Techniques and Other Pragmatics of Lambda Calculus Graph ReductionAvailable 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

1 | |

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 |

227 | |

### Common terms and phrases

_ app app _ app lam _ lam _ abstract machine abstract reducers abstraction context algorithm am_ app AP-SH app lam _ app0 arguments Berkling BETAR3 BF-HOR Bruijn indices BTRD Church Numerals clos lam closure costs defun delayed substitutions env phi environment Figure fun-of term graph reduction head normal form Head Order Reduction head variable HOR reducer HOR-SH implementation in-the-large integer lam _ app lam _ lam Lambda Calculus lambda expressions left spine linear Macintosh Common Lisp memory mk-app normal order normal-order notation number of reductions operand operator optimizations overall pointer ratios recursive redex reduction algorithm reduction counts reduction in isolation reduction system relatively free variables representation result rterm RTNF/RTLF rules runtime SECD SECD machine sequence shexp stack phi strategy strong normal structure subterm susp suspension symbol Table term env Term Stack Env tfac traversal updates Wadsworth whnf Y combinator ρ φ