[{"type":"book","title":"On computational interpretations of the modal logic S4. IIIa. Termination, confluence, conservativity of lambda-evQ","issued":{"date-parts":[["1996"]]},"author":[{"family":"Goubault-Larrecq","given":"Jean"}],"note":"Karlsruhe 1996. (Interner Bericht. Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe. 1996,33.)","abstract":"\nA language of constructions for minimal logic is the\n$\\lambda$-calculus, where cut-elimination is encoded as\n$\\beta$-reduction. We examine corresponding languages for the\nminimal version of the modal logic S4, with notions of reduction\nthat encodes cut-elimination for the corresponding sequent system.\nIt turns out that a natural interpretation of the latter\nconstructions is a $\\lambda$-calculus extended by an idealized\nversion of Lisp's \\verb\/eval\/ and \\verb\/quote\/ constructs.\n\nIn this Part IIIa, we examine the termination and confluence\nproperties of the ${\\lambda\\mbox{\\tt ev\\\/}Q}$ and negative:\nthe typed calculi do not terminate, the subsystems $\\Sigma$ and\n$\\Sigma_H$ that propagate substitutions, quotations andevaluations\ndownwards do not terminate either in the untyped case, and the\nuntyped ${\\lambda\\mbox{\\tt ev\\\/}Q}_H$-calculus is not confluent.\nHowever, the typed versions of $\\Sigma$ and $\\Sigma_H$ do terminate,\nso the typed ${\\lambda\\mbox{\\tt ev\\\/}Q}$-calculus is confluent.\nIt follows that the typed ${\\lambda\\mbox{\\tt ev\\\/}Q}$-calculus is a\nconservative extension of the typed ${\\lambda_{\\rm S4}}$-calculus.\n\nPart IIIb will cover the confluence of the typed\n${\\lambda\\mbox{\\tt ev\\\/}Q}_H$-calculus,\nwhich is not dealt with here.\n","kit-publication-id":"40296"}]