A Few Remarks on SKInT
Résumé
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$.