Неинтерпретированная функция
В математической логике неинтерпретируемая функция [1] или функциональный символ [2] это тот, который не имеет никаких других свойств, кроме имени и n-арной формы. Функциональные символы используются вместе с константами и переменными для формирования термов .
Теорию неинтерпретируемых функций также иногда называют свободной теорией , поскольку она свободно порождается и, таким образом, является свободным объектом , или пустой теорией , являющейся теорией , имеющей пустой набор предложений (по аналогии с исходной алгеброй ). Теории с непустым набором уравнений известны как эквациональные теории . Проблема выполнимости свободных теорий решается путем синтаксической унификации ; алгоритмы для последнего используются интерпретаторами различных компьютерных языков, например Пролога . Синтаксическая унификация также используется в алгоритмах решения проблемы выполнимости некоторых других эквациональных теорий, см. Унификация (информатика) .
Пример [ править ]
В качестве примера неинтерпретируемых функций для SMT-LIB, если эти входные данные передаются решателю SMT :
(объявить-fun f (Int) Int)
(утверждать (= (f 10) 1))
решатель SMT вернет «Этот ввод является выполнимым». Это происходит потому, что f является неинтерпретированной функцией (т.е. всем, что известно о f это его подпись ), поэтому возможно, что f(10) = 1. Но применив ввод ниже:
(объявить-fun f (Int) Int)
(утверждать (= (f 10) 1))
(утверждать (= (f 10) 42))
решатель SMT вернет «Этот ввод неудовлетворителен». Это происходит потому, что f, будучи функцией, никогда не может возвращать разные значения для одного и того же ввода.
Обсуждение [ править ]
Проблема принятия решений для свободных теорий особенно важна, поскольку с ее помощью можно редуцировать многие теории. [3]
Свободные теории могут быть решены путем поиска общих подвыражений для формирования конгруэнтного замыкания . [ нужны разъяснения ] Решатели включают в себя решатели теорий выполнимости по модулю .
См. также [ править ]
Примечания [ править ]
Ссылки [ править ]
- ^ Брайант, Рэндал Э.; Лахири, Шувенду К.; Сешиа, Санджит А. (2002). «Моделирование и проверка систем с использованием логики контрарифметики с лямбда-выражениями и неинтерпретируемыми функциями» (PDF) . Компьютерная проверка . Конспекты лекций по информатике. Том. 2404. стр. 78–92. дои : 10.1007/3-540-45657-0_7 . ISBN 978-3-540-43997-4 . S2CID 9471360 .
- ^ Баадер, Франц ; Нипков, Тобиас (1999). Переписывание терминов и все такое . Издательство Кембриджского университета. п. 34. ISBN 978-0-521-77920-3 .
- ^ де Моура, Леонардо; Бьёрнер, Николай (2009). Формальные методы: основы и приложения: 12-й Бразильский симпозиум по формальным методам, SBMF 2009, Грамаду, Бразилия, 19–21 августа 2009 г.: переработанные избранные статьи (PDF) . Берлин: Шпрингер. ISBN 978-3-642-10452-7 .
 | Эта формальным методам статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее . |