Equivalência De Programas

Equivalência de Programas

Eventualmente, pode ser desejado analisar a equivalência de programas em uma dada máquina, caracterizando uma noção de equivalência mais fraca que a apresentada até o momento.

Sejam P e Q dois programas arbitrários, não necessariamente do mesmo tipo e uma máquina M qualquer. Então o par (P, Q) está na Relação Equivalência de Programas na Máquina M, denotado por:

P M Q

Se, e somente se, as correspondentes funções parciais computadas são iguais, ou seja:

〈P, M〉 = 〈Q, M〉

Neste caso, P e Q são ditos Programas Equivalentes na Máquina M, ou simplesmente Programas M-Equivalentes.

Existem máquinas nas quais não se pode provar a existência de um algoritmo para determinar se, dados dois programas, eles são ou não M-equivalentes.

Analogamente às equivalências de programas, pode-se estabelecer noções de equivalência de máquinas. Afirma-se que duas máquinas são equivalentes se uma pode simular a outra e vice-versa.

Simulação Forte de Máquinas:

Sejam M = (VM, X, Y, πXM, πYM, πFM, πTM) e

N = (VN, X, Y, πXN, πYN, πFN, πTN)

duas máquinas arbitrárias.

N Simula Fortemente M se, e somente se, para qualquer programa P para M, existe um programa Q para N, tal que as correspondentes funções parciais computadas coincidem, ou seja:

〈P, M〉 = 〈Q, N〉

É importante observar que a igualdade de funções exige que os conjuntos de domínio e contra-domínio sejam iguais. É necessário que as duas máquinas possuam os mesmos conjuntos de valores de entrada e saída

Simulação de Máquinas:

Sejam M = (VM, XM, YM, πXM, πYM, πFM, πTM) e

N = (VN, XN, YN, πXN, πYN, πFN, πTN)

duas máquinas arbitrárias.

N Simula M se, e somente se, para qualquer programa P para M, existe um programa Q para N e existem

Função de Codificação c: XM XN

Função de Decodificação d: YN YM

Tais que: 〈P, M〉 = d • 〈Q, N〉 • c

Sejam M e N duas máquinas arbitrárias. Então o par (M, N) está na Relação Equivalência de Máquinas, se, e somente se:

M simula N e N simula M.

Verificação da equivalência forte de programas

São descritas formas de se determinar se dois programas, sob determinadas condições, são ou não equivalentes fortemente. Mostra-se que existe um algoritmo para decidir a equivalência forte entre programas monolíticos. Todo programa iterativo possui um programa monolítico equivalente fortemente. A verificação de que dois programas monolíticos são equivalentes fortemente usa os seguintes conceitos:

Máquina de Traços: Produz um rastro ou histórico