Función no interpretada - Uninterpreted function
En lógica matemática , una función o símbolo de función no interpretado es uno que no tiene otra propiedad que su nombre y su forma n-aria . Los símbolos de función se utilizan, junto con constantes y variables, para formar términos .
La teoría de funciones no interpretadas a veces también se denomina teoría libre , porque se genera libremente y, por lo tanto, es un objeto libre , o la teoría vacía , ya que la teoría tiene un conjunto vacío de oraciones (en analogía con un álgebra inicial ). Las teorías con un conjunto de ecuaciones no vacías se conocen como teorías de ecuaciones . El problema de la satisfacibilidad de las teorías libres se resuelve mediante la unificación sintáctica ; Los intérpretes de varios lenguajes informáticos utilizan algoritmos para este último, como Prolog . La unificación sintáctica también se usa en algoritmos para el problema de satisfacibilidad para ciertas otras teorías de ecuaciones, ver E-Unificación y Estrechamiento .
Ejemplo
Como ejemplo de funciones no interpretadas para SMT-LIB, si esta entrada se proporciona a un solucionador SMT :
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
el solucionador SMT devolvería "Esta entrada es satisfactoria". Eso sucede porque f es una función no interpretada (es decir, todo lo que se conoce f es su firma ), por lo que es posible que f(10) = 1 . Pero aplicando la entrada a continuación:
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(assert (= (f 10) 42))
el solucionador SMT devolvería "Esta entrada no es satisfactoria". Eso sucede porque aunque f no tiene interpretación, es imposible que devuelva valores diferentes para la misma entrada.
Discusión
El problema de la decisión de las teorías libres es particularmente importante, porque muchas teorías pueden reducirse.
Las teorías libres se pueden resolver buscando subexpresiones comunes para formar el cierre de congruencia . Los solucionadores incluyen solucionadores de teorías de módulo de satisfacibilidad .
Ver también
Notas
Referencias
 |
Este artículo relacionado con métodos formales es un fragmento . Puedes ayudar a Wikipedia expandiéndolo . |
