Raciocínio do programa sobre o código-fonte próprio

15

A inspiração para esta pergunta é a seguinte (vaga) pergunta: Quais são os fundamentos lógicos / da linguagem de programação para ter uma IA que possa raciocinar sobre seu próprio código-fonte e modificá-lo?

Isso não é rigoroso, então aqui está minha tentativa de extrair uma questão concreta. Há duas coisas que me interessam:

(A) Uma linguagem de programação P que pode representar e manipular seus próprios programas como um programa de tipo de dados (por exemplo, como um AST). (Se desejado, um objeto do tipo Programa pode ser convertido em uma String, que é o texto de um programa válido nesse idioma. Isso seria o oposto do que um compilador faz.)

(B) Um método para raciocinar sobre o que um programa na linguagem P faz. Aqui estão dois níveis em que estou pensando:

Outra linguagem Q (com recursos de prova de teoremas) que modela o que um programa P faz. Deveria poder expressar e provar declarações como "o resultado da execução do Programa p é foo".
Uma maneira de raciocinar sobre o que um programa p: Program faz na própria linguagem P. (Portanto, estamos considerando P = Q acima.)

Até que ponto algo como isso foi implementado ou qual é o progresso nessa direção? Quais são os obstáculos práticos? À luz da intenção original da pergunta, qual é a melhor maneira de formalizar o problema?

*

Como as respostas mostram (obrigado!), Ambos (A) e (B1) podem ser feitos separadamente, embora pareça que fazê-los juntos seja mais uma questão de pesquisa.

Aqui estavam alguns dos meus primeiros pensamentos sobre a questão (aviso: bastante vago). Veja também meus comentários sobre a resposta de Martin Berger.

Estou interessado na linguagem de programação que modela a mesma linguagem de programação, em vez de uma mais simples (então P = Q acima). Isso seria uma "prova de conceito" de um programa capaz de "raciocinar sobre seu próprio código-fonte". Linguagens de programação tipicamente dependentes podem dar garantias sobre as saídas de suas funções, mas isso não conta como "raciocínio sobre seu próprio código-fonte" mais do que um "Olá, mundo!" conta como um quine em um idioma que automaticamente imprime uma string nua --- precisa haver algum tipo de citação / auto-referência. O analógico aqui está tendo um tipo de dados representando o Programa.

Parece um projeto bastante grande - quanto mais simples a linguagem, mais difícil é expressar tudo nela; quanto mais complicada a linguagem, mais trabalho deve ser feito para modelar a linguagem.

No espírito do Teorema da Recursão, um programa pode "obter" seu próprio código-fonte e modificá-lo (ou seja, gerar uma versão modificada de si mesmo). (B2) nos diz que o programa deve ser capaz de expressar uma garantia sobre o programa modificado (isso deve ser capaz de se recuperar, ou seja, deve ser capaz de expressar algo sobre todas as modificações futuras-).

pl.programming-languages ai.artificial-intel recursion Holden Lee
fonte

1

Por que você precisa que a linguagem atue como um provador de teoremas para estabelecer que "o resultado da execução do Programa p é foo"? A linguagem poderia simplesmente rodar p! De fato, é isso que está acontecendo.

Martin Berger

3

pt.wikipedia.org/wiki/Reflection_(computer_programming)

Kaveh 4/15

3

Observe que, em princípio, toda linguagem que pode implementar um intérprete por si só pode fazer as coisas que você precisa. De uma maneira mais matemática, o teorema da recursão vale para qualquer modelo de computação suficientemente forte. Algumas linguagens de programação apenas facilitam a integração. O mesmo vale para o raciocínio: você pode implementar qualquer sistema de raciocínio nessas linguagens. É claro que não se pode esperar raciocinar tudo, por exemplo, o problema de interrupção dos programas.

Kaveh

2

Eu acho que a pergunta não é muito clara. Você deve dar uma olhada nas linguagens de programação como Python, Java e aquelas mencionadas por Martin em sua resposta e esclarecer a pergunta para que fique claro que elas atendem ao que você está procurando ou, se não, por que não.

Kaveh

1

@HoldenLee Como a "P = Q", a terminologia estabelecida é "homogénea meta-programação", que se opõe ao "heterogéneo meta-programação" onde P

Q.

\neq

$\neq$

Martin Berger

14

Eu acho que você está perguntando sobre duas coisas diferentes.

A capacidade de uma linguagem de programação representar todos os seus programas como dados.
Raciocínio sobre programas como dados.

Para fins analíticos, é útil mantê-los separados. Vou me concentrar no primeiro.

A capacidade de um linguagens de programação para representar, manipular (e executar) seus programas como dados vai sob termos como meta-programação ou homoiconicity .

De uma maneira (estranha), todas as linguagens de programação conhecidas podem fazer metaprogramação, usando o tipo de dados string em conjunto com a capacidade de chamar programas externos (compilador, vinculador etc.) em strings (por exemplo, gravando-os no arquivo sistema primeiro). No entanto, provavelmente não é isso que você quer dizer. Você provavelmente tem uma boa sintaxe em mente. Strings não são uma sintaxe agradável para a representação de programas, porque quase todas as strings não representam programas, ou seja, o tipo de dados da string contém muito 'lixo' quando visto como um mecanismo de representação de programa. Para piorar a situação, a álgebra das operações de cadeia de caracteres não tem essencialmente nenhuma conexão com a álgebra da construção do programa.

O que você provavelmente tem em mente é algo muito melhor. Por exemplo, se for um programa, então é , mas como dados, a mão para manipulação e análise. Isso geralmente é chamado de cotação . Na prática, a cotação é inflexível; portanto, usamos quase-cotação , que é uma generalização da cotação em que a cotação pode ter 'buracos' nos quais programas podem ser executados que fornecem dados para 'preencher' os buracos. Por exemplo $P$ $\newcommand{\QUOTE}[1]{\langle #1\rangle}\QUOTE{P}$ $P$ é um quasi-citação representando uma condição onde em vez de uma condição que tem um furo . Se o programa avaliada como os dados , em seguida, o quasi-citação

⟨ i f [\cdot] t h e n 7 e l s e 8 + 9 ⟩

$\newcommand{\SYNTAX}[1]{\mathsf{#1}} \newcommand{\IF}[3]{\SYNTAX{if}\; #1 \; \SYNTAX{then}\; #2\; \SYNTAX{else}\; #3}\QUOTE{\IF{[\cdot]}{7}{8+9}}$

[\cdot]

$[\cdot]$

M

$M$

⟨ x > 0 ⟩

$\QUOTE{x > 0}$

avaliada como os dados

⟨ i f [M] t h e n 7 e l s e 8 + 9 ⟩

$\QUOTE{\IF{[M]}{7}{8+9}}$

⟨ i f x > 0 t h e n 7 e l s e 8 + 9 ⟩ .

$\QUOTE{\IF{x > 0}{7}{8+9}}.$

(Observe que é um programa normal (não um programa como dados) que retorna um programa entre aspas, ou seja, programa como dados.) Para que isso funcione, é necessário um tipo de dados para representar os programas. Normalmente, esse tipo de dados é chamado AST (árvore de sintaxe abstrata) e você pode ver (quase) cotações como mecanismos de abreviação para ASTs. $M$

Várias linguagens de programação oferecem quase-aspas e outros recursos para a metaprogramação. Foi a Lisp, com sua funcionalidade de macro que foi pioneira nessa capacidade de tratar programas como dados. Talvez, infelizmente, o poder das macros baseadas em Lisp permanecesse por muito tempo na maior parte da sintaxe minimalista do Lisp; não foi até o MetaML (1) que uma linguagem moderna e sintaticamente rica mostrou ser capaz de meta-programação. Desde então, o MetaOCaml (2) (um descendente do MetaML, importante para sua descoberta na busca ainda em andamento para resolver o problema de como digitar programas como dados), Template Haskell (3) e Converge (4) (o primeiro idioma para (considere todos os principais recursos de metaprogramação na minha opinião) mostraram que uma variedade de linguagens de programação modernas pode abrigar a metaprogramação. É importante perceber que podemos tomarqualquer linguagem de programação e transformá-la em uma linguagem de metaprogramação que seja juntamente com a capacidade de representar (e avaliar) seus próprios programas como dados. $L$ $L_{mp}$ $L$

$\newcommand{\EVAL}{\mathsf{eval}}\EVAL(\cdot)$ $P$ $\QUOTE{P}$ $P$ $P$ $\EVAL(\QUOTE{P})$ $P$ $\QUOTE{P}$

Quanto à segunda dimensão, raciocínio sobre programas dados como dados. Assim que você pode converter programas em dados, eles são dados 'normais' e podem ser considerados dados. Você pode usar todo tipo de tecnologia de comprovador, por exemplo, tipos ou contratos dependentes ou provadores de teoremas interativos ou ferramentas automatizadas, como Joshua apontou. No entanto, você terá que representar a semântica do seu idioma no processo de raciocínio. Se essa linguagem, como você precisa, possui habilidades de metaprogramação, as coisas podem se tornar um pouco complicadas e pouco trabalho foi feito nessa direção, com (5) a única lógica de programa para esse fim. Há também um trabalho baseado em Curry-Howard sobre o raciocínio sobre metaprogramação (6, 7, 8). Observe que essas abordagens baseadas em lógica, e a abordagem baseada em tipo (2) pode de fato expressar propriedades válidas para todos os estágios futuros de metaprogramação. Além de (2) nenhum desses documentos foi implementado.

Em resumo: o que você solicitou foi implementado, mas é bastante sutil, e ainda existem perguntas em aberto, em particular relacionadas a tipos e raciocínio simplificado.

W. Taha. Programação em vários estágios: sua teoria e aplicações .
W. Taha e MF Nielsen. Classificadores de ambiente .
T. Sheard e S. Peyton Jones. Meta-programação de modelos para Haskell .
L. Tratt. Meta-programação em tempo de compilação em uma linguagem OO de tipo dinâmico .
M. Berger, L. Tratt, Lógicas de Programas para Meta-Programação Homogênea .
R. Davies, F. Pfenning, Uma análise modal da computação faseada .
R. Davies, Uma Abordagem Lógica-Temporal da Análise em Tempo Vinculativo .
T. Tsukada, A. Igarashi. Uma base lógica para classificadores de ambiente .

Martin Berger
fonte

Você está certo - a linguagem de programação P pode ser diferente da linguagem Q que expressa teoremas / provas sobre programas nessa linguagem (que podem estar no Coq, por exemplo). O tipo de teorema em que estou pensando é assim: suponha que tenhamos um programa cuidadosamente projetado A_1. Thm: Para cada n o seguinte é válido: O programa A_n será exibido (m_n, A_ {n + 1}), onde m_n é um número inteiro, A_ {n + 1} é outro programa (por exemplo, obtido pela modificação de A_n de alguma forma) e para todos os n, temos esse m_n> 0.

Holden Lee

(A versão de ficção científica disso é que temos uma "prova" de que um programa que se modifica constantemente, nunca pressiona o botão que lança um míssil nuclear, por exemplo, ou que o programa sempre otimiza uma certa quantidade.)

Holden Lee

É por isso que eu queria fazer uma distinção entre executar o programa e raciocinar sobre o que o programa produzirá - queremos saber as propriedades do que ele fará antes de ser executado, sem executá-lo. Note que se queremos que A_n seja capaz de "modificar seu código fonte" para produzir A_ {n + 1}, P terá necessariamente habilidades de metaprogramação (o que nos coloca na posição de (5)).

Holden Lee

Ainda me parece que seria interessante para P = Q. Hipoteticamente, A é um programa de IA e a maneira que se modifica é raciocinando sobre seu próprio código - por exemplo, escreva teoremas sobre bits de código, provando-os e só depois modificando seu código. Então, parece que P precisaria ter as capacidades de Q.

Holden Lee

@HoldenLee É possível escrever programas como A_n. Se você usa strings como representante de programas, isso pode ser feito trivialmente em qualquer idioma; se você quiser quase aspas ou similares, isso é possível, por exemplo, no Converge. Eu não entendo o papel de m_n na construção.

Martin Berger

6

Não, não existe um sistema atual que execute todas as quatro etapas em seu sistema. Se você deseja projetar um sistema, um dos primeiros requisitos é a linguagem homoicônica. No mínimo, você deseja que sua linguagem de programação principal seja a menor possível, para que, ao entrar no sistema e começar a fazê-lo se interpretar, ele funcione. Portanto, você deseja um intérprete metacircular que foi pioneiro no lisp. Outras línguas o fizeram também, mas há uma enorme quantidade de pesquisas existentes sobre o ceceio.

O primeiro passo, se você quiser fazer isso, é ter uma linguagem homoicônica como Lisp ou alguma estrutura em que possa raciocinar sobre um programa em execução. Lisp é usado para isso pelo único motivo de que você pode definir um intérprete metacircular no idioma ou pode apenas tratar seu código como dados. Tratar o código como dados é a coisa mais importante. Há uma discussão sobre o que significa homoicônico no c2 wiki.

Por exemplo, no Lisp, o tipo de dados "Programa" é um programa válido de lisp. Você passa os programas lisp para um intérprete e ele calcula alguma coisa. Ele é rejeitado pelo intérprete se você não programar um "Programa" válido.

Portanto, uma linguagem homoicônica faz três de seus requisitos. Você pode até definir em lisp a idéia de um programa formal.

Você pode modelar lisp dentro de lisp? Sim, isso geralmente é feito principalmente como um exercício no final de um livro de programação para testar suas habilidades. SICP

No momento, a edição quatro é uma pergunta de pesquisa e abaixo é o que eu descobri que tenta responder a essa pergunta.

Eu diria que existem muitos tipos de programas que tentam fazer isso. Abaixo estão todos os programas que eu conheço.

JSLint é um exemplo de analisador estático que pega código de máquina ou alguma outra linguagem e procura bugs explicitamente. Em seguida, solicita que um programador corrija isso.
Coq é um ambiente que permite especificar provas usando uma linguagem de programação. Ele também possui táticas, onde sugere maneiras de resolver o problema. Ainda assim, espera que um humano faça o trabalho. Coq usa tipos dependentes para trabalhar e, portanto, é muito teórico do tipo. É muito popular entre cientistas da computação e pessoas que trabalham com a teoria dos tipos de homotopia.
O ACL2, por outro lado, é um provador de teoremas automatizado. Este sistema provará declarações baseadas em algo que você programa.
O ACL2 e o Coq possuem um plug-in de software que interage com o sistema com um sistema de aprendizado de máquina . O que é usado para treinar esses sistemas são programas escritos anteriormente. Pelo meu entendimento, esses sistemas acrescentam outro recurso em que você tem não apenas suas táticas, mas sugeriu teoremas que auxiliam no desenvolvimento de provas.

Abaixo está mais uma base do que sua pergunta significa.

O gcc é um exemplo de um compilador de otimização que pode ser usado como entrada e, em seguida, gerar uma versão otimizada de si mesmo. A idéia de um compilador que converte programas de uma representação para outra e melhora a velocidade devido a algum sinalizador de otimização é muito bem entendida. Depois de inicializar o compilador e ele gerar código de máquina válido, você pode adicionar uma otimização e recompilar o compilador, criando uma versão mais eficiente de si mesma.

Joshua Herman
fonte

1

Não há necessidade de tornar o idioma o mínimo possível. Você pode adicionar os recursos relevantes de metaprogramação a qualquer idioma. O trabalho MetaML de Taha mostrou isso. De fato, a adição de recursos de metaprogramação é mecânica.

Martin Berger

1

Também discordo que "nenhum sistema atual executa todas as quatro etapas". A pergunta 4 fala apenas sobre a execução de programas fornecidos como código. Isso é perfeitamente possível, na verdade, até a avaliação do Javascript faz isso.

Martin Berger

@MartinBerger, o que quero dizer é que você torna o kernel principal o mínimo possível. Além disso, se você começar a querer ter esperança de que seu sistema funcione nº 4, você desejará um sistema que você possa treinar não apenas seres humanos, mas computadores para usar, de modo que seria benéfico ter um sistema mínimo e que elas tenham bibliotecas codificadas em que o sistema como um modelo de programação meta

Joshua Herman

Depende do que (4) estamos falando. A pergunta original contém duas elaborações. O primeiro é trivial, você acabou de executar o programa. O segundo pode ser tratado pela lógica que citei como (5) na minha resposta do sistema de digitação (2). O posterior é implementado no MetaOCaml. Mas há espaço para mais pesquisas: nem (2) nem (5) podem lidar com formas arbitrárias de metaprogramação, e as propriedades garantidas por (2) são um pouco fracas (afinal, é um sistema de digitação com inferência de tipos) .

Martin Berger

1

Quanto a "você torna o kernel principal o mínimo possível": isso não é necessário. Você pode adicionar metaprogramação completa a qualquer idioma.

Martin Berger

5

Como a resposta de @ user217281728 menciona, há um tipo de máquina mais relacionada à inferência e à IA, chamada Gödel Machines

Uma máquina Gödel é um programa de computador auto-aperfeiçoado inventado por Jürgen Schmidhuber que resolve problemas da melhor maneira possível. Ele usa um protocolo de auto-aperfeiçoamento recursivo no qual reescreve seu próprio código quando pode provar que o novo código fornece uma estratégia mais ideal. A máquina foi inventada por Jürgen Schmidhuber, mas recebeu o nome de Kurt Gödel, que inspirou as teorias matemáticas.

A publicação referenciada de Jürgen Schmidhuber sobre "Máquinas Goedel: solucionadores de problemas universais auto-referenciais que possibilitam auto-aprimoramentos idealmente ótimos", (2006) arXiv: cs / 0309048v5

O modo como a máquina trabalha para implementar a meta-aprendizagem tem duas fases:

Aprendendo com dados (nível 1, aprender)
Usando dados aprendidos para modificar / otimizar seu código-fonte / algoritmo (nível 2, aprender a aprender)

Como a máquina modifica sua própria fonte, é auto-referencial, ou seja, possui a propriedade de auto-modificação (veja também aqui ).

Nesse sentido, ele pode modificar o próprio algoritmo de aprendizado em um sentido rigoroso (provando ótimas auto-modificações). Existem os problemas de auto-referência e indecidibilidade que, neste caso, assumem a forma:

..uma máquina Gödel com recursos computacionais ilimitados deve ignorar as auto-melhorias cuja eficácia não pode ser comprovada

Outros idiomas (e suas máquinas intérpretes associadas) que possuem a propriedade de autod modificação são, por exemplo, LISP .

No código LISP, os dados são intercambiáveis ou o código-fonte AST está disponível como dados no programa LISP e pode ser modificado como dados. Por outro lado, os dados podem ser vistos como AST, para algum código-fonte.

atualizar

Há outras máquinas bem , como máquinas de auto-programação (entre outros) que combinam auto-referência , auto-reprodução e auto-programação .

Um aspecto interessante do exposto acima é que a auto-referência não é problemática , mas é um elemento necessário nos autômatos de auto-reprodução / auto-programação .

Para mais detalhes (e mais publicações), consulte JP Moulin, CR Biologies 329 (2006)

abstrato

Os sistemas vivos são capazes de ter respostas adequadas ao ambiente imprevisível. Esse tipo de auto-organização parece operar como uma máquina de auto-programação, ou seja, uma organização capaz de se modificar. Até agora, os modelos de auto-organização dos seres vivos propostos são funções soluções de sistemas diferenciais ou funções de transição de autômatos. Essas funções são fixas e, portanto, esses modelos não podem modificar sua organização. Por outro lado, a ciência da computação propõe muitos modelos com as propriedades dos sistemas adaptativos dos seres vivos, mas todos esses modelos dependem da comparação entre um objetivo e os resultados e escolhas engenhosas de parâmetros pelos programadores, enquanto que não há intenção do programador. nem escolha nos sistemas vivos. $\mathbb{m}_\mathbb{sp}$ $\mathbb{M}_\mathbb{sp}$

Nikos M.
fonte

3

Este artigo de Jurgen Schmidthuber pode ser interessante:

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

NietzscheanAI
fonte

plz dar um resumo, pelo menos

vzn

Raciocínio do programa sobre o código-fonte próprio

Respostas: