Existe-t-il des langages de programmation (ou logique) qui peuvent implémenter (ou exprimer) une fonction si et seulement si est une fonction bijective calculable? ff:N→Nf:N→Nf:\mathbb{N}\to
J'ai essayé de résoudre l'exercice suivant mais je suis resté coincé en essayant de trouver toutes les paires critiques . J'ai les questions suivantes: Comment savoir quelle paire critique a produit une nouvelle règle? Comment savoir si j'ai trouvé toutes les paires critiques? Soit où est binaire,...
Dans les méta-mathématiques de Chaitin ! The Quest For Omega , il parle brièvement du 10ème problème de Hilbert. Il dit ensuite que toute équation diophantienne peut être changée en deux polynômes égaux avec des coefficients entiers positifs: p = 0p = 0p=0p=0 .p = 0⟺p1= p2p=0⟺p1=p2p=0 \iff p_1 =...
Selon Peter Selinger , le Lambda Calculus est algébrique (PDF). Au début de cet article, il dit: L'interprétation combinatoire du calcul lambda est connue pour être imparfaite, car elle ne satisfait pas à la règle ξξξ : selon l'interprétation, M=NM=NM = N n'implique pas λx.M=λx.Nλx.M=λx.N\lambda...
En ce qui concerne le thread Prouvant que la conversion de CNF en DNF est NP-Hard (et un thread Math connexe ): Que diriez-vous de l'autre direction, de DNF à CNF? Est-ce facile ou difficile? À la page 2 de cet article , ils semblent suggérer que les deux directions sont également difficiles quand...
J'ai posté ceci sur MathUnderflow mais je n'ai reçu aucune réponse, alors j'ai pensé l'essayer ici, Je lis l'ancien article de Rabin et Fischer [publiera un lien si possible] où, entre autres, la complexité doublement exponentielle de l'arithmétique Presburger est prouvée. La preuve repose sur...
Dans Girard's Proofs and Types, nous pouvons lire: D'un point de vue algorithmique, le calcul séquentiel n'a pas d'isomorphisme de Curry-Howard, en raison de la multitude de façons d'écrire la même preuve. Cela nous empêche de l'utiliser comme un -calculus typé, bien que nous apercevions une...
J'ai récemment discuté avec un ami d'un site Web qui proposait des défis d'expression régulière, correspondant principalement à un groupe de mots avec une propriété spéciale. Il cherchait une expression régulière qui correspond à des chaînes comme ||||||||où le nombre de |est premier. Je lui ai...
Dans l'article de Chris Okasaki « Aplatir les combinateurs: survivre sans parenthèses », il montre que deux combinateurs sont à la fois suffisants et nécessaires comme base pour coder des expressions complètes de Turing sans avoir besoin d'un opérateur d'application ou de parenthèses. Comparé aux...
On sait que les logiques temporelles LTL, CTL, CTL * peuvent être traduites / intégrées dans le μμ\mu-calcul. En d'autres termes, le (modal)μμ\mu-calculus subsume ces logiques, (c'est-à-dire qu'il est plus expressif.) Pourriez-vous s'il vous plaît m'expliquer / pointer vers des articles / livres...
J'essaie de m'enseigner différentes approches de la vérification logicielle. J'ai lu quelques articles. Pour autant que je sache, la logique propositionnelle avec le temporel utilise généralement la vérification de modèle avec des solveurs SAT (dans les systèmes en cours - réactifs), mais qu'en...
Il existe donc un algorithme pour convertir les termes de calcul lambda en logique combinatoire à l'aide de combinateurs SK. Il produit des choses qui explosent en taille. J'aimerais en savoir plus sur cette explosion de taille. Je n'arrive pas à penser à un meilleur algorithme cependant. J'ai...
Il est bien connu que chaque fonction booléenne peut être réalisée en utilisant un circuit booléen de profondeur 2 (sur les variables, leur négation et leurs valeurs constantes) contenant des portes ET au premier niveau et une seule porte OU au niveau supérieur; c'est simplement la représentation...
J'aimerais en savoir plus sur la programmation concaténative à travers la création d'un petit langage simple, basé sur la pile et suivant le paradigme concaténatif. Malheureusement, je n'ai pas trouvé beaucoup de ressources concernant les langages concaténatifs et leur mise en œuvre, alors...
Comme il existe un calcul lambda non typé et un calcul lambda simplement tapé (comme décrit, par exemple, dans le livre Types et langages de programmation de Benjamin Pierce), existe-t-il une logique combinatoire simplement tapée? Par exemple, il semblerait que les types naturels des combinateurs...
Donné n∈Nn∈Nn \in \mathbb{N} et p,q∈N[x1,…,xn]p,q∈N[x1,…,xn]p,q \in \mathbb{N}[x_1,\ldots,x_n] on peut définir la formule suivante dans le langage de l'arithmétique formelle φ(n,p,q)=∀x1⋯∀xn:¬(p(x1,…,xn)=q(x1,…,xn))φ(n,p,q)=∀x1⋯∀xn:¬(p(x1,…,xn)=q(x1,…,xn))\varphi(n,p,q) = \forall x_1 \cdots \forall...
La satisfiabilité générale (à quelques exceptions telles que les clauses de Horn) ne semble pas avoir de solution algorithmique. Cependant, l'algorithme suivant semble être une solution pour la satisfiabilité générale. Quel est exactement le défaut de l'algorithme suivant? Laisser WWW être un...
Je comprends ce que c'est, mais je ne vois pas à quoi ça sert les algorithmes ou quoi que ce soit. Peut-être que je manque quelque chose. J'ai besoin que quelqu'un me donne un exemple de la façon dont il peut être utilisé pour que je puisse mieux le
Imaginons que nous ayons une formule satisfaisante Le problème à résoudre est "Y a-t-il une affectation pour les variables qui fera F insatisfaisant? ". Une façon de résoudre est de trouver toutes les solutions pour F en termes de variables et si le nombre est < , la solution manquante sera la...
Comme défini par Wikipedia, (La correspondance Curry-Howard) est une généralisation d'une analogie syntaxique entre les systèmes de logique formelle et les calculs computationnels qui a été découverte pour la première fois par le mathématicien américain Haskell Curry et le logicien William Alvin...