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 

Click to download this file (264kB)


This file may not be suitable for users of assistive technology.
Request an accessible format


Postscript
Language: English 

Click to download this file (222kB)
Preview

Preview 
This file may not be suitable for users of assistive technology.
Request an accessible format


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:  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:  https://kar.kent.ac.uk/id/eprint/21244 (The current URI for this page, for reference purposes) 
Kahrs, Stefan:  https://orcid.org/0000000150999375 
 Link to SensusAccess
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):