Bounding normalization time through intersection types

TL;DR

This paper uses non-idempotent intersection types to establish a bound on the length of beta-reduction sequences in lambda calculus, linking the bound to the term's size.

Contribution

It introduces a novel method to bound normalization time using intersection types, providing a quantitative measure of reduction length.

Findings

Bound on beta-reduction sequence length expressed as a function of term size

Method applicable to analyzing normalization complexity

Provides theoretical insights into lambda calculus reduction behavior

Abstract

Non-idempotent intersection types are used in order to give a bound of the length of the normalization beta-reduction sequence of a lambda term: namely, the bound is expressed as a function of the size of the term.