kouzdra (kouzdra) wrote,
kouzdra
kouzdra

и еще о сложности

Кстати пример из предыдущего поста я придумал в совершенно прикладных целях: лет 10+ назад - как раз когда generics в жабе появились, у нас на работе стояла задача научиться их обрабатывать. И понятно что при ее решении начали вылазить всякие такие вот вещи.

Вылезла и эта - что "в лоб написанный" алгоритм вывода и проверки типов тут довольно очевидным образом попадает на экспоненту. Поскольку реальным требованием было не "понимать любой код на жабе", а понимать тот код, который понимает сановский компилятор - проверил. После выяснения что "у птичек тоже самое" было принято мудрое решение "значит и нафиг проблему"

Так вот тут как ни странно вылезает реальный недостаток неразрешимых языков: сама-то по себе неразрешимость ничему особенно не мешает - но язык оказывается принципиально неопределимым в разумном смысле на уровне описания - что такое корректная программа определяется реализацией.

Для Жабы, Хаскеля или Окамля (да и многих других) это не слишком большой недостаток - поскольку референтная реализация у них одна. Но вообще-то не очень хорошо.

NB: Правда замечу - разрешимость и тут далеко не главная проблема - дыры в перфомансе типа вышеприведенной например ею не накрываются, равно как и вопрос достаточности ресурсов: стандарт ANSI C кстати содержит подробнейший список количественных ограничений на максимальные длинны строк, имен, вложенности инклудов etc etc - и в общем-то это правильно - именно потому что на деле почему именно неоткомпилировалась программа которая должна компилироваться везде - не слишком важно

Но применительно к "традиционным" языкам эти все проблемы достаточно маргинальны.

А вот в поигранках с автоматической верификацией, где плотность подобных проблем "почти везде", ситуация когда "оттранслируется или нет" сильно зависит от того какой proof assistant подцеплен и даже от того, какая его версия используется, уже не слишком приемлема.
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.
  • 5 comments