Каковы пределы общего функционального программирования?

19

Каковы ограничения общего функционального программирования? Он не является полным по Тьюрингу, но все еще поддерживает большое количество возможных программ. Существуют ли важные конструкции, которые вы могли бы написать на языке Тьюринга, но не на полном функциональном языке?

И правильно ли говорить, что программы, написанные на полных функциональных языках, могут быть полностью статически проанализированы, в то время как статический анализ на полных по Тьюрингу языках ограничен такими вещами, как проблема остановки? При этом я не имею в виду, что во всех функциональных языках все может быть определено статически, потому что некоторые вещи известны только во время выполнения, но я имею в виду, что в теории программы, написанные на идеальном полном функциональном языке программирования, можно анализировать так, чтобы все, что теоретически может быть определен статически, может быть определен статически. Или все еще существуют неразрешимые проблемы, наследуемые во всех функциональных языках, которые делают статический анализ неполным? Некоторые проблемы всегда будут неразрешимыми, независимо от того, на каком языке они написаны, но меня интересуют такие проблемы, которые унаследованы от языка,

Маттис Стин
источник

Ответы:

16

Это зависит от общего функционального языка .

Этот ответ звучит как отговорка, но ничего более конкретного сказать нельзя. В конце концов, подумайте о любой важной разрешимой программе, которая вас интересует. Напишите программу на вашем любимом языке Тьюринга, чтобы решить ее. Поскольку проблема разрешима, ваша программа остановится на всех входах.

(Возможно, у неразрешимой проблемы могут быть интересные программы, но не такие, которые могут использовать люди, потому что они никогда не смогут ждать достаточно долго, чтобы узнать ответ.)

Теперь определите новый язык таким образом, чтобы он имел только одну действительную программу ввода: программу, которую вы только что написали, с той же семантикой, что и раньше. Он, безусловно, тотален, поскольку все входные данные для всех программ, написанных на нем (из которых есть только одна), всегда заканчиваются.

Этот дешевый трюк на самом деле полезен: язык Coq , например, является полноценным функциональным языком, в котором нет проверки типов программ, если нет подтверждения его завершения. (Если бы вы отказались от этого требования, оно было бы выполнено по Тьюрингу, поэтому единственным препятствием является нахождение доказательства прекращения.)

Я не уверен, что вы подразумеваете под «все, что теоретически может быть определено статически, может быть определено статически»; это звучит тавтологически верно. Тем не менее, тотальные языки не всегда легко анализировать; Вы знаете, что ничто не расходится, что является полезным фактом, но связь между входом и выходом все еще сложна. (В частности, есть еще бесконечно много возможных входных данных, поэтому вы не можете исчерпывающе попробовать их все, даже в теории.)

Пол Стансифер
источник
Спасибо за Ваш ответ. Таким образом, быть тотальным помогает несколько, но это остается очень сложной проблемой. Я имел в виду «все, что теоретически можно определить статически, можно определить статически», так это то, что было бы возможно, чрезвычайно сложно или нет, проанализировать все взаимосвязи между входом и выходом, если бы у вас было достаточно ресурсов для этого. , Или это фундаментальные причины, почему это ограничено? Подобно теореме Райса, доказательство того, что это имеет место для частичных функций. Или я неправильно понимаю теорему Райс?
Маттис Стин
Я думаю, это может зависеть от того, что вы подразумеваете под «отношения». В частности, если вы просто имеете в виду «вход A идет на выход B», это легко определить в общем функциональном языке; просто запустите программу. Но вы, вероятно, заинтересованы в анализе, который говорит что-то о бесконечном классе входных данных.
Пол Стэнсифер
(ой, хит ввести случайно) ... но это открывает еще один глупый трюк, потому что я могу задать неразрешимые вопросы о тождественной функции , если я хочу: «Для некоторых X, это (identity X)машина Тьюринга , которая останавливается?» Конечно, это не кажется, о identity , но как вы определяете «о»?
Пол Стэнсифер
Да, я хочу знать, верно ли это для всех возможных входных значений некоторого определения, а не для отдельных входных данных. Поэтому, если я вас правильно понимаю, вы имеете в виду, что всегда будут возникать неразрешимые вопросы, независимо от того, какой тип языка программирования используется? Хотя некоторые из этих неразрешимых вопросов можно обойти, предотвратив, во-первых, возникновение проблемы, например, общие функциональные языки для решения проблемы остановки? Потому что разве твой вопрос о функции тождества не может быть решен на полном функциональном языке?
Маттис Стин
Да; модифицированная версия проблемы, в которой «машина Тьюринга» заменяется на «выходит из строя после истечения срока гарантии на машину Тьюринга», решается тривиально. Для этих целей довольно проблематично, что проблема остановки - это пример неразрешимой проблемы, когда исследование программ переполнено неразрешимостью.
Пол Стансифер
16

Каковы ограничения общего функционального программирования? Он не является полным по Тьюрингу, но все еще поддерживает большое количество возможных программ. Существуют ли важные конструкции, которые вы могли бы написать на языке Тьюринга, но не на полном функциональном языке?

Если предположить , что функциональный язык позволяет кодировать арифметические операции, есть одна программа , которую вы можете рассчитывать на что не представимы , если это общее , а именно: интерпретатор , написанный в .L LLLL

  1. Доказательством этого факта является по существу теорема Гёделя о неполноте, рассматриваемая через призму соответствия Карри-Ховарда. Напомним, что доказательство непротиворечивости является доказательством того, что ложь не выводима в логической системе. Поскольку CH говорит, что доказательства - это программы, доказательство согласованности, следовательно, является доказательством того, что не существует закрытых программ пустого типа. (Обратите внимание, что нетерминация дает вам простой способ обитания для всех типов, поскольку циклической программе может быть присвоен любой тип, который вам нравится, поскольку он никогда не будет оцениваться как значение.) Таким образом, в общем функциональном языке, самоинтерпретатор для дает доказательство в что каждая программа в завершается, и, следовательно, доказывает, чтоL L LLLLLсогласуется. Это как раз то, что исключает теорема Геделя, если вы умеете делать арифметику. Итак, мы знаем, что мы не можем писать самоинтерпретаторы на всех функциональных языках.

  2. Обратная сторона этого, тем не менее, заключается в том, что ограничения на выразительную силу тотальных языков по сути являются ограничениями на выразительную силу самой математики . Например, функции, определяемые в Coq (помощник по проверке), - это те, которые могут быть доказаны вычислимыми с использованием ZFC со счетным количеством недоступных кардиналов. Так что, по сути, любая функция, которую вы могли бы доказать в полном объеме к удовлетворению работающего математика, определяется в Coq.

  3. Обратная сторона обратной стороны - математика сложна! Поэтому нет простого смысла в том, что все языки «полностью анализируемы» - даже если вы знаете, что функция завершается, вам все равно придется проделать большую творческую работу, чтобы доказать, что она обладает желаемым свойством. Например, простое знание того, что функция из списков в списки является полной, не поможет вам доказать, что она является функцией сортировки ....

Нил Кришнасвами
источник
Спасибо за Ваш ответ. Я читал пост об этой проблеме в веб-блоге Lambda the Ultimate , но некоторые люди в комментариях утверждают, что, хотя невозможно иметь собственный оценщик как обычный явно конструируемый термин, было бы возможно создать работающий оценщик с некоторыми хитростями. Поэтому мне интересно, есть ли проблемы, которые не могут быть решены (или приближены) на полном функциональном языке с некоторыми хитростями обходных путей?
Маттис Стин
Я бы сказал, что самооценка не считается проблемой, потому что она варьируется в зависимости от языка. Проблема «оценить программу на языке X» - это та же проблема, независимо от того, пытаетесь ли вы решить ее на языке X или Y. В частности, если язык X является тотальным функциональным языком, проблема разрешима на каком-то полном функциональном языке. , используя тот же глупый трюк, который я использовал раньше.
Пол Стэнсифер
Нил, кажется, должно быть гораздо проще, чем доказать, что тотальный язык не может поддерживать своего интерпретатора. Я вас неправильно понимаю? С помощью простой диагонализации любой язык с функцией без фиксированных точек не может поддерживать свой собственный интерпретатор (поддерживает ли он арифметику или нет). Аргумент разработан Конором МакБрайдом здесь: mail.haskell.org/pipermail/haskell-cafe/2003-May/004343.html
Том Эллис
@TomEllis: Мой аргумент по сути такой же, как и у Конора. Фактически, его пост уже делает это наблюдение (с характерным остроумием Конора), когда он называет это «аргументом Эпименида / Кантора / Рассела / Куайна / Годеля / Тьюринга».
Нил Кришнасвами