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)

PDF
 Preview
Postscript
 Preview
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, Faculties > Sciences > School of Computing > Theoretical Computing Group Mark Wheadon 19 Aug 2009 18:53 UTC 09 Sep 2019 14:12 UTC https://kar.kent.ac.uk/id/eprint/21244 (The current URI for this page, for reference purposes)