Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Categories:

Фикспоинт всюду срёт

Посмотрел я на литературу по теме отказа от индукции.

При использовании индукции доказательства получаются короткими, но их нереально найти компьютером. Поэтому есть ACL2 (Boyer-Moore family), который почти в одиночку пытается искать индуктивные доказательства перебором, и все остальные.

Все остальные делятся на индуктивные MLTT-пруверы, неиндуктивные SMT-солверы и нетипизированные пруверы а ля Isabelle (LCF family). MLTT бывают полуавтоматические и ручные. SMT-солверов ручных я не видел.

При отказе от индукции и заодно от PA часто получается даже полная decision procedure в NP. Но доказательства становятся очень длинными и их часто даже не пытаются печатать, не то что составлять руками. Тем не менее попытки что-то достать из солвера и независимо проверить существуют.

Индустрия (aerospace, automotive, transportation, medical, telecom, business information) забила на MLTT, случаи верификации чего-то на Coq на фоне общих усилий по формализации разработки выглядят как "а давайте для смеху". Все пользуют модел-чекеры (которые архитектурно являются специализированными SMT-солверами). Кроме того сертификация идёт путём refinement - т.е. верифицируют не полные требования, а от фонаря дописывают инварианты в надежде что солвер их подтвердит. Ну и в процессе обнаруживают достаточное кол-во багов, разумеется. Короче, гарантии в результате получаются довольно смешными, сплошные звёздочки и мелкий шрифт.

Что в этой связи делать? А хез. Слабых типизированных теорий с короткими доказательствами, которые можно искать полуавтоматически, я не видел пока.

P.S. Идея, что типичный математический аппарат не годится для CS из-за того что разработан был для решения проблем с бесконечностями, и нужно что-то особое, является довольно распространённый. Хороших решений нет, но есть например finite model theory. Но там всё равно общие слова - по сути, если запретить бесконечные модели, пропадает много полезных (математикам, не в разрезе народного хозяйства) свойств.
Tags: programming
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 4 comments