Bonelli, Eduardo <br/><br/>
A normalisation result for higher-order calculi with explicit substitutions 

 - ref_localidad@37940 :  ,  2003 
 - ^p Datos electrónicos (1 archivo : 323 KB) .
<br/><br/> Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática-UNLP (Colección BIPA / Biblioteca.) -- Disponible también en línea vía suscripción BECyT (Cons. 10-03-2008) 
<br/><br/> Explicit substitutions (ES) were introduced as a bridge between the theory of rewrite systems with binders and substitution, such as the λ-calculus, and their implementation. In a seminal paper P.- A. Melli`es observed that the dynamical properties of a rewrite system and its ES-based implementation may not coincide: he showed that a strongly normalising term (i.e. one which does not admit infinite derivations) in the λ-calculus may lose this status in its ES-based implementation. This paper studies normalisation for the latter systems in the general setting of higher-order rewriting: Based on recent work extending the theory of needed strategies to non-orthogonal rewrite systems we show that needed strategies normalise in the ES-based implementation of any orthogonal pattern higher-order rewrite system. 
<br/><br/>
<br/><br/><label>Standard No.: </label>DIF002275 
<br/><br/><label>Subjects--Topical Terms: </label><br/>LÓGICA COMPUTACIONAL<br/>SISTEMAS DE REESCRITURA<br/>CÁLCULO LAMBDA