Синтез программы - Program synthesis

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

Источник

Во время Летнего института символической логики в Корнельском университете в 1957 году Алонзо Черч сформулировал задачу синтеза схемы на основе математических требований. Несмотря на то, что работа относится только к схемам, а не к программам, эта работа считается одним из самых ранних описаний синтеза программ, и некоторые исследователи называют синтез программ «проблемой Чёрча». В 1960-х годах аналогичная идея для «автоматического программиста» была изучена исследователями искусственного интеллекта.

С тех пор различные исследовательские сообщества рассмотрели проблему синтеза программ. Известные работы включают теоретико-автоматный подход Бюхи и Ландвебера 1969 г. , а также работы Манна и Вальдингера (ок. 1980 г.). Развитие современных языков программирования высокого уровня также можно понимать как форму синтеза программ.

События 21 века

В начале 21 века наблюдался всплеск практического интереса к идее программного синтеза в сообществе формальной верификации и в смежных областях. Армандо Солар-Лезама показал, что можно закодировать задачи синтеза программ в булевой логике и использовать алгоритмы для задачи булевой выполнимости для автоматического поиска программ. В 2013 году исследователи из UPenn , Калифорнийского университета в Беркли и Массачусетского технологического института предложили унифицированную основу для задач синтеза программ . С 2014 года проводится ежегодное соревнование по синтаксису программ, в котором сравниваются различные алгоритмы синтеза программ на соревнованиях, соревнование по синтаксическому синтезу или SyGuS-Comp. Тем не менее, доступные алгоритмы способны синтезировать только небольшие программы.

Каркас Манна и Вальдингера

Правила разрешения без клауза (объединяющие замены не показаны)

№	Утверждения	Цели	Программа	Источник
51	${\ displaystyle E [p]}$
52	${\ displaystyle F [p]}$
53		${\ displaystyle G [p]}$	s
54		${\ displaystyle H [p]}$	т
55	${\ displaystyle E [{\ text {true}}] \ lor F [{\ text {false}}]}$			Решимость (51,52)
56		${\ displaystyle \ lnot F [{\ text {true}}] \ land G [{\ text {false}}]}$	s	Решимость (52,53)
57 год		${\ displaystyle \ lnot F [{\ text {false}}] \ land G [{\ text {true}}]}$	s	Решимость (53,52)
58		${\ displaystyle G [{\ text {true}}] \ land H [{\ text {false}}]}$	п ? s : t	Решимость (53,54)

Структура Манна и Вальдингера , опубликованная в 1980 году, начинается с заданной пользователем формулы спецификации первого порядка . Для этой формулы строится доказательство, тем самым синтезируя функциональную программу из унифицирующих замен.

Фреймворк представлен в виде таблицы, столбцы которой содержат:

• Номер строки («Nr») для справки.
• Формулы, которые уже были установлены, включая аксиомы и предварительные условия, («Утверждения»)
• Формулы еще предстоит доказать, включая постусловия, («Цели»),
• Термины, обозначающие допустимое выходное значение («Программа»)
• Обоснование текущей строки («Исходная точка»)

Первоначально в таблицу вводятся базовые знания, предварительные и пост-условия. После этого соответствующие правила проверки применяются вручную. Фреймворк был разработан для повышения читабельности промежуточных формул для человека: в отличие от классического разрешения , он не требует клаузальной нормальной формы , но позволяет рассуждать с помощью формул произвольной структуры и содержащих любые соединительные элементы (« неклаузальное разрешение »). Доказательство завершено, если оно было выведено в столбце « Цели» или, что то же самое, в столбце « Утверждения» . Программы, полученные с помощью этого подхода, гарантированно удовлетворяют формуле спецификации, начиная с; в этом смысле они правильны по построению . Только минималистский, но Тьюринг , чисто функциональный язык программирования , состоящий из условной, рекурсии и арифметических и других операторов поддерживаются. В тематических исследованиях, выполненных в рамках этой структуры, были синтезированы алгоритмы для вычисления, например, деления , остатка , квадратного корня , объединения терминов , ответов на запросы реляционной базы данных и нескольких алгоритмов сортировки . ${\ displaystyle {\ it {true}}}$${\ displaystyle {\ it {false}}}$

Правила доказательства

Правила доказательства включают:

• Неклаузальное разрешение (см. Таблицу).

Например, строка 55 получается путем разрешения формул утверждения из 51 и 52, которые имеют общие подформулы . Резольвента формируется как дизъюнкция , с замененной на , и с замененной на . Эта резольвента логически следует из конъюнкции и . В более общем плане и необходимо иметь только две унифицируемые подформулы и , соответственно; их резольвентное затем формируется из и , как и раньше, где это наиболее общий объединитель из и . Это правило обобщает разрешение статей .${\ displaystyle E}$${\ displaystyle F}$${\ displaystyle p}$${\ displaystyle E}$${\ displaystyle p}$${\ displaystyle {\ it {true}}}$${\ displaystyle F}$${\ displaystyle p}$${\ displaystyle {\ it {false}}}$${\ displaystyle E}$${\ displaystyle F}$${\ displaystyle E}$${\ displaystyle F}$${\ displaystyle p_ {1}}$${\ displaystyle p_ {2}}$${\ displaystyle E \ theta}$${\ displaystyle F \ theta}$${\ displaystyle \ theta}$${\ displaystyle p_ {1}}$${\ displaystyle p_ {2}}$

Термины программы родительских формул объединяются, как показано в строке 58, для формирования выходных данных резольвенты. В общем случае применяется и к последнему. Поскольку подформула появляется в выходных данных, необходимо проявлять осторожность, чтобы разрешить только подформулы, соответствующие вычислимым свойствам.${\ displaystyle \ theta}$${\ displaystyle p}$

• Логические преобразования.

Например, можно преобразовать в ) как в утверждениях, так и в целях, поскольку оба они эквивалентны.${\ Displaystyle Е \ земля (Ф \ лор G)}$${\ Displaystyle (Е \ земля F) \ лор (Е \ земля G)}$

• Разделение конъюнктивных утверждений и дизъюнктивных целей.

Пример показан в строках с 11 по 13 приведенного ниже примера игрушки.

• Структурная индукция .

Это правило позволяет синтезировать рекурсивные функции . Для заданного предусловия и постусловия «Учитывая такое, что найти такое, что » и соответствующего заданного пользователем правильного упорядочивания домена всегда целесообразно добавить Утверждение « ». Разрешение этого утверждения может привести к рекурсивному вызову в термине Program.${\ displaystyle x}$${\ Displaystyle {\ textit {pre}} (х)}$${\ Displaystyle е (х) = у}$${\ displaystyle {\ textit {post}} (х, у)}$ ${\ Displaystyle \ Prec}$${\ displaystyle x}$${\ displaystyle x '\ Prec x \ land {\ textit {pre}} (x') \ подразумевает {\ textit {post}} (x ', f (x'))}$${\ displaystyle f}$

Пример приведен в Manna, Waldinger (1980), p.108-111, где синтезирован алгоритм для вычисления частного и остатка от двух заданных целых чисел с использованием правильного порядка, определенного (p.110).${\ Displaystyle (п ', д') \ пре (п, д)}$${\ Displaystyle 0 \ Leq п '<п}$

Мюррей показал, что эти правила полны для логики первого порядка . В 1986 году Манна и Уолдингер добавили обобщенные правила E-разрешения и парамодуляции, чтобы также обеспечить равенство; позже эти правила оказались неполными (но, тем не менее, здравыми ).

Пример

Пример синтеза максимальной функции

№	Утверждения	Цели	Программа	Источник
1	${\ displaystyle A = A}$			Аксиома
2	${\ Displaystyle A \ leq A}$			Аксиома
3	${\ Displaystyle A \ leq B \ lor B \ leq A}$			Аксиома
10		${\ Displaystyle х \ Leq M \ земля y \ leq M \ земля (x = M \ lor y = M)}$	M	Технические характеристики
11		${\ Displaystyle (х \ Leq M \ земля у \ Leq M \ земля х = M) \ лор (х \ Leq M \ земля у \ Leq M \ земля у = M)}$	M	Distr (10)
12		${\ Displaystyle х \ Leq M \ земля у \ leq M \ земля х = M}$	M	С разрезом (11)
13		${\ Displaystyle х \ leq M \ земля y \ leq M \ земля y = M}$	M	С разрезом (11)
14		${\ Displaystyle х \ Leq х \ земля у \ leq х}$	Икс	Решимость (12,1)
15		${\ displaystyle y \ leq x}$	Икс	Решимость (14,2)
16		${\ Displaystyle \ lnot (х \ Leq у)}$	Икс	Решимость (15,3)
17		${\ displaystyle x \ leq y \ land y \ leq y}$	у	Решимость (13,1)
18		${\ displaystyle x \ leq y}$	у	Решимость (17,2)
19		${\ displaystyle {\ textit {true}}}$	х <у ? у : х	Решимость (18,16)

В качестве примера игрушки, функциональная программа для вычисления максимума двух чисел , и может быть получена следующим образом . ${\ displaystyle M}$${\ displaystyle x}$${\ displaystyle y}$

Исходя из описания требования « Максимум больше или равен любому заданному числу и является одним из заданных чисел », формула первого порядка получается как ее формальный перевод. Эта формула требует доказательства. Путем обратной сколемизации получается спецификация в строке 10, где прописные и строчные буквы обозначают переменную и константу Сколема соответственно. ${\ displaystyle \ forall X \ forall Y \ существует M: X \ leq M \ land Y \ leq M \ land (X = M \ lor Y = M)}$

После применения правила преобразования для закона распределения в строке 11 целью доказательства является дизъюнкция, и поэтому его можно разделить на два случая, а именно. строки 12 и 13.

Обращаясь к первому случаю, сопоставление строки 12 с аксиомой в строке 1 приводит к созданию экземпляра программной переменной в строке 14. Интуитивно последний конъюнкт строки 12 задает значение, которое должно принимать в этом случае. Формально правило разрешения отсутствия клауза, показанное в строке 57 выше, применяется к строкам 12 и 1, при этом ${\ displaystyle M}$${\ displaystyle M}$

• p является общим экземпляром x = x для A = A и x = M , полученным синтаксическим объединением последних формул,
• Р [ р ] является истинным ∧ х = х , получается из конкретизированной линии 1 (соответственно дополняетсячтобы сделать контекст F [⋅] вокруг р видно), и
• G [ p ] является x ≤ x ∧ y ≤ x ∧ x = x , полученным из созданной строки 12,

дает истину ∧ ложь ) ∧ ( x ≤ x ∧ y ≤ x ∧ true , что упрощается до . ${\ displaystyle \ lnot (}$${\ displaystyle)}$${\ Displaystyle х \ Leq х \ земля у \ leq х}$

Аналогичным образом строка 14 дает строку 15, а затем строку 16 по разрешению. Кроме того, второй случай в строке 13 обрабатывается аналогичным образом, в результате чего получается строка 18. ${\ Displaystyle х \ leq M \ земля y \ leq M \ земля y = M}$

На последнем этапе оба случая (т.е. строки 16 и 18) объединяются с использованием правила разрешения из строки 58; Чтобы применить это правило, был необходим подготовительный шаг 15 → 16. Интуитивно строка 18 может быть прочитана как «в случае , если выходные данные действительны (относительно исходной спецификации), а в строке 15 говорится:« в случае , если выходные данные действительны »; на шаге 15 → 16 установлено, что оба случая 16 и 18 дополняют друг друга. Поскольку обе строки 16 и 18 содержат термин программы, условное выражение приводит к столбцу программы. Поскольку формула цели была получена, доказательство выполнено, и столбец программы в строке " " содержит программу. ${\ displaystyle x \ leq y}$${\ displaystyle y}$${\ displaystyle y \ leq x}$${\ displaystyle x}$${\ displaystyle {\ textit {true}}}$${\ displaystyle {\ textit {true}}}$

Смотрите также

• Индуктивное программирование
• Метапрограммирование
• Вывод программы
• Программирование на естественном языке
• Реактивный синтез

Примечания

использованная литература

• Зохар Манна, Ричард Уолдингер (1975). «Знание и рассуждение в синтезе программ». Искусственный интеллект . 6 (2): 175–208. DOI : 10.1016 / 0004-3702 (75) 90008-9 .