An estimation for the lengths of reduction sequences of the \lambda\mu\rho\theta-calculus

DOI10.23638/LMCS-14(2:17)2018zbMATH Open1453.03007arXiv1703.05930MaRDI QIDQ4580321FDOQ4580321

Karim Nour, Péter Battyányi

Publication date: 15 August 2018

Abstract: Since it was realized that the Curry-Howard isomorphism can be extended to the case of classical logic as well, several calculi have appeared as candidates for the encodings of proofs in classical logic. One of the most extensively studied among them is the $lambdamu$-calculus of Parigot. In this paper, based on the result of Xi presented for the $lambda$-calculus Xi, we give an upper bound for the lengths of the reduction sequences in the $lambdamu$-calculus extended with the $ho$- and $heta$-rules. Surprisingly, our results show that the new terms and the new rules do not add to the computational complexity of the calculus despite the fact that $mu$-abstraction is able to consume an unbounded number of arguments by virtue of the $mu$-rule.

Full work available at URL: https://arxiv.org/abs/1703.05930

zbMATH Keywords

standardizationclassical logic\(\lambda\mu\)-calculuslength of reduction sequence

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Intensional interpretations of functionals of finite type I
• A symmetric lambda calculus for classical program extraction
• An environment machine for the λμ-calculus
• Proofs of strong normalisation for second order classical natural deduction
• Classical logic, storage operators and second-order lambda-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Normalization without reducibility
• An Arithmetical Proof of the Strong Normalization for the λ-Calculus with Recursive Equations on Types
• Title not available (Why is that?)
• Upper bounds for standardizations and an application
• Why the usual candidates of reducibility do not work for the symmetric \(\lambda\mu\)-calculus
• Typed Lambda Calculi and Applications
• Lambda-calcul, évaluation paresseuse et mise en mémoire
• Arithmetical proofs of strong normalization results for symmetric lambda calculi
• The Cost of Usage in the ?-Calculus

Cited In (2)

• Title not available (Why is that?)
• An encoding of the \(\lambda \)-calculus in the string MultiSet rewriting calculus

This page was built for publication: An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4580321)