Skip to main content

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)

Language: English
Click to download this file (264kB)
[thumbnail of varcont.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Language: English
Click to download this file (222kB) Preview
[thumbnail of]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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
DOI/Identification number: 10.1007/3-540-61254-8_22
Uncontrolled keywords: HRS, free variables, finitary PCF
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 19 Aug 2009 18:53 UTC
Last Modified: 16 Nov 2021 09:59 UTC
Resource URI: (The current URI for this page, for reference purposes)
Kahrs, Stefan:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.