The variable containment problem

Abstract

The essentially free variables of a term t in some λ-calculus, FV _β (t), form the set {x ¦ ∀u.t = _β u ⇒ x ∈ FV(u)}. This set is significant once we consider equivalence classes of λ-terms rather than λ-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 θ and contexts C[]that FV _β (C[t] ^θ)$\supseteq$FV _β (C[u ^θ])?

This property is important when we want to consider t → u as a rewrite rule and keep n-step rewriting decidable. Variable containment is in general not implied by FV _β (t)$\supseteq$FV _β (u). We give a decision procedure for the variable containment problem of the second-order fragment of λ^→. For full λ^→ 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.

The research reported here was partially supported by SERC grant GR/J07303.