Thèse de doctorat : Informatique : INPL : 2007. / Titre provenant de l'écran-titre.

Th.--Informatique--Paris 7, 1987. / 1988 d'après la déclaration de dépôt légal. Bibliogr. p. 233-237. Index. Résumé en français.

Thèse de doctorat : Informatique : Vandoeuvre-les-Nancy, INPL : 2005. / Titre provenant de l'écran-titre. Bibliogr.

Thèse de doctorat : Informatique : Nancy 1 : 2008. / Titre provenant de l'écran-titre.

Thèse doctorat : Informatique : Nancy 1 : 2007. / Titre provenant de l'écran-titre.

Thèse de 3e cycle : Informatique : Lille 1 : 1998. / Résumé en français et en anglais. Bibliogr. p. 103-112.

Cette thèse étudie la construction automatique de représentations sémantiques comme lambda-termes simplement typés. Nous introduisons la sémantique formelle et computationnelle et présentons une tentative de construction sémantique à l'aide d'outils d'inférence. <br />Nous expliquons les limites de cette approche et en proposons une autre, basée sur un outil appelé Nessie. Cet outil construit des représentations sémantiques grâce à un lexique spécifiant le sens des mots et à un arbre guidant la construction. L'implantation de l'outil est présentée et ses résultats sont comparés à ceux du système évoqué plus haut. Nous appliquons ensuite Nessie à deux tâches différentes.<br />D'abord, nous montrons comment il peut être utilisé (avec des outils d'inférence) pour étudier la sémantique du temps et de l'aspect des verbes polonais. Ensuite, nous présentons deux approches de la construction compositionnelle du sens de discours basées sur la théorie des types. Nous montrons que Nessie peut être utilisé pour calculer des représentations de discours dans ces deux formalismes; cette double implantation permet de souligner les points forts et les points faibles de chacune et de les comparer. Enfin, nous prouvons que notre approche de la construction sémantique est compatible avec une large gamme de formalismes syntaxiques: ceux reconnus par une grammaire catégorielle abstraite d'ordre 2. Une conséquence de cette caractérisation est que Nessie peut gérer une large gamme de grammaires inversibles et peut donc, théoriquement, être utilisé aussi bien en génération qu'en analyse. <br />Nous concluons en discutant de la pertinence du lambda calcul simplement<br />typé pour la sémantique des langues naturelles.

Le calcul de réécriture ou rho-calcul est une généralisation du lambda-calcul avec filtrage et agrégation de termes. L'abstraction sur les variables est étendue à une abstraction sur les motifs et le filtrage correspondant peut être effectué modulo une théorie <br />équationnelle a priori arbitraire. L'agrégation est utilisée pour collecter les différents résultats possibles.<br />Dans cette thèse, nous étudions différentes combinaisons des ingrédients fondamentaux du rho-calcul: le filtrage, l'agrégation et les mécanismes d'ordre supérieur.<br />Nous étudions le filtrage d'ordre supérieur dans le lambda-calcul pur modulo une restriction de la beta-conversion appelée super-développements. Cette nouvelle approche est suffisamment expressive pour traiter les problèmes de filtrage du second-ordre et ceux avec des motifs d'ordre supérieur à la Miller.<br />Nous examinons ensuite les modèles catégoriques du<br />lambda-calcul parallèle qui peut être vu comme un enrichissement du lambda-calcul avec l'agrégation de termes. Nous montrons que ceci est une étape significative vers la sémantique dénotationnelle du calcul de réécriture.<br />Nous proposons également une étude et une comparaison des calculs avec motifs éventuellement dynamiques, c'est-à-dire qui peuvent être instanciés et réduits. Nous montrons que cette étude, et plus particulièrement la preuve de confluence, est suffisamment générale pour<br />s'appliquer à l'ensemble des calculs connus. Nous étudions ensuite l'implémentation de tels calculs en proposant un calcul de réécriture avec filtrage et substitutions explicites.

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.

Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela signifie que pour mettre un ensemble Delta de formules en hypothèse, il est requis de donner une substitution sigma telle que les instances de formules sigma(Delta) soient démontrables. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet peut être construit. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version radicale de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondant: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans ce rapport une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple / Pedagogical formal systems have appeared recently for propositional calculus (up to the higher order), and it consists of systematically give examples of introduced notions (hypotheses). Formally, it means that to use a set Delta of formulas as hypotheses, one must first give a substitution sigma such that all the instances of formulas sigma(Delta) can be proved. This neccesity of giving examples has been pointed out by Poincaré (1913) as a common-sense practice: a definition of an object by means of assumptions has interest only if such an object can be constructed. This restriction applied to intuitionistic formal systems is consistent with the idea of negationless mathematics advocated by Griss (1946) in the middle of the past century, and shown as a more radical view of intuitionism. Through the Curry-Howard isomorphism (1980), the computational counterpart is the utility of programs defined in the associated functional systems: every function can be applied to a closed value. First results concerning propositional calculi up to the second-order has recently been published by Colson and Michel (2007, 2008, 2009). In this thesis we present an attempt to standardize and to extend to the Calculus of Constructions (CC) those previous results. First a formal and precise definition of pedagogical sub-systems of the Calculus of Constructions is introduced, and different such sub-systems are exhibited as examples