Неинтерпретируемая функция - Uninterpreted function
В математической логике , неосмысленные функции или функция символ является тот , который не имеет никакого другого свойства , чем его имя и п-ичная форма. Функциональные символы используются вместе с константами и переменными для образования терминов .
Теория неинтерпретированных функций также иногда называют свободную теорию , потому что она свободно порождена, и , таким образом, свободный объект , или пустой теория , будучи теорией , имеющей пустое множество предложений (по аналогии с исходной алгебры ). Теории с непустым набором уравнений известны как эквациональные теории . Проблема выполнимости свободных теорий решается синтаксической унификацией ; алгоритмы для последнего используются интерпретаторами для различных компьютерных языков, таких как Prolog . Синтаксическая унификация также используется в алгоритмах проблемы выполнимости для некоторых других эквациональных теорий, см. Е-унификация и сужение .
Пример
В качестве примера неинтерпретируемых функций для SMT-LIB, если этот ввод передан решателю SMT :
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
решающая программа SMT вернет «Этот ввод допустим». Это происходит потому, что f это неинтерпретируемая функция (то есть все, что известно о f ее сигнатуре ), поэтому возможно, что f(10) = 1 . Но применив ввод ниже:
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(assert (= (f 10) 42))
решающая программа SMT вернет «Этот ввод неудовлетворителен». Это происходит потому, что хотя f не имеет интерпретации, но невозможно, чтобы он возвращал разные значения для одного и того же ввода.
Обсуждение
Проблема решения для свободных теорий особенно важна, потому что с ее помощью можно свести к минимуму многие теории.
Свободные теории могут быть решены путем поиска общих подвыражений, образующих замыкание конгруэнции . Решатели включают в себя решатели теорий выполнимости по модулю .
Смотрите также
Заметки
Рекомендации
 |
Эта статья, посвященная формальным методам, является незавершенной . Вы можете помочь Википедии, расширив ее . |
