En lógica matemática , una función no interpretada [1] o símbolo de función [2] es aquella que no tiene otra propiedad que su nombre y su forma n-aria . Los símbolos de funciones 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 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 de ecuaciones no vacío se conocen como teorías ecuacionales . El problema de la satisfacibilidad de las teorías libres se resuelve mediante la unificación sintáctica ; Los algoritmos para este último son utilizados por intérpretes de varios lenguajes informáticos, como Prolog . La unificación sintáctica también se utiliza en algoritmos para el problema de satisfacibilidad de otras teorías ecuacionales; consulte Unificación (informática) .
Como ejemplo de funciones no interpretadas para SMT-LIB , si esta entrada se proporciona a un solucionador SMT :
(declarar-divertido f (Int) Int)(afirmar (= (f 10) 1))el solucionador SMT devolvería "Esta entrada es satisfactoria". 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 aplicando la siguiente entrada:
(declarar-divertido f (Int) Int)(afirmar (= (f 10) 1))(afirmar (= (f 10) 42))el solucionador SMT devolvería "Esta entrada no es satisfactoria". 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 la clausura de congruencia . [ se necesita aclaración ] Los solucionadores incluyen solucionadores de teorías de módulo de satisfacibilidad .