School of Computing

The variable containment problem

Stefan Kahrs

In Gilles Dowek, Jan Heering, Karl Meinke, and Bernhard M"oller, editors, Higher-Order Algebra, Logic, and Term Rewriting, volume 1074 of Lecture Notes in Computer Science, pages 182-196. Springer, September 1995.

Abstract

The \emph{essentially} free variables of a term (unknown variable t)$ in some $\lambda$-calculus, $\mathrm{FV}_{\beta}(t)$, form the set $\{ x\mid \forall u.\:t=_\beta u \Rightarrow x\in\mathrm{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 \emph{variable containment problem}: given two terms (unknown variable t)$ and (unknown variable u)$, do we have for all substitutions $\theta$ and contexts (unknown variable C)[~]$ that $\mathrm{FV}_{\beta}(C[\subst{t}{\theta}])\supseteq \mathrm{FV}_{\beta}(C[\subst{u}{\theta}])$?

This property is important when we want to consider (unknown variable t)\to u$ as a rewrite rule and keep (unknown variable n)$-step rewriting decidable. Variable containment is in general \emph{not} implied by $\mathrm{FV}_{\beta}(t)\supseteq\mathrm{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.

Download publication 83 kbytes

Bibtex Record

@conference{565,
author = {Stefan Kahrs},
title = {The variable containment problem},
month = {September},
year = {1995},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1995/565},
    ISBN = {3-540-61254-8},
    booktitle = {Higher-Order Algebra, Logic, and Term Rewriting},
    editor = {Gilles Dowek and Jan Heering and Karl Meinke and Bernhard M"oller},
    publisher = {Springer},
    refereed = {yes},
    series = {Lecture Notes in Computer Science},
    volume = {1074},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014