L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte. / The objective of this thesis is to develop a type theory for the linear-algebraic λ-calculus, an extension of λ-calculus motivated by quantum computing. This algebraic extension encompass all the terms of λ-calculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.

L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte.

Avec les espaces de finitude, Ehrhard a exhibé une sémantique de la logique linéaire contenant une opération de différentiation. Dans ce cadre, l'interprétation des formules est décomposable en séries de Taylor. Cette étude a engendré des syntaxes différentielles. Cette thèse de sémantique dénotationnelle prolonge ce travail par une exploration de sémantiques vectorielles de la logique linéaire, et contribue à l'étude sémantique et syntaxique de la formule de Taylor. La première partie aborde la sémantique. Nous présentons l'interprétation des constructions de la logique linéaire dans les espaces vectoriels munis d'une topologie linéarisée, les espaces de Lefschetz. Nous définissons une notion intrinsèque d'espaces de finitude, les espaces de Lefschetz finitaires. Nous caractérisons les espaces de Lefschetz réflexifs complets à l'aide de bornologies linéaires. Enfin, nous montrons que la décomposition de Taylor reste valide dans ces espaces. La seconde partie porte sur les syntaxes différentielles. La formule de Taylor syntaxique traduit un terme en une superposition de termes différentiels qui sont autant de possibilités d'exécutions. Comme l'ont montré Ehrhard et Regnier, les termes issus de cette traduction vérifient une relation de cohérence. Nous introduisons une sémantique totale qui capture cette relation. Puis, nous construisons une extension vectorielle du lambda-calcul, le calcul barycentrique, interprété par cette sémantique totale. Enfin, dans le cadre des réseaux différentiels, nous présentons un algorithme non déterministe qui permet de décider si un ensemble fini de réseaux différentiels provient de la traduction d'un réseau de la logique linéaire par la formule de Taylor syntaxique.

La thèse montre que les contraintes temporelles du fonctionnement didactique induisent des apprentissages invisibles à l'enseignant. Ces apprentissages n'assurent pas la progression didactique, mais ils jouent un rôle important dans la réussite des élèves. <br />Leur existence est établie par l'observation d'épisodes didactiques au moyen de techniques d'approche biographique originales. La méthode est appliquée à l'observation des difficultés des élèves avec le calcul algébrique au Lycée, et à leur explication.

Cette thèse s’intéresse à l’élaboration d’alternatives pour l’enseignement du calcul algébrique au collège et en particulier de la propriété de distributivité qui joue un rôle central.En appui sur des recherches antérieures en didactique de l’algèbre, nous analysons les spécificités des savoirs à enseigner et enseignés sur le calcul algébrique, au regard de difficultés protomathématiques (Chevallard 1985) prégnantes du côté des élèves. Ceci conduit à appréhender de nouvelles formes de savoirs à enseigner accompagnant les savoirs mathématiques liés aux aspects sémantiques et syntaxiques des écritures symboliques algébriques. La notion de transformation de mouvement (Drouhard 1992) et l’exploration des caractères formalisateur, unificateur et généralisateur (ou FUG, Robert 1998) amène à envisager la distributivité au regard d’un domaine d’étude plus large, à la fois numérique et algébrique. L’étude d’une transposition possible des savoirs à enseigner permet de dégager des conditions et des contraintes pour élaborer une ingénierie didactique. Les résultats d’une expérimentation en classe de 5e (élèves de 12-13 ans) à partir d’analyses a priori et a posteriori, concernent les discours dont les élèves parviennent à s’emparer, justifiant et soutenant leurs techniques de calcul, ainsi que les organisations de connaissances qui émergent. Une nouvelle étude didactique et épistémologique relative à la notion de substitution vient clore la thèse afin de déterminer en quoi elle pourrait fonder un prolongement possible aux enjeux FUG pour l’enseignement de la distributivité et poursuivre l’ingénierie didactique amorcée visant à enseigner le calcul algébrique tout au long du collège. / This thesis seeks to explore alternatives for the teaching of algabraic calculus in second grade, and more specifically of the distributive law that plays a central role.Drawing on prior researches on didactic of algebra, characteristics of the knowledge to be taught and the knowledge taught about algebraic calculus are analyzed towards protomathematics difficulties (Chevallard 1985) constantly arising in students’work. This leads to consider new forms of knowledge, along with mathematical knowledge, that would be linked to semantic and syntactic aspects of symbolic algebraic expressions.Exploring the notion of movement transformation (Drouhard 1992) and the potential of formalizing, unifying, and generalizing (or FUG, Robert 1998), brings out the distributive law in a larger study field both numerical and algebraic.The study of a possible transposition of the knowledge to be taught yields a set of conditions and constraints to design a didactic situation. The results from a first experiment in a 5th grade class (12-13 year-olds) are based on a priori and a posteriori analysis. They focus on the discourses built and used by the students, justifying and supporting their manipulations, along with the knowledge organizations arising out.The last chapter addresses a new didactic and epistemological study of the notion of substitution aiming at discussing its potential to extend the FUG point of view on the teaching of the distributive property, and further on to provide a new perspective of research to carry on with our didactic design to teach algebraic calculus all along secondary school.

Cette thèse porte sur les propriétés opérationnelles de deux extensions quantitatives du λ-calcul pur : le λ-calcul algébrique et le λ-calcul probabiliste.Dans la première partie, nous étudions la théorie de la β-réduction dans le λ-calcul algébrique. Ce calcul permet la formation de combinaisons linéaires finies de λ-termes. Bien que le système obtenu jouisse de la propriété de Church-Rosser, la relation de réduction devient triviale en présence de coefficients négatifs, ce qui la rend impropre à définir une notion de forme normale. Nous proposons une solution qui permet la définition d'une relation d'équivalence sur les termes, partielle mais cohérente. Nous introduisons une variante de la β-réduction, restreinte aux termes canoniques, dont nous montrons qu'elle caractérise en partie la notion de forme normale précédemment établie, démontrant au passage un théorème de factorisation.Dans la seconde partie, nous étudions la bisimulation et l'équivalence contextuelle dans un λ-calcul muni d'un choix probabliste. Nous donnons une technique pour établir que la bisimilarité applicative probabiliste est une congruence. Bien que notre méthode soit adaptée de celle de Howe, certains points techniques sont assez différents, et s'appuient sur des propriétés non triviales de « désintrication » sur les ensembles de nombres réels. Nous démontrons finalement que, bien que la bisimilarité soit en général strictement plus fine que l'équivalence contextuelle, elles coïncident sur les λ-termes purs. L'égalité correspondante est celle induite par les arbres de Lévy-Longo, généralement considérés comme l'équivalence extensionnelle la plus fine pour les λ-termes en évaluation paresseuse. / In this thesis we deal with the operational behaviours of two quantitative extensions of pure λ-calculus, namely the algebraic λ-calculus and the probabilistic λ-calculus.In the first part, we study the β-reduction theory of the algebraic λ-calculus, a calculus allowing formal finite linear combinations of λ-terms to be expressed. Although the system enjoys the Church-Rosser property, reduction collapses in presence of negative coefficients. We exhibit a solution to the consequent loss of the notion of (unique) normal form, allowing the definition of a partial, but consistent, term equivalence. We then introduce a variant of β-reduction defined on canonical terms only, which we show partially characterises the previously established notion of normal form. In the process, we prove a factorisation theorem.In the second part, we study bisimulation and context equivalence in a λ-calculus endowed with a probabilistic choice. We show a technique for proving congruence of probabilistic applicative bisimilarity. While the technique follows Howe's method, some of the technicalities are quite different, relying on non-trivial "disentangling" properties for sets of real numbers. Finally we show that, while bisimilarity is in general strictly finer than context equivalence, coincidence between the two relations is achieved on pure λ-terms. The resulting equality is that induced by Lévy-Longo trees, generally accepted as the finest extensional equivalence on pure λ-terms under a lazy regime.

Les Logiciels Tuteurs Fermés, ou LTF, sont utilisés dans les classes dans de nombreux collèges en mathématiques. Pour analyser leur place potentielle dans l'École, nous avons construit un modèle centré sur la notion d'institution, centrale dans la Théorie Anthropologique du Didactique, définie, par nous, à partir des critères suivants : la réalité sociale, la légitimité, la stabilité et la spécificité. Pour comprendre si un LTF peut être utilisé en tant qu'institution d'enseignement et d'apprentissage, chacun des quatre logiciels de notre étude a été inspecté entièrement par un expert dont les captures vidéos nous ont permis des comparaisons avec le travail des élèves de notre expérimentation. Le décryptage de l'ensemble de ces données a été conduit grâce à un logiciel d'analyse du comportement, The Observer de chez Noldus. Plus spécifiquement, en ce qui concerne l'apprentissage des mathématiques, nous avons choisi d'analyser la façon dont les quatre LTF proposent un apprentissage du calcul, qu'il soit arithmétique, numérique ou algébrique. Nous avons pour cela étendu au numérique le cadre théorique conçu par Houdement et Kuzniak pour l'apprentissage de la géométrie, et notamment les notions de paradigme et d'espace de travail. Les analyses que nous avons conduites nous ont permis de montrer que les LTF de notre étude ne peuvent que difficilement être utilisés en tant qu'institution autonome de l'institution principale qu'est la classe ordinaire. Mais leur usage peut être valorisé pour l'apprentissage des élèves en créant des institutions parallèles adaptées.