Lógica de transações

Origem: Wikipédia, a enciclopédia livre.

A lógica de transações é uma extensão da Lógica de Predicados que responde de uma forma limpa e declarativa para o fenômeno de mudanças de estado em programas lógicos e bancos de dados. Esta extensão adiciona conectivos projetados especificamente para combinar ações simples em transações complexas e para fornecer controle sobre a sua execução. A lógica tem uma natural Teoria dos modelos e uma sólida e completa Teoria da Prova. A Lógica de Transações tem um subconjunto de cláusulas de Horn, que tem um procedimento, bem como uma semântica declarativa. As características importantes da lógica incluem atualizações hipotéticas e empenhadas, restrições dinâmicas na execução da transação, não-determinismo e atualizações em massa. Desta forma, Lógica de Transações é capaz de capturar declarativamente um número de fenômenos não-lógicos, incluindo conhecimentos procedurais (ou também, conhecimentos imperativos) em inteligência artificial, bancos de dados ativos e métodos com efeitos colaterais em bancos de dados de objetos.

A Lógica de Transações foi originalmente proposta em [1] por Anthony Bonner e Michael Kifer e posteriormente descrita em mais detalhes em [2] e [3]. A mais compreensível descrição aparece em [4].

Anos depois, Lógica de Transações foi ampliada em várias aspectos, incluindo concorrência [5], raciocínio revogável [6], ações parcialmente definidas [7] e outras características [8][9].

Em 2013, o trabalho original em Lógica de Transações [1] venceu o 20-years Test of Time Award como o mais influente trabalho do processo da ICLP 1993 conference nos últimos 20 anos.

Exemplo[editar | editar código-fonte]

Coloração de grafos. Aqui tinsert denota a operação elementar de atualização da inserção transacional. O conectivo ⊗ é chamado conjunção serial.

colorNode <-  // colore um nó corretamente
    node(N) ⊗ &neg; colored(N,_) ⊗ color(C)
    ⊗ ¬(adjacent(N,N2) ∧ colored(N2,C))
    ⊗ tinsert(colored(N,C)).
colorGraph <- ¬uncoloredNodesLeft.
colorGraph <- colorNode ⊗ colorGraph.

Pirâmide de empilhamento. A operação elementária de atualização tdelete representa a operação de remoção transacional.

stack(N,X) <- N>0 ⊗ move(Y,X) ⊗ stack(N-1,Y).
stack(0,X).
move(X,Y) <- pickup(X) ⊗ putdown(X,Y).
pickup(X) <- clear(X) ⊗ on(X,Y) ⊗
             ⊗ tdelete(on(X,Y)) ⊗ tinsert(clear(Y)).
putdown(X,Y) <-  wider(Y,X) ⊗ clear(Y) 
                 ⊗ tinsert(on(X,Y)) ⊗ tdelete(clear(Y)).

Execução hipotética. Aqui <> é o operador modal de possibilidade: Se ambos action1 e action2 são possíveis, execute action1. Caso contrário, se somente action2 é possível, então execute ela.

 execute <- <>action1 ⊗ <>action2 ⊗ action1.
 execute <- ¬<>action1 ⊗ <>action2 ⊗ action2.

Jantar dos filósofos. Aqui | é o conectivo lógico da conjunção paralela da Lógica de Transações Concorrente [5].

diningPhilosophers <- phil(1) | phil(2) | phil(3) | phil(4).

Implementações[editar | editar código-fonte]

Existe um número de implementações da Lógica de Transações. A implementação original está disponível aqui. Uma implementação da Lógica de Transações Concorrente está disponível aqui. A Lógica de Transações aperfeiçoada com apresentação pode ser encontrada aqui. Uma implementação da Lógica de Transações teve sido incorporada como parte do Flora-2, sistema de raciocínio e representação do conheciento. Todas estas implementações são de código aberto.

Trabalhos adicionais em Lógica de Transações podem ser encontrados no sítio do Flora-2.

Referências

  1. a b A.J. Bonner and M. Kifer (1993), Transaction Logic Programming, International Conference on Logic Programming (ICLP), 1993.
  2. A.J. Bonner and M. Kifer (1994), An Overview of Transaction Logic, Theoretical Computer Science, 133:2, 1994.
  3. A.J. Bonner and M. Kifer (1998), Logic Programming for Database Transactions in Logics for Databases and Information Systems, J. Chomicki and G. Saake (eds.), Kluwer Academic Publ., 1998.
  4. A.J. Bonner and M. Kifer (1995), Transaction Logic Programming (or A Logic of Declarative and Procedural Knowledge). Technical Report CSRI-323, November 1995, Computer Science Research Institute, University of Toronto.
  5. a b A.J. Bonner and M. Kifer (1996), Concurrency and communication in Transaction Logic, Joint Intl. Conference and Symposium on Logic Programming, Bonn, Germany, September 1996
  6. P. Fodor and M. Kifer (2011), Transaction Logic with Defaults and Argumentation Theories. In Technical communications of the 27th International Conference on Logic Programming (ICLP), July 2011.
  7. M. Rezk and M. Kifer (2012), Transaction Logic with Partially Defined Actions. Journal on Data Semantics, August 2012, vol. 1, no. 2, Springer.
  8. H. Davulcu, M. Kifer and I.V. Ramakrishnan (2004), CTR-S: A Logic for Specifying Contracts in Semantic Web Services. Proceedings of the 13-th World Wide Web Conference (WWW2004), May 2004.
  9. P. Fodor and M. Kifer (2010), Tabling for Transaction Logic. In Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), July 2010.