Kahrs, Stefan (1995) The variable containment problem. In: Dowek, Gilles and Heering, Jan and Meinke, Karl and Möller, Bernhard, eds. HigherOrder Algebra, Logic, and Term Rewriting Second International Workshop. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 109123. ISBN 9783540612544. EISBN 9783540683896. (doi:10.1007/3540612548_22) (KAR id:21244)
PDF
Language: English 

Download (397kB)
Preview



Postscript
Language: English 

Download (222kB)
Preview



Official URL http://dx.doi.org/10.1007/3540612548_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 higherorder rewriting. An important problem for (generalised) higherorder 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 secondorder 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 thirdorder case.
Item Type:  Book section 

DOI/Identification number:  10.1007/3540612548_22 
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:  06 May 2020 03:04 UTC 
Resource URI:  https://kar.kent.ac.uk/id/eprint/21244 (The current URI for this page, for reference purposes) 
Kahrs, Stefan:  https://orcid.org/0000000150999375 
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):