Système formel de Church utilisé en calculabilité, langages de programmation et théorie des preuves pour représenter des fonctions efficaces, des programmes et leur calcul, et des preuves.
Je suis en train de lire sur le calcul lambda pour "apprendre à le connaître". Je le vois comme une forme alternative de calcul par opposition à la machine de Turing. C'est une manière intéressante de faire les choses avec des fonctions / réductions (en gros). Certaines questions continuent à me...
Existe-t-il une relation entre la machine de Turing et le calcul Lambda - ou est-ce qu'ils se sont produits à peu près au même
J'ai trois sous-questions liées, qui sont soulignées par des points dans la liste ci-dessous (non, elles ne pourraient pas être divisées, si vous vous le demandez). Andrej Bauer a écrit ici que certaines fonctions sont réalisables avec une machine de Turing, mais pas avec le lambda-calcul. Une...
Y a-t-il des avantages à calculer la complexité temporelle d'un algorithme utilisant le calcul lambda? Ou existe-t-il un autre système conçu à cet effet? Toute référence serait
Dans l'introduction et l'explication, les classes de complexité P et NP souvent données par la machine de Turing. L'un des modèles de calcul est le lambda-calcul. Je comprends que tous les modèles de calcul sont équivalents (et si nous pouvons introduire n'importe quoi en termes de machine de...
Je lis actuellement " Lambda-Calculus and Combinators " par Hindley et Seldin. Je ne suis pas un expert, mais je me suis toujours intéressé au calcul lambda en raison de son implication dans la programmation fonctionnelle (à commencer par Lisp et SICP, et maintenant avec R et Haskell). Dans "...
Je ne peux pas penser à un tel modèle, peut-être une forme de calcul lambda typé? un automate cellulaire élémentaire? Cela réfuterait presque le «principe d'équivalence informatique» de Wolfram: Presque tous les processus qui ne sont évidemment pas simples peuvent être considérés comme des calculs...
J'ai lu qu'au départ, Church proposait le -calculus dans le cadre de ses postulats de logiqueλλ\lambda (qui est une lecture dense). Mais Kleene a prouvé son "système" incohérent après quoi, Church a extrait des éléments pertinents pour son travail sur la "calculabilité effective" et a abandonné ses...
Dans une catégorie cartésienne ( CCC ), il existe les soi-disant objets exponentielles , écrit . Lorsqu'un CCC est considéré comme un modèle de simplement typé -calcul , un objet exponentielle comme caractérise l'espace de fonction à partir du type type . Un objet exponentiel est introduit par une...
Le CoC serait le point culminant des trois dimensions du Lambda Cube. Cela ne m’apparaît pas du tout. Je pense que je comprends les dimensions individuelles, et la combinaison de deux semble entraîner une union relativement simple (peut-être que je manque quelque chose?). Mais quand je regarde le...
Je sais que la complexité de la plupart des variétés de calculs lambda typés sans la primitive combinateur Y est bornée, c'est-à-dire que seules les fonctions de complexité bornée peuvent être exprimées, la borne devenant plus grande à mesure que l'expressivité du système de types croît. Je...
Existe-t-il un calcul lambda typé où la logique correspondante sous la correspondance de Curry-Howard est cohérente et où il existe des expressions lambda typables pour chaque fonction calculable? Il s'agit certes d'une question imprécise, dépourvue d'une définition précise du «calcul lambda typé»....
Récemment, Dana Scott a proposé le calcul lambda stochastique, une tentative d'introduire des éléments probabilistes dans le calcul lambda (non typé) basé sur une sémantique appelée modèle graphique. Vous pouvez retrouver ses slides en ligne par exemple ici et son article dans Journal of Applied...
Je m'intéresse au concept de "complétude r-Turing", tel que défini par Axelsen et Glück (2011) . Un système est r-Turing complet s'il peut calculer le même ensemble de fonctions qu'une machine de Turing réversible, sans produire de données "poubelles". C'est la même chose que de pouvoir calculer...
Quelqu'un peut-il expliquer brièvement (si c'est possible!) Ou me renvoyer à une référence, résumant les différences entre le calcul lambda non typé et les calculs lambda typés plus courants? Je recherche en particulier des énoncés de leur puissance expressive, des équivalences avec des systèmes...
Dans un récent fil de discussion sur la liste de diffusion d'Agda, la question des lois ηη\eta est apparue, dans laquelle Peter Hancock a fait une remarque stimulante . Ma compréhension est que les lois ηη\eta viennent avec des types négatifs, c'est-à-dire. connecteurs dont les règles...
Je sais qu'il est impossible de décider de l' équivalence pour le calcul lambda non typé. Citant Barendregt, HP Le calcul lambda: sa syntaxe et sa sémantique. Hollande du Nord, Amsterdam (1984). :ββ\beta Si A et B sont des ensembles de termes lambda disjoints et non vides qui sont fermés sous...
Je pense que je ne le comprends pas, mais -conversion me semble être une -conversion qui ne fait rien, un cas particulier de -conversion où le résultat n'est que le terme dans l'abstraction lambda car il n'y a rien à faire, une sorte de conversion inutile.β β βηη\etaββ\betaββ\betaββ\beta Alors...
Cet article suggère qu'il existe des combinateurs (représentant des calculs symboliques) qui ne peuvent pas être représentés par le calcul Lambda (si je comprends bien les
Est-il possible de tester algorithmiquement si un nombre calculable est rationnel ou entier? En d'autres termes, serait-il possible pour une bibliothèque qui implémente des nombres calculables de fournir les fonctions isIntegerou isRational? Je suppose que ce n'est pas possible, et que cela est en...