The variable containment problem

Kahrs, Stefan (1995) The variable containment problem. In: UNSPECIFIED. (Full text available)

Download (397kB) Preview
Download (222kB)


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.

Item Type: Conference or workshop item (UNSPECIFIED)
Uncontrolled keywords: HRS, free variables, finitary PCF
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 19 Aug 2009 18:53 UTC
Last Modified: 15 Jul 2014 07:48 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year