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

Prévia do material em texto

Primeira Prova
Teoria da Computac¸a˜o
Programa de Po´s-Graduac¸a˜o em Informa´tica
Universidade de Bras´ılia
Prof. Mauricio Ayala-Rinco´n
2 de Outubro de 2017
Nome: Matr´ıcula:
Durac¸a˜o: 110 min.
Inicio: 10:00 AM. Entrega: 11:50 AM.
3 Pa´ginas, 4 Questo˜es.
Observac¸o˜es gerais:
• Todas as explicac¸o˜es e ca´lculos realizados para justificar as suas respostas devem ser orde-
nadamente apresentados exclusivamente nas folhas de rascuho (folhas em branco).
• Na˜o sera˜o consideradas respostas acertadas sem a devida apresentac¸a˜o ordenada das ex-
plicac¸o˜es e/ou ca´lculos que as justifiquem.
1. (2.0 pontos) Demonstre usando o princ´ıpio de resoluc¸a˜o no ca´lculo proposicional que
a fo´rmula
φ = r ∧ ¬q
e´ consequeˆncia lo´gica do conjunto
Φ = {p ∨ r,¬q ∧ ¬s, p→ (t ∨ ¬p), t→ s}
Para isto siga o roteiro padra˜o:
(a) (1.0 ponto) Construa um conjunto de ca´usulas proposicionais para Φ e ¬φ.
(b) (1.0 ponto) Construa enta˜o uma refutac¸a˜o para o conjunto de ca´usulas do item
precedente.
Conforme o me´todo de resuluc¸a˜o no ca´lculo proposicional, demonstra-se que o conjunto
de fo´rmulas {¬φ} ∪ Φ e´ inconsistente.
(a) Inicialmente as fo´rmulas em Φ e a fo´rmula ¬φ sa˜o transformadas na forma de
cla´usulas:
{¬φ} Φ
= =
{¬(r ∧ ¬q)} {p ∨ r,¬q ∧ ¬s, p→ (t ∨ ¬p), t→ s}
≡ ≡
{¬r ∨ ¬¬q} {p ∨ r,¬q,¬s,¬p ∨ t ∨ ¬p,¬t ∨ s}
≡
{¬r ∨ q}
(b) A seguir demonstra-se que o conjunto de cla´usulas
{¬r ∨ q} ∪ {p ∨ r,¬q,¬s,¬p ∨ t ∨ ¬p,¬t ∨ s}
e´ inconsistente:
¬r ∨ q
&&
¬q
zz¬r
$$
p ∨ r
yy
¬p ∨ t ∨ ¬p
��
p
&&
¬p ∨ t
uut
))
¬t ∨ s
uu¬s
&&
s
uu�
2. (3.0 pontos) Considere o seguinte programa definido, onde sum e´ um s´ımbolo de pred-
icado, s um s´ımbolo de func¸a˜o e 0 um s´ımbolo de constante:
P :=
{
C1 : sum(0, X,X)
C2 : sum(s(X), Y, s(Z))← sum(X, Y, Z)
}
Indicando todos os ca´lculos necessa´rios, encontre:
(a) (0.2 pontos) UP ;
(b) (0,2 pontos) BP ;
(c) (1.0 pontos) TP ↑ ω;
(d) (1.0 pontos) TP ↓ ω;
(e) (0.3 pontos) o mı´nimo ponto fixo de TP (mPF(TP )) e
(f) (0.3 pontos) o ma´ximo ponto fixo de TP (MPF(TP )).
(a) UP = {sk(0) |l k ∈ N};
BP = {sum(sk(0), sl(0), sm(0)) | k, l,m ∈ N};
(b)
TP ↑ ω :
TP ↑ 0 = ∅;
TP ↑ 1 = {sum(0, sl(0), sl(0)) | l ∈ N};
TP ↑ 2 = {sum(sk(0), sl(0), sl+k(0)) | k, l ∈ N, k < 2};
TP ↑ 3 = {sum(sk(0), sl(0), sl+k(0)) | k, l ∈ N, k < 3};
...
TP ↑ n = {sum(sk(0), sl(0), sl+k(0)) | k, l ∈ N, k < n};
...
TP ↑ ω = {sum(sk(0), sl(0), sl+k(0)) | k, l ∈ N}.
(c)
TP ↓ ω :
TP ↓ 0 = BP ;
TP ↓ 1 = Bp \ {sum(0, sl(0), sm(0)) | l,m ∈ N, l 6= m};
TP ↓ 2 = Bp \ {sum(sk(0), sl(0), sm(0)) | k, l,m ∈ N, k < 2, k + l 6= m};
TP ↓ 3 = Bp \ {sum(sk(0), sl(0), sm(0)) | k, l,m ∈ N, k < 3, k + l 6= m};
...
TP ↓ n = Bp \ {sum(sk(0), sl(0), sm(0)) | k, l,m ∈ N, k < n, k + l 6= m};
...
TP ↓ ω = Bp \ {sum(sk(0), sl(0), sm(0)) | k, l,m ∈ N, k + l 6= m}.
(d) e (e) mPF(TP ) = MPF(TP ) = Tp ↑ ω.
3. (3.0 pontos) Considere novamente o programa P da questa˜o 2, mas adicionando um
novo par de cla´usulas, como abaixo.
P :=

C1 : sum(0, X,X)
C2 : sum(s(X), Y, s(Z))← sum(X, Y, Z)
C3 : sum(Y, 0, Y )
C4 : sum(Y, s(X), s(Z))← sum(Y,X,Z)

Uma refutac¸a˜o para o objetivo← sum(s(0), s(0), U) com o novo programa P e´ ilustrada
abaixo.
← sum(s(0), s(0), U)
��
sum(s(X1), Y1, s(Z1))← sum(X1, Y1, Z1)
rr
θ1 = {U/s(Z1), X1/0, Y1/s(0)}
← sum(0, s(0), Z1)
��
sum(0, X2, X2)
qq
θ2 = {Z1/s(0), X2/s(0)}
�
Note que a resposta computada esta´ dada por {U/s2(0)}.
Construa a a´rvore de derivac¸a˜o para o objetivo ← sum(s(0), s(0), U). Em cada
aresta da a´rvore indique
• a cla´usula de P usada (renomeando varia´veis),
• o unificador computado e,
• para cada uma das folhas de sucesso indique a resposta computada.
Uma das ramas de sucesso dessa a´rvore de derivac¸a˜o corresponde a` refutac¸a˜o acima.
Ajuda: a a´rvore tem va´rias folhas.
Por simplicidade, sum(x, y, z) e´ abreviado como “+xyz” e si(0) por i, para i ∈ N; veja
Fig. 1.
4. (2.0 pontos)
Que a noc¸a˜o informal de “computa´vel” coincida com noc¸o˜es de “com-
putabilidade” formalizadas via modelos espec´ıficos de computac¸a˜o, como
sa˜o as Ma´quinas de Turing, o Ca´lculo Lambda, a Teoria de Reescrita, etc.,
e´ o que se conhece como a Tese de Church-Turing. Os primeiros resultados
neste sentido, desenvolvidos na de´cada de 1930, relacionam as func¸o˜es re-
cursivas parciais e as func¸o˜es computa´veis com ma´quinas de Turing assim
como as defin´ıveis no ca´lculo lambda.
Neste sentido, para provar a adequac¸a˜o computacional da SLD-resoluc¸a˜o ,
basta demonstrar que as func¸o˜es recursivas parciais sa˜o computa´veis via
programas definidos. Isto e´ demonstrado por induc¸a˜o na estrutura destas
func¸o˜es, que podem ser constro´ıdas a partir das func¸o˜es ba´sicas: Zero,
Sucessor e Projec¸o˜es e operac¸o˜es de composic¸a˜o, recurreˆncia primitiva e
minimizac¸a˜o.
No passo indutivo dessa demonstrac¸a˜o, para provar que e´ poss´ıvel especificar func¸o˜es
constro´ıdas por minimizac¸a˜o, temos o seguinte sketch:
Suponha que f e´ definida como
f(x1, . . . , xn) = µy(g(x1, . . . , xn, y) = 0)
sendo g uma func¸a˜o recursiva parcial. Onde µy(g(x1, . . . , xn, y) = 0) denota o
mı´nimo y tal que g(x1, . . . , xn, y) = 0 e g(x1, . . . , xn, z) esta´ definida para todo
z ≤ y e e´ indefinida caso contra´rio.
Pela hipo´tese de induc¸a˜o, existe um programa definido Pg e um predicado pg para
g.
Defina enta˜o, Pf como Pg juntamente com as seguintes cla´usulas:
pf (x1, . . . , xn, y)← pg(x1, . . . , xn, 0, z1), r(x1, . . . , xn, 0, z1, y).
r(x1, . . . , xn, y, 0, y).
r(x1, . . . , xn, y, s(z1), z)← pg(x1, . . . , xn, s(y), u), r(x1, . . . , xn, s(y), u, z).
←
+
11
U
C
2
,{U
/
s(
Z
1
)}
rr
C
4
,{U
/
s(
Z
3
)}
,,
←
+
0
1Z
1
C
1
,{Z
1
/
1
}
xx
C
4
,{Z
1
/
s(
Z
2
)}
''
←
+
10
Z
3
C
2
,{Z
3
/
s(
Z
4
)}
ww
C
3
,{Z
3
/
1
}
&&
�
←
+
00
Z
2
C
1
,{Z
2
/
0
}
ww
C
3
,{Z
2
/
0
}
&&
←
+
00
Z
4
C
1
,{Z
4
/
0
}
xx
C
3
,{Z
4
/
0
} ''
�
{U
/
2
}
�
�
�
�
{U
/
2
}
{U
/
2}
{U
/
2
}
{U
/
2
}
{U
/
2
}
F
ig
u
re
1:
A´
rv
or
e
d
e
d
er
iv
ac¸
a˜o
p
ar
a
←
su
m
(s
(0
),
s(
0)
,U
),
ab
re
v
.
←
+
11
U
,
(Q
u
es
ta˜
o
3)
Observe que o predicado r e´ utilizado para computar em ordem ascendente, uti-
lizando o predicado pg, imagens de g(x1, . . . , xn, 0), g(x1, . . . , xn, s(0)), . . ., ate´ que
seja obtida uma com valor zero. O processo sera´ interrumpido caso se atinge uma
tu´pla para a qual g esteja indefinida.
Questa˜o: Complete a demonstrac¸a˜o desta parte do passo indutivo provando que as
respostas computadas para pf correspondem exatamente a`s imagens da func¸a˜o f .
Por simplicidade, ~x denotara´ ambos um n-vector de naturales x1, . . . , xn, ou s
x1 , . . . , sxn ,
segundo convenieˆncia; assim, para x1, . . . , xn, i ∈ N e u uma varia´vel, g(~x, i) denota
g(x1, . . . , xn, i) e, pg(~x, s
i(0), u) denota pg(s
x1(0), . . . , sxn(0), si(0), u).
Por hipo´tese de induc¸a˜o, temos que o programa Pg resolve completa e corretamente o
objetivo ← pg(~x, si(0), z), no sentido de que se g(~x, i) = k, as respostas computadas
ligam {z/sk(0)} e, caso g(~x, i) indefinida, a a´rvore de derivac¸a˜o para esse objetivo tem
unicamente ramas de falha ou infinitas.
Demonstra-se, utilizando induc¸a˜o para g como acima, e por induc¸a˜o em i, que ←
pf (~x, y) tem resposta computada {y/si(0)} se e somente se f(~x) = i, que por definic¸a˜o
de minimizac¸a˜o significa que para todo j < i, g(~x, j) definida e diferente de zero, e
g(~x, i)= 0. Em particular, demonstra-se que a resoluc¸a˜o do objetivo← pf (~x, y) produz
o objetivo ← pg(~x, si(0), zi), r(~x, si(p), zi, y) se e somente se g(~x, j) esta´ definido e e´
diferente de zero, para todo j < i.
BI g(~x, 0) = 0 sse f(~x) = 0 sse o objetivo ← pf (~x, y) tem resposta computada {y/0}.
Com efeito, o objetivo resolve-se da seguinte maneira:
← pf (~x, y)
��
C1
ss
← pg(~x, 0, z0), r(~x, 0, z0, y)
�� vv
i.h. para pg {z0/0}
r(~x, 0, 0, y)
��
C2
rr
{y/0}
�
Caso, g(~x, 0) = k 6= 0, tem-se a seguinte resoluc¸a˜o:
← pf (~x, y)
��
C1
rr
← pg(~x, 0, z0), r(~x, 0, z0, y)
�� vv
i.h. para pg {z0/sk(0)}
← r(~x, 0, sk(0), y)
��
C3
rr
← pg(~x, s(0), z1), r(~x, s(0), z1, y)
Finalmente, caso g(~x, 0) indefinido, por h.i. para pg, o objetivo← pg(~x, 0, z0) na˜o pode
ser resolvido:
← pf (~x, y)
��
C1
ss
← pg(~x, 0, z0), r(~x, 0, z0, y)
�� vv
i.h. para pg
sem resoluc¸a˜o
PI Seja agora i > 0, e suponha para todo j < i, g(~x, sj(0)) e´ definido e diferente de
zero.
Por hipo´tese de induc¸a˜o, temos as seguintes treˆs possiveis derivac¸o˜es, considerando os
casos poss´ıveis para g(~x, i).
Caso g(~x, i) = 0:
← pf (~x, y)
��
C1
rr
← pg(~x, 0, z0), r(~x, 0, z0, y)
�� vv
i.h. para pg {zj/skj (0)}, kj 6= 0, j < i
← r(~x, si−1(0), ski−1(0), y)
��
C3
rr
← pg(~x, si(0), zi), r(~x, s(0), zi, y)
�� vv
i.h. para pg {zi/0}
r(~x, si(0), 0, y)
��
C2
rr
{y/0}
�
Caso g(~x, i) = ki 6= 0:
← pf (~x, y)
��
C1
rr
← pg(~x, 0, z0), r(~x, 0, z0, y)
�� uu
i.h. para pg {zj/skj (0)}, kj 6= 0, j < i
← r(~x, si−1(0), ski−1(0), y)
��
C3
rr
← pg(~x, si(0), zi), r(~x, s(0), zi, y)
�� uu
i.h. para pg {zi/ski(0)}
r(~x, si(0), ski(0), y)
�� ��
C3
rr
← pg(~x, si+1(0), zi+1), r(~x, si+1(0), zi+1, y)
Caso g(~x, i) indefinido:
← pf (~x, y)
��
C1
rr
← pg(~x, 0, z0), r(~x, 0, z0, y)
�� vv
i.h. para pg {zj/skj (0)}, kj 6= 0, j < i
← r(~x, si−1(0), ski−1(0), y)
��
C3
rr
← pg(~x, si(0), zi), r(~x, s(0), zi, y)
�� vv
i.h. para pg
sem resoluc¸a˜o