Lógica Paraconsistente: Máquina de Turing Paraconsistente Não Separáveis

As Máquina de Turing Paraconsistente Não Separáveis (MTPNSs) permitem a mistura de caminhos indiscriminadamente não permitindo aproveitar de forma adequada o paralelismo. Isso ocorre porque todas as possíveis combinações de estados e símbolos nas células da fita são considerados na execução das instruções. Essa é uma característica de algumas propriedades da LFI1 como a conjunção que valida a regra de separação (se ├LFI1 A^B então ├LFI1 A e ├LFI1 B) e a regra de adjunção (se ├LFI1 A e ├LFI1 B então ├LFI1 A^B). Assim, se Δ_LFI1 (M(n)) ├ Qi(t, x) ^ Sj(t, x) e Δ_LFI1 (M(n)) ├  Qk(t, x) ^ Sl(t, x), é também possível deduzir Δ_LFI1 (M(n)) ├ Qi(t, x) ^ Sl(t, x) Δ_LFI1 (M(n)) ├ Qk(t, x) ^ Sj(t, x). Consequentemente, se quiser definir um modelo de MTPs onde os diferentes caminhos de computação não se misturem totalmente, deve-se considerar uma lógica paraconsistente onde não seja valida a regra de separação ou a regra de adjunção (ou ambas).

Existem lógicas paraconsistentes com conjunções não-adjuntivas, como a lógica discursiva de primeira ordem D2. Para utilizá-la novos axiomas teriam que ser propostos para indicar quando diferentes elementos no processo de computação podem ser considerados em conjunto. Como não existem lógicas paraconsistentes onde a regra de separação não seja válida, é preferível definir uma lógica paraconsistente na qual não seja valida a regra de separação, de forma a permitir interpretar os diferentes elementos da máquina correspondentes a um caminho de computação como estando inter-relacionados, o que permitirá pensar em caminhos de computação independentes.

Uma lógica paraconsistente não-separável (PNS5) é obtida a partir da lógica modal S5 através da função de tradução do conjunto de fórmulas ForPNS5 → ForS5. Dessa maneira a lógica PNS5 fica definida e é uma sublógica de S5. A definição dos conectivos em PNS5 são:

• O conectivo • de inconsistência: •A = A ^◊ ￢◊A = ◊A ^ ◊￢A, em S5;
• O conectivo ◦ de consistência: ◦A = ￢◊•A = □￢A v □A em S5;
• A negação clássica ￢: ￢A = ￢◊A ^◊ ◦A = ◊￢A ^ (□￢A v □A) em S5;
• A conjunção clássica: A^B = (A ^◊ B) ^◊ (◦A ^◊ ◦B) = ◊(A ^ B) ^ (□(A ^ B) v □(A ^ ￢B) v □(￢A ^ B) v □(￢A ^ ￢B)) em S5.

Com estas definições, os princípios de explosão passam a ser teoremas de PNS5. Tendo em conta tais características PNS5 pode legitimamente ser considerada como uma LFI. Para poder usar PNS5 em lugar da LFI1, é necessário estende-la à primeira ordem incluindo os quantificadores e a igualdade, S5Q⁼.

Lógica Paraconsistente: Máquina de Turing Paraconsistente

Nas Máquinas de Turing Paraconsistentes (MTPs) é possível, em principio, usar qualquer lógica paraconsistente de primeira ordem. A versão de primeira ordem utilizada foi a LFI1 lógica de inconsistência formal (LFI) que estende a lógica positiva clássica incluindo conectivos de consistência ◦ e inconsistência •, além de ter uma semântica simples e bem estabelecida.

As noções de inconsistência e contradição coincidem, através da equivalência •A ↔ (A^￢A), e o conectivo de consistência serve para recuperar o caráter explosivo das contradições:

• se Δ |- _LFI1 a e Δ |- _LFI1￢a
• então Δ , ◦α |- _LFI1 β para toda fórmula β.

Além disso, ela permite codificar todas as inferências validas da lógica de primeira ordem clássica.

Pelo fato de LFI1 ser uma extensão da lógica positiva clássica, a aplicação de múltiplas instâncias de esquemas de axiomas do tipo Aij (I), Aij (II) ou Aij (III), para o mesmo instante de tempo t, denota a execução simultânea das respectivas instruções, o que pode levar a multiplicidade de símbolos em algumas células da fita, ou a multiplicidade de estados ou posições da máquina. Tal multiplicidade, em conjunção com o uso de axiomas do tipo (Aqi) ou (Asj), necessariamente leva a contradições, as quais em LFI1 são identificadas com inconsistências.

Adicionando condições de inconsistência nos dois símbolos iniciais das instruções de forma a controlar sua execução, q•i indicará que a instrução será executada unicamente no caso em que a maquina esteja em múltiplos estados ou posições, enquanto s•j indicará que a instrução será executada unicamente no caso em que a célula da fita (onde a instrução vai ser executada) contenha múltiplos símbolos. Estas condições correspondem formalmente a colocar o conectivo •, respectivamente, na frente do predicado Qi ou Sj no antecedente dos axiomas que expressam instruções. Estas condições permitem aproveitar o paralelismo das MTPs.

Lógica Paraconsistente: Máquina de Turing

Para falarmos da máquina de Turing, precisamos conhecer seu criador: Alan Mathison Turing (1912-1954), conhecido também como Alan Turing. Ele foi um matemático britânico nascido em 23 de junho de 1912 na cidade de Paddington, na Inglaterra. Estudou na tradicional Escola Sherbourne tendo-se graduado em 1931 em Matemática pela Universidade de Cambridge.

Alan Turing

Depois de formado, e após muito estudo, criou uma máquina automatizada que calcula qualquer algoritmo e processa as instruções mecanicamente na própria máquina. Essa é a tão famosa Máquina de Turing que serviu como protótipo para os computadores atuais e permitiu o desenvolvimento do “Enigma” que foi capaz de decifrar os códigos nazistas na Segunda Guerra Mundial.

Máquina de Turing

Uma Máquina de Turing pode ser descrita como sendo constituída por uma cabeça de leitura/escrita e uma fita unidimensional potencialmente infinita em ambas as direções. A fita e dividida em células, cada uma das quais com capacidade de conter um único símbolo. Em cada instante de tempo a máquina se encontra em um determinado estado, e com a cabeça lendo uma célula especifica da fita, a qual ela considerada como sendo a posição atual da maquina. A configuração atual da maquina consiste na junção do estado atual e do símbolo que esta sendo lido na posição atual.

O comportamento da máquina é determinado por um conjunto de instruções, as quais indicam a operação a se realizar dependendo da configuração atual. As únicas operações que a maquina pode realizar são: escrever um novo símbolo na posição atual (substituindo o símbolo anterior) ou realizar um movimento da cabeça a esquerda ou direita, passando a uma célula subsequente da atual. Os estados, os símbolos de leitura/escrita e as instruções são conjuntos finitos.