On étudie dans cette thèse une structure de semi-anneau dont le produit est basé sur la règle de résolution de la programmation logique. Cet objet mathématique a été initialement introduit dans le but de modéliser la procédure d'élimination des coupures de la logique linéaire, dans le cadre du programme de géométrie de l'interaction. Il fournit un cadre algébrique et abstrait, tout en étant présenté sous une forme syntaxique et concrète, dans lequel mener une étude théorique du calcul. On reviendra dans un premier temps sur l'interprétation interactive de la théorie de la démonstration dans ce semi-anneau, via l'axiomatisation catégorique de l'approche de la géométrie de l'interaction. Cette interprétation établit une traduction des programmes fonctionnels vers une forme très simple de programmes logiques. Dans un deuxième temps, on abordera des problématiques de théorie de la complexité: bien que le problème de la nilpotence dans le semi-anneau étudié soit indécidable en général, on fera apparaître des restrictions qui permettent de caractériser le calcul en espace logarithmique (déterministe et non-déterministe) et en temps polynomial (déterministe). / We study in this thesis a semiring structure with a product based on the resolution rule of logic programming. This mathematical object was introduced initially in the setting of the geometry of interaction program in order to model the cut-elimination procedure of linear logic. It provides us with an algebraic and abstract setting, while being presented in a syntactic and concrete way, in which a theoretical study of computation can be carried on. We will review first the interactive interpretation of proof theory within this semiring via the categorical axiomatization of the geometry of interaction approach. This interpretation establishes a way to translate functional programs into a very simple form of logic programs. Secondly, complexity theory problematics will be considered: while the nilpotency problem in the semiring we study is undecidable in general, it will appear that certain restrictions allow for characterizations of (deterministic and non-deterministic) logarithmic space and (deterministic) polynomial time computation.

Cette thèse est une étude de la géométrie de l'interaction dans le facteur hyperfini (GdI5), introduite par Jean-Yves Girard, et de ses liens avec les constructions plus anciennes. Nous commençons par montrer comment obtenir des adjonctions purement géométriques comme une identité entre des ensembles de cycles apparaissant entre des graphes. Il est alors possible, en choisissant une fonction qui mesure les cycles, d'obtenir une adjonction numérique. Nous montrons ensuite comment construire, sur la base d'une adjonction numérique, une géométrie de l'interaction pour la logique linéaire multiplicative additive où les preuves sont interprétées par des graphes. Nous expliquons également comment cette construction permet de définir une sémantique dénotationnelle de MALL, et une notion de vérité. Nous étudions finalement une généralisation de ce cadre afin d'interpréter les exponentielles et le second ordre. Les constructions sur les graphes étant paramétrées par une fonction de mesure des cycles, nous entreprenons ensuite l'étude de deux cas particuliers. Le premier s'avère être une version combinatoire de la GdI5, et nous obtenons donc une interprétation géométrique de l'orthogonalité basée sur le déterminant de Fuglede-Kadison. Le second cas particulier est une version combinatoire des constructions plus anciennes de la géométrie de l'interaction, où l'orthogonalité est basée sur la nilpotence. Ceci permet donc de comprendre le lien entre les différentes versions de la géométrie de l'interaction, et d'en déduire que les deux adjonctions — qui semblent à première vue si différentes — sont des conséquences d'une même identité géométrique. / This work is a study of the geometry of interaction in the hyperfinite factor introduced by Jean-Yves Girard, and of its relations with ancient constructions. We start by showing how to obtain purely geometrical adjunctions as an identity between sets of cycles appearing between graphs. It is then possible, by chosing a function that measures those cycles, to obtain a numerical adjunction. We then show how to construct, on the basis of such a numerical adjunction, a geometry of interaction for multiplicative additive linear logic where proofs are interpreted as graphs. We also explain how to define from this construction a denotational semantics for MALL, and a notion of truth. We extend this setting in order to deal with exponential connectives and show a full soundness result for a variant of elementary linear logic (ELL). Since the constructions on graphs we define are parametrized by a function that measures cycles, we then focus our study to two particular cases. The first case turns out to be a combinatorial version of GoI5, and we thus obtain a geometrical caracterisation of its orthogonality which is based on Fuglede-Kadison determinant. The second particular case we study will giveus a refined version of older constructions of geometry of interaction, where orthogonality is based on nilpotency. This allows us to show how these two versions of GoI, which seem quite different, are related and understand that the respective adjunctions are both consequences of a unique geometrical property. In the last part, we study the notion of subjective truth.