Teoria da Computação (Mestrado) -Segunda Prova Resolvida - 2º/2017 (Ayala)

Prévia do material em texto

Gabarito da Segunda Prova
316296 Teoria da Computac¸a˜o
Instituto de Cieˆncias Exatas, Universidade de Bras´ılia
Prof. Mauricio Ayala-Rinco´n
29 de Novembro de 2017
Nome: Matr´ıcula:
Durac¸a˜o: 110 min.
Inicio: 10:00 AM. Entrega: 11:50 AM.
3 pa´ginas, 10 Questo˜es.
Selecione (“X”) unicamente 4 questo˜es,
sendo no mı´nimo uma de cada grupo.
G. 1 G. 2 G. 3
1 2 3 4 5 6 7 8 9 10
Somente sera˜o consideradas as respostas das questo˜es aqui selecionadas (use “X”)
Propriedades ba´sicas dos sistemas de reescrita
1. Demonstre o Lema do Diamante de Newman: para sistemas de reescrita terminantes as propriedades de
conflueˆncia e de conflueˆncia local sa˜o equivalentes; i.e.,
← ◦ → ⊆ ↓ ⇔ ∗← ◦ →∗ ⊆ ↓
Veja notas de aula.
2. A terminac¸a˜o dos sistemas de reescrita e´ uma propriedade essencial, mas de d´ıficil ana´lise ainda para sistemas
simples. Com efeito, a indecidibilidade desta propriedade corresponde a` indecidibilidade do problema da
parada para ma´quinas de Turing segundo demonstrado originalmente por Huet & Lankford em 1978.
Considere o sistema de reescrita R consistente da regra u´nica:
R : f(a, f(x, y))→ f(x, f(x, f(b, b)))
(a) Demonstre que R na˜o e´ terminante.
(b) Demonstre que R e´ debilmente terminante (i.e., qualquer termo tem uma forma normal).
Ajuda: observe os dois redices do termo f(a, f(a, f(b, b))).
(a) Existe uma reduc¸a˜o circular: f(a, f(a, f(b, b)))→ f(a, f(a, f(b, b))).
(b) Basta observar que reduzindo redices mais internos, obtem-se formas normais. Por exemplo, para o
item anterior temos f(a, f(a, f(b, b)))→ f(a, f(b, f(b, f(b, b))))→ f(b, f(b, f(b, b))). Para formalizar que
reduc¸a˜o dos redices mais internos e´ com efeito uma estrateˆgia que gera formas normais, observe que com
essa estrateˆgia, em geral temos reduc¸o˜es da forma abaixo, nas quais s e t sa˜o formas normais:
C[f(a, f(s, t))]→ C[f(s, f(s, f(b, b)))]
Assim, como medida para um termo pode ser escolhido o multi-conjunto dos n´ıveis dos redices da regra
no termo. Note, por exemplo que para o item (a) temos o multi-conjunto {{0, 2}} que se mante´m com
a reduc¸a˜o mais externa; mas com a estrateˆgia de reduc¸a˜o mais interna, passamos desse multi-conjunto
para o multi-conjunto {{0}}, e logo para o multi-conjunto vazio. Considerando o caso geral, que e´
o de um contexto C[f(a, f(s, t))] no qual temos o redex f(a, f(s, t)) no n´ıvel k, e s e t sa˜o formas
normais, a estrateˆgia passa de um multi-conjunto para outro no qual uma ocorreˆncia de k e´ eliminada:
{{. . . k . . .}} >> {{. . .}}. Dessa maneira, garante-se que a estrateˆgia mais interna sucede.
3. Sejam R1 e R2 dois sistemas de reescrita de termos. A unia˜o direta de R1 e R2 e´ o sistema de reescrita de
termos que se obte´m ao unir os dois conjuntos de regras, diferenciando poss´ıveis s´ımbolos de func¸a˜o e constante,
que sejam sintaticamente iguais em ambos os sistemas. Propriedades modulares sa˜o aquelas que se preservam
na unia˜o direta de dois sistemas; por exemplo, a terminac¸a˜o na˜o e´ uma propriedade modular. Somente sobre
hipo´teses espe´cificas terminac¸a˜o e´ preservada.
Demonstre que a terminac¸a˜o na˜o e´ uma propriedade modular dos sistemas de reescrita.
Para isto observe os seguintes sistemas de reescrita:
R1 : f(a, b, x)→ f(x, x, x)
R2 : G(x, y)→ x
G(x, y)→ y
Prove, enta˜o, o seguinte:
(a) R1 e R2 sa˜o terminantes;
Use a ordem de multiconjuntos conformados por elementos que sa˜o a altura da a´rvore de cada redex
com a forma f(a, b, ) em um termo; por exemplo,
||f(a, b, f(a, b, f(a, b, f(a, a))))|| = {{4, 3, 2}}
Note que
f(a, b, f(a, b, f(a, b, f(a, a))))→ f(f(a, b, f(a, b, f(a, a))), f(a, b, f(a, b, f(a, a))), f(a, b, f(a, b, f(a, a))))
e
||f(f(a, b, f(a, b, f(a, a))), f(a, b, f(a, b, f(a, a))), f(a, b, f(a, b, f(a, a))))|| = {{3, 3, 3, 2, 2, 2}}
Tambe´m,
f(a, b, f(a, b, f(a, b, f(a, a))))→ f(a, b, f(f(a, b, f(a, a)), f(a, b, f(a, a)), f(a, b, f(a, a))))
e
||f(a, b, f(f(a, b, f(a, a)), f(a, b, f(a, a)), f(a, b, f(a, a))))|| = {{4, 2, 2, 2}}
Com esta ordem, denotando a altura de um termo u como h(u), ao reduzir um redex f(a, b, u) em um
termo t[f(a, b, u)] temos t[f(u, u, u)] e assim, ||t[f(a, b, u)]|| >> ||t[f(u, u, u)]||, sempre que ||f(a, b, u)|| =
{{h(u) + 1}} ∪ ||u|| >> ||u|| ∪ ||u|| ∪ ||u|| = ||f(u, u, u)||. Basta observar que a altura de cada redex de
f(a, b, ) em u e´ menor que h(u) + 1, que e´ a altura do redex f(a, b, u).
(b) a unia˜o direta de R1 e R2 na˜o e´ terminante.
Ajuda: examine derivac¸o˜es desde f com argumentos funcionais constro´ıdos com a func¸a˜o G.
Basta utilizar a medida |t|G, nu´mero de ocorreˆncias de G em t.
Demonstre agora, que a conflueˆncia de sistemas comutantes e´ preservada.
(c) Demonstre o teorema de Hindley-Rossen: se R1 e R2 comutam e sa˜o confluentes, enta˜o R1∪R2 e´ tambe´m
confluente.
Considere o sistema R∗1 ∪R∗2. Note que (R∗1 ∪R∗2)∗ = (R1∪R2)∗. Assim, basta demonstrar que a relac¸a˜o
(R∗1 ∪R∗2) e´ confluente. Verifica-se que cada divergeˆncia local da relac¸a˜o R∗1 ∪R∗2 junta-se em um passo:
(R−11 )
∗ ◦ R∗2 ⊆ R∗2 ◦ (R−11 )∗ por comutatividade, (R−11 )∗ ◦ R∗1 ⊆ R∗1 ◦ (R−11 )∗ por confueˆncia de R1, e
(R−12 )
∗ ◦ R∗2 ⊆ R∗2 ◦ (R−12 )∗ por confueˆncia de R2. Assim, R∗1 ∪ R∗2 e´ demonstrado confluente, e sempre
que (R∗1 ∪R∗2)∗ = (R1 ∪R2)∗, conclui-se que a relac¸a˜o R1 ∪R2 e´ confluente.
4. Demonstre que TRSs ortogonais, i.e. lineares a` esquerda e sem pares criticos, sa˜o confluentes segundo os
seguintes passos.
(a) Sejam→1,→2 relac¸o˜es abstratas de reescrita. Demonstre que se→1⊆→2⊆→∗1 e→2 e´ fortemente conflu-
ente, enta˜o →1 e´ confluente. Lembre-se que relac¸o˜es de reescrita fortemente confluentes sa˜o confluentes.
(b) Demonste que se R e´ um TRS ortogonal enta˜o a realac¸a˜o de reescrita em paralelo associada, →|| , satisfaz
←|| ◦ →|| ⊆→|| ◦ ←|| . Deve considerar casos como na prova do lema dos pares cr´ıticos de Knuth-Bendix.
(c) Usando os resultados dos itens anteriores, demonstre que TRSs ortogonais sa˜o confluentes. Observe que
→⊆→|| ⊆→∗.
(d) Considerando o exemplo
R : f(x, x)→ a
f(x, g(x))→ b
c→ g(c)
verifique que a hipo´tese de linearidade a` esquerda e´ essencial; i.e., verifique que CP (R) = ∅, R na˜o e´
linear a` esquerda e R na˜o e´ confluente.
Ca´lculo Lambda e expressividade computacional do modelo computacional de
reescrita
5. Utilizando os numerais de Church, definidos por Cn ≡ λx.λy.(xn y), para todo n ∈ N, Rosser mostrou como
computar func¸o˜es nume´ricas elementares.
P. ex. para a suma de naturais defina
A+ ≡ λx.λy.λp.λq.((x p) ((y p) q)), abreviando λxypq.xp(ypq)
Demonstre que para todo n,m > 0 ∈ N, A+CnCm = Cn+m.
A+CnCm =
(λxypq.xp(ypq))(λxy.xn y)(λxy.xm y) →β
(λypq.(λxy.xn y)p(ypq))(λxy.xm y) →β
(λypq.(λy.pn y)(ypq))(λxy.xm y) →β
(λypq.pn (ypq))(λxy.xm y) →β
λpq.pn ((λxy.xm y) pq) →β
λpq.pn ((λy.pm y) q) →β
λpq.pn (pm q) = Cn+m.
6. Para demonstrar que o modelo computacional de reescrita e´ adequado; i.e., que com este e´ poss´ıvel com-
putar qualquer func¸a˜o computa´vel ou que e´ Turing completo, e´ preciso demonstrar que as func¸o˜es recursivas
ba´sicas (zero, sucessor e projec¸o˜es) sa˜o λ-defin´ıveis e que as func¸o˜es λ-defin´ıveis sa˜o fechadas para composic¸a˜o,
recorreˆncia primitiva e minimizac¸a˜o. Demonstre o seguinte caso simplificado de que as func¸o˜es λ-defin´ıveis sa˜o
fechadas para recorreˆncia primitiva:
Suponha que f e´ definida por recorreˆncia primitiva como f(0) = m0 e f(n + 1) = h(f(n), n). Para a func¸a˜o
bina´ria recursiva h, λ-defin´ıvel como H. Indique como definir um term F para f no ca´lculo λ.
Ajuda: considere o seguinte “mecanismo de iterac¸a˜o” no ca´lculo λ como segue:
T ≡ λp.〈S(p True), H(p False)(p True)〉
Assim, para todo k temos, T 〈Ck, Cf(k)〉 =
λp.〈S(p True), H(p False)(p True)〉〈Ck, Cf(k)〉 →β
〈S(〈Ck, Cf(k)〉 True), H(〈Ck, Cf(k)〉 False)(〈Ck, Cf(k)〉 True)〉 =
〈S(Ck), H(Cf(k))(Ck)〉.
Agora, por induc¸a˜o e´ fa´cildemonstrar, enta˜o, que Tn〈C0, Cf(0)〉 = 〈Cn, Cf(n)〉.
Temos que,
Cf(n) = CnT 〈C0, Cf(0)〉 False. (1)
Observe que o lado direito de (1) e´ equivalente a` (((CnT )〈C0, Cf(0)〉) False), de acordo com a notac¸a˜o definida
anteriormente. A igualdade em (1) justifica-se por:
CnT 〈C0, Cf(0)〉 False→β
(λv.Tnv)〈C0, Cf(0)〉 False→β
Tn 〈C0, Cf(0)〉 False =
〈Cn, Cf(n)〉 False = Cf(n).
Concluindo, f pode ser especificada no ca´lculo λ como:
F ≡ λx.xT 〈C0, Cm0〉 False
Observe novamente que F deve ser aplicada a numerais de Church.
Crite´rios de conflueˆncia e me´todo de completac¸a˜o de Knuth-Bendix e
7. Considere o conjunto de equac¸o˜es B para Booleanos. Ele pode ser orientado de esquerda para direita obtendo
o sistema de reescrita de termos RB.
B =

[1] ¬(false) = true
[2] ¬(¬(x)) = x
[3] or(true, x) = true
[4] or(false, x) = x
[6] and(x, y) = ¬(or(¬(x),¬(y)))

(a) Demonstre que o sistema e´ terminante, mas na˜o confluente.
(b) Utilize o me´todo de Knuth-Bendix para completar o sistema.
(a) As duas primeiras regras gera˜o o par cr´ıtico:
〈false,¬(true)〉
false e ¬(true) sa˜o formas normais. Assim, o sistema na˜o e´ confluente. Para provar terminac¸a˜o, use
como medida dos termos:
(|t|and, |t|)
onde |t|and e´ o nu´mero de ocorreˆncias do operador and em t, e |t| o tamanho do termo. Use enta˜o a
ordem lexicogra´fica bina´ria >lex, sobre essa medida para demonstrar que e´ uma ordem de reduc¸a˜o para
RB.
(b) O u´nico par cr´ıtico poss´ıvel e´ o apresentado no item (a). Este pode ser orientado como a regra ¬(true)→
false. O novo sistema e´ terminante e confluente, sempre que na˜o sa˜o gerados pares cr´ıticos na˜o junta´veis:
B =

[1] ¬(false)→ true
[2] ¬(¬(x))→ x
[3] or(true, x)→ true
[4] or(false, x)→ x
[6] and(x, y)→ ¬(or(¬(x),¬(y)))
[7] ¬(true)→ false

8. Considere o seguinte sistema de regras de reescrita para a lo´gica combinato´ria RC :
RC =

[S] (((S · x) · y) · z)→ ((x · z) · (y · z))
[K] ((K · x) · y)→ x
[I] (I · x)→ x

Note que S,K e I sa˜o constantes e · um operador bina´rio. Associando pareˆntesis a` esquerda, estes podem ser
abreviados e o u´nico operador (·) eliminado. Assim, as regras podem ser escritas como:
RC =

[S] Sxyz → x z (y z)
[K] Kxy → x
[I] Ix→ x

(a) Demonstre que o sistema na˜o e´ terminante.
(b) Demonstre que o sistema e´ confluente.
(a) Para verificar que o sistema na˜o e´ terminante note que SII(SII) gera reduc¸o˜es infinitas:
SII(SII)→ I(SII)(I(SII))→ SII(I(SII))→ SII(SII)→ · · ·
(b) Para verificar que o sistema e´ confluente, use o crite´rio de ortogonalidade de Rosen. Com efeito, o sistema
e´ linear a` esquerda e na˜o tem pares cr´ıticos. Logo e´ ortogonal.
9. Considere os seguintes sistemas de regras de reescrita de termos (programas) para a func¸a˜o de Ackermann
[1] Ack(0, n)→ n+ 1
[2] Ack(m+ 1, 0)→ Ack(m, 1)
[3] Ack(m+ 1, n+ 1)→ Ack(m,Ack(m+ 1, n))
[1′] Ack’(0, n)→ n+ 1
[2′] Ack’(m+ 1, 0)→ Ack’(m, 1)
[3′] Ack’(m+ 1, n+ 1)→ Ack’(Ack’(m,n+ 1), n)
Deseja-se analisar qual das especificac¸o˜es e´ uma func¸a˜o bem definida? Para isso prove que o respectivo sistema
de reescrita e´
(a) terminante e
(b) confluente.
Ajuda: para terminalidade use uma ordem lexicogra´fica para constroir uma ordem de multi-conjuntos. Para
conflueˆncia, use o crite´rio dos pares cr´ıticos de Knuth-Bendix, ou ainda ortogonalidade.
Tanto o sistema para Ack quanto o sistema para Ack′ sa˜o lineares a` esquerda e sem pares cr´ıticos. Logo
utilizando o teorema de conflueˆncia de sistemas orthogonais, tem-se que ambos os sistemas sa˜o confluentes.
Para o sistema de Ack, observa-se que os chamados recursivos de Ack especificados na segunda e terceira regra
sa˜o aplicados a argumentos que decrementam para a ordem lexicogra´fica constro´ıda para o primeiro e segundo
paraˆmetro, utilizando a ordem usual em N:
(m+ 1, 0) >lex (m, 1)
(m+ 1, n+ 1) >lex (m,Ack(m+ 1, n))
(m+ 1, n+ 1) >lex (m+ 1, n)
Para concluir, utiliza-se a ordem de reduc¸a˜o da ordem de multiconjuntos >lex>lex para argumentos de Ack
induzida pela ordem >lex:
Assim, para a segunda regra temos:
{{(m+ 1, 0)}} >lex>lex {{(m, 1)}}
E para a terceira temos:
{{(m+ 1, n+ 1)}} >lex>lex {{(m,Ack(m+ 1, n)), (m+ 1, n)}}
10. Os grupoides centrais e laterais sa˜o axiomatizados pelos sistemas equacionais abaixo, respectivamente:
Gc =
{
[1] (x · y) · (y · z) = y }
Gl =
{
[1′] (x · y) · (z · x) = x }
Aplique o procedimento de completac¸a˜o para cada um dos sistemas equacionais para obter conjuntos de regras
de reescrita RGc e RGl , convergentes e equivalentes, respectivamente, a Gc e Gl.
Use o fato dos sistemas obtidos serem convergentes para demonstrar que os teoremas equacionais abaixo, valem
na teoria dos grupoides centrais e laterais, respectivamente:
y · ((y · u) · z) = (x · (y · u)) · u
x · (u · (x · v)) = ((x · v) · z) · v
RGc :
[1] (x · y) · (y · z)→ y
[2] y · ((y · x) · z)→ y · x
[3] (x · (z · y)) · y → z · y
RGl :
[1′] (x · y) · (z · x)→ x
[2′] x · (z · (x · y))→ x · y
[3′] ((z · x) · y) · x→ z · x
Em RGc tem-se: y · ((y · u) · z)→ y · u← (x · (y · u)) · u.
Em RGl tem-se: x · (u · (x · v))→ x · v ← ((x · v) · z) · v