On Computational Interpretations of the Modal Logic S4 IIIb. Confluence, Termination of the $\lambda\mbox{ev}Q_H$-Calculus - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 1997

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

Jean Goubault-Larrecq

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.

Dates and versions

inria-00073524 , version 1 (24-05-2006)

Identifiers

• HAL Id : inria-00073524 , version 1

Cite

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⟩

124 View