Программа рассуждения о собственном исходном коде

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

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

(A) Язык программирования P, который может представлять и манипулировать своими собственными программами как Программа типа данных (например, как AST). (При желании объект типа Program может быть преобразован в String, который является текстом допустимой программы на этом языке. Это будет противоположно тому, что делает компилятор.)

(B) Метод рассуждения о том, что делает программа на языке P. Вот два уровня, о которых я думаю:

1. Другой язык Q (с возможностями доказательства теорем), который моделирует, что делает P-программа. Он должен быть в состоянии выразить и доказать утверждения типа «результат запуска Программы - это».
2. Способ рассуждения о том, что программа p: Program делает на самом языке P. (Таким образом, мы берем P = Q выше.)

Насколько реализовано нечто подобное или каков прогресс в этом направлении? Каковы практические препятствия? В свете первоначального замысла вопроса, как лучше всего формализовать проблему?

*

Как показывают ответы (спасибо!), И (A), и (B1) можно сделать отдельно, хотя кажется, что их совместная работа - это скорее вопрос исследования.

Здесь были некоторые из моих первых мыслей по этому вопросу (предупреждение: довольно расплывчато). Смотрите также мои комментарии к ответу Мартина Бергера.

Я заинтересован в том, чтобы язык программирования моделировал тот же язык программирования, а не более простой (поэтому P = Q выше). Это было бы «доказательством концепции» программы, способной «рассуждать о своем собственном исходном коде». Зависимо типизированные языки программирования могут дать гарантии о выходных данных своих функций, но это не считается «рассуждением о своем собственном исходном коде», как «Hello world!» считается языком квин на языке, который автоматически распечатывает пустую строку - должна быть какая-то цитата / ссылка на себя. Аналог здесь имеет тип данных, представляющий Программу.

Кажется, это довольно большой проект - чем проще язык, тем сложнее выразить все в нем; чем сложнее язык, тем больше работы нужно выполнить для моделирования языка.

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

Я думаю, что вы спрашиваете о двух разных вещах.

• Способность языка программирования представлять все свои программы в виде данных.
• Рассуждая о программах как данных.

Для аналитических целей полезно держать их отдельно. Я сосредоточусь на первом.

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

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

То, что вы, вероятно, имеете в виду, является чем-то более приятным. Например, если - это программа, то - это , но в качестве данных для манипуляций и анализа. Это часто называют цитатой . На практике цитата негибкая, поэтому мы используем вместо нее квази-цитату , которая является обобщением цитаты, где в цитате могут быть «дыры», в которых могут быть запущены программы, предоставляющие данные для «заполнения» дыр. Например, - это квази-кавычка, представляющая условие, где вместо условия у нас есть отверстие$P$$\newcommand{\QUOTE}[1]{\langle #1\rangle}\QUOTE{P}$⟨ я $P$

(Обратите внимание, что - это обычная программа (не программа в качестве данных), которая возвращает программу в кавычках, то есть программу в качестве данных.) Чтобы это работало, вам нужен тип данных для представления программ. Обычно этот тип данных называется AST (абстрактное синтаксическое дерево), и вы можете видеть (квази) кавычки как механизмы сокращения для AST.$M$

Несколько языков программирования предлагают квази-кавычки и другие функции для метапрограммирования. Именно Lisp с его макро-функциональностью открыл эту возможность для обработки программ как данных. Возможно, к сожалению, сила макросов, основанных на Лиспе, долгое время основывалась на минималистическом синтаксисе Лиспа; только в MetaML (1) было показано, что современный, синтаксически богатый язык способен метапрограммировать. С тех пор MetaOCaml (2) (потомок MetaML, важен для своего прорыва в продолжающемся поиске решения проблемы ввода программ в виде данных), Template Haskell (3) и Converge (4) (первый язык для поймите, что все ключевые функции метапрограммирования были правильными) показали, что метапрограммирование может содержать множество современных языков программирования. Важно понимать, что мы можем принятьлюбой язык программирования и превратить его в язык метапрограммирования который является вместе с возможностью представления (и оценки) своих собственных программ в качестве данных.L m p$L$$L_{mp}$$L$

Представление результатов работы программы, представленной в виде данных, достигается добавлением функции которая принимает программу (заданную как данные) в качестве входных данных и запускает ее , возвращая свой результат. Например, если - программа, оценивающая 17 и , (квази) цитируемая версия , то есть качестве данных, то также возвращает 17. Существуют все способы тонкости здесь, что я игнорирую здесь, такие как вопрос, когдаР ⟨ Р ⟩ Р Р е V л ( ⟨ Р ⟩ ) Р ⟨ Р $\newcommand{\EVAL}{\mathsf{eval}}\EVAL(\cdot)$$P$$\QUOTE{P}$$P$$P$$\EVAL(\QUOTE{P})$метапрограммируемые программы оцениваются (что приводит к различию между метапрограммированием во время компиляции и во время выполнения), что делать с типами или с ошибочными оценками, что происходит со связанными и свободными переменными в процессе перехода от к или наоборот.$P$$\QUOTE{P}$

Что касается второго измерения, рассуждения о программах приведены в виде данных. Как только вы можете конвертировать программы в данные, они становятся «нормальными» данными и могут быть обоснованы как данные. Вы можете использовать всевозможные технологии проверки, например, зависимые типы или контракты, интерактивные средства проверки теорем или автоматизированные инструменты, как указывал Джошуа. Однако вам придется представлять семантику вашего языка в процессе рассуждения. Если этот язык, как вам требуется, обладает способностями метапрограммирования, все может стать немного сложнее, и в этом направлении не было проделано большой работы, при этом (5) является единственной программной логикой для этой цели. Существует также работа Карри-Говарда, основанная на рассуждениях о метапрограммировании (6, 7, 8). Обратите внимание, что эти логические подходы, и основанный на типе подход (2) действительно может выражать свойства, которые сохраняются для всех будущих этапов метапрограммирования. Помимо (2) ни один из этих документов не был реализован.

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

1. У. Таха. Многоступенчатое программирование: его теория и приложения .

2. В. Таха и М. Ф. Нильсен. Классификаторы среды .

3. Т. Шеард и С. Пейтон Джонс. Шаблон метапрограммирования для Haskell .

4. Л. Тратт Мета-программирование во время компиляции на динамически типизированном ОО-языке .

5. М. Бергер, Л. Тратт, Программная логика для однородного метапрограммирования .

6. Р. Дэвис, Ф. Пфеннинг, Модальный анализ поэтапных вычислений .

7. Р. Дэвис, Временно-логический подход к анализу времени привязки .

8. Т. Цукада, А. Игараси. Логическая основа для классификаторов среды .

Нет, в настоящее время нет системы, которая делает все четыре шага в вашей системе. Если вы хотите спроектировать систему, одним из первых требований является гомоиконический язык. Как минимум, вы бы хотели, чтобы ваш основной язык программирования был как можно меньшим, чтобы при входе в систему и ее интерпретации она работала. Поэтому вам нужен метациклический переводчик, который впервые появился в LISP. Это сделали и другие языки, но существует огромное количество исследований, посвященных LISP.

Первый шаг, если вы хотите сделать это, - это использовать гомоиконический язык, такой как Lisp, или какой-то фреймворк, в котором вы можете рассуждать о работающей программе. Лисп используется для этой цели по той единственной причине, что вы можете определить метациклический интерпретатор в языке или вы можете просто рассматривать свой код как данные. Обработка кода как данных - самая важная вещь. В c2 wiki обсуждается, что значит гомоиконик.

Например, в Лиспе ваш тип "Program" - это действительные программы lisp. Вы передаете программы lisp переводчику, и он что-то вычисляет. Переводчик отклоняет его, если вы не запрограммировали действительную «Программу».

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

Можете ли вы моделировать лисп внутри лиспа? Да, это часто делается в основном как упражнение в конце книги по программированию на lisp, чтобы проверить свои способности. SICP

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

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

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

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

• ACL2, с другой стороны, является автоматическим средством проверки теорем. Эта система будет доказывать утверждения, основанные на том, что вы программируете.

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

Ниже приведено больше основ того, что означает ваш вопрос.

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

Как упоминается в ответе @ user217281728, существует тип машин, связанных в большей степени с логическим выводом и ИИ, называемых машинами Геделя.

Машина Гёделя - это самосовершенствующаяся компьютерная программа, изобретенная Юргеном Шмидхубером, которая оптимальным образом решает проблемы. Он использует рекурсивный протокол самосовершенствования, в котором он переписывает свой собственный код, когда он может доказать, что новый код обеспечивает более оптимальную стратегию. Машина была изобретена Юргеном Шмидхубером, но названа в честь Курта Гёделя, который вдохновил математические теории.

Ссылочная публикация Юргена Шмидхубера «Машины Гёделя: универсальные самореферентные решения проблем, обеспечивающие оптимальное самоосуществление», (2006) arXiv: cs / 0309048v5

То, как машина работает для реализации метаобучения, имеет две фазы:

1. Изучение данных (уровень 1, обучение)
2. Использование изученных данных для изменения / оптимизации исходного кода / алгоритма (уровень 2, научиться изучать)

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

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

..a машина Гёделя с неограниченными вычислительными ресурсами должна игнорировать те самосовершенствования, эффективность которых она не может доказать

Другими языками (и связанными с ними машинами-интерпретаторами), которые обладают свойством самоизменения, являются, например, LISP .

В LISP код и данные взаимозаменяемы, или исходный код AST доступен в виде данных в программе LISP и может быть изменен как данные. С другой стороны, данные могут рассматриваться как AST для некоторого исходного кода.

Обновить

Есть и другие машины , такие как машины самопрограммирования (среди прочих), которые сочетают в себе самореференцию , самовоспроизведение и самопрограммирование .

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

Для получения дополнительной информации (и большего количества публикаций) см. JP Moulin, CR Biologies 329 (2006).

абстрактный

Живые системы способны адекватно реагировать на непредсказуемую среду. Этот вид самоорганизации, по-видимому, действует как машина самопрограммирования, то есть организация, способная к самовосстановлению. До сих пор предложенные модели самоорганизации живых существ являются функциями-решениями дифференциальных систем или переходными функциями автоматов. Эти функции являются фиксированными, и поэтому эти модели не могут изменить их организацию. С другой стороны, информатика предлагает множество моделей, обладающих свойствами адаптивных систем живых существ, но все эти модели зависят от сравнения цели и результатов и искусного выбора параметров программистами, тогда как программист не намерен ни выбор в живых системах.$\mathbb{m}_\mathbb{sp}$$\mathbb{M}_\mathbb{sp}$

Эта статья Юргена Шмиртубера может представлять интерес:

http://arxiv.org/pdf/cs/0309048.pdf