# The variable containment problem

Kahrs, Stefan (1995) The variable containment problem. In: Dowek, Gilles and Heering, Jan and Meinke, Karl and Möller, Bernhard, eds. Higher-Order Algebra, Logic, and Term Rewriting Second International Workshop. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 109-123. ISBN 978-3-540-61254-4. E-ISBN 978-3-540-68389-6. (doi:10.1007/3-540-61254-8_22) (KAR id:21244)

 PDF Language: English Download this file(PDF/264kB) Request a format suitable for use with assistive technology e.g. a screenreader Postscript Language: English Download this file(Postscript/222kB) Preview Request a format suitable for use with assistive technology e.g. a screenreader Official URL:http://dx.doi.org/10.1007/3-540-61254-8_22

## Abstract

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.

Item Type: Book section 10.1007/3-540-61254-8_22 HRS, free variables, finitary PCF Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing Mark Wheadon 19 Aug 2009 18:53 UTC 16 Nov 2021 09:59 UTC https://kar.kent.ac.uk/id/eprint/21244 (The current URI for this page, for reference purposes)

## University of Kent Author Information

### Kahrs, Stefan.

Creator's ORCID: https://orcid.org/0000-0001-5099-9375