On Computational Interpretations of the Modal Logic S4 IIIb. Confluence, Termination of the $\lambda\mbox{ev}Q_H$-Calculus

Abstract : A language of proof terms for minimal logic is the $\lambda$-calculus, where cut-elimination is encoded as $\beta$-reduction. We examine corresponding languages for the minimal version of the modal logic S4, with notions of reduction that encodes cut-elimination for the corresponding sequent system. It turns out that a natural interpretation of the latter constructions is a $\lambda$-calculus extended by an idealized version of Lisp's \verb/eval/ and \verb/quote/ constructs. In this Part~IIIb, we complete the results of Part~IIIa. We show that the typed $\lambda\mbox{ev}Q_H$-calculus is confluent. It follows that the typed $\lambda\mbox{ev}Q_H$-calculus is a conservative extension of the typed ${\lambda_S4}_H$-calculus. We also prove that the typed $\lambda\mbox{ev}Q_H$-calculus is weakly terminating. Some problems remain open. In particular, we still don't know whether the typed $\lambda\mbox{ev}Q$-calculus terminates weakly, or whether the untyped $\lambda\mbox{ev}Q$-calculus is confluent.
Type de document :
Rapport
[Research Report] RR-3164, INRIA. 1997
Liste complète des métadonnées

https://hal.inria.fr/inria-00073524
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:07:15
Dernière modification le : samedi 17 septembre 2016 - 01:27:38
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:49:22

Fichiers

Identifiants

  • HAL Id : inria-00073524, version 1

Collections

Citation

Jean Goubault-Larrecq. On Computational Interpretations of the Modal Logic S4 IIIb. Confluence, Termination of the $\lambda\mbox{ev}Q_H$-Calculus. [Research Report] RR-3164, INRIA. 1997. 〈inria-00073524〉

Partager

Métriques

Consultations de la notice

125

Téléchargements de fichiers

116