1,721,006 research outputs found
Addressing Machines as models of lambda-calculus
No full textTuring machines and register machines have been used for decades in theoretical computer science as abstract models of computation. Also the lambda-calculus has played a central role in this domain as it allows to focus on the notion of functional computation, based on the substitution mechanism, while abstracting away from implementation details. The present article starts from the observation that the equivalence between these formalisms is based on the Church-Turing Thesis rather than an actual encoding of lambda-terms into Turing (or register) machines. The reason is that these machines are not well-suited for modelling lambda-calculus programs.
We study a class of abstract machines that we call addressing machine since they are only able to manipulate memory addresses of other machines. The operations performed by these machines are very elementary: load an address in a register, apply a machine to another one via their addresses, and call the address of another machine. We endow addressing machines
with an operational semantics based on leftmost reduction and study their behaviour. The set of addresses of these machines can be easily turned into a combinatory algebra. In order to obtain a model of the full untyped lambda-calculus, we need to introduce a rule that bares similarities with the omega-rule and the rule zeta_eta from combinatory logic
A Lambda Calculus Satellite (Invited Talk)
No full textWe shortly summarize the contents of the book "A Lambda Calculus Satellite", presented at the 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Models and theories of lambda calculus
Full text linkA quarter of century after Barendregt's main book, a wealth of interesting problems about models and theories of the untyped lambda-calculus are still open. In this thesis we will be mainly interested in the main semantics of lambda-calculus (i.e., the Scott-continuous, the stable, and the strongly stable semantics) but we will also define and study two new kinds of semantics: the relational and the indecomposable semantics. Models of the untyped lambda-calculus may be defined either as reflexive objects in Cartesian closed categories (categorical models) or as combinatory algebras satisfying the five axioms of Curry and the Meyer-Scott axiom (lambda-models). Concerning categorical models we will see that each of them can be presented as a lambda-model, even when the underlying category does not have enough points, and we will provide sufficient conditions for categorical models living in arbitrary cpo-enriched Cartesian closed categories to have H^* as equational theory. We will build a categorical model living in a non-concrete Cartesian closed category of sets and relations (relational semantics) which satisfies these conditions, and we will prove that the associated lambda-model enjoys some algebraic properties which make it suitable for modelling non-deterministic extensions of lambda-calculus. Concerning combinatory algebras, we will prove that they satisfy a generalization of Stone representation theorem stating that every combinatory algebra is isomorphic to a weak Boolean product of directly indecomposable combinatory algebras. We will investigate the semantics of lambda-calculus whose models are directly indecomposable as combinatory algebras (the indecomposable semantics) and we will show that this semantics is large enough to include all the main semantics and all the term models of semi-sensible lambda-theories, and that it is however largely incomplete. Finally, we will investigate the problem of whether there exists a non-syntactical model of lambda-calculus belonging to the main semantics which has an r.e. (recursively enumerable) order or equational theory. This is a natural generalization of Honsell-Ronchi Della Rocca's longstanding open problem about the existence of a Scott-continuous model of lambda-beta or lambda-beta-eta. Then, we introduce an appropriate notion of effective model of lambda-calculus, which covers in particular all the models individually introduced in the literature, and we prove that no order theory of an effective model can be r.e.; from this it follows that its equational theory cannot be lambda-beta or lambda-beta-eta. Then, we show that no effective model living in the stable or strongly stable semantics has an r.e. equational theory. Concerning Scott-continuous semantics, we prove that no order theory of a graph model can be r.e. and that many effective graph models do not have an r.e. equational theory.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
Models and theories of lambda calculus
No full textIn this paper we briefly summarize the contents of Manzonetto's PhD thesis which concerns denotational semantics and equational/order theories of the pure untyped lambda-calculus. The main research achievements include: (i) a general construction of lambda-models from reflexive objects in (possibly non-well-pointed) categories; (ii) a Stone-style representation theorem for combinatory algebras; (iii) a proof that no effective lambda-model can have lambda-beta or lambda-beta-eta as its equational theory (this can be seen as a partial answer to an open problem introduced by Honsell-Ronchi Della Rocca in 1984)
Models and theories of lambda calculus
No full textIn this paper we briefly summarize the contents of Manzonetto's PhD thesis which concerns denotational semantics and equational/order theories of the pure untyped lambda-calculus. The main research achievements include: (i) a general construction of lambda-models from reflexive objects in (possibly non-well-pointed) categories; (ii) a Stone-style representation theorem for combinatory algebras; (iii) a proof that no effective lambda-model can have lambda-beta or lambda-beta-eta as its equational theory (this can be seen as a partial answer to an open problem introduced by Honsell-Ronchi Della Rocca in 1984)
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
A story of lambda-calculus and approximation
No full textLes arbres de Böhm sont historiquement la première notion d'approximation pour le lambda-calcul, ils ont été introduit dans [Barendregt, 1977] pour le lambda-calcul en Appel-par-Nom. Ils jouissent d'un lien intéressant avec l'autre notion d'approximation qu'est l'expansion de Taylor ([Ehrhard and Regnier, 2003]) : la forme normale de l'expansion de Taylor d'un lambda-terme correspond à l'expansion de Taylor de son arbre de Böhm. La théorie de l'approximation des programmes est beaucoup moins développée pour le lambda -calcul en Appel-par-Valeur. Nous présentons la première notion d'arbre de Böhm dans ce contexte, en utilisant le lambda-calcul Appel-par-Valeur étendu par les règles de permutation de [Carraro and Guerrieri, 2014]. Nous constatons que les lambda-termes avec les mêmes arbres de Böhm sont équivalents observationnellement, et nous caractérisons les ensembles d'approximants qui correspondent aux arbres de Böhm de lambda-termes. Ensuite nous caractérisons la solvabilité en utilisant des approximants plus précis. La connexion entre nos arbres de Böhm et l'expansion de Taylor est légèrement différente du cas Appel-par-Nom : ici la forme normale de l'expansion de Taylor d'un lambda-terme correspond à une version normalisée de l'expansion de Taylor de l'arbre de Böhm de ce terme. Dans la seconde partie de ce travail, nous nous intéressons au lambda-calcul en Appel-par-Nom. Nous introduisons les modèles de graphe catégorifiés dans une sémantique bicatégorique basée sur les distributeurs. Ils peuvent être vus comme une catégorification des modèles relationnels traditionnels et pareillement ils peuvent être présentés comme des systèmes de type intersection. Dans ce cadre, nous prouvons un théorème d'approximation : l'interprétation d'un lambda-terme correspond à la colimite filtrée de l'interprétation de ses approximants i.e. à l'interprétation de son arbre de Böhm. Nos modèles sont sensibles aux preuves : l'interprétation ne contient pas seulement les typages mais les dérivations de type. De cette information supplémentaire, comparé aux modèles traditionnels, nous déduisons un théorème de commutation : la forme normale de la dénotation d'un lambda-terme coïncide avec la dénotation de son arbre de Böhm. D'une dérivation nous trouvons un approximant minimal avec les bon types et environnement et nous montrons qu'une dérivation dans l'interprétation d'un terme M mais pas dans celle d'un autre terme N induit un approximant de M qui n'approxime pas N. Nous en déduisons la caractérisation de la théorie de nos modèles : cette théorie est B, les interprétations de deux lambda-termes sont isomorphes si et seulement si ces termes ont le même arbre de Böhm.Böhm trees are historically the first notion of lambda-calculus approximation, and were introduced in [Barendregt, 1977] for the Call-by-Name lambda-calculus. They enjoy an interesting link with the other notion of approximation that is the Taylor expansion from [Ehrhard and Regnier, 2003]: the normal form of the Taylor expansion of a lambda-term corresponds to the Taylor expansion of its Böhm tree.The theory of program approximation in the Call-by-Value lambda-calculus is far less developed. We present the first notion of Böhm tree in this context, using the Call-by-Value setting enhanced with permutation rules from [Carraro and Guerrieri, 2014]. We observe that the lambda-terms with the same Böhm tree are observationally equivalent and we provide a characterisation on a set of approximants for it to be the Böhm tree of some lambda-term. A refinement of those approximants allows to characterise solvability. The connection between our Böhm trees and the Taylor expansion is slightly different than for the Call-by-Name case: here the normal form of the Taylor expansion of a lambda-term corresponds with the normalised Taylor expansion of the Böhm tree of this term. In the second part of this work, we focus on the Call-by-Name case. We introduce a class of categorified graph models in a distributor-induced bicategorical semantics. Those models can be seen as a categorification of traditional relational models and they can similarly be presented as intersection type systems. We prove an approximation theorem for them: the interpretation of a lambda-term corresponds to the filtered colimit of the interpretations of its approximants i.e. the interpretation of its Böhm tree. Our models are actually proof-relevant: the interpretation does not contain only typings but whole type derivations. This additional information, compared to traditional models, allows to prove a commutation theorem: the normal form of the denotation of a lambda-term coincides with the denotation of its Böhm tree. From a derivation we can reconstruct a minimal approximant with the desired type in the same environment and we demonstrate that any derivation in the interpretation of a lambda-term M but not in the interpretation of another lambda-term N induces an approximant of M but not of N . From this, we deduce the characterisation of the theory of categorified graph models: this theory is B, two lambda-terms have isomorphic interpretations if and only if their Böhm trees are the same
- …
