Kahrs, Stefan
(1995)
The variable containment problem.
In: UNSPECIFIED.
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):
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_postscript.png)
