Языки программирования для эффективных вычислений

32

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

Например, для чего-то вроде : возьмите свой любимый язык программирования, и после того, как вы напишите свою программу (соответствующую Turing Machine ), добавьте три значения в заголовок: целое число и целое число и вывод по умолчанию . Когда программа скомпилирована, выведите машину Тьюринга которой задан ввод размера выполняющий на для шагов. Если не останавливается до выполнения шагов , выведите вывод по умолчаниюPMckdMxnMxcnkMcnkd, Если я не ошибаюсь, эти языки программирования позволят нам выразить все вычисления в и ничего более. Однако этот предложенный язык по своей сути неинтересен.P

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

Артем Казнатчеев
источник
7
Несколько простых примеров языков программирования, которые захватывают подмножества вычислимых функций: регулярные выражения и грамматики без контекста.
Юкка Суомела
2
На самом деле языки, которые охватывают класс сложности как (который определяется аналогично примитивным рекурсивным функциям с рекурсией, замененной ограниченной рекурсией), довольно интересны (по крайней мере, с теоретической точки зрения). :)P VппВ
Kaveh
Линейное и целочисленное программирование фиксируют интересные подмножества вычислимых функций.
Диего де Эстрада
Datalog может выражать только алгоритмы полиномиального времени, но я не знаю, может ли он выражать все алгоритмы полиномиального времени.
Жюль
Хорошо известная статья «Тотальное функциональное программирование» утверждает, что языки программирования, в которых нет неразрешимой проблемы остановки, на самом деле практичны и полезны. jucs.org/jucs_10_7/total_functional_programming
нет

Ответы:

32

Одним из языков, пытающихся выразить только вычисления за полиномиальное время, является мягкое лямбда-исчисление . Система типов основана на линейной логике. В недавнем тезисе рассматриваются исчисления полиномиального времени и дается хорошее резюме последних разработок, основанных на этом подходе. Мартин Хофманн уже давно работает над этой темой. Более старый список соответствующих работ можно найти здесь ; Многие из его работ продолжаются в этом направлении.

Другая работа заключается в проверке того, что программа использует определенное количество ресурсов, используя зависимые типы или язык типизированных ассемблеров .

Тем не менее, другие подходы основаны на ограниченных ресурсом формальных исчислениях , таких как варианты окружающего исчисления.

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

Ранняя работа в этой области посвящена строгой нормализации исчислений, а это означает, что все хорошо типизированные программы останавливаются. Система F , известная как полиморфное лямбда-исчисление, сильно нормализуется. У него нет оператора с фиксированной точкой, но, тем не менее, он достаточно выразителен, хотя я не думаю, что известно, какому классу сложности он соответствует. По определению, любое сильно нормализующее исчисление выражает некоторый класс завершающих вычислений.

Язык программирования Charity - довольно выразительный функциональный язык, который останавливается на всех входах. Я не знаю, какой класс сложности он может выражать, но функцию Аккермана можно написать в Charity.

Дэйв Кларк
источник
Что вы подразумеваете под «по крайней мере» здесь?
nponeccop
«По крайней мере» здесь означает «некоторые». Я изменю свой ответ, чтобы сделать его немного более точным.
Дейв Кларк
Я почти уверен, что сложность функций, определяемых в системе F, - это класс функций, которые заканчиваются во времени "некоторой доказуемо полной функцией арифметики 2-го порядка" ввода. Не очень обычный класс сложности, но все же ...
Коди
cody: согласно «теоремам Вадлера о свободе», система F может выражать «любую рекурсивную функцию, которая может быть доказана полной в арифметике Пеано второго порядка», и которая «включает [...] функцию Аккерманна». Я не уверен, что это то же самое, что вы описываете. Главной особенностью Charity является поддержка кодовых данных, хотя я думаю, что проверка завершения Agda обеспечивает большую выразительность, чем Coq и System F, гарантируя завершение.
Blaisorblade
10

Взгляните на статью Гийома Бонфанте, в которой предложены две характеристики пространства логарифмирования и полиномиального времени с использованием языков программирования.

Гийом Бонфанте, Некоторые языки программирования для Logspace и Ptime, AMAST 2006, LNCS 4019, с. 66-80, 2006

Мухаммед Аль-Туркистани
источник
8

Я также хотел бы упомянуть неявную теорию сложности в качестве подхода к этому, поскольку я видел, что она возникла в нескольких связанных с этим вопросах. Процитирую этот ответ Нила Кришнасвами :

Основной метод состоит в том, чтобы связать классы сложности с подсистемами линейной логики (так называемые «легкие линейные логики»), с идеей, что исключение разреза для логической системы должно быть полным для данного класса сложности (такого как LOGSPACE, PTIME и т. Д.). Затем через Curry-Howard вы получаете язык программирования, на котором точно выражены программы в данном классе.

Крис Пресси
источник
5

Я удивлен, что никто не упомянул примитивную рекурсию. Ограничивая ограниченные циклы (т. Е. Количество итераций для каждого цикла должно быть рассчитано до начала цикла), полученная программа является примитивно-рекурсивной и, следовательно, суммарной. Дуглас Хофштадтер предложил язык программирования BLOOP, который допускает все и только примитивные рекурсивные функции.

Дэвид Харрис
источник
1
Это правильный подкласс всех функций, но назвать его классом «эффективных» функций может быть немного натянуто.
Рафаэль
пп
Другие упоминали System F и другие строго нормализующие языки, которые в некотором смысле поддерживают только «примитивную рекурсию». Однако, поскольку они поддерживают первоклассные функции, они позволяют писать больше программ (например, функцию Аккермана).
Blaisorblade