"Contraction-Aware Lambda-Calculus"

Abstract

A simply-typed lambda-calculus is presented whose normal forms exactly represent the cut-free derivations of the so-called contraction-free sequent calculus, invented independently by Hudelmaier and Dyckhoff. Its crucial property is termination of proof search without need for loop-detection.

The proposed lambda-calculus LambdaJT follows the paradigm of generalized eliminations put forward by von Plato and consequently also has permutative conversions. It will be shown that strong normalization of the beta-reductions and permutative conversions nevertheless can be established elegantly - even yielding an embedding of the system with beta-reductions only into Girard's polymorphic lambda-calculus. The full system, however, also has specific rules for the elimination of contractions. Unfortunately, a proof of weak normalization along the lines of the recent JSL paper by Dyckhoff and Negri has not yet been successful: Although their lemmas could be lifted to the more general situation of LambdaJT, the proof of termination of the normalization algorithm is still missing.