• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 2
  • Tagged with
  • 2
  • 2
  • 2
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

λ-calcul différentiel et logique classique : interactions calculatoires

Vaux, Lionel 23 November 2007 (has links) (PDF)
Cette thèse de théorie de la démonstration étudie les interactions entre le λ-calcul différentiel d'Ehrhard et Regnier d'un côté, et certaines émanations calculatoires de la logique classique (le λμ-calcul de Parigot et le λ-barre-μ-calcul de Herbelin) de l'autre. L'étude est initiée et guidée par la décomposition de ces calculs dans des extensions de la logique linéaire de Girard.<br /><br />Dans une première partie, on définit un cadre commun pour ces extensions, dans le formalisme des réseaux d'interaction de Lafont, et on y rappelle des résultats de la littérature ou du folklore. On donne en particulier la traduction du λμ-calcul et du λ-barre-μ-calcul dans les réseaux polarisés de Laurent et celle du fragment finitaire du λ-calcul différentiel dans les réseaux différentiels d'Ehrhard et Regnier.<br /><br />Dans la deuxième partie, on introduit les réseaux différentiels polarisés (RDP), comme l'extension par une polarisation à la Laurent des réseaux différentiels. La pertinence des règles de réduction nouvelles est soulignée par l'étude d'un modèle dénotationnel commun aux réseaux différentiels et aux réseaux polarisés.<br /><br />Enfin, on présente trois calculs de termes, chacun pouvant être considéré comme une lecture en arrière de tout ou partie des interactions définies par les RDP : un λμ-calcul différentiel, qui correspond à la réunion des réseaux différentiels et des réseaux polarisés ; un λ-barre-μ-calcul avec produit de convolution sur les piles, qui fait intervenir la structure de bigèbre des types polarisés introduite dans les RDP, mais pas la dérivée ; enfin, un λ-barre-μ-calcul différentiel qui développe toute l'expressivité des RDP.
2

Une étude combinatoire du lambda-calcul avec ressources uniforme / A combinatory study of uniforme resource lambda-calculus

Midez, Jean baptiste 15 December 2014 (has links)
Le lambda-calcul avec ressources est une variante du lambda-calcul fondée sur la linéarité : les lambda-termes avec ressources sont aux lambda-termes ce que sont les polynômes aux fonctions réelles, c'est à dire des approximations multi-linéaires. En particulier les réductions dans le lambda-calcul avec ressources peuvent être vues comme des approximations des beta-réductions, mais la contrainte de linéarite a des conséquences importantes, notamment la forte normalisation de la réduction avec ressources. Pour ainsi dire, la beta-réduction est obtenue par passage à la limite des réductions avec ressources qui l'approximent. Cette thèse étudie les aspects combinatoires, très riches, du lambda-calcul avec ressources. On commence par définir précisément la notion de réduction avec ressource associée à une beta-réduction: étant donné un lambda-terme $t$, un approximant $s$ de celui-ci et $t'$ une beta-réduction de $t$, on lui associe une réduction avec ressources (appelée gamma-réduction) de $s$ qui réduit les «mêmes» redex que celle de $t$ et produit un ensemble $S'$ d'approximants de $t'$. Cette définition permet de retrouver une preuve légèrement plus intuitive de l'un des théorèmes fondamentaux de la théorie, qui permet également de le généraliser. Dans un second temps on étudie les relations «familiales» entre termes avec ressources, la question centrale étant de caractériser le fait que deux termes avec ressources sont des réduits d'un même terme. Ce problème central et difficile n'est pas pleinement résolu, mais la thèse présente plusieurs résultats préliminaires et développe les bases d'une théorie pour arriver à cette fin. / The resource lambda-calculus is a variant of lambda-calculus based on linearity: resource lambda-terms are to lambda-terms as polynomials are to real functions. In particular reductions in resource lambda-calculus can be viewed as approximations of beta-reductions. But the linearity constraint has important consequences, especially the strong normalisation of resource reduction. So to speak, beta-reduction is obtained by passage to the limit of resource reduction which approximates it. This thesis is a study of the combinatory aspect of resource lambda-calculus. First, we define precisely the notion of resource reduction associated to beta-reduction: let t be a lambda-term, s an approximant of t and t' a beta-reduction of t, we associate a resource reduction (called gamma-reduction) of s which reducts the "same" redex as the beta-reduction of t and this generates a set S' of approximants of t'. This definition allows to find a new proof (who is more intuitive) of one of the fundamental theorems of this theory and it also allows to generalize it. Then we study the "family" relations between resource lambda-terms. The main question is to characterize the resource lambda-terms which are reducts of same term. This central problem is hard and not completely resolved, but this thesis exhibits several preliminary results and lays the foundations of a theory aimed at resolving it.

Page generated in 0.1266 seconds