Execution Time of lambda-Terms via Denotational Semantics and Intersection Types

TL;DR

This paper establishes a connection between the size of type derivations in a non-idempotent intersection type system and the execution time of lambda-terms on Krivine's machine, using a relational model of linear logic.

Contribution

It introduces a novel link between denotational semantics, intersection types, and execution time analysis of lambda-calculus terms.

Findings

Type derivation size correlates with execution time.

Type sizes provide bounds on lambda-term execution durations.

Relational model offers a semantic foundation for complexity analysis.

Abstract

The multiset based relational model of linear logic induces a semantics of the type free lambda-calculus, which corresponds to a non-idempotent intersection type system, System R. We prove that, in System R, the size of the type derivations and the size of the types are closely related to the execution time of lambda-terms in a particular environment machine, Krivine's machine.