To see the other types of publications on this topic, follow the link: Lambda calculi.
Dissertations / Theses on the topic 'Lambda calculi'
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the top 50 dissertations / theses for your research on the topic 'Lambda calculi.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Browse dissertations / theses on a wide variety of disciplines and organise your bibliography correctly.
1
Yang, Liqun. "Logical relation categories and lambda calculi." Thesis, University of Ottawa (Canada), 1996. http://hdl.handle.net/10393/9876.
Full textAbstract:
An aspect of programming languages is the study of the operational semantics, which, in the case of a lambda calculus, is based on a directed form of equational reasoning called reduction. In computer science terminology, reduction may be regarded as a form of symbolic evaluation. It models a sequential computation process step by step. The crucial properties for a rewriting system are confluence, also called the Church-Rosser property and termination, the (Strong) normalization property, respectively. These are studied in depth in Chapter 2 and 6. The problem whether all $\lambda$-terms satisfy termination corresponds to the halting problem. From a different point of view, studying the problem of both Church-Rosser and strong normalization corresponds to, in a particular field, studying the word problem. The notion of categories is familiar to mathematicians as a branch of algebra. It has been developed quite rapidly in less than 40 years. In particular, recently more and more computer scientists are using categories for their own purposes. It is the connection between categories and $\lambda$-calculi that interests computer scientists. This connection is a thread that goes through the whole thesis. (Abstract shortened by UMI.)
2
Madiot, Jean-Marie. "Higher-order languages : dualities and bisimulation enhancements." Thesis, Lyon, École normale supérieure, 2015. http://www.theses.fr/2015ENSL0988/document.
Full textAbstract:
Les comportements des processus concurrents peuvent être exprimés en utilisant des calculs de processus, des langages formels simples qui permettent de démontrer des résultats mathématiques précis sur les interactions entre processus. Un exemple très simple est CCS, un autre exemple est le pi-calcul, plus expressif grâce à un mécanisme de communication de canaux. Dans ce dernier, on peut instaurer un système de types (pour raffiner l'analyse aux environnements plus contraints) et encoder le lambda-calcul (qui représente les calculs séquentiels).Certains de ces calculs, comme CCS ou des variantes du pi-calcul comme les calculs de fusions, ont une certaine propriété de symétrie. On utilise dans un premier temps cette symétrie comme un outil, pour prouver que deux encodages du lambda-calcul dans le pi-calcul sont en fait équivalents.Cette preuve nécessitant un système de types et une forme de symétrie, on se pose la question de l'existence d'un système de types pour les autres calculs symétriques, notamment les calculs de fusion, à laquelle on répond par la négative avec un théorème d'impossibilité.En analysant ce théorème, on découvre un contrainte fondamentale de ces calculs qui empêche l'utilisation des types, à savoir la présence d'une notion de relation d'équivalence entre les canaux de communication. Le relâchement de cette contrainte pour obtenir une relation de pré-ordre engendre un calcul intéressant qui recouvre des notions importantes du pi-calcul, absentes dans les calculs de fusion : les types et les noms privés. La première partie de la thèse se concentre sur l'étude de ce calcul.La deuxième partie de la thèse se concentre sur la bisimulation, une méthode pour établir l'équivalence de deux agents dans des langages d'ordre supérieur, par exemple le pi-calcul ou le lambda-calcul. Une amélioration de cette méthode est la théorie des techniques modulo, très puissante, mais qui malheureusement s'applique uniquement aux systèmes de premier ordre, comme les automates ou CCS.Cette thèse s'applique alors à décrire les langages d'ordre supérieur en tant que systèmes du premier ordre. On récupère ainsi la théorie générale des techniques modulo pour ces langages, en prouvant correctes la correspondance induite et les techniques spécifiques à chaque langage. On détaille les tenants et aboutissants de cette approche, pour fournir les outils nécessaires à son utilisation pour d'autres langages d'ordre supérieurThe behaviours of concurrent processes can be expressed using process calculi, which are simple formal languages that let us establish precise mathematical results on the behaviours and interactions between processes. A very simple example is CCS, another one is the pi-calculus, which is more expressive thanks to a name-passing mechanism. The pi-calculus supports the addition of type systems (to refine the analysis to more subtle environments) and the encoding of the lambda-calculus (which represents sequential computations).Some of these calculi, like CCS or variants of the pi-calculus such as fusion calculi, enjoy a property of symmetry. First, we use this symmetry as a tool to prove that two encodings of the lambda-calculus in the pi-calculus are in fact equivalent.This proof using a type system and a form of symmetry, we wonder if other existing symmetric calculi can support the addition of type systems. We answer negatively to this question with an impossibility theorem.Investigating this theorem leads us to a fundamental constraint of these calculi that forbids types: they induce an equivalence relation on names. Relaxing this constraint to make it a preorder relation yields another calculus that recovers important notions of the pi-calculus, that fusion calculi do not satisfy: the notions of types and of privacy of names. The first part of this thesis focuses on the study of this calculus, a pi-calculus with preorders on names.The second part of this thesis focuses on bisimulation, a proof method for equivalence of agents in higher-order languages, like the pi- or the lambda-calculi. An enhancement of this method is the powerful theory of bisimulations up to, which unfortunately only applies for first-order systems, like automata or CCS.We then proceed to describe higher-order languages as first-order systems. This way, we inherit the general theory of up-to techniques for these languages, by proving correct the translations and up-to techniques that are specific to each language. We give details on the approach, to provide the necessary tools for future applications of this method to other higher-order languages
3
ZORZI, Margherita. "Lambda calculi and logics for quantum computing." Doctoral thesis, Università degli Studi di Verona, 2009. http://hdl.handle.net/11562/337380.
Full textAbstract:
In questa tesi proponiamo diversi risultati originali riguardo i lambda
calcoli e le logiche per le computazioni quantistiche. Il lavoro `e diviso
in tre parti.
Nella prima parte richiamiamo alcune nozioni fondamentali di algebra
lineare, logica e computazione quantistica.
La seconda parte volge l’attenzione ai lambda calcoli quantistici.
Introdurremo dapprima Q, un lambda calcolo quantistico con controllo
classico. Studieremo le sue proprie`a classiche, come la confluenza e
la Subject Reduction, proseguendo poi con un’importante propriet`a
quantistica, chiamata standardizzazione. In seguito sar`a studiato il
potere espressivo di Q, attraverso la provata equivalenza con il formalismo
delle famiglie di circuiti quantistici.
A partire da Q, sar`a poi definito e studiato il sottolinguaggio SQ, ispirato
alla Soft Linear Logic ed intrinsecamente polytime.
Sia Q sia SQ non hanno nella sintassi un operatore di misurazione,
e quindi un’implicita misurazione viene assunta alla fine delle computazioni.
I problemi relativi alla misura sono studiati in un terzo lambda calcolo
chiamato Q*, che estende Q con un operatore di misura. Partendo
dall’osservazione che un esplicito operatore di misura interrompe
l’evoluzione altrimenti deterministica del calcolo, importando un comportamento
probabilistico, sono stati definiti dei nuovi strumenti tecnici
quali le computazioni probabilistiche e gli stati misti. Proveremo
un forte teorema di confluenza, valido anche nell’importante caso delle
computazioni infinite.
Nella terza parte della tesi studieremo invece due sistemi modali
etichettati, chiamati rispettivamente MSQS e MSpQS, che permettono
di ragionare qualitativamente sulle computazioni quantistiche. I due
sistemi rappresentano un possibile punto di partenza verso un nuovo
modello per ragionare qualitativamente sulle trasformazioni
computazionali degli stati quantistici, viste come modelli di Kripke.
1In this thesis we propose several original results about lambda calculi and logics for quantum computing. The work is divided into three parts. The first one is devoted to recall the main notions about linear algebra, logics and quantum computing. The second and main part focalizes on quantum lambda calculi. We start with Q, a quantum lambda calculus with classical control. We study its classical properties, such as confluence and Subject Reduction. We go on with an important quantum property of Q, called standardization, and successively, we study the expressive power of the proposed calculus, by proving the equivalence with the computational model of quantum circuit families. From the calculus Q, subsequently a sublanguage of Q called SQ is defined and studied: SQ is inspired to the Soft Linear Logic and it is a quantum lambda calculus intrinsically poly-time. Since Q and SQ have not an explicit measurement operator in the syntax, an implicit measurement at the end of the computations is assumed. Measurement problems are explicitly studied in a third quantum lambda calculus called Q*, an extension of Q with a measurement operator. Starting from the observation that an explicit measurement operator breaks the deterministic evolution of the computation by importing a probabilistic behavior, new technical instruments, such as the probabilistic computations and the mixed states are defined. We prove a confluence result for the calculus, also for the relevant case of infinite computations. In the last part of the thesis, we propose two labeled modal deduction systems able to describe quantum computations from a qualitative point of view. The two systems, called respectively MSQS and MSpQS, represent a starting point toward a new model to deal (in a qualitative way) with computational quantum structures, seen as Kripke models. 1
4
Barral, Freiric. "Decidability for Non-Standard Conversions in Typed Lambda-Calculi." Diss., lmu, 2008. http://nbn-resolving.de/urn:nbn:de:bvb:19-97617.
Full text
5
Ritter, Eike. "Categorical abstract machines for higher-order typed lambda calculi." Thesis, University of Cambridge, 1992. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.281971.
Full text
6
Carraro, Alberto <1983>. "Models and theories of pure and resource lambda calculi." Doctoral thesis, Università Ca' Foscari Venezia, 2011. http://hdl.handle.net/10579/1089.
Full textAbstract:
Parte I: Un problema aperto da lungo tempo è se esiste un modello del lambda calcolo non tipato nella categoria CPO degli ordinamenti parziali completi e funzioni Scott-continue, la cui teoria equazionale è esattamente la minima lambda-teoria λβ o la minima lambda-teoria estensionale λβη: è il Problema 22 nella lista dei problemi aperti TLCA (http://tlca.di.unito.it/opltlca/problem22.pdf). In questa tesi si analizza la classe dei dominii di Scott riflessivi, i modelli del lambda calcolo che vivono nella categoria dei dominii di Scott (una sottocategoria piena di CPO). Noi isoliamo, tra i domini riflessivi di Scott, una classe di modelli a trama derivanti dai sistemi informativi di Scott, che noi chiamiamo i-modelli. La classe degli i-modelli comprende, ad esempio, tutti i modelli preordinati coerenti, tutti i modelli a filtro che vivono in CPO e tutti i dominii di Scott estensionali riflessivi. Effettuando uno studio a dettagliato, di una versione "effettiva" dei sistemi informativi di Scott degli i-modelli si ottengono i seguenti risultati principali: c'è un'importante classe di i-modelli che non è completa per il lambda calcolo estensionale e tale nessun suo membro ha una teoria dell'ordine ricorsivamente enumerabile.
Un lambda-termine chiuso M è facile se, per qualsiasi altro termine chiuso N, la lambda-teoria generata dall'equazione M=N è consistente, mentre è facile semplice se, dato un tipo intersezione τ arbitrario, si può trovare un pre-ordine adeguato sui tipi che permette di derivare τ per M. La facilità semplice implica la facilità. La questione se la facilità implichi o meno la facilità semplice costituisce il Problema 19 nella lista dei problemi aperti TLCA (http://tlca.di.unito.it/opltlca/problem19.pdf). Come sottoprodotto del nostro lavoro sugli i-modelli, siamo in grado di risolvere questo problema: diamo una risposta negativa, fornendo un insieme non vuoto di lambda-termini facili ma non facili semplici.
Parte II: Dato un semi-anello con unità che soddisfi alcune condizioni, si definisce un funtore esponenziale della categoria degli insiemi e relazioni che consente di definire un modello denotazionale della Logica Lineare Differenziale e del lambda calcolo con risorse . Si dimostra che, quando il semi-anello è un elemento che è "infinitario", questo modello non convalida la formula di Taylor e che è possibile costruire, nella categoria Cartesiana chiusa di Kleisli associata, un modello del lambda calcolo puro che non è sensibile. Questo è un analogo quantitativo della costruzione del grafo modello di Park nella categoria dei dominii di Scott.
Abbiamo avviato uno studio puramente algebrico del lambda calcolo con risorse di Ehrhard e Regnier, introducendo tre varietà algebriche: algebre combinatorie con risorse, lambda-algebre con risorse e algebre di lambda-astrazione con risorse. Stabiliamo le relazioni tra di esse, e gettiamo le basi per una teoria dei modelli del lambda calcolo con risorse. Mostriamo anche che il completamento ideale di un'algebra combinatoria (resp. lambda-algebra, algebra di lambda-astrazione) con risorse induce un'algebra combinatoria (resp. lambda-algebra, algebra di lambda-astrazione) "classica'', e che qualsiasi modello del lambda calcolo classico proveniente da una lambda-algebra con risorse determina una lambda-teoria che identifica tutti i termini che hanno lo stesso albero di Bohm.Part I: A longstanding open problem is whether there exists a model of the untyped lambda calculus in the category CPO of complete partial orderings and Scott continuous functions, whose theory is exactly the least lambda-theory λβ or the least extensional lambda-theory λβη: it is Problem 22 in the TLCA list of open problems (http://tlca.di.unito.it/opltlca/problem22.pdf). In this thesis we analyze the class of reflexive Scott domains, the models of lambda calculus living in the category of Scott domains (a full subcategory of CPO). We isolate, among the reflexive Scott domains, a class of webbed models arising from Scott's information systems, that we call i-models. The class of i-models includes, for example, all preordered coherent models, all filter models living in CPO and all extensional reflexive Scott domains. By performing a fine-grained study of an ''effective'' version of Scott's information systems and i-models we obtain the following main results: there is an important class of i-models which is not complete for the extensional calculus and whose members never have a recursively enumerable order theory. A closed lambda-term M is easy if, for any other closed term N, the lambda-theory generated by the equation M = N is consistent, while it is simple easy if, given an arbitrary intersection type τ, one can find a suitable pre-order on types which allows to derive τ for M. Simple easiness implies easiness. The question whether easiness implies simple easiness constitutes Problem 19 in the TLCA list of open problems (http://tlca.di.unito.it/opltlca/problem19.pdf). As a byproduct of our work on i-models, we are in the position of solving this problem: we answer negatively, providing a nonempty set of easy, but non simple easy, lambda-terms. Part II: Given a semi-ring with unit which satisfies some conditions, we define an exponential functor on the category of sets and relations which allows to define a denotational model of Differential Linear Logic and of the lambda-calculus with resources. We show that, when the semi-ring has an element which is ''infinitary", this model does not validate the Taylor formula and that it is possible to build, in the associated Kleisli cartesian closed category, a model of the pure lambda-calculus which is not sensible. This is a quantitative analogue of the Park's graph model construction in the category of Scott domains. We initiate a purely algebraic study of Ehrhard and Regnier's resource lambda-calculus, by introducing three algebraic varieties: resource combinatory algebras, resource lambda-algebras and resource lambda-abstraction algebras. We establish the relations between them, laying down foundations for a model theory of resource lambda calculus. We also show that the ideal completion of a resource combinatory algebra (resp. lambda-algebra, lambda-abstraction algebra) induces a ''classical'' combinatory algebra (resp. lambda-algebra, lambda-abstraction algebra), and that any model of the pure lambda calculus raising from a resource lambda-algebra determines a lambda-theory which equates all terms having the same Bohm tree.
7
Loader, Ralph. "Models of lambda calculi and linear logic : structural, equational and proof-theoretic characterisations." Thesis, University of Oxford, 1994. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.282167.
Full text
8
Kuc̆an, Jakov. "Metatheorems about convertibility in typed lambda calculi : applications to CPS transform and "free theorems"." Thesis, Massachusetts Institute of Technology, 1997. http://hdl.handle.net/1721.1/42606.
Full text
9
Solieri, Marco. "Sharing, Superposition and Epansion : Geometrical Studies on the semantics and Implementation of lambda-calculi and proof-nets." Thesis, Sorbonne Paris Cité, 2016. http://www.theses.fr/2016USPCD015/document.
Full textAbstract:
Des sémantiques élégantes et des implémentations efficaces des langages de programmation fonctionnels peuvent être décrits par les mêmes structures mathématiques, notamment dans la correspondance Curry-Howard, où le programmes, les types et l’exécution, coïncident aux preuves, formules et normalisation. Une telle flexibilité est aiguisé par l’approche déconstructive et géométrique de la logique linéaire (LL) et les réseaux de preuve, et de la réduction optimale et les graphes de partage (SG).En adaptent la géométrie de l’interaction de Girard, cette thèse propose une géométrie de l’interaction des ressources (GoRI), une sémantique dynamique et dénotationnelle, qui décrit algébriquement par leurs chemins, les termes du calcul des ressources (RC), une variation linéaire et non-déterministe du lambda calcul (LC). Les séries infinis dans RC sont aussi le domaine du développement de Taylor-Ehrhard-Regnier, une linéarisation du LC. La thèse explique la relation entre ce dernier et la réduction démontrant qu’ils commutent, et présente une version développé de la formule d’exécution pour calculer les chemins du LC typé.Les SG sont un modèle d’implémentation du LC, dont les pas sont locales et asynchrones, et le partage implique et les termes et les contextes. Bien que les tests ont montré des accélérations exceptionnelles, jusqu à exponentielles, par rapport aux implémentations traditionnelles, les SG n’ont pas que des avantages. La thèse montre que, dans le cas restreint des réseaux élémentaires, où seule le cœur des SG est requis, les désavantages sont au plus quadratique, donc inoffensifsElegant semantics and efficient implementations of functional programming languages can both be described by the very same mathematical structures, most prominently with in the Curry-Howard correspondence, where programs, types and execution respectively coincide with proofs, formulæ and normalisation. Such a flexibility is sharpened by the deconstructive and geometrical approach pioneered by linear logic (LL) and proof-nets, and by Lévy-optimal reduction and sharing graphs (SG).Adapting Girard’s geometry of interaction, this thesis introduces the geometry of resource interaction (GoRI), a dynamic and denotational semantics, which describes, algebra-ically by their paths, terms of the resource calculus (RC), a linear and non-deterministic variation of the ordinary lambda calculus. Infinite series of RC-terms are also the domain of the Taylor-Ehrhard-Regnier expansion, a linearisation of LC. The thesis explains the relation between the former and the reduction by proving that they commute, and provides an expanded version of the execution formula to compute paths for the typed LC. SG are an abstract implementation of LC and proof-nets whose steps are local and asynchronous, and sharing involves both terms and contexts. Whilst experimental tests on SG show outstanding speedups, up to exponential, with respect to traditional implementations, sharing comes at price. The thesis proves that, in the restricted case of elementary proof-nets, where only the core of SG is needed, such a price is at most quadratic, hence harmless
Semantiche eleganti ed implementazioni efficienti di linguaggi di programmazione funzionale possono entrambe essere descritte dalle stesse strutture matematiche, più notevolmente nella corrispondenza Curry-Howard, dove i programmi, i tipi e l’esecuzione coincidono, nell’ordine, con le dimostrazioni, le formule e la normalizzazione. Tale flsesibilità è acuita dall’approccio decostruttivo e geometrico della logica lineare (LL) e le reti di dimostrazione, e della riduzione ottimale e i grafi di condivisione (SG).Adattando la geometria dell’interazione di Girard, questa tesi introduce la geometria dell’interazione delle risorse (GoRI), una semantica dinamica e denotazionale che descrive, algebricamente tramite i loro per-corsi, i termini del calcolo delle risorse (RC), una variante lineare e non-deterministica del lambda calcolo ordinario. Le serie infinite di termini del RC sono inoltre il dominio dell’espansione di Taylor-Ehrhard-Regnier, una linearizzazione del LC. La tesi spiega la relazione tra quest’ultima e la riduzione dimostrando che esse commutano, e fornisce una versione espansa della for-mula di esecuzione per calcolare i percorsi del LC tipato. I SG sono un modello d’implementazione del LC, i cui passi sono loc-ali e asincroni, e la cui condivisione riguarda sia termini che contesti. Sebbene le prove sperimentali sui SG mostrino accellerazioni eccezionali, persino esponenziali, rispetto alle implementazioni tradizionali, la condivisione ha un costo. La tesi dimostra che, nel caso ristretto delle reti elementari, dove è necessario solo il cuore dei SG, tale costo è al più quad-ratico, e quindi innocuo
10
Taylor, Amelia V. "A unifying framework for Lambda Calculi and their extensions with explicit substitution operators that is useful for verifying confluence." Thesis, Heriot-Watt University, 2006. http://hdl.handle.net/10399/119.
Full text
11
Herbelin, Hugo. "Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes." Phd thesis, Université Paris-Diderot - Paris VII, 1995. http://tel.archives-ouvertes.fr/tel-00382528.
Full textAbstract:
L'objet de cette thèse est l'étude des systèmes formels du type des systèmes LJ et LK de Gentzen (couramment appelés calculs des séquents) dans leur rapport avec la calculabilité. Le procédé de calcul dans ces systèmes consiste en « l'élimination des coupures ». Deux interprétations sont considérées.Le lambda-calcul constitue le support de la première interprétation. Nous établissons une correspondance de type Curry-Howard entre LJ et une variante syntaxique du lambda-calcul avec opérateur explicite de substitution (de type « let _ in _ »). Une procédure de normalisation/élimination des coupures confluente et terminant fortement est donnée et l'extension de la correspondance à LK se fait en considérant l'opérateur mu du lambda-mu-calcul de Parigot.
La théorie des jeux constitue le support de la deuxième interprétation: les preuves des calculs des séquents sont vues comme des stratégies gagnantes pour certains types de jeux à deux joueurs (dialogues) se disputant la validité de la formule prouvée. Nous donnons deux résultats.
Dans un premier temps, nous montrons qu'il suffit de considérer des restrictions LJQ de LJ puis LKQ de LK pour établir, dans le cas propositionnel, une bijection entre les preuves de ces systèmes et les E-dialogues intuitionnistes puis classiques définis par Lorenzen dans un but de fondement de la prouvabilité en termes de jeux. Ceci affine et généralise un résultat de Felscher d'équivalence entre l'existence d'une preuve d'une formule A dans LJ et l'existence d'une stratégie gagnante pour le premier des joueurs dans un E-dialogue à propos de A.
Dans un deuxième temps, nous partons d'une logique propositionnelle infinitaire sans variable considérée par Coquand pour y définir une interaction prouvée terminante entre les preuves vues comme stratégies gagnantes. Nous montrons une correspondance opérationnelle entre ce procédé d'interaction et l'élimination « faible de tête » des coupures, celle-ci étant indépendamment prouvée terminante.
12
Herbelin, Hugo. "Sequents qu'on calcule : de l'interpretation du calcul des sequents comme calcul de lambda-termes et comme calcul de strategies gagnantes." Paris 7, 1995. https://tel.archives-ouvertes.fr/tel-00382528.
Full textAbstract:
L'objet de cette these est l'etude des systemes formels du type des systemes lj et lk de gentzen (couramment appeles calculs des sequents) dans leur rapport avec la calculabilite. Le procede de calcul dans ces systemes consiste en l'elimination des coupures. Deux interpretations sont considerees. Le lambda-calcul constitue le support de la premiere interpretation. Nous etablissons une correspondance de type curry-howard entre lj et une variante syntaxique du lambda-calcul avec operateur explicite de substitution (de type let - in - ). Une procedure de normalisation/elimination des coupures confluente et terminant fortement est donnee et l'extension de la correspondance a lk se fait en considerant l'operateur mu du lambda-mu-calcul de parigot. La theorie des jeux constitue le support de la deuxieme interpretation : les preuves des calculs des sequents sont vues comme des strategies gagnantes pour certains types de jeux a deux joueurs (dialogues) se disputant la validite de la formule prouvee. Nous donnons deux resultats. Dans un premier temps, nous montrons qu'il suffit de considerer des restrictions ljq de lj puis lkq de lk pour etablir, dans le cas propositionnel, une bijection entre les preuves de ces systemes et les e-dialogues intuitionnistes puis classiques definis par lorenzen dans un but de fondement de la prouvabilite en termes de jeux. Ceci affine et generalise un resultat de felscher d'equivalence entre l'existence d'une preuve d'une formule a dans lj et l'existence d'une strategie gagnante pour le premier des joueurs dans un e-dialogue a propos de a. Dans un deuxieme temps, nous partons d'une logique propositionnelle infinitaire sans variable consideree par coquand pour y definir une interaction prouvee terminante entre les preuves vues comme strategies gagnantes. Nous montrons une correspondance operationnelle entre ce procede d'interaction et l'elimination faible de tete des coupures, celle-ci etant independamment prouvee terminante.
13
Régnier, Laurent. "Lambda-calcul et reseaux." Paris 7, 1992. http://www.theses.fr/1992PA077165.
Full textAbstract:
Les liens etroits qu'entretient le lambda-calcul de church avec la logique et en particulier avec la theorie de la demonstration, en font un outil abstrait particulierement adequat a l'etude de l'execution des programmes. Le propos de la these est de developper une nouvelle theorie de l'execution des lambda-termes basee sur la notion geometrique de trace. Cette alternative a la notion habituelle de calcul, la beta-reduction, est issue des travaux de girard sur les reseaux et la geometrie de l'interaction, et a ete introduite par danos dans sa these (paris 7, 1990). Elle correspond a une decomposition de la beta-reduction en operations locales et est donc un pas important vers une definition d'une execution partagee des lambda-termes. La these est en quatre parties. Les deux premieres introduisent le lambda-calcul et les reseaux. On montre que la syntaxe des reseaux code correctement les lambda-termes, et que les reseaux sont dotes d'une bonne structure geometrique. Les deux parties suivantes developpent les bases d'une theorie des traces et de l'execution
14
Nebel, Frank. "Nominal lambda calculus." Thesis, University of Leicester, 2015. http://hdl.handle.net/2381/31396.
Full textAbstract:
Since their introduction, nominal techniques have been widely applied in computer science to reason about syntax of formal systems involving name-binding operators. The work in this thesis is in the area of “nominal" type theory, or more precisely the study of “nominal" simple types. We take Nominal Equational Logic (NEL), which augments equational logic with freshness judgements, as our starting point to introduce the Nominal Lambda Calculus (NLC), a typed lambda calculus that provides a simple form of name-dependent function types. This is a key feature of NLC, which allows us to encode freshness in a novel way. We establish meta-theoretic properties of NLC and introduce a sound model theoretic semantics. Further, we introduce NLC[A], an extension of NLC that captures name abstraction and concretion, and provide pure NLC[A] with a strongly normalising and confluent βη-reduction system. A property that has not yet been studied for “nominal" typed lambda calculi is completeness of βη-conversion for a nominal analogue of full set-theoretic hierarchies. Aiming towards such a result, we analyse known proof techniques and identify various issues. As an interesting precursor, we introduce full nominal hierarchies and demonstrate that completeness holds for βη-conversion of the ordinary typed lambda calculus. The notion of FM-categories was developed by Ranald Clouston to demonstrate that FM-categories correspond precisely to NEL-theories. We augment FM-categories with equivariant exponentials and show that they soundly model NLC-theories. We then outline why NLC is not complete for such categories, and discuss in detail an approach towards extending NLC which yields a promising framework from which we aim to develop a future (sound and complete) categorical semantics and a categorical type theory correspondence. Moreover, in pursuit of a categorical conservative extension result, we study (enriched/ internal) Yoneda isomorphisms for “nominal" categories and some form of “nominal" gluing.
15
Goyet, Alexis. "The [lambda lambda-bar]-calculus : a dual calculus for unconstrained strategies." Paris 7, 2013. http://www.theses.fr/2013PA077281.
Full textAbstract:
Nous présentons un calcul qui combine une représentation simple, à la CCS, des comportements finis. Pour cela nous utilisons deux lieurs duaux: lambda et lambda-bar. Les comportements infinis sont obtenus grâce à un opérateur de point fixe, qui est en particulier utilisé pour donner une traduction des lambda termes. La dualité du calcul rend symétriques les rôles d'une fonction et de son environnement. Comme à l'accoutumé, l'environnement est autorisé à appeler une fonction à n'importe quel moment, à chaque fois avec un argument différent. De manière duale, la fonction est autorisée à répondre à n'importe quel appel, avec à chaque fois un comportement différent. Ceci donne aux termes de notre langage le pouvoir des références fonctionnelles. L'inspiration de ce langage provient de la Sémantique des Jeux. En effet, les formes normales donnent une syntaxe concrète simple pour les stratégies finies, qui sont de façon inhérentes non innocentes. Cette correspondance très directe nous permet de décrire, de manière syntaxique, un certain nombre de traits de la Sémantique des Jeux. L'expansion du point fixe dans un lambda terme traduit corresponds à la génération de parties infinies à partir des vues finies d'une stratégie innocente. La dualité syntaxique entre termes et co-termes corresponds à la dualité entre le Joueur et l'Opposant. Cette dualité donne aussi lieu à un lemme de type Bôhm-outWe present a calculus which combines a simple, CCS-like representation of finite behaviors, with two dual binders lambda and lambda. Infinite behaviors are obtained through a syntactical fixed-point operator, which is used to give a translation of lambda-terms. The duality of the calculus makes the roles of a function and its environment symmetrical. As usual, the environment is allowed to call a function at any given point, each time with a different argument. Dually, the function is allowed to answer any given call, each time with a different behavior. This grants terms in our language the power of functional references. The inspiration for this language cornes from Game Semantics. Indeed, its normal forms give a simple concrete syntax for finite strategies, which are inherently non-innocent. This very direct correspondence allows us to describe, in syntactical terms, a number of features from Game Semantics. The fixed-point expansion of translated lambda-terms corresponds to the generation of infinite plays from the finite views of an innocent strategy. The syntactical duality between ternis and co-ternis corresponds to the duality between Player and Opponent. This duality also gives vise to a Biihm-out lemma
16
Midez, Jean baptiste. "Une étude combinatoire du lambda-calcul avec ressources uniforme." Thesis, Aix-Marseille, 2014. http://www.theses.fr/2014AIXM4093/document.
Full textAbstract:
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 finThe 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
17
Even, Christian. "Autour du lambda-calcul partiel." Lille 1, 1993. http://www.theses.fr/1993LIL10045.
Full textAbstract:
Cette thèse a pour objet l'étude des aspects syntaxiques, algébriques et catégoriques du lambda-calcul partiel, qui est un outil théorique pour étudier l'équivalence de programmes exécutées selon un mécanisme d'appel par valeur. En appliquant des techniques éprouvées dans le lambda-calcul pur et en les adaptant à ce calcul on a ainsi obtenu: 1) une preuve de la confluence pour un lambda-calcul partiel simplifie; 2) la caractérisation d'une classe de termes fortement normalisables par un système de types simples; 3) la caractérisation des termes égalisables à une valeur dans le lambda-calcul partiel comme conséquence de celle obtenue par un système de types dans le lambda-calcul par valeur, calcul antérieur et de même vocation que le précédent, mais moins expressif; 4) l'élaboration d'une notion d'algèbre combinatoire répondant à celle de modèle du lambda-calcul partiel et de la relation de cette notion avec la donnée d'une catégorie cartesienne fermée partielle munie d'un objet réflexif
18
Blum, William. "The safe lambda calculus." Thesis, University of Oxford, 2009. http://ora.ox.ac.uk/objects/uuid:537d45e0-01ac-4645-8aba-ce284ca02673.
Full textAbstract:
We consider a syntactic restriction for higher-order grammars called safety that constrains occurrences of variables in the production rules according to their type-theoretic order. We transpose and generalize this restriction to the setting of the simply-typed lambda calculus, giving rise to what we call the safe lambda calculus. We analyze its expressivity and obtain a result in the same vein as Schwichtenberg's 1976 characterization of the simply-typed lambda calculus: the numeric functions representable in the safe lambda calculus are exactly the multivariate polynomials; thus conditional is not definable. We also give a similar characterization for representable word functions. We then examine the complexity of deciding beta-eta equality of two safe simply-typed terms and show that this problem is PSPACE-hard. The safety restriction is then extended to other applied lambda calculi featuring recursion and references such as PCF and Idealized Algol (IA for short). The next contribution concerns game semantics. We introduce a new concrete presentation of this semantics using the theory of traversals. It is shown that the revealed game denotation of a term can be computed by traversing some souped-up version of the term's abstract syntax tree using adequately defined traversal rules. Based on this presentation and via syntactic reasoning we obtain a game-semantic interpretation of safety: the strategy denotations of safe lambda-terms satisfy a property called P-incremental justification which says that the player's moves are always justified by the last pending opponent's move of greater order occurring in the player's view. Next we look at models of the safe lambda calculus. We show that these are precisely captured by Incremental Closed Categories. A game model is constructed and is shown to be fully abstract for safe IA. Further, it is effectively presentable: two terms are equivalent just if they have the same set of complete O-incrementally justified plays---where O-incremental justification is defined as the dual of P-incremental justification. Finally we study safety from the point of view of algorithmic game semantics. We observe that in the third-order fragment of IA, the addition of unsafe contexts is conservative for observational equivalence. This implies that all the upper complexity bounds known for the lower-order fragments of IA also hold for the safe fragment; we show that the lower-bounds remain the same as well. At order 4, observational equivalence is known to be undecidable for IA. We conjecture that for the order-4 safe fragment of IA, the problem is reducible to the DPDA-equivalence problem and is thus decidable.
19
Moggi, Eugenio. "The partial lambda calculus." Thesis, University of Edinburgh, 1988. http://hdl.handle.net/1842/419.
Full textAbstract:
This thesis investigates various formal systems for reasoning about partial functions or partial elements, with particular emphasis on lambda calculi for partial functions. Beeson's (intuitionistic) logic of partial terms (LPT) is taken as the basic formal system and some of its metamathematical properties are established (for later application). Three different flavours of Scott's logic of partial elements (LPE) are considered and it is shown that they are conservative extensions of LPT. This result, we argue, corroborates the choice of LPT as the basic formal system. Variants of LPT are introduced for reasoning about partial terms with a restriction operator ↾, monotonic partial functions (monLPT), lambda-terms λ_p-calculus) and λY-terms λ_pμY-calculus). The expressive powers of some (in)equational fragments are compared in LPT and its variants. Two equational formal systems are related to some of the logics above: Obtulowicz's p-equational logic is related to LPT+↾ and Plotkin's λ_v-calculus is related to one flavour of LPE. The deductive powers of LPT and its variants are compared, using various techniques (among them logical relations). The main conclusion drawn from this comparison is that there are four different lambda calculi for partial functions: intuitionistic or classical, partial or monotonic partial functions. An (in)equational presentation of the intuitionistic lambda calculus for (monotonic) partial functions is given as an extension of p-equational logic. We conjecture that there is no equational presentation of the classical λ_p-calculus. Via a special kind of diamond property, the (in)equational formal system is characterized in terms of β-reduction for partial functions and some decidability problems are solved.
20
Cuti, Filippo. "The finite lambda calculus." Master's thesis, Alma Mater Studiorum - Università di Bologna, 2015. http://amslaurea.unibo.it/8203/.
Full text
21
Rouyer, Joseph. "Développements d'algorithmes dans le calcul des constructions." Vandoeuvre-les-Nancy, INPL, 1994. http://www.theses.fr/1994INPL042N.
Full textAbstract:
Le calcul des constructions est d'abord un lambda-calcul type d'ordre supérieur avec polymorphisme et types dépendants. La forte normalisation de ce lambda-calcul a été prouvée par Thierry Coquand qui en a fait un langage logique d'ordre supérieur permettant de coder la logique naturelle intuitionniste. Il en a démontré la cohérence et en a réalisé les premières implantations. Ce calcul des constructions initial a été enrichi (à la suite des travaux de Christine Paulin-Mohring) par de nouvelles sortes puis par les types inductifs et un procédé d'extraction de programmes. C'est dans l'implantation v5. 8 de cette dernière version que nous avons développé un algorithme d'unification au premier ordre (celui de Robinson), puis deux algorithmes de recherche de recouvrements connexes d'un graphe pondère, celui de Prim et celui de Kruskal. Ces algorithmes ont été entièrement synthétises. Il ne s'agit pas de simples preuves de programmes. Le revers de la médaille est que les programmes que l'on extrait de ces preuves contiennent des calculs provenant de la preuve de terminaison qui ne servent pas dans la construction du résultat. Pour l'algorithme d'unification nous montrons de deux manières comment, en réalisant un axiome d'induction non structurelle, on peut réduire au maximum les traces de la preuve de terminaison
22
Madet, Antoine. "Complexité Implicite de Lambda-Calculs Concurrents." Phd thesis, Université Paris-Diderot - Paris VII, 2012. http://tel.archives-ouvertes.fr/tel-00794977.
Full textAbstract:
Contrôler la consommation en ressources des programmes informatiques est d'importance capitale, non seulement pour des raisons de performance, mais aussi pour des questions de sécurité quand par exemple certains systèmes mobiles ou embarqués disposent de quantités limitées de ressources. Dans cette thèse, nous développons des critères statiques pour contrôler la consommation en ressources de programmes concurrents d'ordre supérieur. Nous prenons comme point de départ le cadre des Logiques Light qui a été étudié afin de contrôler la complexité de programmes fonctionnels d'ordre supérieur au moyen de la correspondance preuves-programmes. La contribution de cette thèse est d'étendre ce cadre aux programmes concurrents d'ordre supérieur. Plus généralement, cette thèse s'inscrit dans le domaine de la complexité implicite qui cherche à caractériser des classes de complexité par des principes logiques ou des restrictions de langage. Les critères que nous proposons sont purement syntaxiques et sont développés graduellement afin de contrôler le temps de calcul des programmes de plus en plus finement: dans un premier temps nous montrons comment garantir la terminaison des programmes (temps fini), puis nous montrons comment garantir la terminaison des programmes en temps élémentaire, et enfin nous montrons comment garantir la terminaison des programmes en temps polynomial. Nous introduisons également des systèmes de types tels que les programmes bien typés terminent en temps borné et retournent des valeurs. Enfin, nous montrons que ces systèmes de types capturent des programmes concurrents intéressants qui itèrent des fonctions produisant des effets de bord sur des structures de données inductives. Dans la dernière partie, nous étudions une méthode sémantique alternative afin de contrôler la consommation en ressources de programmes impératifs d'ordre supérieur. Cette méthode est basée sur la réalisabilité quantitative de Dal Lago et Hofmann et permet d'obtenir plusieurs bornes de complexité de manière uniforme. Cette dernière partie est un travail en collaboration avec Aloïs Brunel.
23
Alberti, Michele. "Risultati di separazione nei calcoli lambda." Master's thesis, Alma Mater Studiorum - Università di Bologna, 2011. http://amslaurea.unibo.it/2738/.
Full text
24
Bertini, Yves. "La notion d'indéfini en lambda calcul." Phd thesis, Chambéry, 2005. http://tel.archives-ouvertes.fr/tel-00415825.
Full textAbstract:
La facilité compte parmi les notions les plus fines de l'indéfini en lambda-calcul. Un terme est dit facile s'il peut être identifié à tout autre terme clos arbitraire sans soulever de contradiction. Introduite en 1975 par Jacopini, elle fait depuis l'objet de recherches qui visent à caractériser la forme des termes faciles. Aujourd'hui, de tous les travaux entrepris il se dégage qu'un tel terme doit posséder une périodicité. Être périodique, c'est être équivalent à un sous-terme propre de l'un de ses réduits. Ici, la périodicité apparaîtra sous les traits de l'auto-similarité. Sont auto-similaires les termes dont l'arbre de Berarducci réapparaît comme sous-arbre propre à lui-même. La facilité de tels termes demeure un mystère. À ce jour, nous n'en connaissons que peu d'exemples. Le terme "Y omega_3" constitue un exemple typique dont la question de la facilité reste ouverte. Dans cette thèse, nous étendrons la connaissance de l'ensemble des termes m identiables à Y Omega_3. Nous montrerons que dans un cas critique où lambda-beta +{Y Omega_3 = m} implique m = delta_3, sous certaines hypothèses, m est lui-même auto-similaire. Ils s'en suit une description possible de toutes les équations dérivées de {Y Omega_3= m} sous la forme de classes confinantes.
25
Petit, Barbara. "Autour du lambda-calcul avec constructeurs." Phd thesis, Ecole normale supérieure de lyon - ENS LYON, 2011. http://tel.archives-ouvertes.fr/tel-00662500.
Full textAbstract:
Le lambda calcul avec constructeurs (de Arbiser, Miquel et Rios) est une extension du lambda calcul avec un mécanisme de filtrage. Le filtrage à la ML y est décomposé en deux étapes: une analyse de cas sur des constantes (telle l'instruction "case" de Pascal), et une commutation de l'application avec la construction de filtrage. Cette règle de commutation entre deux constructions de natures différentes induit une géométrie de calcul surprenante, a priori incompatible avec les intuitions habituelles de typage. Cependant il a été montré que ce calcul est confluent, et vérifie la propriété de séparation (à la Böhm). Cette thèse propose un système de types du polymorphique pour ce calcul, et décrit ensuite un modèle de réalisabilité, qui adapte les candidats de réductibilité de Girard au lambda calcul avec constructeurs. La normalisation forte du calcul typé et l'absence d'erreur de filtrage lors de l'évaluation en découlent immédiatement. Nous nous intéressons ensuite à la sémantique du lambda calcul avec constructeurs non typé. Une notion générique de modèle catégorique pour ce calcul est définie, puis un modèle particulier (le modèle syntaxique dans la catégorie des PERs) est construit. Nous en déduisons un résultat de complétude. Enfin, nous proposons une traduction CPS du lambda calcul avec constructeurs dans le lambda calcul simplement typé avec paires. Le lambda calcul avec constructeurs peut ainsi être simulé dans un calcul bien connu, et cette traduction nous permet aussi de transformer tout modèle par continuation en modèle du lambda calcul avec constructeurs. Une équation catégorique caractéristique de ces modèles apparait alors, qui permet de construire des modèles non syntaxiques (dans les domaines) de Scott du lambda calcul avec constructeurs.
26
LAVATELLI, CAROLINA. "Semantique du lambda calcul avec ressources." Paris 7, 1996. http://www.theses.fr/1996PA077230.
Full textAbstract:
Le lambda calcul avec ressources, defini par g. Boudol en connexion avec le codage du lambda calcul dans le pi calcul de r. Milner, est un raffinement non-deterministe du calcul faible a la abramsky, introduisant la notion de blocage pendant l'evaluation par le moyen d'arguments constitues d'un nombre possiblement fini de ressources. Nous abordons dans cette these l'etude de la semantique operationnelle et des modeles du calcul avec ressources. L'equation aux domaines standard pour les calculs faibles n'est pas assez expressive pour permettre l'interpretation des arguments finis du calcul avec ressources. Nous proposons deux nouvelles equations de la forme d = m(d) d qui different dans la construction m(d). Cette construction correspond intuitivement, dans les deux cas, au domaine des multi-ensembles d'elements de d. Les presentations logiques des solutions canoniques des equations - dans la categorie des treillis complets algebriques, constituent des modeles adequats du calcul. Le premier est un modele de cones, le deuxieme un modele de filtres, qui ont, chacun, un systeme de types avec intersection a la coppo associe. La particularite de ces systemes est le traitement multiplicatif de la conjonction, autrement dit l'impossibilite d'effectuer des contractions d'hypotheses (qui correspond au caractere fini des arguments). Aucun des modeles n'est pourtant completement adequat pour le calcul de ressources. L'ajout d'un operateur de test de convergence suffit pour le modele de cones. Nous conjecturons que c'est aussi suffisant pour le modele de filtres
27
MOUNIER, GEORGES. "Un lambda-calcul intuitionniste avec exceptions." Chambéry, 1999. http://www.theses.fr/1999CHAMS005.
Full textAbstract:
La these decrit un systeme de -calcul type etendu par un traitement des exceptions. Le -calcul type est une bonne description abstraite des langages de programmation fonctionnels, mais les exceptions sortent de son cadre. Apres avoir examine trois -calculs types recemment proposes pour donner une interpretation logique des mecanismes de controle et verifie qu'aucun ne permet de decrire completement le mecanisme des exceptions, tel qu'il est, par exemple, mis en oeuvre dans la langage caml, la these decrit un systeme de -calcul type original ex2 integrant declaration, levee et capture des exceptions. Les proprietes du systeme ex2 sont ensuite prouvees : la reduction des termes est confluente ; tout terme typable est fortement normalisable ; le type se conserve non dans la reduction ordinaire, mais dans une forme parallelisee de la reduction qui produit les memes formes normales ; seuls les termes equivalents aux entiers de church ont le type entier. Le systeme ex2 permet d'utiliser les exceptions aussi bien pour abreger un calcul, que pour denoter une impossibilite a poursuivre : plusieurs exemples en sont fournis. Enfin nous prouvons que ex2 est un calcul de preuve intuitionniste, resultat qui amene a s'interroger sur l'opinion couramment admise qui relie operateurs de controle et logique classique.
28
He, Fanny. "The atomic lambda-mu calculus." Thesis, University of Bath, 2018. https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.761031.
Full textAbstract:
A cornerstone of theoretical computer science is the Curry-Howard correspondence where formulas are types, proofs are programs, and proof normalization is computation. In this framework we introduce the atomic λμ-calculus, an interpretation of a classical deep inference proof system. It is based on two extensions of the λ-calculus, the λμ-calculus and the atomic λ-calculus. The former interprets classical logic, featuring continuation-like constructs, while the latter interprets intuitionistic deep inference, featuring explicit sharing operators. The main property of the atomic λ-calculus is reduction on individual constructors, derived from atomicity in deep inference. We thus work on open deduction, a deep inference formalism, allowing composition with connectives and with derivations, and using the medial rule to obtain atomicity. One challenge is to find a suitable formulation for deriving a computational interpretation of classical natural deduction. A second design challenge leads us to work on a variant of the λμ-calculus, the ΛμS-calculus, adding streams and dropping names. We show that our calculus has preservation of strong normalization (PSN), confluence, fully-lazy sharing, and subject reduction in the typed case. There are two challenges with PSN. First, we need to show that sharing reductions strongly normalize, underlining that only β, μ-reductions create divergence. Our proof is new and follows a graphical approach to terms close to the idea of sharing. Second, infinite reductions of the atomic calculus can appear in weakenings, creating infinite atomic paths corresponding to finite ΛμS-paths. Our solution is to separate the proof into two parts, isolating the problem of sharing from that of weakening. We first translate into anintermediate weakening calculus, which unfolds shared terms while keeping weakened ones, and preserves infinite reductions. We then design a reduction strategy preventing infinite paths from falling into weakenings.
29
Madet, Antoine. "Complexité implicite dans des Lambda -calculs concurrents." Paris 7, 2012. http://www.theses.fr/2012PA077222.
Full textAbstract:
Contrôler la consommation en ressources des programmes informatiques est d'importance capitale, non seulement pour des raisons de performance, mais aussi pour des questions de sécurité quand par exemple certains systèmes mobiles ou embarqués disposent de quantités limitées de ressources. Dans cette thèse, nous développons des critères statiques pour contrôler la consommation en ressources de programmes concurrents d'ordre supérieur. Nous prenons comme point de départ le cadre des Logiques Light qui a été étudié afin de contrôler la complexité de programmes fonctionnels d'ordre supérieur au moyen de la correspondance preuves-programmes. La contribution de cette thèse est d'étendre ce cadre aux programmes concurrents d'ordre supérieur. Plus généralement, cette thèse s'inscrit dans le domaine de la complexité implicite qui cherche à caractériser des classes de complexité par des principes logiques ou des restrictions de langage. Les critères que nous proposons sont purement syntaxiques et sont développés graduellement afin de contrôler le temps de calcul des programmes de plus en plus finement: dans un premier temps nous montrons comment garantir la terminaison des programmes (temps fini), puis nous montrons comment garantir la terminaison des programmes en temps élémentaire, et enfin nous montrons comment garantir la terminaison des programmes en temps polynomial. Nous introduisons également des systèmes de types tels que les programmes bien typés terminent en temps borné et retournent des valeurs. Enfin, nous montrons que ces systèmes de types capturent des programmes concurrents intéressants qui itèrent des fonctions produisant des effets de bord sur des structures de données inductives. Dans la dernière partie, nous étudions une méthode sémantique alternative afin de contrôler la consommation en ressources de programmes impératifs d'ordre supérieur. Cette méthode est basée sur la réalisabilité quantitative de Dal Lago et Hofmann et permet d'obtenir plusieurs bornes de complexité de manière uniforme. Cette dernière partie est un travail en collaboration avec Aloïs BrunelControlling the resource consumption of programs is crucial: besides performance reasons, it has many applications in the field of computer security where e. G. Mobile or embedded Systems dispose of limited amounts of resources. In this thesis, we develop static criteria to control the resource consumption of higher-order concurrent programs. Our starting point is the framework of Light Logics which has been extensively studied to control the complexity of higher-order functional programs through the proofs-as-programs correspondent. The contribution of this thesis is to extend this framework to higher-order concurrent programs. More generally, this thesis fits in the research field of Implicit Computational Complexity which aims at characterizing complexity classes by logical principles or language restrictions. The criteria that we propose are purely syntactic and are developed gradually to control the computational time of programs in a finer and finer way: first, we show how to guarantee the termination of programs (finite time); then, we show how to guarantee the termination of programs in elementary time and last, we show how to guarantee the termination of programs in polynomial time. We also introduce type Systems so that well-typed programs are guaranteed to terminate in bounded time and to return values. Finally, we show that the type Systems capture some interesting concurrent programs that iterate functions producing side effects over inductive data structures. In the last part, we study an alternative semantic method to control the resource consumption of higher-order imperative programs. The method is based on Dal Lago and Hofmann's quantitative realizability framework and allows to obtain various complexity bounds in a uniform way. This last par is joint work with Aloïs Brunel
30
Manzonetto, Giulio. "Models and theories of lambda calculus." Phd thesis, Université Paris-Diderot - Paris VII, 2008. http://tel.archives-ouvertes.fr/tel-00715207.
Full textAbstract:
Dans cette thèse on s'intéresse surtout aux sémantiques principales du λ-calcul (c'est- a-dire la sémantique continue de Scott, la sémantique stable, et la sémantique fortement stable) mais on introduit et étudie aussi deux nouvelles sémantiques : la sémantique relationnelle et la sémantique indécomposable. Les modèles du λ-calcul pur peuvent être définis soit comme des objets réflexifs dans des catégories Cartésiennes fermées (modèles catégoriques) soit comme des algèbres combinatoires satisfaisant les cinq axiomes de Curry et l'axiome de Meyer-Scott ( λ-modèles). En ce qui concerne les modèles catégoriques, on montre que tout modèle catégorique peut être présenté comme un λ-modèle, même si la ccc (catégorie Cartésienne fermée) sous-jacente n'a pas assez de points, et on donne des conditions su santes 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 ccc d'ensembles et relations (sémantique relationnelle) et qui satisfait ces conditions. De plus, on montre que le λ-modèle associe possède des propriétés algébriques qui le rendent apte a modéliser des extensions non-déterministes du -calcul. En ce qui concerne les algèbres combinatoires, on montre qu'elles satisfont une généralisation du Théorème de Représentation de Stone qui dit que toute algèbre combinatoire est isomorphe a un produit Booléen faible d'algèbres combinatoires directement indécomposables. On étudie la sémantique du λ-calcul dont les modèles sont directement indécomposable comme algèbres combinatoires (sémantique indécomposable); on prouve en particulier que cette sémantique est assez générale pour inclure d'une part les trois sémantiques principales et d'autre part les modèles de termes de toutes les λ-théories semi-sensibles. Par contre, on montre aussi qu'elle est largement incomplète. Finalement, on étudie la question de l'existence d'un modèle non-syntaxique du λ-calcul appartenant aux sémantiques principales et ayant une théorie équationnelle ou inéquationnelle r.e. (récursivement énumérable). Cette question est une généralisation naturelle du problème de Honsell et Ronchi Della Rocca (ouvert depuis plus que vingt ans) concernant l'existence d'un modèle continu de λβ ou λβη. On introduit une notion adéquate de modèles effectifs du λ-calcul, qui couvre en particulier tous les modèles qui ont été introduits individuellement en littérature, 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 λβ ou λβη. 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. En ce qui concerne la sémantique continue de Scott, 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.
31
Blanc, Tomasz. "Propriétés de sécurité dans le lambda-calcul." Phd thesis, Ecole Polytechnique X, 2006. http://pastel.archives-ouvertes.fr/pastel-00002090.
Full textAbstract:
Nous examinons les propriétés de sécurité du lambda-calcul au travers du prisme du lambda-calcul étiqueté. Les étiquettes expriment dynamiquement la dépendance des termes présents vis-à-vis des réductions passées. Nous montrons que le lambda-calcul étiqueté vérifie la propriété d'irréversibilité des contextes: une fois qu'un contexte est intervenu dans une réduction, il disparaît irréversiblement dans la suite de cette réduction. Nous examinons les propriétés fondamentales de variantes du lambda-calcul étiqueté. Pour cela, nous introduisons une preuve élégante du théorème des développements finis dans la cadre du lambda-calcul par valeur étiqueté. Puis nous prouvons que les étiquettes du lambda-calcul faible expriment le partage. Les étiquettes du lam! bda-calcul permettent d'exprimer des politiques de sécurité telles que l'inspection de pile et la Muraille de Chine. Nous définissons la notion de réduction indépendante de deux principaux A et B: une telle réduction peut se décomposer en deux réductions: une réduction qui ignore A et une réduction qui ignore B. Nous prouvons que la Muraille de Chine garantit cette propriété d'indépendance. Les étiquettes du lambda-calcul permettent aussi d'exprimer la propriété d'interférence: il s'agit ici d'identifier les sous-termes d'un terme M qui influencent le résultat de la réduction de M. Dans le lambda-calcul muni de références, en plus de l'interférence fonctionnelle déjà présente dans le lambda-calcul pur, on identifie l'interférence de mémoire due à l'utilisation des référe! nces. Les étiquettes permettent d'identifier les int! ervalles de temps pendant lesquels une référence influence le résultat d'une réduction.
32
Pino, Pérez Ramón. "Contribution a l'etude du lambda-calcul partiel." Paris 7, 1992. http://www.theses.fr/1992PA077153.
Full textAbstract:
Le lambda calcul-partiel est un formalisme qui se situe entre le lambda-calcul et le lambda-calcul par valeur. Il est mieux adapte a l'etude de l'equivalence de programmes ou le mecanisme d'evaluation est l'appel par valeur, ce qui est le cas de la plupart des langages fonctionnels existants. Nous etudions des proprietes syntaxiques et semantiques du lambda-calcul ainsi que des rapports entre ce dernier et d'autres formalismes tels que les algebres combinatoires partielles et la logique categorique combinatoire partielle. Un theoreme de decidabilite concernant une sous-theorie du lambda-calcul partiel, des theoremes d'equivalence et plusieurs methodes de construction des modeles sont les resultats principaux de ce travail
33
Battyanyi, Péter. "Propriétés de normalisation de calculs logiques symétriques." Chambéry, 2007. http://www.theses.fr/2007CHAMS038.
Full textAbstract:
Dans cette thèse quelques-uns des calculs ont été étudiés qui peuvent être mis en rapport avec la logique classique à l'aide de l'isomorphisme de Curry-Howard. On étudie tout d'abord le λμ-calcul simplement typé de Parigot. Parigot a prouvé que son calcul est fortement normalisable. Ensuite, David et Nour ont donné une preuve arithmétique de la normalisation forte du λμμ'-calcul. Cependant, si l'on ajoute au λμμ'-calcul la règle ρ de simplification, la normalisation forte est perdue. On montre que le μμ'ρ-calcul non-typé est faiblement normalisable et que le λμμ'ρ-calcul typé est aussi faiblement normalisable. On établit ensuite une borne de la longueur des séquences de réductions en λμρθ-calcul simplement typé. Ce résultat est une extension de celui de Xi pour le λ-calcul simplement typé. Dans le chapitre suivant on présente une preuve arithmétique de la normalisation forte du λ-calcul symétrique de Berardi et Barbanera. Enfin, on établit des traductions entre le λ-calcul symétrique de Berardi et Barbanera et le λμ*-calcul, qui est le calcul de Curien et Herbelin étendu avec une négation, de telle manière que la normalisation forte d'un de ces calculs implique celle de l'autreThis thesis examines, from proof theoretical point of view, some of the calculi which can be related to classical logic by the Curry-Howard isomorphism. First of all, we study the simply typed λμ-calculus defined by Parigot. Parigot proved that the λμ-calculus is strongly normalizing. David and Nour showed that the strong normalization is preserved for the λμμ'-calculus also. This is no more true if we add the ρ-rule to the λμμ'-calculus. However, the weak normalization still holds. We prove that the untyped μμ'ρ calculus as well as the typed λμμ'ρ-calculus are weakly normalizing. Next, a bound for the lengths of the reduction sequences in the simply typed λμρθ-calculus is established, extending a result of Xi stated for the simply typed λ-calculus. Then we give an arithmetical proof for the strong normalization of the simply typed symmetric λ-calculus defined by Berardi and Barbanera. Finally, we define a translation between the simply typed symmetric λ-calculus and an extension of the λμ*-calculus of Curien and Herbelin in such a way that the strong normalization of one of the calculi implies that of the other one
34
Curzi, Gianluca. "Non-laziness in implicit computational complexity and probabilistic λ-calculus." Thesis, Université de Paris (2019-....), 2020. http://www.theses.fr/2020UNIP7010.
Full textAbstract:
Cette thèse explore les avantages de la “non-paresse” dans la Complexité Computationnelle implicite et dans le lambda calcul probabiliste. Plus précisément, cette thèse peut être divisée en deux parties principales. Dans la première, nous étudions dans tous les sens les mécanismes d’effacement et de duplication linéaire, qui nous conduisent aux systèmes de typage LEM (Lin- early Exponential Multiplicative Type Assignment) et LAM (Linearly Additive Multiplicative Type Assignment). Le premier est capable d’exprimer des versions plus faibles des règles exponentielles de la Logique Linéaire, tandis que le second est doté de règles additifs plus faibles, appelées additifs linéaires. Ces systèmes bénéficient respectivement d’une élimination de coupure cubique et d’un résultat de normalisation linéaire. Étant donné que les additifs linéaires ne nécessitent pas d’évaluation paresseuse pour éviter l’explosion exponentielle de la normalisation (contraire- ment aux additifs standard), ils peuvent être utilisés pour obtenir une caractérisation implicite des fonctions calculables en temps polynomial probabiliste qui ne dépend pas du choix de la stratégie de réduction. Ce résultat a été réalisé dans STA, un système obtenu en dotant STA (Soft Type Assignment) d’une formulation aléatoire des additifs linéaires, qui capture aussi les classes de complexité PP et BPP. La deuxième partie de la thèse est centrée sur le lambda calcul probabiliste doté d’une sémantique opérationnelle basée sur la réduction de tête, c’est-à-dire une politique d’évaluation non paresseuse d’appel par nom. Nous prouvons que la bisimilarité probabiliste est “fully abstract” par rapport à l’équivalence observationnelle. Ce résultat témoigne le pouvoir discriminant de la non-paresse, qui permet de retrouver une correspondance parfaite entre les deux équivalences qui manquait dans le cadre paresseux. De plus, nous montrons que la similarité probabiliste est correcte mais pas complète par rapport au préordre observationnelThis thesis explores the benefits of non-laziness in both Implicit Computational Complexity and probabilistic computation. More specifically, this thesis can be divided in two main parts. In the first one, we investigate in all directions the mechanisms of linear erasure and duplication, which lead us to the type assignment systems LEM (Linearly Exponential Multiplicative Type Assignment) and LAM (Linearly Additive Multiplicative Type Assignment). The former is able to express weaker versions of the exponential rules of Linear Logic, while the latter has weaker additive rules, called linear additives. These systems enjoy, respectively, a cubic cut-elimination and a linear normalization result. Since linear additives do not require a lazy evaluation to avoid the exponential blow up in normalization (unlike the standard additives), they can be employed to obtain an implicit characterization of the functions computable in probabilistic polynomial time that does not depend on the choice of the reduction strategy. This result is achieved in STA⊕, a system that extends STA (Soft Type Assignment) with a randomized formulation of linear additives. Also, this system is able to capture the complexity classes PP and BPP. The second part of the thesis is focused on the probabilistic λ-calculus endowed with an operational semantics based on the head reduction, i.e. a non-lazy call-by-name evaluation policy. We prove that probabilistic applicative bisimilarity is fully abstract with respect to context equivalence. This result witnesses the discriminating power of non-laziness, which allows to recover a perfect match between the two equivalences that was missing in the lazy setting. Moreover, we show that probabilistic applicative similarity is sound but not complete for the context preorder
35
Diepenveen, Emily. "Relational models of the lambda calculus." Thesis, University of Ottawa (Canada), 2008. http://hdl.handle.net/10393/27679.
Full textAbstract:
In [7], Ehrhard et al. present a model of the untyped lambda calculus built from an object without enough points in a cartesian closed category MRel. This thesis presents the background needed to construct and understand this model. In particular we describe what it means for models to have enough points and exhibit connections between MRel with various categorical models of lambda calculus in the literature. In particular, we are able to relate the graph model to MRel. We also describe connections with various kinds of Kleisli categories arising from comonads and their associated theory.
36
Henderson, Robert John. "Cumulative learning in the lambda calculus." Thesis, Imperial College London, 2013. http://hdl.handle.net/10044/1/24759.
Full textAbstract:
I design a machine learning system capable of 'cumulative learning', which means that it automatically acquires the knowledge necessary for solving harder problems through experience of solving easier ones. Working within the learning framework of inductive programming, I propose that the technique of abstraction, familiar from software engineering, is a suitable mechanism for accumulating knowledge. In abstraction, syntactic patterns in solutions to past problems are isolated as re-usable units and added to background knowledge. For the system's knowledge representation language, I argue that lambda calculus is a more suitable choice than first-order logic because lambda calculus supports abstraction readily. However, more mature and theoretically well-founded base inference techniques are available within first-order Inductive Logic Programming (ILP). Therefore, my approach is to adapt ILP inference techniques to lambda calculus. Central to ILP is the idea of 'generality', and I show that a suitable concept of generality in lambda calculus arises from its standard denotational semantics. Consequently, notions of entailment, subsumption, refinement, and inverse deduction have direct analogues in the lambda calculus setting. I argue that the conventional 'compression' measure used in ILP is inflexible in capturing prior assumptions, particularly in the context of an expanding background knowledge. Instead I introduce a non-parametric Bayesian prior over hypotheses and background knowledge. I then design an inductive inference algorithm for the lambda calculus setting based on refinement and proof-directed search. I give a formal proof of correctness of this algorithm. To enable automatic invention of abstractions, I design two algorithms. The first is a heuristic search that uses anti-unification to discovering opportunities for abstraction within a corpus of knowledge. I give a formal characterisation of its search space. The second algorithm performs inverse deduction in order to refactor knowledge in terms of an abstraction. I prove that this refactoring process is semantics-preserving.
37
Manzonetto, Giulio <1980>. "Models and theories of lambda-calculus." Doctoral thesis, Università Ca' Foscari Venezia, 2008. http://hdl.handle.net/10579/575.
Full text
38
Souza, João Nunes de. "Representação de conhecimento utilizando o 'lambda'-calculo tipado." [s.n.], 1989. http://repositorio.unicamp.br/jspui/handle/REPOSIP/261197.
Full textAbstract:
Orientador: Wagner Caradori do AmaralTese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica
Made available in DSpace on 2018-07-15T16:56:04Z (GMT). No. of bitstreams: 1 Souza_JoaoNunesde_D.pdf: 12097520 bytes, checksum: 6aa96dc3547fd563a0ed50eb97d3a98c (MD5) Previous issue date: 1989
Resumo: Neste trabalho propõe-se um estudo da representação hierárquica de conhecimento a partir dos conceitos básicos do 'lambda¿-cálculo tipado. A representação do conhecimento é feita por programas funcionais definidos como conjuntos de fórmulas do 'lambda¿-cálculo tipado. Os conjuntos de fórmulas são associados a critérios de derivação que determinam os argumentos das funções dos programas. estabelecendo o seqüenciamento da execução destas funções e possibilitando a derivação de novos conhecimentos. Propõe-se um conjunto de relações de complexidade entre as fórmulas do 'lambda¿-cálculo tipado. que se baseia em uma classificação destas fórmulas. A classificação se fundamenta na estrutura sintática dos símbolos para tipo associados às fórmulas. A ordem dos símbolos para tipo determina relações de ordem entre as fórmulas do 'lambda¿-cálculo tipado, definindo as relações de complexidade. As relações de complexidade são utilizadas em uma representação sintática das relações hierárquicas de complexidade do conhecimento representado em um sistema. Demonstra-se um conjunto de condições necessárias ... Observação: O resumo, na íntegra, poderá ser visualizado no texto completo da tese digital
Abstract: A knowledge hierarchic representation based on the typed 'lambda¿-calculus foundat ions is proposed in this work. The knowledge representation is based in functional programms defined as typed h-calculus formulas set. The formulas set is associated to derivation criterias that determines the programms functions arguments and the execution function sequence. A typed 'lambda¿-calculus formulas complexity relationship based on a typed h-calculus formulas classification is proposed. The classification is based on the formulas and type simbols sintat ic structure. The type simbols orders determines typed 'lambda¿-calculus formulas order relations wich define the complexity relationship. The complexity relationship is used to represent a sintatic representation of a knowledge system hierarchic relationship complexity ... Note: The complete abstract is available with the full electronic digital thesis or dissertations
Doutorado
Doutor em Engenharia Elétrica
39
Faure, Germain. "Structures et modèles de calculs de réécriture." Phd thesis, Université Henri Poincaré - Nancy I, 2007. http://tel.archives-ouvertes.fr/tel-00164576.
Full textAbstract:
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 équationnelle a priori arbitraire. L'agrégation est utilisée pour collecter les différents résultats possibles.
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.
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.
Nous examinons ensuite les modèles catégoriques du
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.
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
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.
40
Saber, Khelifa. "Etude d’un Lambda-calcul issu d’une logique classique." Chambéry, 2007. http://www.theses.fr/2007CHAMS015.
Full textAbstract:
Le llm ÙÚ- calcul est une extension du l-calcul associée à la déduction naturelle classique où sont considérés tous les connecteurs. Les principaux résultats de cette thèse sont : -La standardisation, la confluence et une extension de la machine de J. -L. Krivine en lmÙÚ-calcul. -Une preuve sémantique de la forte normalisation du théorème d'élimination des coupures. -Une sémantique de réalisabilité pour Ie calcul qui permet de caractériser Ie comportement calculatoire de certains termes types. -Un théorème de complétude pour Ie lmÙÚ-calcul simplement typé. -Une introduction et un lmÙÚ-calcul par valeur confluentThe lmÙÚ-calculus is an extension of the l-calculus associated to the full classical natural deduction. The main results of this thesis are : -A standardization theorem, the confluence theorem, and an extension of J. -1. Krivine machine to the lmÙÚ-calculus. -A semantical proof of the strong normalization theorem of the cut elimination procedure. -A semantics of realizability for the lmÙÚ-calculus and characterization of the operational behavior of some closed typed terms. -A completeness theorem for the simply typed lm-calculus. -A confluent call-by-value lmÙÚ-calculus
41
Leventis, Thomas. "Lambdas-théories probabilistes." Thesis, Aix-Marseille, 2016. http://www.theses.fr/2016AIXM4085/document.
Full textAbstract:
Le lambda-calcul est un formalisation de la notion de calcul. Dans cette thèse nous nous intéresserons à certaines variantes non déterministes, et nous nous pencherons plus particulièrement sur le cas probabiliste.L'étude du lambda-calcul probabiliste n'est pas nouvelle, mais les travaux précédents considéraient le comportement probabiliste comme un effet de bord. Notre objectif est de présenter ce calcul d'une manière plus équationnelle, en intégrant le comportement probabiliste à la réduction.Tout d'abord nous définissons une sémantique opérationnelle déterministe et contextuelle pour le lambda-calcul probabiliste en appel par nom. Afin de traduire la signification de la somme nous définissons une équivalence syntaxique dans notre calcul, dont nous démontrons qu'il ne déforme pas la réduction: considérer une réduction modulo équivalence revient à considérer simplement le résultat du calcul modulo équivalence. Nous prouvons également un résultat de standardisation.Dans ce cadre nous définissons une notion de théorie équationnelle pour le lambda-calcul probabiliste. Nous étendons certaines notions usuelles, et en particulier celle de bon sens. Cette dernière se formalise facilement dans un cadre déterministe mais est bien plus complexe dans le cas probabiliste.Pour finir nous prouvons une correspondance entre l'équivalence observationnelle, l'égalité des arbres de Böhm et la théorie cohérente sensée maximale. Nous définissons une notion d'arbres de Böhm probabilistes dont nous prouvons qu'elle forme un modèle. Nous démontrons ensuite un résultat de séparabilité disant que deux termes avec des arbres de Böhm distincts ne sont pas observationnellement équivalentsThe lambda-calculus is a way to formalize the notion of computation. In this thesis we will be interested in some of these variants introducing non deterministim, and we will focus mostly on a probabilistic calculus.The probabilistic lambda-calculus has been studied for some time, but the probabilistic behaviour has always been treated as a side effect. Our purpose is to give a more equational representation of this calculus, by handling the probabilities inside the reduction rather than as a side effect.To begin with we give a deterministic and contextual operational semantics for the call-by-name probabilistic lambda-calculus. To express the probabilistic behaviour of the sum we introduce a syntactic equivalence in our calculus, and we show it has little consequence on the calculus: reducing modulo equivalence amount to reducing and then looking at the result modulo equivalence. We also prove a standardization theorem.Then using this operational semantics we define a notion of equational theories for the probabilistic lambda-calculus. We extend some usual notions to this setting, and in particular the sensibility of a theory. This notion is quite simple in a deterministic setting but becomes more complicated when we have a probabilistic computation.Finally we prove a generalization of the equality between the observational equivalence, the Böhm tree equality and the maximal coherent sensible lambda-theory. We give a notion of probabilistic Böhm trees, and prove that this forms a model of the probabilistic lambda-calculus. Then we prove a separability result stating that two terms with different Böhm trees are separable, i.e. are not observationally equivalent
42
Alberti, Michele. "On operational properties of quantitative extensions of lambda-calculus." Thesis, Aix-Marseille, 2014. http://www.theses.fr/2014AIXM4076/document.
Full textAbstract:
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 paresseuseIn 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
43
Ker, Andrew D. "Innocent game models of untyped lambda calculus." Thesis, University of Oxford, 2000. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.365708.
Full text
44
Watson, Paul. "The parallel reduction of lambda calculus expressions." Thesis, University of Manchester, 1986. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.377690.
Full text
45
Staursky, Joseph N. "Lambda Calculus for Binary Security and Analysis." University of Cincinnati / OhioLINK, 2021. http://rave.ohiolink.edu/etdc/view?acc_num=ucin161710963374672.
Full text
46
Silvia, Gilezan. "Intersection types in lambda calculus and logic." Phd thesis, Univerzitet u Novom Sadu, Prirodno-matematički fakultet u Novom Sadu, 1993. https://www.cris.uns.ac.rs/record.jsf?recordId=73293&source=NDLTD&language=en.
Full text
47
RIOS, ALEJANDRO. "Contributions a l'etude des lambda-calculs avec substitutions explicites." Paris 7, 1993. http://www.theses.fr/1993PA077091.
Full textAbstract:
Le lambda-sigma-calcul (ls) a deux sortes de termes: terme propre et substitution. Le ls-calcul est confluent sur les termes clos, mais il n'est pas localement confluent sur tous les termes. La confluence locale est atteinte en ajoutant quatre regles. Le calcul ainsi obtenu est appele lsp, et sa non-confluence sur la totalite des termes a ete recemment montree. Cependant, le lsp-calcul et le lsp-calcul extensionnel sont confluents sur l'ensemble des termes semi-clos (ceux qui n'admettent que de variables de sorte terme propre). Ces resultats sont obtenus en utilisant la methode d'interpretation; pour l'appliquer, la normalisation forte du sp-calcul de substitutions associe est necessaire. Une nouvelle technique est developpee pour l'assurer. Dans le cadre type, on introduit une interpretation du ls-calcul type du premier ordre dans le lambda-calcul, pour laquelle la correction et la completude sont etablies. La normalisation forte du tau-calcul est un probleme ouvert. Un premier pas est franchi en montrant la normalisation faible. Le lambda-nu-calcul (ln) traite la substitution explicite en abandonnant la notation de de bruijn. La correction de ln ne peut etre obtenue qu'en imposant des restrictions aux variables du terme de depart. On introduit une condition et une strategie de reduction qui la preserve, pour laquelle ln est correct et confluent modulo alpha-conversion
48
BASTONERO, OLIVIER. "Modeles fortement stables du lambda-calcul et resultats d'incompletude." Paris 7, 1996. http://www.theses.fr/1996PA077170.
Full textAbstract:
La semantique fortement stable donne de nouveaux modeles du lambda-calcul. Une construction d'objets reflexifs est donnee, celle-ci s'inscrit dans le cadre des hypercoherences. La classe de modeles obtenue est la classe des i-modeles fortement stables. On montre ensuite que les classes des modeles continus, stables et fortement stables sont incompletes vis a vis des lambda theories. Enfin on etablit l'incomparabilite des ensembles des theories engendrees par ces classes
49
ZYLBERAJCH, CECILE. "Syntaxe et semantique de la facilite en lambda-calcul." Paris 7, 1991. http://www.theses.fr/1991PA077272.
Full textAbstract:
Un terme clos du lambda-calcul est dit facile s'il peut etre egalise sans contradiction a un terme clos arbitraire. Cette notion a ete introduite par jacopini et venturini-zilli. Il existe un lien entre ce probleme qui porte sur le lambda-calcul pur et les proprietes de certains types recursifs simples. Une etude de ces types revele certaines proprietes syntaxiques des termes qui leur sont associes. En particulier un argument syntaxique base sur une methode de jacopini et venturini-zilli permet de caracteriser des familles de termes faciles. Sous leur aspect semantique ces liens sont etablis par un critere semantique de facilite, obtenu en generalisant la construction utilisee par baeten et boerboom pour prouver semantiquement la facilite du terme non resoluble bien connu omega. En fait tous les termes satisfaisant ce critere sont simultanement egalisables sans contradiction a un meme terme clos arbitraire. Ceci conduit a la notion d'ensemble facile; un ensemble de lambda-termes est facile si tous ses elements peuvent etre simultanement egalises, sans contradiction, a un meme terme clos arbitraire; et a la construction d'un ensemble facile infini
50
Pardon, Aurélien. "Théories symétriques monoïdales closes, applications au lambda-calcul et aux bigraphes." Thesis, Lyon, École normale supérieure, 2011. http://www.theses.fr/2011ENSL0622.
Full textAbstract:
En se fondant sur les travaux de Trimble et al., puis Hughes, on donne une notion de théorie symétrique monoïdale close (smc) et une construction explicite de la catégorie smc engendrée, formant ainsi une adjonction entre théories et catégories. On étudie les exemples du lambda-calcul pur linéaire, du lambda-calcul pur standard, puis des bigraphes de Milner. À chaque fois on donne une théorie smc et on compare la catégorie smc engendrée avec la présentation standard. Entre autres, dans les trois cas, on montre une équivalence entre les deux sur les termes closFrom the work of Trimble et al. and Hughes, we define a notion of symmetric monoidal closed (smc) theory and give an explicit construction of the smc category generated by it. This construction yields a monadic adjunction between smc theories and smc categories. We study in our algebraic framework different models of programming languages: the linear λ-calculus, the pure λ-calculus and Milner's bigraphs. For each model, we give a smc theory and compare the generated smc category with the standard presentation. We show that, in each case, there is an equivalence on closed terms