Кто-нибудь на самом деле создал систему, которая пишет компьютерные программы из спецификации?

17

Кто-нибудь когда-либо писал систему (программное обеспечение или подробное объяснение на бумаге с простыми примерами), которая генерирует компьютерные программы? Я ввожу и он создает программу, которая перечисляет простые числа меньше 10. P r i m e ( x ) просто определяется как 1 < x ∧ ∄ Aпряме(Икс)∧Икс<10пряме(Икс) Профессора говорят, что могут, но никто не приводит реальных полных примеров.

1<Икс∧∄As,T,1<A∧A<Икс∧Иксзнак равноA×В, с A,В∈N
logic type-theory coq proof-assistants Коди
источник
13
Вы имеете в виду, как вы знаете, компилятор для языка программирования общего назначения?
Сашо Николов
1
Привет - добро пожаловать в cheheory! К сожалению, ваш вопрос не является вопросом исследовательского уровня в теоретической информатике и является не по теме на этом сайте.
На самом деле, это хороший вопрос, на вершине текущих исследований, и очень многообещающий. Однако зачастую очень сложно точно указать, что вы хотите. Если вам удастся указать это, то вам нужна система, которая докажет, что это имеет смысл, что это осуществимо, и для этого потребуется математическое доказательство. Из этого доказательства программа может быть извлечена. Но исследования по автоматизации доказательств и извлечению программ все еще находятся в зачаточном состоянии, хотя и добились значительного прогресса. Вы можете посмотреть, например, на Coq в Википедии. - - cc @LevReyzin
babou
2
Вот книга, соответствующая вашему вопросу. Есть и другие. Это не просто понять. Толпа Coq и Isabelle (еще одна такая система) включает пользователей SE, которые могут дать вам больше информации и примеров, если вопрос не будет закрыт. Я нашел это, ища в Интернете: coq пример программы синтеза.
Бабу
2
Область компьютерных наук, которая охватывает то, о чем я спрашиваю, называется программным синтезом и является активной областью исследований.
Гек Беннетт

Ответы:

11

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

Он тесно связан с результатом в логике, называемой соответствием Карри-Говарда (или изоморфизмом), который показывает, что компьютерные программы и математические доказательства очень похожи.

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

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

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

Несколько систем были разработаны в прошлом, чтобы прояснить эти идеи. Одним из наиболее известных был LCF с помощью Робин Милнер , который создал язык ML для этой цели. Одна из самых современных систем Coq .

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

Babou
источник
9

Необычный ответ: Да, но на момент написания, для большинства нетривиальных программ спецификации кажутся такими же сложными для написания и отладки, как и программы.

Если серьезно, ответ бабу хороший, но я также собираюсь предложить проверить область зависимых типов. Есть довольно хорошая книга, использующая Coq (полный отказ от ответственности: написанный моим другом), но есть также Epigram, Agda и Idris. Изабель / HOL также стоит проверить.

Все они основаны на исчислении конструкций. Если вы хотите знать теоретические основы, посмотрите теорию типов Мартина-Лёфа. Есть несколько хороших представлений вокруг.

Псевдоним
источник
Я полностью согласен в отношении спецификаций (а также остальной части вашего ответа, но вы знаете это лучше, чем я). Любой настоящий программист знает, как трудно полностью определить, что должна делать программа. Это основная проблема в разработке программного обеспечения. И это также переводится и здесь, хотя рассматриваемые проблемы в целом более математичны. Однако я не хотел показаться слишком обескураживающим (особенно если учесть историю этого вопроса, проиллюстрированную первым комментарием).
Бабу
4

Идя по касательной, генераторы программ (то есть системы, которые давали высокоуровневое описание чего-то на каком-то особом языке) существовали вечно. Любой компилятор является одним из них, как и любой из множества генераторов парсеров. В свое время системы, называемые «языки третьего поколения», которые генерировали (большую часть) код типичного бизнес-приложения с учетом описания высокого уровня и каталога доступных данных, были популярны.

vonbrand
источник
1

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

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

Возможно, вы захотите попробовать ECLiPSe для конкретной (с открытым исходным кодом) реализации такой системы.

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