Kahrs, Stefan
(1995)
*
The variable containment problem.
*
In: UNSPECIFIED.
(Full text available)

## Abstract

The emphessentially free variables of a term t in some λ-calculus, mathrmFV<sub>β</sub>(t), form the set { xmid ∀ u.:t=<sub>β</sub> u ⇒ x∈mathrmFV(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 emphvariable containment problem: given two terms t and u, do we have for all substitutions θ and contexts C[~] that mathrmFV<sub>β</sub>(C[substtθ])⊇ mathrmFV<sub>β</sub>(C[substuθ])? 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 emphnot implied by mathrmFV<sub>β</sub>(t)⊇mathrmFV<sub>β</sub>(u). We give a decision procedure for the variable containment problem of the second-order fragment of λ<sup>→</sup>. For full λ<sup>→</sup> 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.

- Depositors only (login required):