Long Bn Normal Forms and Confluence

C. Barry Jay

Abstract: Eta-conversion and surjective pairing can be treated as expansion rules in the simply-typed lambda-calculus with terminal object, surjective pairing and iterator, to obtain a fully confluent and essentially normalising rewriting system. By adding some categorically motivated, but syntactic, restrictions to these expansions, one obtains a confluent reduction system which is strongly normalising to the long Beta-eta normal forms.

LFCS report ECS-LFCS-91-183

Previous | Index | Next