Searcharxiv⌕ Search

arXiv subjects

Karim Nour

Publications and source records attributed to Karim Nour.

At least 37 records · Page 2Linked to original sources
arXiv2009

A conjecture on numeral systems

A numeral system is an infinite sequence of different closed normal $λ$-terms intended to code the integers in $λ$-calculus. H. Barendregt has shown that if we can represent, for a numeral system, the functions : Successor, Predecessor, and Zero Test, then all total recursive functions can be represented. In this paper we prove the independancy of these particular three functions. We give at the end a conjecture on the number of unary functions necessary to represent all total recursive functions.

math.LO↗
arXiv2009

Arithmetical proofs of strong normalization results for symmetric lambda calculi

We give arithmetical proofs of the strong normalization of two symmetric $λ$-calculi corresponding to classical logic. The first one is the $\barλμ\tildeμ$-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value". The second one is the symmetric $λμ$-calculus. It is the $λμ$-calculus introduced by Parigot in which the reduction rule $μ'$, which is the symmetric of $μ$, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.

math.LO↗
arXiv2009

S-storage operators

In 1990, J.L. Krivine introduced the notion of storage operator to simulate, for Church integers, the "call by value" in a context of a "call by name" strategy. In this present paper, we define, for every $λ$-term S which realizes the successor function on Church integers, the notion of S-storage operator. We prove that every storage operator is a $S-storage operator. But the converse is not always true.

math.LO↗
arXiv2009

Mixed Logic and Storage Operators

In 1990 J-L. Krivine introduced the notion of storage operators. They are $λ$-terms which simulate call-by-value in the call-by-name strategy and they can be used in order to modelize assignment instructions. J-L. Krivine has shown that there is a very simple second order type in AF2 type system for storage operators using Gödel translation of classical to intuitionistic logic. In order to modelize the control operators, J-L. Krivine has extended the system AF2 to the classical logic. In his system the property of the unicity of integers representation is lost, but he has shown that storage operators typable in the system AF2 can be used to find the values of classical integers. In this paper, we present a new classical type system based on a logical system called mixed logic. We prove that in this system we can characterize, by types, the storage operators and the control operators. We present also a similar result in the M. Parigot's $λμ$-calculus.

math.LO↗
arXiv2009

A General Type for Storage Operators

In 1990, J.L. Krivine introduced the notion of storage operator to simulate, in $λ$-calculus, the "call by value" in a context of a "call by name". J.L. Krivine has shown that, using Gödel translation from classical into intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In this present paper, we give a general type for storage operators in a slight extension of AF2. We give at the end (without proof) a generalization of this result to other types.

math.LO↗
arXiv2009

Storage operators and forall-positive types of system TTR

In 1990, J.L. Krivine introduced the notion of storage operator to simulate "call by value" in the "call by name" strategy. J.L. Krivine has shown that, using Gödel translation of classical into intuitionitic logic, we can find a simple type for the storage operators in AF2 type system. This paper studies the $\forall$-positive types (the universal second order quantifier appears positively in these types), and the Gödel transformations (a generalization of classical Gödel translation) of TTR type system. We generalize, by using syntaxical methods, the J.L. Krivine's Theorem about these types and for these transformations. We give a proof of this result in the case of the type of recursive integers.

math.LO↗
arXiv2009

An example of a non adequate numeral system

A numeral system is defined by three closed $λ$-terms : a normal $λ$-term $d_0$ for Zero, a $λ$-term $S_d$ for Successor, and a $λ$-term for Zero Test, such that the $λ$-terms $({S_d}^{i} ~ d_0)$ are normalizable and have different normal forms. A numeral system is said adequate iff it has a closed $λ$-term for Predecessor. This Note gives a simple example of a non adequate numeral system.

math.LO↗
arXiv2009

La Valeur d'un Entier Classique en $λμ$-Calcul

In this paper, we present three methods to give the value of a classical integer in $λμ$-calculus. The first method is an external method and gives the value and the false part of a normal classical integer. The second method uses a new reduction rule and gives as result the corresponding Church integer. The third method is the M. Parigot's method which uses the J.L. Krivine's storage operators.

math.LO↗
arXiv2009

Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés

A numeral system is a sequence of an infinite different closed normal $λ$-terms which has closed $λ$-terms for successor and zero test. A numeral system is said adequate iff it has a closed $λ$-term for predecessor. A storage operator for a numeral system is a closed $λ$-term which simulate "call-by-value" in the context of a "call-by-name" strategy. E. Tronci conjectured the following result : a numeral system is adequate if it has a storage operator. This paper gives a negative answer to this conjecture for the numeral systems typable in the J.-Y. Girard type system F. The E. Tronci's conjecture remains open in pure $λ$-calculus.

math.LO↗
arXiv2009

Résultats de complétude pour des classes de types du système AF2

J.-L. Krivine introduced the AF2 type system in order to obtain programs ($λ$-terms) which calculate functions, by writing demonstrations of their totalities. We present in this paper two results of completness for some types of AF2 and for many notions of reductions. These results generalize a theorem of R. Labib-Sami established in the system F of J.-Y. Girard.

math.LO↗
arXiv2009

A completeness result for a realisability semantics for an intersection type system

In this paper we consider a type system with a universal type $ω$ where any term (whether open or closed, $β$-normalising or not) has type $ω$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $λ$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (based on weak head reduction and normal $β$-reduction) we obtain the same interpretation for types. Since the presence of $ω$ prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class ${\mathbb U}^+$ of the so-called positive types (where $ω$ can only occur at specific positions). We show that if a term inhabits a positive type, then this term is $β$-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for ${\mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${\mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${\mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties.

math.LO↗
arXiv2009

A completeness result for the simply typed $λμ$-calculus

In this paper, we define a realizability semantics for the simply typed $λμ$-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. This result serves to give characterizations of the computational behavior of some closed typed terms. We also prove a completeness result of our realizability semantics using a particular term model.

math.LO↗
arXiv2009

Propositional Mixed Logic: Its Syntax and Semantics

In this paper, we present a propositional logic (called mixed logic) containing disjoint copies of minimal, intuitionistic and classical logics. We prove a completeness theorem for this logic with respect to a Kripke semantics. We establish some relations between mixed logic and minimal, intuitionistic and classical logics. We present at the end a sequent calculus version for this logic.

math.LO↗