Author(s):
Espírito Santo, José 
Date: 2011
Persistent ID: http://hdl.handle.net/1822/14680
Origin: RepositóriUM - Universidade do Minho
Document details
A note on preservation of strong normalisation in the lambda-calculus
Description
An auxiliary notion of reduction ρ on the λ-terms preserves strong normalisation if all strongly normalising terms for β are also strongly normalising for β∪ρ.Wegive a sufficient condition for ρ to preserve strong normalisation. As an example of application, we check easily the sufficient condition for Regnier’s σ-reduction rules and the ‘‘assoc’’-reduction rule inspired by calculi with let-expressions. This gives the simplest proof so far that the union of all these rules preserves strong normalisation.
An auxiliary notion of reduction ρ on the λ-terms preserves strong normalisation if all strongly normalising terms for β are also strongly normalising for β∪ρ.Wegive a sufficient condition for ρ to preserve strong normalisation. As an example of application, we check easily the sufficient condition for Regnier’s σ-reduction rules and the ‘‘assoc’’-reduction rule inspired by calculi with let-expressions. This gives the simplest proof so far that the union of all these rules preserves strong normalisation.
Document Type
Article
Language English
Language English
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||