Higher Order Matching of Linear Terms is Decidable

I'm presenting the results of my Master's project. I've been working with Prof. Kfoury on the Linear Lambda Calculus. Interest in the Linear Lambda Calculus has been inspired by the work of the Church group. So far, the Linear Lambda Calculus hasn't appeared as a theory by itself; however, a lot of related results may give new insights if combined. I specifically look at the matching problem in the context of the Linear Lambda Calculus.

Abstract

The matching problem is: Given two terms A and B, determine whether there is a substitution sigma for the free variables in A such that sigma(A)=B. In this paper, we prove that the matching problem is decidable for the particular case of linear higher order terms. A term is linear iff. every variable, free or bound, occurs at most once. Our terms are untyped but we show how our proof generalizes to simply typed terms. We also provide an overview of other results and open problems about the matching problem and the linear lambda-calculus.