заголовок длинный, потому что SO не разрешил. Решает ли GHC проблему остановки наполовину? почему-то
Конечно, не собственно проблема остановки, а подзадача конечной памяти.
Я игрался с метапрограммированием а-ля набрав техническое интервью и решил написать интерпретатор brainfuck на уровне типов. Это было достаточно просто, и в течение получаса я перешел от написания интерпретатора к попыткам написать программы, которые зависают от компилятора.
+[+] выполнил столько же, сколько ответы на этот вопрос, который я связал выше, переполнение стека сокращения. Я передал GHC флаг -freduction-depth=0, снова скомпилировал, и мне не хватило памяти. Неудивительно — это создаст очень большую ячейку S (S (S (...(S Z)...))) на ленте.
Реальная проблема, как я решил, состоит в том, чтобы повесить компилятор с ограниченным использованием памяти. Естественно, +[] (или Cons Inc (Cons (Loop Nil) Nil) как тип) был моей первой попыткой. Увеличьте текущую ячейку, затем ничего не делайте, пока текущая ячейка не равна нулю. Я надеялся таким образом избежать создания все больших значений, таких как большая ячейка или длинная лента. Но GHC перехитрил меня здесь:
λ> foo = undefined :: Eval NoHalt BlankTape t => t
λ> :t foo
foo :: t
Компиляция завершилась в мгновение ока, выдав значение forall t. t, которое, я полагаю, имеет смысл как ⊥ в мире, в котором типы являются значениями.
Поэтому я решил немного усложнить петлю. Может быть, GHC может обнаруживать только особенно простые циклы? Но +[+-] и +[><] вели себя одинаково, так что мне пришлось провернуть это на ступеньку выше с помощью очень сложного и дорогого цикла без операций. Остановился на подсчете, вычислении логарифма каждого значения и сбросе счетчика и продолжении выполнения после достижения некоторой степени двойки.
Святая корова, GHC хорош. Максимум, на что могли опереться мои 8 ГБ памяти, — это считать до 64 на каждой итерации, и компиляция завершилась примерно за 20 секунд с тем же результатом, что и раньше. В этот момент я принял поражение.
Оказывается, набор не останавливающихся программ, использующих конечную память, рекурсивно перечислим, поэтому теоретически GHC может обнаружить любую такую программу и остановить ее. И единственные другие программы без остановок используют бесконечную память, поэтому они также не зависают GHC, как я надеялся.
Делает ли это GHC? Даже с UndecidableInstances он невосприимчив к зависанию, не потребляя больше памяти, как постулирует luqui?
Я перевел интерпретатор и программу в шаблоны C++ и наблюдал примерно такое же поведение в GCC, только с ошибкой вместо нижнего значения.
