Fonction non interprétée - Uninterpreted function
En logique mathématique , une fonction ou un symbole de fonction non interprété est celui qui n'a pas d'autre propriété que son nom et sa forme n-aire . Les symboles de fonction sont utilisés, avec des constantes et des variables, pour former des termes .
La théorie des fonctions non interprétées est aussi parfois appelée théorie libre , car elle est librement générée, et donc un objet libre , ou la théorie vide , étant la théorie ayant un ensemble vide de phrases (par analogie avec une algèbre initiale ). Les théories avec un ensemble d'équations non vide sont appelées théories équationnelles . Le problème de la satisfiabilité des théories libres est résolu par l' unification syntaxique ; les algorithmes de ces derniers sont utilisés par les interprètes de divers langages informatiques, tels que Prolog . L'unification syntaxique est également utilisée dans les algorithmes pour le problème de satisfiabilité pour certaines autres théories équationnelles, voir E-Unification et Narrowing .
Exemple
À titre d'exemple de fonctions non interprétées pour SMT-LIB, si cette entrée est donnée à un solveur SMT :
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
le solveur SMT renverrait "Cette entrée est satisfaisable". Cela se produit parce que f c'est une fonction non interprétée (c'est-à-dire que tout ce dont on sait f est sa signature ), donc c'est possible f(10) = 1 . Mais en appliquant l'entrée ci-dessous:
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(assert (= (f 10) 42))
le solveur SMT renverrait "Cette entrée n'est pas satisfaisante". Cela se produit parce que bien f n'a pas d'interprétation, mais il est impossible qu'il renvoie des valeurs différentes pour la même entrée.
Discussion
Le problème de la décision pour les théories libres est particulièrement important, car de nombreuses théories peuvent être réduites par lui.
Les théories libres peuvent être résolues en recherchant des sous-expressions communes pour former la fermeture de congruence . Les solveurs incluent les solveurs de théories modulo de satisfiabilité .
Voir également
Remarques
Les références
 |
Cet article relatif aux méthodes formelles est un bout . Vous pouvez aider Wikipedia en le développant . |
