The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors

TL;DR

This paper demonstrates that third order pattern matching is undecidable in certain typed lambda-calculi, highlighting fundamental computational limitations in systems with dependent types or type constructors.

Contribution

It establishes the undecidability of third order pattern matching in typed lambda-calculi with dependent types or type constructors through a reduction from second order unification.

Findings

Third order pattern matching is undecidable in calculi with dependent types.

Undecidability is proven via reduction from second order unification.

Results impact the design of type inference algorithms.

Abstract

We prove the undecidability of the third order pattern matching problem in typed lambda-calculi with dependent types and in those with type constructors by reducing the second order unification problem to them.