Что такое «Полное функциональное программирование»?
Википедия говорит следующее:
Total functional programming (also known as strong functional programming, to be contrasted with ordinary, or weak functional programming) is a programming paradigm which restricts the range of programs to those which are provably terminating.
и
These restrictions mean that total functional programming is not Turing-complete. However, the set of algorithms which can be used is still huge. For example, any algorithm which has had an asymptotic upper bound calculated for it can be trivially transformed into a provably-terminating function by using the upper bound as an extra argument which is decremented upon each iteration or recursion.
Также есть Lambda The Ultimate Post о статье о Полное функциональное программирование.
Я не встречал этого до прошлой недели в списке рассылки.
Есть ли еще какие-либо ресурсы, ссылки или какие-либо примеры реализации, о которых вы знаете?
Ха, я никогда не думал об этой тривиальной трансформации. Это довольно круто.
@VinkoVrsalovic, это реализовано в Coq в настоящее время (и было в '08, afaik). Теперь другое дело, используется ли Coq или нет ;-)
Ответы 3
Если я правильно понял, Total Functional Programming означает именно это: Programming with Total Functions. Если я правильно помню свои курсы математики, итоговая функция - это функция, которая определена во всей своей области, а частичная функция - это функция, в определении которой есть «дыры».
Теперь, если у вас есть функция, которая для некоторого входного значения v переходит в бесконечную рекурсию или бесконечный цикл или вообще не завершается каким-либо другим образом, тогда ваша функция не определена для v и, следовательно, частичная, т.е. общее.
Total Functional Programming не позволяет вам написать такую функцию. Все функции всегда возвращают результат для всех возможных входов; и средство проверки типов гарантирует, что это так.
Я предполагаю, что это значительно упрощает обработку ошибок: их нет.
Оборотная сторона уже упоминается в вашей цитате: она не полная по Тьюрингу. Например. Операционная система - это, по сути, гигантский бесконечный цикл. В самом деле, мы не выполняем хочу операционной системы для завершения работы, мы называем такое поведение «сбоем» и кричим об этом на наши компьютеры!
большая вещь, которую это не позволяет, - это безграничная минимизация. Я знаю, что иногда эти стили также позволяют программы, которые никогда не завершаются, поскольку они также могут быть полезны (например, операционные системы). Трудно иметь дело с функциями, которые могут завершиться, поскольку вы не можете знать, даст ли ваша программа ответ (или остановится).
Я не согласен, если вы читаете статью и публикуете, у вас может быть общая функция, которая «работает вечно», это просто коиндуктивно определенная функция, а не индуктивно определенная функция, это именно как, вы бы написали операционную систему, используя этот метод программирования.
@KristopherMicinski означает ли индуктивное рекурсивное? Так коиндуктивный означает корекурсивный? Означает ли это, что полное функциональное программирование по-прежнему позволяет не прекращать работу, проводя различие между данными и кодами?
Индуктивное / рекурсивное различие на самом деле не очень хорошо определено, я различаю их с помощью логической сортировки (например, «Set» против «Prop» в Coq). Полное функциональное программирование допускает отсутствие прекращения с помощью кодовых данных, но только с ограничением, что эти кодовые данные являются продуктивными (т.е. любое конечное наблюдение производит что-то, на что можно «взглянуть»).
Этот ответ фактически неверен. «Функция», которую якобы не может быть записана, не является функцией. Вполне возможно, что для некоторых входных данных конкретный алгоритм обеспечивает бесконечный вычислительный процесс. Многие тотальные языки программирования позволяют конструировать бесконечные процессы путем коиндукции. Операционные системы должны быть полностью коиндуктивными программами, т. Е. Всегда существующими. Тотальный язык программирования может точно объяснить, что такое потенциально бесконечный процесс, выполняемый машиной Тьюринга: он просто не может обещать, что он всегда конечен, потому что это не так. Частичные языки не годятся для обещаний.
Благотворительность - еще один язык, гарантирующий увольнение:
http://pll.cpsc.ucalgary.ca/charity1/www/home.html
Юм - это язык с 4 уровнями. Внешний уровень завершен по Тьюрингу, а самый внутренний уровень гарантирует завершение:
http://www-fp.cs.st-andrews.ac.uk/hume/report/
Хотя это старый вопрос, я думаю, что ни один из ответов до сих пор не упоминает реальный мотивация для полного функционального программирования, а именно:
Если программы являются доказательствами, а доказательства - программами, тогда программы, в которых есть «дыры», не имеют никакого смысла в качестве доказательств и вносят логическую несогласованность.
По сути, если доказательством является программа, можно использовать бесконечный цикл для доказательства что-нибудь. Это действительно плохо и дает большую мотивацию для того, чтобы мы могли полностью программировать. В других ответах, как правило, не учитывается обратная сторона статьи. Хотя языки технически не завершены по Тьюрингу, вы можете восстановить множество интересных программ, используя коиндуктивные определения и функции. Мы очень склонны думать о данных индуктивный, но кодата служит важной цели на этих языках, где вы можете полностью определить определение, которое является бесконечным (и при выполнении реальных вычислений, которые завершаются, вы потенциально можете использовать только конечную часть этого , а может и нет, если вы пишете операционную систему!).
Также следует отметить, что большинство помощников по доказательству работают на этом принципе, например, Coq.
Это правда, что несоответствие дает вашей логической системе AID, но для программистов (а название этой ветки - «программирование») это не конец света. Это просто означает, что вам нужно быть более осторожным, рассуждая о своей системе. Если у вас могут быть неограничивающие условия, тогда вы не можете (обязательно) заменить n - n на 0. (Это стирает эффект завершения, который может быть или не быть кошерным). Однако программисты, как правило, не заботятся о крайних случаях, когда их можно списать. Возможно, такой случай крайне редок или маловероятен, а приложение не является критически важным.
@ Tac-Tics, вы правы, я должен был пояснить, что «логическая несогласованность» не отображается напрямую на «плохую программу» в реалистическом смысле. Вот почему, например, большинство людей не пишут код на Coq: потому что крайние случаи, которые возникают в функциональных спецификациях, часто просто не имеют достаточного значения, чтобы оправдать дополнительное время, потраченное на доказательство всех свойств ваших программ!
Я думаю, что на данный момент это всего лишь идея, не имеющая реализации. Хотя я бы хотел, чтобы меня доказали, что он ошибается Извините, я не проверил сообщение LtU перед тем, как написать ответ, который я удалил.