Неинтерпретированная функция

В математической логике функция неинтерпретируемая ^[1] или функциональный символ ^[2] это тот, который не имеет никаких других свойств, кроме имени и n-арной формы. Функциональные символы используются вместе с константами и переменными для формирования термов .

Теорию неинтерпретируемых функций также иногда называют свободной теорией , поскольку она свободно порождается и, таким образом, является свободным объектом , или пустой теорией , являющейся теорией , имеющей пустой набор предложений (по аналогии с исходной алгеброй ). Теории с непустым набором уравнений известны как эквациональные теории . Проблема выполнимости свободных теорий решается путем синтаксической унификации ; алгоритмы для последнего используются интерпретаторами различных компьютерных языков, например Пролога . Синтаксическая унификация также используется в алгоритмах решения проблемы выполнимости некоторых других эквациональных теорий, см. Унификация (информатика) .

Пример

В качестве примера неинтерпретируемых функций для 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, будучи функцией, никогда не может возвращать разные значения для одного и того же ввода.

Обсуждение

Проблема принятия решений для свободных теорий особенно важна, поскольку с ее помощью можно редуцировать многие теории. ^[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 .

Эта формальным методам, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее .

[1] Брайант, Рэндал Э.; Лахири, Шувенду К.; Сешиа, Санджит А. (2002). «Моделирование и проверка систем с использованием логики контрарифметики с лямбда-выражениями и неинтерпретируемыми функциями» (PDF) . Компьютерная проверка . Конспекты лекций по информатике. Том. 2404. стр. 78–92. дои : 10.1007/3-540-45657-0_7 . ISBN 978-3-540-43997-4 . S2CID 9471360 .

[2] Баадер, Франц ; Нипков, Тобиас (1999). Переписывание терминов и все такое . Издательство Кембриджского университета. п. 34. ISBN 978-0-521-77920-3 .

[3] де Моура, Леонардо; Бьёрнер, Николай (2009). Формальные методы: основы и приложения: 12-й Бразильский симпозиум по формальным методам, SBMF 2009, Грамаду, Бразилия, 19–21 августа 2009 г.: переработанные избранные статьи (PDF) . Берлин: Шпрингер. ISBN 978-3-642-10452-7 .

[1]

[2]

[3]