Decidability of Higher Order Matching, Colin Stirling.

Higher-order unification is the problem: given an equation *t = u* containing free variables, is there a solution substitution Θ such that *t*Θ and uΘ have the same normal form? The terms are drawn from the simply typed lambda calculus and the same normal form is up to βη-equality. Higher order matching is the particular instance: when the term *u* is closed, can *t* be pattern matched to *u*? Although higher-order unification is undecidable (even if free variables are only second-order), higher-order matching was conjectured to be decidable by Huet. [...] In this paper, we confirm Huet's conjecture that higher-order matching is decidable.

This paper is very technical, but I think it's a problem of significant interest, since decidable fragments of higher-order unification are very important to theorem proving systems. As an aside, Huet conjectured that higher order matching was decidable in 1976, so it's taken thirty years of effort to prove this.

## Recent comments

8 weeks 2 days ago

8 weeks 4 days ago

8 weeks 6 days ago

15 weeks 5 days ago

21 weeks 3 days ago

21 weeks 4 days ago

22 weeks 3 days ago

25 weeks 2 days ago

26 weeks 5 days ago

26 weeks 5 days ago