Abrir menu principal
Ambox rewrite.svg
Esta página precisa ser reciclada de acordo com o livro de estilo (desde março de 2014).
Sinta-se livre para editá-la para que esta possa atingir um nível de qualidade superior.

Lógica dinâmica é uma extensão da lógica modal originalmente planejada para raciocinar sobre programas de computador e, posteriormente, aplicada a mais comportamentos complexos gerais decorrentes da linguística, filosofia, Inteligência Artificial, e outros campos.

Índice

LinguagensEditar

Logica modal é caracterizada pelos operadores modais   (box p) afirmando que   é necessariamente o caso, e   (diamond p) afirmando que p\,\! é possivelmente o caso. Lógica dinâmica estende isso associando a cada ação   os operadores modais   e  , assim formando a lógica multimodal. O significado de   é que depois de executar uma ação   é necessariamente o caso que   se verifica, isto é,   deve acarretar  . O significado de   é que depois de realizar   é possivel que   se verifique, ou seja,   deve acarretar  . Estes operadores estão relacionados por   e  , analogamente para a relação entre quantificadores universais ( ) e existenciais ( ).

Lógica dinâmica permite ações compostas construídas a partir de ações menores. Enquanto os operadores de controle de base de qualquer linguagem de programação pode ser utilizada para este fim, operadores de expressão regular de Kleene são uma boa combinação para a lógica modal. Dadas ações   e  , a componente  , escolha, pode-se escrever também   ou  , é realizada através da realização de um dos   ou  . O componente  , sequencia, é realizado efetuando primeiro   e depois  . O componente  , iteração, é é realizado efetuando   zero ou mais vezes, sequencialmente. A constante   ou BLOCK não faz nada e não finaliza, ao passo que a constante   ou SKIP ou NOP, definivel como  , não faz nada porém finaliza.

AxiomasEditar

Esses operadores podem ser axiomatizada pela lógica dinâmica da seguinte forma, tomando como já dado uma axiomatização adequada de lógica modal incluindo os axiomas para operadores modais como o axioma acima mencionad   e as duas regras de inferência modus ponens (  e   implica ) e necessitarão (  implica  ).

A1.  

A2.  

A3.  

A4.  

A5.  

A6.  

Axiom A1 faz a promessa vazia que quando o BLOCK termina,   vai manter, mesmo que   é a proposição 'falsa. (Assim, 'BLOCK abstrai a essência da ação do inferno congelar de novo.)
A2 diz que [NOP] age como a função identidade em proposições, ou seja, ele transforma   em si mesmo.
A3 diz que se fazer um dos   ou   deve acarretar  , então   deve acarretar   e também para  , e vice-versa.
A4 diz que se fazer   e   deve acarretar  , then   deve acarretar a uma situação em que   deve acarretar  .
A5 é o resultado evidente de aplicação de , A3 e A4 à equação de   de "Kleene álgebra".
A6 afirma que, se   se verifica agora , e não importa quantas vezes fazemos   continua a ser a veracidade de   depois que a execução implica a sua veracidade, depois de mais uma execução de  , então   deve permanecer verdadeiro não importa quantas vezes fazemos  . A6 é reconhecível como indução matemática com a ação n := n+1 de incrementar n generalizada de ações arbitrárias  . <br

DerivaçõesEditar

O axioma da lógica modal   permite a obtenção das seguintes seis teoremas correspondentes à seguir:

T1.  

T2.  

T3.  

T4.  

T5.  

T6.  

T1 afirma a impossibilidade de acarretar qualquer coisa ao realizar BLOCK.
T2 observa novamente que NOPmuda nada, tendo em conta que NOP é tanto determinista e finalizador donde   e  tem a mesma força.
T3 diz que, se a escolha do um   ou   poderia acarretar em p  , Em seguida, tanto  quanto   sozinhos poderia acarretar  .
T4 é como A4.
T5 é explicada como a A5.
T6 se afirma que é possível conseguir   efetuando   suficientemente, em seguida   é verdade agora ou é possível executar  repetidamente para criar uma situação em que  (ainda) é falsa, mas mais uma execução de   poderia acarretar  .<br

"Box" e "diamante" são totalmente simétricos em relação ao qual se toma como primitivo. Uma axiomatização alternativa teria sido a tomar o teoremas T1-T6 como axiomas, a partir do qual poderíamos, então, ter derivados A1-A6 como teoremas.

A diferença entre implicação e inferência é a mesma em lógica dinâmica como em qualquer outra lógica: enquanto a implicação   afirma que, se   é verdade, então que assim seja  , a inferência   afirma que, se   é válida, então que assim seja  . No entanto, a natureza dinâmica da lógica dinâmica move esta distinção fora do reino de axiomática abstratas para a experiência de senso comum de situações em fluxo. A regra de inferência  , for example, por exemplo, é o som, pois sua premissa afirma que   detém em todos os momentos, de onde, não importa onde um   pode nos levar,   será verdade. A implicação   não é válido, porque a verdade de   no momento atual não é garantida a sua veracidade após a realização de  . Por exemplo,   será verdade em qualquer situação onde   é falso, ou em qualquer situação onde   é verdade, mas a afirmação   é falsa em qualquer situação onde   tem o valor 1, e, portanto, não é válida.

Regras derivadas de inferênciaEditar

Quanto à lógica modal, as regras de inferência modus ponens' e necessitação também bastam para a lógica dinâmica como as únicas regras primitivas de que necessita, como descrito acima. No entanto, como é habitual na lógica, muito mais regras podem ser derivadas a partir destas, com a ajuda dos axiomas. Um exemplo de instância de uma regra derivada em lógica dinâmica é que, se chutar uma TV quebrada uma vez não há como consertá-la, em seguida, repetidamente chutá-la não pode consertá-la também. Escrita   para a ação de chutar a TV, e   para a proposição de que a TV está quebrada, a lógica dinâmica expressa esta inferência como  , tendo como premissa   e, como conclusão  .O significado de   é que é garantido que depois de chutar a TV, ela está quebrada. Daí a premissa  significa que se a TV está quebrada, então depois de chutá-la, uma vez que ainda vai continuar quebrada.   denota a ação de chutar a TV zero ou mais vezes. Daí a conclusão   significa que se a TV está quebrado, então depois chutando zero ou mais vezes ainda vai continuar quebrada. Porque, se não, depois do segundo ao último chute a TV estaria em um estado onde chutando-a uma vez mais iria consertá-lo, que as reivindicações premissa nunca pode acontecer em qualquer circunstância.

A inferência   é o som. No entanto, a implicação   não é válida porque podemos facilmente encontrar situações em que   se mantem mas   não. Em qualquer situação contra-exemplo,   deve manter, mas   deve ser falso, enquanto   deve ser verdade. Mas isso pode acontecer em qualquer situação em que a TV está quebrada, mas pode ser revivido com dois chutes. A implicação falhar (não é válido), porque ele só exige que   segure agora, enquanto a inferência sucede (é som), porque ele requer que   manter em todas as situações, e não apenas a atual.

Um exemplo de uma implicação válida é a proposição  . Este diz que se   é maior ou igual a 3, depois de incrementação de  ,  deve ser maior ou igual a 4. No caso de ações deterministas  que está garantido para terminar, como  , "pode" e "deve" ter a mesma força, ou seja,   and   tem o mesmo significado. Daí a proposta anterior, é equivalente a   afirmando que se   é maior ou igual a 3, em seguida, após realização  ,   pode ser maior ou igual a 4.

AtribuiçãoEditar

A forma geral de um comando de atribuição é   onde   é uma variável e   é uma expressão construída a partir de constantes e variáveis ​​com o que quer que as operações são fornecidos pela linguagem, como adição e multiplicação. O axioma Hoare para a atribuição não é dado como um único axioma, mas sim como um esquema de axioma.

A7.  

Este é um esquema no sentido de que   pode ser instanciado com qualquer fórmula   containing contendo zero ou mais ocorrências de uma variável  . O significado de   é   com essas ocorrências   que ocorre livre em  ,Ou seja, não vinculados por algum quantificador como em  , Substituído por  . Por exemplo, podemos instanciar A7 com  , Ou com  . Tal esquema axiomatico permite um número infinito de axiomas ter um formulário comum a escrita como uma expressão finita conotando essa forma.

A instância   da A7 nos permite calcular mecanicamente que o exemplo   encontrado alguns parágrafos atrás é equivalente a  , Que por sua vez é equivalente a   pela álgebra elementar.

Um exemplo que ilustra a atribuição, em combinação com   é a proposição  . Este afirma que é possível, incrementando   suficientemente, muitas vezes, para fazer   igua a 7. Isto, obviamente, nem sempre é verdade, por exemplo, se   é de 8 para começar, ou 6.5, de onde esta proposição não é um teorema da lógica dinâmica. Se   é do tipo inteiro no entanto, esta proposição é verdadeira se e somente se   é, no máximo, 7, para começar, ou seja, ela é apenas uma maneira indireta de dizer  .

Indução matemática pode ser obtido como o exemplo de A6, em que a proposição   é instanciado como  , a ação   como  , e  como  . As duas primeiras dessas três instâncias são simples, convertendo a A6  . No entanto, a simples substituição de ostensivamente   para   não é tão simples, pois traz à tona o chamado opacidade referencial da lógica modal, no caso quando uma modalidade pode interferir com uma substituição.

Quando substituído   para  , estávamos pensando no símbolo proposição   como um designador rígido com respeito à modalidade  , que significa que é a mesma proposição após incrementando   como antes, embora incrementando   podem afetar sua verdade. Do mesmo modo, a ação   ainda é a mesma ação depois incrementando  , embora incrementando   resultará em sua execução em um ambiente diferente. No entanto,   em si não é um designador rígido com respeito à modalidade  ; e, se ele denota 3 antes incrementando  , denota 4 depois. Portanto, não podemos apenas substituir   para   em todos os lugares em A6.

Uma forma de lidar com a opacidade das modalidades é eliminá-los. Para este fim, expandir   como o conjunto infinito  , Isto é, o conjunto durante toda   de  . Agora aplique A4 para transformar   em  , possuindo   modalidades. Em seguida, aplique o axioma de Hoare   vezes a este para produzir  , então simplificar este conjunto infinito de  . Esta redução todo deve ser aplicado a ambas as instâncias do   na A6, originando  . A modalidade remanescente pode agora ser eliminados com mais um uso do axioma de Hoare para dar  .

Com as modalidades opacos agora fora do caminho, podemos substituir com segurança   para   na forma usual de lógica de primeira ordem para obter Peano é celebrado axioma  , indução ou seja matemático.

Uma sutileza que encoberto aqui é que   deve ser entendido como que varia ao longo dos números naturais, em que   é o expoente na expansão de   como a união de   sobre todos os números naturais  . A importância de manter esta informação digitação se torna reta aparente se   tinha sido do tipo inteiro, ou mesmo real, para qualquer um dos que A6 é perfeitamente válido como um axioma. Como um exemplo disso, se   é uma variável real e   é o predicado   é um número natural, então axioma A6 após as duas primeiras substituições, ou seja,  , é igualmente válida, isto é, a verdadeira em cada estado, independentemente do valor de   nesse estado, como quando   é do tipo número natural. Se em um determinado estado   é um número natural, então o antecedente do principal implicação A6 detém, mas, em seguida,   também é um número natural, para a conseqüente também detém. Se   não é um número natural, então o antecedente é falso e assim A6 permanece verdadeiro, independentemente da verdade do conseqüente. Podemos fortalecer A6 para uma equivalência   sem afetar nada disso, o outro sentido de ser provada a partir de A5, a partir do qual podemos ver que, se o antecedente de A6 acontece ser falsa em algum lugar, em seguida, o conseqüente deve ser falsa.

TesteEditar

Associados lógica dinâmica para cada proposição   uma ação   chamado um ensaio. Quando   detém, o teste   atua como um NOP, mudando nada, permitindo a ação de seguir em frente. Quando   é falso,   atua como BLOCK. Os testes podem ser axiomatizada como se segue.

A8.  

O teorema correspondente para   é:

T8.  

A construção se p então uma outra b é realizado em lógica dinâmica como  . Esta ação expressa uma escolha guardado: se   detém, em seguida,   é equivalente a  , enquanto   é equivalente ao "bloco" e   é equivalente a  . Assim, quando   é verdade que o performer da ação só pode tomar o ramo esquerdo, e quando   é falsa a direita.

A construção, enquanto que p faz a realizado como  . Isso realiza   zero ou mais vezes e em seguida, executa  . Enquanto que   ontinua a ser verdade, a   nos blocos finais do performer de terminar a iteração prematuramente, mas assim que ela se torna falso, mais iterações do corpo   são bloqueados e, em seguida, o cantor não tem escolha, mas para sair através do teste  .

Quantificação como atribuição aleatóriaEditar

A declaração de atribuição aleatória  denota a ação não determinístico de criação   para um valor arbitrário.   em seguida, diz que   detém, não importa o que você definir   a, enquanto   diz que é possível definir   para um valor que faz   verdade.   assim, tem o mesmo significado que o quantificador universal  , enquanto   similarmente corresponde ao quantificador existencial  . Ou seja, a lógica de primeira ordem pode ser entendida como a lógica de programas de dinâmica a forma  .

Semântica de mundos possíveisEditar

Lógica modal é mais comumente interpretada em termos de possíveis mundo semântica ou estruturas de Kripke. Esta semântica transporta mais naturalmente a lógica dinâmica interpretando mundos como estados de um computador na aplicação de programa de verificação, ou estados de nosso ambiente de aplicações para a linguística, AI, etc. Um papel para possíveis semântica de mundos é formalizar as noções intuitivas de verdade e validade, que por sua vez permitem que as noções de solidez e integridade a ser definida para sistemas axiomáticos. Uma regra de inferência é emitido quando a validade de suas premissas implica na validade da sua conclusão. Um sistema de axioma é boa quando todos os seus axiomas são válidas e as suas regras de inferência são sólidos. Um sistema de axioma é completa quando cada fórmula válida é derivável como um teorema desse sistema. Esses conceitos se aplicam a todos os sistemas de lógica , incluindo a lógica dinâmica.

Lógica dinâmica proposicionalEditar

Ordinário ou lógica de primeira ordem tem dois tipos de termos, respectivamente afirmações e dados. Como pode ser visto a partir dos exemplos acima, a lógica dinâmica adiciona um terceiro tipo de acções de duração denotando. A afirmação lógica dinâmica   contém todos os três tipos:  ,  , e   são dados,   é uma ação, e   e  são afirmações. lógica proposicional é derivado da lógica de primeira ordem, omitindo termos de dados e razões apenas cerca de proposições abstratas, que podem ser simples variáveis ​​proposicionais ou átomos ou proposições compostas construídas com esses conectivos lógicos como AND, OR e NOT.

Lógica dinâmica proposicional, ou PDL, foi derivado de lógica dinâmica em 1977 por Michael J. Fischer e Richard Ladner. PDL combina as ideias por trás lógica proposicional e lógica dinâmica, adicionando ações, enquanto a omissão de dados, daí os termos do PDL são ações e proposições. O exemplo da TV acima é expressa em PDL considerando que o próximo exemplo envolvendo   está na primeira ordem DL. PDL é (de primeira ordem) lógica dinâmica como a lógica proposicional é a lógica de primeira ordem.

Fischer e Ladner mostraram em seu artigo de 1977 que satisfatibilidade em PDL é de complexidade computacional, no máximo, tempo exponencial não determinístico, e pelo menos tempo exponencial determinístico no pior caso. Esta lacuna foi fechada em 1978 por Vaughan Pratt, que mostrou que PDL era decidível em tempo exponencial determinístico. Em 1977, Krister Segerberg propôs uma axiomatização completa do PDL, ou seja, qualquer axiomatização completa de lógica modal K juntamente com axiomas A1-A6 como dado acima. Provas de completude dos axiomas de Segerberg foram encontradas por Gabbay (nota não publicada), Parikh (1978), Pratt (1979), e Kozen e Parikh (1981).

HistóriaEditar

Lógica Dinâmica foi desenvolvida por Vaughan Pratt em 1974 em notas para uma disciplina sobre verificação de programas como uma abordagem para a atribuição de sentido à lógica de Hoare, expressando a fórmula de Hoare   as  . A abordagem foi posteriormente publicado em 1976 como um sistema lógico em si próprio. Os sistemas paralelos "sistema de algoritimo lógico de A. Salwicki" e "noção de transformadores de predicado de pré-condição mais fraca de Edsger Dijkstra"  . Com   correspondendo à pré-condição liberal mais fraca de Dijkstra  . Essas lógicas no entanto não estabeleceram nenhuma ligação com lógica modal, a semântica de Kripke, expressões regulares, ou o cálculo de relações binárias; lógica dinâmica, portanto, pode ser vista como um refinamento da lógica algorítmica e transformadores de predicados que a conecta com a axiomática e a semântica de Kripke da modal lógica, bem como para o cálculo de relações binárias e expressões regulares.

o "Concurrency Challenge"Editar

A lógica de Hoare, a lógica algorítmica, as pré-condições mais fracas, e a lógica dinâmica são todas bem adaptadas ao discurso e raciocínio sobre o comportamento sequencial. Estender essas lógicas para comportamento concorrente no entanto revelou-se problemático. Existem várias abordagens, mas todas elas carecem da elegância do caso seqüencial. Por outro lado, o sistema de lógica temporal de Amir Pnueli de 1977, outra variante da lógica modal que compartilha muitas características em comum com a lógica dinâmica, é diferente de todas as lógicas acima mencionadas por ser o que Pnueli caracterizou como uma lógica "endógena", sendo as outras lógicas "exógenas". Por isso Pnueli quis dizer que as afirmações lógicas temporais são interpretadas dentro de um quadro comportamental universal em que uma única situação global muda com o passar do tempo, ao passo que as afirmações das outras lógicas são feitas externamente às várias ações sobre as quais elas falam. A vantagem da abordagem endógena é que ela não faz suposições fundamentais sobre o que causa o que como o ambiente muda com o tempo. Ao contrário, uma fórmula lógica temporal pode falar de duas partes independentes de um sistema, que, porque eles não estão relacionados tacitamente evoluir em paralelo. Com efeito conjunção lógica comum de afirmações temporais é o operador de composição simultânea de lógica temporal. A simplicidade desta abordagem para a concorrência resultou em lógica temporal sendo a lógica modal de escolha para o raciocínio sobre sistemas concorrentes com seus aspectos de sincronização, interferência, independência, impasse, justiça, etc. Essas preocupações de concorrência parece ser menos críticas para a linguística, filosofia e inteligência artificial, as áreas em que a lógica dinâmica é mais frequentemente encontrada hoje em dia.

ReferênciasEditar

  • Vaughan Pratt, "Semantical Considerations on Floyd-Hoare Logic", Proc. 17th Annual IEEE Symposium on Foundations of Computer Science, 1976, 109-121.
  • David Harel, Dexter Kozen, and Jerzy Tiuryn, "Dynamic Logic". MIT Press, 2000 (450 pp).
  • David Harel, "Dynamic Logic", In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, chapter 10, pages 497-604. Reidel, Dordrecht, 1984.

Ligações externasEditar