En lógica matemática , una función no interpretada [1] o símbolo de función [2] 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)(afirmar (= (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)(afirmar (= (f 10) 1))(afirmar (= (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. [ cita requerida ]
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 módulo de satisfacibilidad .
Ver también
Notas
Referencias
- ^ Bryant, Randal E .; Lahiri, Shuvendu K .; Seshia, Sanjit A. (2002). "Modelado y verificación de sistemas usando una lógica de contra aritmética con expresiones Lambda y funciones no interpretadas" (PDF) . Verificación asistida por computadora . Apuntes de conferencias en Ciencias de la Computación. 2404 . págs. 78–92. doi : 10.1007 / 3-540-45657-0_7 . ISBN 978-3-540-43997-4.
- ^ Baader, Franz ; Nipkow, Tobias (1999). Reescritura de términos y todo eso . Prensa de la Universidad de Cambridge. pag. 34. ISBN 978-0-521-77920-3.