Deciding equivalence with sums and the empty type

TL;DR

This paper introduces a logical technique to decide equivalence in a typed lambda calculus with sums and the empty type, proving decidability and correspondence with contextual equivalence.

Contribution

It extends focusing techniques to positive types, establishing decidability of $eta ext{-} ext{eta}$-equivalence with sums and the empty type, and demonstrates a finite model property.

Findings

Decidability of $eta ext{-} ext{eta}$-equivalence with sums and empty type

Equivalence coincides with contextual equivalence

Finite model property established

Abstract

The logical technique of focusing can be applied to the $\lambda$-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with $\beta\eta$-normal forms. Introducing a saturation phase gives a notion of quasi-normal forms in presence of positive types (sum types and the empty type). This rich structure let us prove the decidability of $\beta\eta$-equivalence in presence of the empty type, the fact that it coincides with contextual equivalence, and a finite model property.