# Differential Logical Relations, Part I: The Simply-Typed Case (Long Version)

## TL;DR

This paper introduces differential logical relations that measure the interactive complexity between programs in the simply-typed lambda calculus, extending traditional logical and metric relations with a novel, structured approach.

## Contribution

It proposes a new form of logical relation that captures the complexity of program differences using mathematical objects, and demonstrates its properties and categorical structure.

## Key findings

- Differential logical relations generalize logical and metric relations.
- They can be organized in a cartesian closed category.
- A soundness theorem is established for the simply-typed lambda calculus.

## Abstract

We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between terms not (necessarily) by a numerical value, but by a mathematical object which somehow reflects the interactive complexity, i.e. the type, of the compared terms. We exemplify this concept in the simply-typed lambda-calculus, and show a form of soundness theorem. We also see how ordinary logical relations and metric relations can be seen as instances of differential logical relations. Finally, we show that differential logical relations can be organised in a cartesian closed category, contrarily to metric relations, which are well-known not to have such a structure, but only that of a monoidal closed category.