A carregar...
Publicação
Atomic polymorphism
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 97.51 KB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
It has been known for six years that the restriction of Girard’s polymorphic system F to
atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus.
We firstly observe that Tait’s method of “convertibility” applies quite naturally to the proof of strong
normalization of the restricted Girard system. We then show that each β-reduction step of the full
intuitionistic propositional calculus translates into one or more βη-reduction steps in the restricted Girard
system. As a consequence, we obtain a novel and perspicuous proof of the strong normalization property
for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role
to η-conversions.
Descrição
Palavras-chave
Predicative polymorphism Strong normalization Natural deduction Second order lambda-calculus
Contexto Educativo
Citação
Editora
The Journal of Symbolic Logic