A Few Remarks on SKInT

Abstract : SKIn and SKInT are two first-order languages that have been proposed recently by Healfdene Goguen and the author. While SKIn encodes lambda-calculus reduction faithfully, standardizes and is confluent even on open terms, it normalizes only weakly in the simply-typed case. On the other hand, SKInT normalizes strongly in the simply-typed case, standardizes and is confluent on open terms, and also encodes lambda-calculus reduction faithfully, although in a less direct way. This report has two goals. First, we show that the natural simple type system for SKInT, seen as a natural deduction system, is not exactly a proof system for intuitionistic logic, but for a very close fragment of the modal logic S4, in which intuitionistic logic is easily coded. This explains why the SKIn and SKInT typing rules are different, and why SKInT encodes lambda-calculus in a less direct way than SKIn. Second, we show that SKInT, like $\lambda\upsilon$ and a few other calculi of explicit substitutions, preserves strong normalization. In fact, SKInT also preserves weak normalization and solvability. We show this as a corollary of a stronger result, analogous to a well-known result in the lambda-calculus: the solvable SKInT-terms are exactly those that are typable in the system $S\omega$ of conjunctive types (inspired from Émilie Sayag), the weakly normalizing SKInT-terms (with or without $\eta$) are exactly those that have a definite positive $S\omega$-typing, and the strongly normalizing SKInT-terms (with or without $\eta$) are exactly those that are typable in the system $S$ of conjunctive types, which does not have the universal type $\omega$.
Type de document :
Rapport
[Research Report] RR-3475, INRIA. 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00073214
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:12:54
Dernière modification le : samedi 17 septembre 2016 - 01:27:26
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:45:22

Fichiers

Identifiants

  • HAL Id : inria-00073214, version 1

Collections

Citation

Jean Goubault-Larrecq. A Few Remarks on SKInT. [Research Report] RR-3475, INRIA. 1998. 〈inria-00073214〉

Partager

Métriques

Consultations de la notice

121

Téléchargements de fichiers

100