Prova 2 - Teoria da Computação 20232 (Ayala)

Prévia do material em texto

Gabarito da Segunda Prova
PPGMAT3976 - FORMALISMOS MATEMÁTICOS DA COMPUTAÇÃO - PPGI0084 - TEORIA DA COMPUTAÇÃO
PPG Matemática e PPG Informática, Universidade de Braśılia
Prof. Mauricio Ayala-Rincón
18 de dezembro de 2023
Nome: Matŕıcula:
Duração: 110 min.
Inicio: 10:00 AM. Entrega: 11:50 AM.
2 páginas, 4 Questões.
Propriedades básicas dos sistemas de reescrita
1. (2 pontos) Demonstre o Lema do Diamante de Newman: para sistemas de reescrita terminantes as
propriedades de confluência e de confluência local são equivalentes; i.e.,
← ◦ → ⊆ ↓ ⇔ ∗← ◦ →∗ ⊆ ↓
Veja notas de aula.
2. (2 pontos) Considere o seguinte sistema de regras de reescrita de termos (programa) para o mdc.
[1] mdc(s(m), 0)→ m + 1
[2] mdc(s(n),m + s(n))→ mdc(s(n),m)
[3] mdc(m + s(n),m)→ mdc(m,m + s(n))
(a) Demonstre que o sistema é terminante.
(b) Demonstre que o sistema é confluente.
(c) Se são incluidas as regras abaixo, continuará confluente o sistema?
[4] 0 + n→ n
[5] s(m) + n→ s(m + n)
Para o item (a) use a ordem lexicográfica nos argumentos de mdc. Para (b) use o critério dos pares
cŕıticos de Knuth-Bendix e o lema de Newman. para o item (c), a resposta é negativa, sempre que
aparecerão os seguintes pares cŕıticos (normalizados):
mdc(s(y), s(x + s(y))) = mdc(s(y), s(x))
mdc(s(x), s(x)) = s(x)
mdc(s(x + s(y)), s(y)) = mdc(s(y), s(x))
Método de completação de Knuth-Bendix
3. (3 pontos) Considere o seguinte conjunto de equações
E =

[1] T (C(A(T (x)))) = T (x),
[2] G(A(G(x))) = A(G(x)),
[3] C(T (C(x))) = T (C(x)),
[4] A(G(T (A(x)))) = A(x),
[5] T (A(T (x))) = C(T (x)

Ao orientar esse conjunto de equações (de esquerada para direita), é posśıvel deduzir o seguinte conjunto
de pares cŕıticos: 
6. T (C(A(T (x)))) = T (C(A(T (x))))
7. T (A(T (x))) = T (C(A(C(T (x)))))
8. A(G(T (A(x)))) = G(A(x))
9. A(G(A(G(x)))) = G(A(A(G(x))))
10. T (C(A(T (x)))),= C(T (x)) =
11. T (C(T (C(x)))),= C(T (T (C(x))))
12. A(T (x)),= A(G(C(T (x))))
13. A(G(T (A(x)))),= A(G(T (A(x))))
14. C(T (C(A(T (x))))),= T (A(T (x)))
15. C(T (A(T (x)))) = T (A(C(T (x))))

(a) Apresente os cálculos para dedução dos pares cŕıticos 8, 10, e 15.
O processo de completação de Knuth-Bendix produz o seguinte sistema de reescrita convergente.
RE =

[12] C(T (x))→ T (x))
[18] T (A(T (x)))→ T (x))
[28] A(G(T (x)))→ A(T (x)))
[31] G(A(x))→ A(x))
[36] A(T (A(x)))→ A(x))
[43] T (C(A(x)))→ T (A(x)))

Nos itens (b) e (c) aplique técnicas de teoria de reescrita para determinar se:
(b) T (A(G(C(T (A(G(C(T (A(G(C(T (x))))))))))))) =E C(T (G(A(C(T (G(A(C(T (x))))))))))
(c) T (A(G(C(T (A(G(C(T (A(G(C(T (x))))))))))))) =E C(T (G(C(T (A(C(T (G(A(C(T (x))))))))))))
(a)
[3, 1] : TCAT R3← CTCAT →R1 CT
[2, 4] : AGTA R2← GAGTA→R4 GA
[5, 5] : CTAT R5← TATAT →R5 TACT
(b) T (A(G(C(T (A(G(C(T (A(G(C(T (x)))))))))))))→! T (x) !← C(T (G(A(C(T (G(A(C(T (x))))))))))
(c) C(T (G(C(T (A(C(T (G(A(C(T (x))))))))))))→! T (G(T (x))).
4. (3 pontos) Considere o seguinte sistema de reescrita de termos
R0 =

[1] add(ln(x), ln(y))→ ln(mul(x, y))
[2] exp(ln(x))→ x
[3] ln(exp(x))→ x

(a) Demonstre se o sistema é terminante.
(b) Complete o sistema de regras. Use a prioridade add > mul, add > exp, add > ln.
Para minimizar a quantidade de cálculos, simplifique e elimine regras e pares cŕıticos (juntáveis,
e triviais) apenas posśıvel. Assim, evitará a dedução de pares cŕıticos desnecessários. A sua
resposta será o sistema convergente:
R4 =

[2] exp(ln(x))→ x
[3] ln(exp(x))→ x
[8] add(x, y)→ ln(mul(exp(x), exp(y))))

(c) Complete agora o sistema de regras de reescrita abaixo, utilizando a prioridade mul > add,mul >
ln,mul > exp.
R′0 =

[1] ln(mul(x, y))→ add(ln(x), ln(y))
[2] exp(ln(x))→ x
[3] ln(exp(x))→ x

(a)
(b) Ao deduzir pares cŕıticos entre todas as regras, obtem-se 〈E0, R0〉:
〈
[4] add(x, ln(y)) = ln(mul(exp(x), y))
[5] add(ln(x), y) = ln(mul(x, exp(y)))
[6] exp(x) = exp(x)
[7] ln(x) = ln(x)
 ,

[1] add(ln(x), ln(y))→ ln(mul(x, y))
[2] exp(ln(x))→ x
[3] ln(exp(x))→ x

〉
A seguir, eliminando equações triviais, orientando, simplificando regras e equações e eliminando
novamente equações triviais, obtem-se 〈E1, R1〉:
〈
∅ ,

[2] exp(ln(x))→ x
[3] ln(exp(x))→ x
[4] add(x, ln(y))→ ln(mul(exp(x), y))
[5] add(ln(x), y)→ ln(mul(x, exp(y)))

〉
Novamente, ao deduzir pares cŕıticos, obtem-se 〈E2, R2〉:
〈
[7] ln(mul(x, exp(ln(y)))) = ln(mul(exp(ln(x)), y))
[8] add(x, y) = ln(mul(exp(x), exp(y)))
[9] ln(mul(exp(ln(x)), y)) = ln(mul(x, exp(ln(y))))
[10] add(x, y) = ln(mul(exp(x), exp(y)))
 ,

[2] exp(ln(x))→ x
[3] ln(exp(x))→ x
[4] add(x, ln(y))→ ln(mul(exp(x), y))
[5] add(ln(x), y)→ ln(mul(x, exp(y)))

〉
Simplificando e eliminando equações, obtem-se 〈E3, R3〉:
〈{
[8] add(x, y) = ln(mul(exp(x), exp(y)))
}
,

[2] exp(ln(x))→ x
[3] ln(exp(x))→ x
[4] add(x, ln(y))→ ln(mul(exp(x), y))
[5] add(ln(x), y)→ ln(mul(x, exp(y)))

〉
Finalmente, ao orientar a equação [8], simplificar as regras [4] e [5], e subsequentemente as equações
assim obtidas, e eliminar (todas as equações resultantes), obtem-se E4 = ∅, e R4.
(c) Inicialmente, se deduzem os seguintes pares cŕıticos.
E′0 =

[4] exp(add(ln(x), ln(y))) = mul(x, y)
[5] exp(x) = exp(x)
[6] ln(x) = ln(x)

Ao eliminar e orientar, e novamente deduzir pares cŕıticos, obtem-se 〈E′1, R′1〉:
〈{
[5] ln(exp(add(ln(x), ln(y)))) = add(ln(x), ln(y))
}
,

[1] ln(mul(x, y))→ add(ln(x), ln(y))
[2] exp(ln(x))→ x
[3] ln(exp(x))→ x
[4] mul(x, y)→ exp(add(ln(x), ln(y)))

〉
Simplificando e eliminando a equação [5], e simplificando a regra [1], a equação resultante, e
eliminando a equação, obtem-se 〈E′2, R′2〉:
〈
∅ ,

[2] exp(ln(x))→ x
[3] ln(exp(x))→ x
[4] mul(x, y)→ exp(add(ln(x), ln(y)))

〉