Models and Theories of Lambda calculus
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
In this thesis, we show that every categorical model of lambda calculus can be viewed as a lambda model, also if the ccc has not enough points and we give sufficient conditions for a categorical model living in a cpo-enriched ccc for having H* as equational theory. We build a categorical model living in a relational semantics and satisfying these conditions. We show that the associated lambda-model satisfies some algebraic properties which make it suitable for modeling a non-deterministic lambda-calculus. We show that combinatory algebras satisfy a generalization of Stone's Representation Theorem. We study the semantics of lambda-calculus whose models are indecomposable; we prove that this semantics is general enough to include the main semantics and the term models of ail semi-sensible theories. We also show that it is largely incomplete. We investigate the question of the existence of a non-syntactical model living in the main semantics and having an r. E. Equational or inequational theory. We introduce an adequate notion of effective models, and we prove that the inequational theory of an effective model is never r. E. ; as a consequence we get that its equational theory cannot be lambda-beta or lambda-beta-eta. We also show that the equational theory of an effective model living in the stable or strongly stable semantics is never r. E. We prove that the inequational theory of a graph model is never r. E. And that there are many effective graph models whose equational theory is never r. E.
Abstract FR:
Dans cette thèse, on montre que tout modèle catégorique du lambda-calcul peut être vu comme un lambda-modèle, même si la ccc sous-jacente n'a pas assez de points, et on donne des conditions suffisantes pour qu'un modèle catégorique vivant dans une ccc cpo-enriched arbitraire ait H* pour théorie équationnelle. On construit un modèle catégorique qui vit dans une sémantique relationnelle et qui satisfait ces conditions. On montre que le lambda-modèle associé possède des propriétés algébriques qui le rendent apte à modéliser un lambda-calcul non-déterministe. On montre que les algèbres combinatoires satisfont une généralisation du Théorème de Représentation de Stone. On étudie la sémantique du lambda-calcul dont les modèles sont indécomposable; on prouve en particulier que cette sémantique est assez générale pour inclure les sémantiques principales et les modèles des termes de toutes les théories semi-sensibles. On montre aussi qu'elle est largement incomplète. On étudie la question de l'existence d'un modèle non-syntaxique appartenant aux sémantiques principales et ayant une théorie équationnelle ou inéquationnelle r. E. On introduit une notion adéquate de modèles effectifs, et on prouve que la théorie inéquationnelle d'un modèle effectif n'est jamais r. E. ; en conséquence sa théorie équationnelle ne peut pas être lambda-bêta ou lambda-beta-eta. On montre aussi que la théorie équationnelle d'un modèle effectif vivant dans la sémantique stable ou fortement stable n'est jamais r. E. On démontre que la théorie inéquationnelle d'un modèle de graphe n'est jamais r. E. Et qu'il existe beaucoup de modèles de graphes effectifs qui ont une théorie équationnelle qui n'est pas r. E.