Каковы ограничения общего функционального программирования? Он не является полным по Тьюрингу, но все еще поддерживает большое количество возможных программ. Существуют ли важные конструкции, которые вы могли бы написать на языке Тьюринга, но не на полном функциональном языке?
И правильно ли говорить, что программы, написанные на полных функциональных языках, могут быть полностью статически проанализированы, в то время как статический анализ на полных по Тьюрингу языках ограничен такими вещами, как проблема остановки? При этом я не имею в виду, что во всех функциональных языках все может быть определено статически, потому что некоторые вещи известны только во время выполнения, но я имею в виду, что в теории программы, написанные на идеальном полном функциональном языке программирования, можно анализировать так, чтобы все, что теоретически может быть определен статически, может быть определен статически. Или все еще существуют неразрешимые проблемы, наследуемые во всех функциональных языках, которые делают статический анализ неполным? Некоторые проблемы всегда будут неразрешимыми, независимо от того, на каком языке они написаны, но меня интересуют такие проблемы, которые унаследованы от языка,
X
, это(identity X)
машина Тьюринга , которая останавливается?» Конечно, это не кажется, оidentity
, но как вы определяете «о»?Если предположить , что функциональный язык позволяет кодировать арифметические операции, есть одна программа , которую вы можете рассчитывать на что не представимы , если это общее , а именно: интерпретатор , написанный в .L LL L L
Доказательством этого факта является по существу теорема Гёделя о неполноте, рассматриваемая через призму соответствия Карри-Ховарда. Напомним, что доказательство непротиворечивости является доказательством того, что ложь не выводима в логической системе. Поскольку CH говорит, что доказательства - это программы, доказательство согласованности, следовательно, является доказательством того, что не существует закрытых программ пустого типа. (Обратите внимание, что нетерминация дает вам простой способ обитания для всех типов, поскольку циклической программе может быть присвоен любой тип, который вам нравится, поскольку он никогда не будет оцениваться как значение.) Таким образом, в общем функциональном языке, самоинтерпретатор для дает доказательство в что каждая программа в завершается, и, следовательно, доказывает, чтоL L LL L L L согласуется. Это как раз то, что исключает теорема Геделя, если вы умеете делать арифметику. Итак, мы знаем, что мы не можем писать самоинтерпретаторы на всех функциональных языках.
Обратная сторона этого, тем не менее, заключается в том, что ограничения на выразительную силу тотальных языков по сути являются ограничениями на выразительную силу самой математики . Например, функции, определяемые в Coq (помощник по проверке), - это те, которые могут быть доказаны вычислимыми с использованием ZFC со счетным количеством недоступных кардиналов. Так что, по сути, любая функция, которую вы могли бы доказать в полном объеме к удовлетворению работающего математика, определяется в Coq.
Обратная сторона обратной стороны - математика сложна! Поэтому нет простого смысла в том, что все языки «полностью анализируемы» - даже если вы знаете, что функция завершается, вам все равно придется проделать большую творческую работу, чтобы доказать, что она обладает желаемым свойством. Например, простое знание того, что функция из списков в списки является полной, не поможет вам доказать, что она является функцией сортировки ....
источник