Coinduction is a proof rule which is the dual of induction. It allows reasoning about non-well-founded sets and is of particular use for reasoning about equivalences. In this thesis I present an automation of coinductive theorem proving. This automation is based on the ideas of proof planning [Bundy 88]. Proof planning as the name suggests, plans the higher level steps in a proof without performing the formal checking which is also required for a verification. The automation has focused on the use of coinduction to prove the equivalence of programs in a small lazy functional language which is similar to Haskell. One of the hardest parts in a coinductive proof is the choice of a relation, called a bisimulation. The automation here described makes an initial simplified guess at a bisimulation and then uses critics, revisions based on failure, and generalisation techniques to refine this guess. The proof plan for coinduction and the critic have been implemented in CLAM [Bundy et al 90b] with encouraging results. The planner has been successfully tested on a number of theorems. Comparison of the proof planner for coinduction with the proof plan for induction implemented in CLAM has gighlighted a number of equivalences and dualities in the process of these proofs and has also suggested improvements to both systems. This work has demonstrated not only the possibility of fully automated theorem provers for coinduction but has also demonstrated the uses of proof planning for comparison of proof techniques. This work has demonstrated not only the possibility of fully automated theorem provers for coinduction but has also demonstrated the uses of proof planning for comparison of proof techniques.

Some programs are not merely sets of batch instructions performed in isolation. They interact, either directly with the user, or with other threads and resources. This dissertation tackles the problem of mathematical description (denotational semantics) of the observable behaviour of such programs. In the tradition of denotational semantics and functional programming, one can distinguish between pure computations, which are regarded as mathematical functions, and effectful ones, like those generating behaviour. Both effects in general and behaviour of interactive systems have been thoroughly studied, and they both have elegant category-theoretic explanations: the frameworks of, respectively, monads and coalgebra. The point of this dissertation is to explore the area where the two meet. The thesis of this dissertation is that the right kind of monads to describe the observable behaviour of programs are completely iterative monads (cims), introduced by Elgot and more recently studied by Adamek and others. They are monads equipped with a certain corecursion scheme that allows us to describe the computation in a coinductive, step-wise manner. To support this, we introduce a formal coinductive semantics parametrised with a cim. We study its properties and show that it instantiates to a number of known approaches, based on metric spaces and final coalgebras. Then, we focus on studying properties of cims, especially those important in semantics and programming, like composability. We show that a number of constructions used in denotational semantics to model different aspects of behaviour are instances of the constructions that we introduce. The most important structure that we study are coinductive resumptions, generalising previous results by Moggi or Hyland, Plotkin, and Power. The language of our development is category-theoretic, and so are the properties that we investigate. We are interested in universal properties, distributive laws, algebras, and monadicity. Thus, the results apply not only to semantics and programming, but can be construed as a general investigation of algebraic structures with iteration.

Nous nous intéressons à la représentation de graphes dans le prouveur Coq. Nous avons choisi de les représenter par des types coinductifs dont nous voulions explorer l'utilisation. Ceux-ci permettent de rendre succincte et élégante la représentation et d'obtenir la navigabilité par construction. Nous avons dû contourner la condition de garde dont le but est d'assurer la validité des opérations effectuées sur les objets coinductifs. Son implantation dans Coq est restrictive et interdit parfois des définitions sémantiquement correctes. Une formalisation canonique des graphes dépasse ainsi l'expressivité directe de Coq. Nous avons donc proposé une solution respectant ces limitations, puis nous avons défini une relation sur les graphes nous permettant d'obtenir la même notion d'équivalence qu'avec une représentation classique tout en gardant les avantages de la coinduction. Nous montrons qu'elle est équivalente à une relation basée sur des observations finies.

Map Theory est une extension équationnelle du lambda-calcul non-typé conçue par Klaus Grue pour être une fondation commune de l'informatique et des mathématiques. Elle permet en particulier une interprétation complète du calcul des prédicats et de ZFC+FA, où ZFC est la théorie de Zermelo-Fraenkel, et FA est l'axiome de bonne fondation usuel. Toutes les notions primitives de la logique du premier ordre et de la théorie des ensembles, valeurs de vérité, connecteurs, quantificateurs, appartenance et égalité, y sont traduites par des termes du lambda-calcul enrichi de quelques constantes. De plus, Map Theory permet de représenter les types de données inductifs et de donner un sens calculatoire immédiat à tous les constructeurs ensemblistes usuels. La version initiale de Map Theory par K. Grue ne considère cependant que les ensembles (ou classes) bien-fondée relativement à la relation d'appartenance. Dans le cadre du renouveau d'intérêt pour l'antifondation induit par les developpements récents de l'informatique théorique, nous montrons dans notre thèse qu'il est possible d'élaborer une version antifondée de Map Theory qui prenne en compte l'existence des objets non-bien-fondés, et qui permette de raisonner sur ces objets par co-induction. Ce nouveau système ouvre la possibilité d'une représentation directe des types de données co-inductifs, et de la modèlisation des phènoménes et processus circulaires. Dans une première partie, nous présenterons l'axiomatisation MTA de ce nouveau système, et nous montrerons que ZFC+AFA, où AFA est l'axiome d'Antifondation de Aczel-Forti-Honsell, y est interprétable syntaxiquement. Dans la deuxième partie, nous montrerons la consistance de MTA relativement à ZFC+SI, où SI est l'axiome exprimant l'existence d'un cardinal fortement inaccessible.

Cette thèse s'articule autour de l'utilisation de stratégies totales pour la représentation des preuves. La première partie porte sur le cadre finitaire. L'analyse commence dans un univers syntaxique : on définit un lambda-calcul unaire fortement normalisant, pour lequel on rappelle la machine à pointeurs (PAM). On réduit le problème de préservation de la totalité par composition à un problème de finitude sur des objets appelés structures de pointeurs. On donne trois preuves différentes de ce résultat de finitude. La première se ramène via la PAM à la normalisation du lambda-calcul unaire, la seconde passe par l'extraction d'une réduction simple sur les arbres d'entiers et la troisième s'inspire d'un argument combinatoire de Coquand. La seconde partie traite d'un calcul de séquents mu-LJ équipé de définitions inductives et coinductives, dans lequel on donne une simulation du système T. On définit les catégories mu-fermées, formant une classe de modèles de mu-LJ. Dans le cadre des jeux on définit les arènes ouvertes, munies de variables de type libres. À chacune de ces arènes ouvertes est associé un foncteur ouvert sur la catégorie des stratégies innocentes. On décrit ensuite sur les arènes ouvertes une construction de boucle dont on montre qu'elle rejoint le modèle de McCusker des types récursifs. Les boucles sont alors enrichies par des conditions de gain inspirées des jeux de parité, ce qui équipe les foncteurs ouverts d'algèbres initiales et coalgèbres terminales et construit une catégorie mu-fermée. On propose finalement une extension de mu-LJ à une syntaxe infinie, pour laquelle le modèle est pleinement complet.

No description available.

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.

Le but de ce travail est de proposer un système formel pour prouver que l'ensemble des succès d'un programme logique est inclus dans l'ensemble correspondant d'un autre programme. Cela permet de prouver que deux programmes logiques, un qui représente la spécification et un représentant l'implantation sont équivalents. Le langage logique considéré est CLPforall qui est le langage le langage de programmation logique avec contraintes (CLP) auquel est ajouté le quantificateur universel. Nous présentons les sémantiques des succès finis et infinis et montrons qu'elles sont données par le plus petit et le plus grand point fixe du même opérateur. Un système de preuve pour l'inclusion des succès finis est présenté. Le système utilise pour les opérateurs et les quantificateurs logiques les mêmes règles que la logique du premier ordre. Pour raisonner sur les prédicats récursifs le système contient une règle d'induction. Nous prouvons la correction du système sous certains conditions. Un système analogue pour l'inclusion des succès infinis est présenté. La règle d'induction est remplacée par une règle de coinduction. La correction est démontrée sous conditions analogues. Les deux systèmes sont équivalents sous certains conditions. Une implantation a été réalisée sous la forme d'assistant de preuve écrit en Prolog. Le programme a environ 4000 lignes et contient des procédures simples mais efficaces de recherche de preuves. Nous présentons des exemples de preuves réalises avec ce programme parmi lesquels la preuve de correction de quicksort.

Nous proposons deux caractérisations des arbres réguliers. La première est sémantique et s'appuie sur les types co-inductifs. La seconde est syntaxique et repose sur une représentation des arbres réguliers par des termes cycliques. Nous prouvons que ces deux caractérisations sont isomorphes.Ensuite, nous étudions le problème de la définition de morphisme d'arbres préservant la propriété de régularité. Nous montrons en utilisant le formalisme des transducteurs d'arbres, l'existence d'un critère syntaxique garantissant la préservation de cette propriété. Enfin, nous considérons des applications de la théorie des arbres réguliers comme la définition de l'opérateur de composition parallèle d'une algèbre de processus ou encore, les problèmes de décidabilité sur les arbres réguliers via une mécanisation d'un vérificateur de modèles pour un mu-calcul coalgébrique. Tous les résultats ont été mécanisés et prouvés corrects dans l'assistant de preuve Coq. / We propose two characterizations of regular trees. The first one is semantic and is based on coinductive types. The second one is syntactic and represents regular trees by means of cyclic terms. We prove that both of these characterizations are isomorphic. Then, we study the problem of defining tree morphisms preserving the regularity property. We show, by using the formalism of tree transducers, the existence of syntactic criterion ensuring that this property is preserved. Finally, we consider applications of the theory of regular trees such as the definition of the parallel composition operator of a process algebra or, the decidability problems on regular trees through a mechanization of a model-checker for a coalgebraic mu-calculus. All the results were mechanized and proved correct in the Coq proof assistant.

Le document traite du raisonnement sur les processus. Les chapitres principaux sont: - Équivalences comportementales : caractérisation logique, axiomatisation et congruence - Inspections et équivalences intensionnelles - Calculs avec localités