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.
Previous | Index | Next An error occured whilst processing this directive