# Intersection Types for Unboundedness Problems

## TL;DR

This paper surveys how intersection types can be used to analyze and estimate quantitative properties of simply typed lambda-terms, focusing on unboundedness problems.

## Contribution

It introduces two type systems that estimate the frequency and maximal occurrences of constants in lambda-terms' normal forms.

## Key findings

- First type system estimates total appearances of a constant.
- Second type system estimates maximum appearances on a branch.
- Provides tools for analyzing unboundedness in lambda calculus.

## Abstract

Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-terms. We present two type systems. The first allows to estimate (by appropriately defined value of a derivation) the number of appearances of a fixed constant 'a' in the beta-normal form of a considered lambda-term. The second type system is more complicated, and allows to estimate the maximal number of appearances of the constant 'a' on a single branch.