On Two Forms of Bureaucracy in Derivations
Kai Bruennler, Stéphane Lengrand · HAL (Le Centre pour la Communication Scientifique Directe) · 2005
We call irrelevant information in derivations bureaucracy. An example of such irrelevant information is the order between two consecutive inference rules that trivially permute. Building on ideas by Guglielmi, we identify two forms of bureaucracy that occur in the calculus of structures (and, in fact, in every non-trivial term rewriting derivation). We develop term calculi that provide derivations that do not contain this bureaucracy. We also give a normalisation procedure that removes bureaucracy from derivations and find that in a certain sense the normalisation process is a process of cut elimination.