A long-standing open problem of Parigot has been solved by David and Nour, namely, they gave a syntactical and arithmetical proof of the strong normalization of the untyped μμ'-reduction. In ...connection with this, we present in this paper a proof of the weak normalization of the μ and μ'-rules. The algorithm works by induction on the complexity of the term. Our algorithm does not necessarily give a unique normal form: sometimes we may get different normal forms depending on our choice. We also give a simpler proof of the strong normalization of the same reduction. Our proof is based on a notion of a norm defined on the terms.
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 $\lambda\mu$-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 $\lambda\mu$-calculus extended with the $\rho$- and $\theta$-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.
In this paper, we define a new realizability semantics for the simply typed lambda-mu-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. We also prove a ...completeness result of our realizability semantics using a particular term model. This paper corrects some errors in 21 by the first author and Saber.
Abstract
In this paper, in connection with the program of extending the Curry–Howard isomorphism to classical logic, we study the
$\lambda \mu$
-calculus of Parigot emphasizing the difference between ...the original version of Parigot and the version of de Groote in terms of normalization properties. In order to talk about a satisfactory representation of the integers, besides the usual
$\beta$
-,
$\mu$
-, and
$\mu '$
-reductions, we consider the
$\lambda \mu$
-calculus augmented with the reduction rules
$\rho$
,
$\theta$
and
$\varepsilon$
. We show that we need all of these rules for this purpose. Then we prove that, with the syntax of Parigot, the calculus enjoys the strong normalization property even when we add the rules
$\rho$
,
$\theta$
, and
$\epsilon$
, while the
$\lambda \mu$
-calculus presented with the more flexible de Groote-style syntax, in contrast, has only the weak normalization property. In particular, we present a normalization algorithm for the
$\beta \mu \mu '\rho \theta \varepsilon$
-reduction in the de Groote-style calculus.
In this paper, in connection with the program of extending the Curry–Howard isomorphism to classical logic, we study the
$\lambda \mu$
-calculus of Parigot emphasizing the difference between the ...original version of Parigot and the version of de Groote in terms of normalization properties. In order to talk about a satisfactory representation of the integers, besides the usual
$\beta$
-,
$\mu$
-, and
$\mu '$
-reductions, we consider the
$\lambda \mu$
-calculus augmented with the reduction rules
$\rho$
,
$\theta$
and
$\varepsilon$
. We show that we need all of these rules for this purpose. Then we prove that, with the syntax of Parigot, the calculus enjoys the strong normalization property even when we add the rules
$\rho$
,
$\theta$
, and
$\epsilon$
, while the
$\lambda \mu$
-calculus presented with the more flexible de Groote-style syntax, in contrast, has only the weak normalization property. In particular, we present a normalization algorithm for the
$\beta \mu \mu '\rho \theta \varepsilon$
-reduction in the de Groote-style calculus.
About the range property for H David, René; Nour, Karim
Logical methods in computer science,
01/2014, Volume:
10, Issue 1, Issue:
1:3
Journal Article
Peer reviewed
Open access
Recently, A. Polonsky has shown that the range property fails for H. We give
here some conditions on a closed term that imply that its range has an infinite
cardinality.
Combinatory logic shows that bound variables can be eliminated without loss of expressiveness. It has applications both in the foundations of mathematics and in the implementation of functional ...programming languages. The original combinatory calculus corresponds to minimal implicative logic written in a system "à la Hilbert''. We present in this paper a combinatory logic which corresponds to propositional classical logic. This system is equivalent to the system $λ ^{Sym}_{Prop}$ of Barbanera and Berardi.
In this paper we give an arithmetical proof of the strong normalization of lambda-Sym-Prop of Berardi and Barbanera 1, which can be considered as a formulae-as-types translation of classical ...propositional logic in natural deduction style. Then we give a translation between the lambda-Sym-Prop-calculus and the lambda-bar-mu-mu-tilde-star-calculus, which is the implicational part of the lambda-bar-mu-mu-tilde-calculus invented by Curien and Herbelin 3 extended with negation. In this paper we adapt the method of David and Nour 4 for proving strong normalization. The novelty in our proof is the notion of zoom-in sequences of redexes, which leads us directly to the proof of the main theorem.
We give in this paper a short semantical proof of the strong normalization for full propositional classical natural deduction. This proof is an adaptation of reducibility candidates introduced by ...J.-Y. Girard and simplified to the classical case by M. Parigot. PUBLICATION ABSTRACT
Some properties of the -calculus Nour, Karim; Saber, Khelifa
Journal of applied non-classical logics,
20/8/1/, Volume:
22, Issue:
3
Journal Article
Peer reviewed
In this paper, we present the
-calculus which at the typed level corresponds to the full classical propositional natural deduction system. The Church-Rosser property of this system is proved using ...the standardisation and the finiteness developments theorem. We also define the leftmost reduction and prove that it is a winning strategy.
PDF
