Языки программирования, которые определяют проблему вместо решения?

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

Это звучит как описание декларативного языка (в частности, языка логического программирования), наиболее известным примером которого является Пролог. Однако я понятия не имею, можно ли распараллеливать Prolog.

По моему опыту, Prolog отлично подходит для решения проблем удовлетворения ограничений (тех, где есть набор условий, которые должны быть выполнены) - вы определяете свой входной набор, определяете ограничения (например, порядок, который должен быть наложен на ранее неупорядоченные входные данные), но патологические случаи возможны, и иногда процесс логического вывода занимает очень много времени.

Если вы можете определить свою проблему в терминах булеву формулу, которую вы можете использовать для решения SAT, но обратите внимание, что проблема 3SAT (назначение логической переменной по предложениям с тремя переменными) является NP-полной, и ее старший брат логики первого порядка, проблема квантифицированной логической формулы (которая использует квантор существования, а также универсальный квантор), является PSPACE-полной.

Есть несколько очень хороших программ доказательства теорем, написанных на OCaml и других FP языки; здесь их целая куча.

И, конечно, всегда существует линейное программирование с помощью симплекс-метода.

Я помню, как читал что-то о вычислениях с использованием ДНК еще в колледже. Вы бы поместили сегменты ДНК в решение, которое представляет сегменты проблемы, и определите его таким образом, что, если ДНК совмещается, это действительное решение. Затем вы позволяете свойствам химикатов решить проблему за вас и ищете готовые пряди, которые представляют собой решение. Это похоже на то, о чем вы говорите.

Я не помню, было ли это теоретическим или было сделано.

Это может показаться легкомысленным, но в каком-то смысле это и есть stackoverflow. Вы объявляете проблему и / или предполагаемый результат, и сообщество предоставляет решение, обычно в виде кода.

Кажется, чрезвычайно сложно моделировать динамические открытые системы до конечного числа решений. Я думаю, что есть причина, по которой большинство языков программирования являются обязательными. Не говоря уже о том, что существуют огромные проблемы P = NP, скрывающиеся в темноте, которые затрудняют проектирование такой системы.

Хотя было бы интересно, если бы существовала формальная структура, которая могла бы использовать человеческий вклад для «вычисления чисел». и предоставить решение, возможно, генерацию императивного кода. Интернет и поисковые системы Google - это своего рода инструмент, но очень примитивный.

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

LINQ можно также рассматривать как еще один декларативный DSL (принимая во внимание аргумент, что он слишком похож на SQL). Опять же, вы объявляете, как выглядит ваше решение, и LINQ решает, как его найти.

Прелесть языков такого типа в том, что вокруг них могут возникать такие проекты, как PLINQ (который я только что нашел). Посмотрите это видео с разработчиками PLINQ (прямая ссылка WMV) о том, как они распараллеливают поиск решений без изменения языка LINQ (много).

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

Позвольте мне попытаться ответить ... может быть Prolog может удовлетворить ваши потребности.

Я бы сказал, Objective Caml (OCaml) тоже ...

Лисп. Существует так много систем Lisp, определенных в терминах правил, а не императивных команд. Google, привет ...

Существуют различные правила на основе Java движки, которые позволяют декларативное программирование - Drools - это тот, с которым я играл, и он кажется довольно интересным.

Хотя математические доказательства не составляют язык программирования, они формируют формальный язык, на котором вы просто определяете решения (при условии, что вы допускаете неконструктивные доказательства). Конечно, это не алгоритмический подход, поэтому «математика» может быть неприемлемым ответом.

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

Серьезно: еще один голос за Пролог и различные типы декларативных DSL.