En lógica matemática , una función no interpretada [1] o símbolo de función [2] es una 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 también se denomina a veces teoría libre , porque se genera libremente y, por lo tanto, es un objeto libre , o teoría vacía , siendo la teoría que tiene un conjunto vacío de oraciones (en analogía con un álgebra inicial ). Las teorías con un conjunto no vacío de ecuaciones se conocen como teorías ecuacionales . El problema de satisfacibilidad de las teorías libres se resuelve mediante unificación sintáctica ; los intérpretes de varios lenguajes informáticos utilizan algoritmos para esta última, como Prolog . La unificación sintáctica también se utiliza en algoritmos para el problema de satisfacibilidad de ciertas otras teorías ecuacionales, véase Unificación (informática) .
Como ejemplo de funciones no interpretadas para SMT-LIB , si se proporciona esta entrada a un solucionador SMT :
(declarar-fun f (Int) Int)(afirmar (= (f 10) 1))El solucionador SMT devolvería "Esta entrada es satisfacible". Esto sucede porque fes una función no interpretada (es decir, todo lo que se conoce fes su firma ), por lo que es posible que f(10) = 1. Pero al aplicar la entrada a continuación:
(declarar-fun f (Int) Int)(afirmar (= (f 10) 1))(afirmar (= (f 10) 42))El solucionador SMT devolvería "Esta entrada no se puede satisfacer". Esto sucede porque f, al ser una función, nunca puede devolver valores diferentes para la misma entrada.
El problema de decisión para las teorías libres es particularmente importante, porque muchas teorías pueden reducirse mediante él. [3]
Las teorías libres se pueden resolver buscando subexpresiones comunes para formar el cierre de congruencia . [ aclaración necesaria ] Los solucionadores incluyen solucionadores de teorías de satisfacibilidad módulo .