Non-idempotent types for classical calculi in natural deduction style

TL;DR

This paper introduces resource-aware, non-idempotent type systems for the { extlambda}{ extmu}-calculus, providing simple combinatorial characterizations of normalization and bounds on reduction lengths, and extends these results to a small-step calculus.

Contribution

It develops novel non-idempotent typing systems for { extlambda}{ extmu}-calculus and its small-step variant, enabling precise normalization characterizations and complexity bounds.

Findings

Typability characterizes head and strongly normalizing terms.

Type derivations provide upper bounds on reduction lengths.

The small-step calculus { extlambda}{ extmu}s} is compatible with extended non-idempotent interpretations.

Abstract

In the first part of this paper, we define two resource aware typing systems for the {\lambda}{\mu}-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head reduction and the maximal reduction sequences to normal-form. In the second part of this paper, the {\lambda}{\mu}-calculus is refined to a small-step calculus called {\lambda}{\mu}s, which is inspired by the substitution at a distance paradigm. The {\lambda}{\mu}s-calculus turns out to be compatible with a natural extensionof the non-idempotent interpretations of {\lambda}{\mu}, i.e., {\lambda}{\mu}s-reduction preserves and decreases typing derivations in an extended appropriate typing system. We thus derive a simple arithmetical characterization of strongly {\lambda}{\mu}s-normalizing terms by means of typing.