The variable containment problem

The essentially free variables of a term \(t\) in some \(\lambda\)-calculus, FV \(_{\beta}(t)\), form the set (\(x\) \(_{\mid}^{\mid}\) \(\forall u.t=_{\beta}u\Rightarrow x\) \(\epsilon\) FV\((u)\)}. This set is significant once we consider equivalence classes of \(\lambda\)-terms rather than \(\lambda\)-terms themselves, as for instance in higher-order rewriting. An important problem for (generalised) higher-order rewrite systems is the variable containment problem: given two terms \(t\) and \(u\), do we have for all substitutions \(\theta\) and contexts \(C\)[] that FV\(_{\beta}(C[t]^{\theta}) \supseteq\) FV\(_{\beta}(C[u^{\theta}])\)?

This property is important when we want to consider \(t \to u\) as a rewrite rule and keep \(n\)-step rewriting decidable. Variable containment is in general not implied by FV \(_{\beta} (t)\supseteq\) FV\(_{\beta}(u)\). We give a decision procedure for the variable containment problem of the second-order fragment of \(\lambda^{\to}\). For full \(\lambda^{\to}\) we show the equivalence of variable containment to an open problem in the theory of PCF; this equivalence also shows that the problem is decidable in the third-order case.