Searcharxiv⌕ Search

arXiv subjects

Karim Nour

Publications and source records attributed to Karim Nour.

At least 19 recordsLinked to original sources
arXiv2025

Normalization properties of $λμ$-calculus using realizability semantics

In this paper, we present a general realizability semantics for the simply typed $λμ$-calculus. Then, based on this semantics, we derive both weak and strong normalization results for two versions of the $λμ$-calculus equipped with specific simplification rules. The novelty in our method, in addition to its more systematic approach, lies in its applicability to a broader set of reduction rules without relying on the usual postponement technique. Our approach is original in that it introduces a parameter into the definition of the model, thus establishing a general result which we can then apply to systems with different sets of reduction rules by adjusting the parameter accordingly. Our saturation conditions also lead to a neat characterization of typable $λμ$-terms.

math.LO↗
arXiv2018

An estimation for the lengths of reduction sequences of the $λμρθ$-calculus

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 $λμ$-calculus of Parigot. In this paper, based on the result of Xi presented for the $λ$-calculus Xi, we give an upper bound for the lengths of the reduction sequences in the $λμ$-calculus extended with the $ρ$- and $θ$-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 $μ$-abstraction is able to consume an unbounded number of arguments by virtue of the $μ$-rule.

math.LO↗
arXiv2017

Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi

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.

math.LO↗
arXiv2014

About the range property for H

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.

math.LO↗
arXiv2009

Strong normalization results by translation

We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system.

math.LO↗
arXiv2009

Realisability Semantics for Intersection Types and Expansion Variables

Expansion was invented at the end of the 1970s for calculating principal typings for $λ$-terms in type systems with intersection types. Expansion variables (E-variables) were invented at the end of the 1990s to simplify and help mechanise expansion. Recently, E-variables have been further simplified and generalised to also allow calculating type operators other than just intersection. There has been much work on denotational semantics for type systems with intersection types, but none whatsoever before now on type systems with E-variables. Building a semantics for E-variables turns out to be challenging. To simplify the problem, we consider only E-variables, and not the corresponding operation of expansion. We develop a realisability semantics where each use of an E-variable in a type corresponds to an independent degree at which evaluation occurs in the $λ$-term that is assigned the type. In the $λ$-term being evaluated, the only interaction possible between portions at different degrees is that higher degree portions can be passed around but never applied to lower degree portions. We apply this semantics to two intersection type systems. We show these systems are sound, that completeness does not hold for the first system, and completeness holds for the second system when only one E-variable is allowed (although it can be used many times and nested). As far as we know, this is the first study of a denotational semantics of intersection type systems with E-variables (using realisability or any other approach).

math.LO↗
arXiv2009

Parametric mixed sequent calculus

In this paper, we present a propositional sequent calculus containing disjoint copies of classical and intuitionistic logics. We prove a cut-elimination theorem and we establish a relation between this system and linear logic.

math.LO↗
arXiv2009

A complete realisability semantics for intersection types and arbitrary expansion variables

Expansion was introduced at the end of the 1970s for calculating principal typings for $λ$-terms in intersection type systems. Expansion variables (E-variables) were introduced at the end of the 1990s to simplify and help mechanise expansion. Recently, E-variables have been further simplified and generalised to also allow calculating other type operators than just intersection. There has been much work on semantics for intersection type systems, but only one such work on intersection type systems with E-variables. That work established that building a semantics for E-variables is very challenging. Because it is unclear how to devise a space of meanings for E-variables, that work developed instead a space of meanings for types that is hierarchical in the sense of having many degrees (denoted by indexes). However, although the indexed calculus helped identify the serious problems of giving a semantics for expansion variables, the sound realisability semantics was only complete when one single E-variable is used and furthermore, the universal type $ω$ was not allowed. In this paper, we are able to overcome these challenges. We develop a realisability semantics where we allow an arbitrary (possibly infinite) number of expansion variables and where $ω$ is present. We show the soundness and completeness of our proposed semantics.

math.LO↗
arXiv2009

An arithmetical proof of the strong normalization for the $λ$-calculus with recursive equations on types

We give an arithmetical proof of the strong normalization of the $λ$-calculus (and also of the $λμ$-calculus) where the type system is the one of simple types with recursive equations on types. The proof using candidates of reducibility is an easy extension of the one without equations but this proof cannot be formalized in Peano arithmetic. The strength of the system needed for such a proof was not known. Our proof shows that it is not more than Peano arithmetic.

math.LO↗
arXiv2009

Arithmetical proofs of strong normalization results for the symmetric $λμ$-calculus

The symmetric $λμ$-calculus is the $λμ$-calculus introduced by Parigot in which the reduction rule $\m'$, which is the symmetric of $μ$, is added. We give arithmetical proofs of some strong normalization results for this calculus. We show (this is a new result) that the $μμ'$-reduction is strongly normalizing for the un-typed calculus. We also show the strong normalization of the $βμμ'$-reduction for the typed calculus: this was already known but the previous proofs use candidates of reducibility where the interpretation of a type was defined as the fix point of some increasing operator and thus, were highly non arithmetical.

math.LO↗
arXiv2009

On Storage Operators

In 1990 Krivine introduced the notion of storage operators. They are $λ$-terms which simulate call-by-value in the call-by-name strategy. Krivine has shown that there is a very simple type in the AF2 type system for storage operators using Gödel translation from classical to intuitionistic logic. Parigot and Krivine have shown that storage operators play an important tool in classical logic. In this paper, we present a synthesis of various results on this subject.

math.LO↗
arXiv2009

Classical Combinatory Logic

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 "`a 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.

math.LO↗
arXiv2009

Les types de données syntaxiques du système F

We give in this paper a purely syntactical definition of input and output types of system F. We define the syntactical data types as input and output types. We show that any type with positive quantifiers is a syntactical data type and that an input type is an output type. We give some restrictions on the $\forall$-elimination rule in order to prove that an output type is an input type.

math.LO↗