SLX:
Procedimentos para WFSX
• SLX (SL with eXplicit negation) é um procedimento topdown para a WFSXp
– Aqui apresenta-se apenas a caracterização de AND-trees
– Os detalhes do procedimento estão em [AP96]:
J. J. Alferes, L. M. Pereira. Reasoning with Logic Programming, LNAI 1111, Springer 1996.
• É semelhante ao SLDNF
– Os nós são sucedidos ou falhados
– Resolução com regras do programa é como em SLDNF
• Em SLX, falha não significa falsidade. Quer antes
dizer não-veracidade (i.e. falso or indefinido)
Sucesso e falha
• Uma árvore finita é sucedida se a sua raiz é
sucedida, e falhada se a sua raiz é falhada
• O estado dum nó da árvore é determinado por:
– Uma folha com um literal objectivo é falhada
– Uma folha com true é sucedida
– Um nó intermédio é sucedido se todos os seus filhos
são sucedidos, e falhado caso contrário
Negação por falha?
• Como em SLS, para resolver recursões positivas
infinitas, árvores infinitas são (por definição) falhadas
• Pode-se usar NAF?
Sim
True de not A sucede se true-or-undefined de A falha
True-or-undefined de not A sucede se true de A falha
É esta a base do SLX. Define:
T-Trees para provar verdade
TU-Trees para provar verdade ou indefinição
T e TU-trees
• Diferem no facto de literais envolvidos em recursão
sobre negação, e portanto indefinidos em WFSXp,
falham em T-Trees mas sucedem em TU-Trees
a  not b
b  not a
T
ax
not b
x
TU
b
T
not a
ax
not b
x
TU
b
not a
…
Negação explícita em SLX
• ¬-literais são tratados como átomos
• Para impôr coerência, usa-se versão semi-normal nas
TU-trees
a  not b
b  not a
¬a
b
ax
¬a
not a
¬a
notx
b notx
true
b
ax
¬a
not a
¬a
not b notx
true
…
Negação explícita em SLX (2)
• Em TU-trees: L também falha se ¬L sucede em T
• I.e. se not ¬L falha em TU
not a
c  not c
b  not c
¬b
ab
¬a
ax
x
bx not ¬a
¬b
¬b
not c notx
true
cx
c
cx
c
cx
not c
not c
not c
not c
not c
x
x
x
…
Definição de T e TU-trees
T-Trees (resp TU-trees) são AND-trees etiquetadas por literais,
construídas de forma top-down a partir da raiz, expandindo nós da
seguinte forma:
Nós com literal objectivo A
Se não há regras com cabeça A, o nó é uma folha
Caso contrário, seleccione-se não-deterministicamente uma regra para A
A  L1,…,Lm, not Lm+1,…, not Ln
Numa T-tree, os filhos de A são L1,…,Lm, not Lm+1,…, not Ln
Numa TU-tree, A tem, para além daqueles, o filho not ¬A
Nós com literals default são folhas
Sucesso e falha
Todas as árvores infinitas são falhadas. Uma árvore finita é sucedida
se a sua raiz é sucedida e falhada caso contrário. O estado dos nós é
determinado por:
Uma folha com etiqueta true é sucedida
Uma folha com um literal objectivo é falhada
Uma folha numa T-tree (resp. TU) com etiqueta not A é sucedida se todas as
TU-trees (resp. T) com raiz A (árvores subsidiárias) são falhadas; é falhada caso
contrário
Um nó intermédio é sucedido se todos os seus filhos são sucedidos; caso
contrário é falhado
Depois de aplicar todas estas regas, alguns literais podem com estado
indeterminado (recursão sobre not)
Nós indeterminados em T-trees (resp.TU) são por definição falhados
(resp. sucedidos)
Exemplo de árvores infinitas
s  not p, not q, not r
p  not s, q, not r
q  r, not p
r  p, not q
s
px
q
not s not r
r
not p
p not q
not p not q not r
q
r
x
not p
p not q
q
not s not r
WFM is:
{s, not p, not q, not r}
r
x
p not q
q
not s not r
r
not p
Exemplo com recursão sobre negação
s  true
q  not p(0), not s
p(N)  not p(s(N))
Query:
s
q
not q
6
not p(0) not s
x
WFM = {s, not q}
p(0)
p(1)
p(2)
not p(1)
not p(2)
not p(3)
x
x
not p(0)
p(0)
p(1)
p(2)
not p(1)
not p(2)
not p(3)
x
x
x
…
x
x
true
…
Garantir terminação
• Por causa de loops, este método não é eficaz
• Para garantir terminação em programas ground:
Ancestors locais dum nó n são literais no caminho entre n e a
raiz, excluindo o próprio n
Ancestors globais são atribuídos a árvores:
• A árvore raiz não tem ancestors globais
• Os ancestors globais de T, uma árvore subsidiária do nó n em T’,
são os ancestors globais de T’ mais os ancestors locais de n
• Os ancestors globais dividem-se entre aqueles que provêm de Ttrees e os que provêm de TU-trees
Regras de Pruning
• Para recursão sobre positivos:
Regra 1
Se a etiqueta de um nó pertence aos seus ancestors locais, então o
nó é falhado e os seus filhos ignorados
Para recursão sobre negação:
Regra 2
Se um literal L numa T-tree ocorre nos seus ancestors globais-T,
então o nó é falhado e os seus filhos ignorados
Regras de prunning (2)
Regra 1
Regra 2
L
L
L
…
L
Outras regras correctas
Regra 3
Se um literal L numa T-tree ocorre nos seus ancestors globais-TU,
então o nó é falhado e os seus filhos ignorados
Regra 4
Se um literal L numa TU-tree ocorre nos seus ancestors globais-T,
então o nó é sucedido e os seus filhos ignorados
Regra 5
Se um literal L numa TU-tree ocorre nos seus ancestors globaisTU, então o nó é sucedido e os seus filhos ignorados
Exemplos de Prunning
a  not b
b  not a
¬a
b
a6
¬a
not a
not b not6¬a
true
b
6
c  not c
b  not c
¬b
ab
not a
c6
a6
Regra 2
¬a
6
b6 not ¬a
¬b
not c not 6¬b
true
not c
6
Regra 3
Caso não-ground
• A caracterização e regra de prunning só se aplica a
programas allowed com perguntas ground
• Como é há muito reconhecido, não é possível aplicar
regras de prunning no caso geral:
p(X)
p(X)  p(Y)
p(a)
Que fazer?
• Se “falha”, então respostas incompletas
p(Y)
• Se “continua” então loop
p(Z)
Tabling
• Para garantir terminação em programas não-ground,
em vez de ancestors e prunning, são necessários
mecanismos de tabulação (tabling)
– Se há um possível loop, suspender a literal e tentar
soluções alternativas
– Quando se encontra uma solução, guarda-se numa tabela
– Acordar nós suspensos com novas soluções da tabela
– Aplicar um algoritmo para determinar a completação do
processo, i.e. deerminar quando já não há mais soluções,
e falhar restantes nós suspensos
Exemplo de Tabling
p(X)  p(Y)
p(a)
• O XSB-Prolog usa tabling e
implementa a WFS
p(X)
1) suspender
p(Y)
2) acordar
X=a
Y=a
Tabela para p(X)
X=a
X=_
• Experimentem em:
http://xsb.sourceforge.net
Tabling (cont.)
• Se a solução já está na tabela, e o predicado
é chamado novamente, então:
– Não é necessário calcular a solução novamente
– Vai-se simplesmente buscar à tabela!
• Isto aumenta a eficiência. Algumas vezes
em ordens de magnitude.
Exemplo de Fibonacci
fib(6,X)
fib(1,1).
X=11
fib(2,1).
fib(X,F) :fib(X-1,F1), fib(X-2,F2),
F is F1 + F2.
Tabela de fib
Q F
2 1
1 1
3 3
4 4
5 7
6 11
fib(5,Y)
Y=7
fib(4,A)
fib(3,B)
B=3
fib(2,C)
fib(1,D)
C=1
D=1
fib(4,H)
H=4
fib(3,F)
A=4
F=3
fib(2,E)
E=1
Linear em vez de
exponencial
XSB-Prolog
• Usado para perguntas na WFS
• Prolog + tabling
– Para usar tabling, eg, no predicado p com 3
argumentos:
:- table p/3.
– Para usar tabling em todos os predicados
necessários:
:- auto_table.
XSB Prolog (cont.)
• As tabelas são usadas de chamada para
chamada até que:
abolish_all_table,abolish_table_pred(P/A)
• Negação WF negation é usada via tnot(Pred)
• (Negação explícita via –Pred)
• A resposta a Q é yes se Q é true ou undefined
no WFM
• É no se Q é false no WFM do programa
Distinguir T de U
• Depois de todas as respostas, as tabelas
guardam literais suspensos por recursão via
negação
→ Residual Program
Se o residual é vazio, então True
Se não é vazio, então Undefined
O residual pode ser examinado através de:
get_residual(Pred,Residual)
Exemplo de Residual program
:- table a/0.
:- table b/0.
:- table c/0.
:- table d/0.
a
c
b
d
::::-
b, tnot(c).
tnot(a).
tnot(d).
d.
| ?no
| ?RA =
no
| ?RB =
no
| ?RC =
no
| ?no
| ?-
a,b,c,d,fail.
get_residual(a,RA).
[tnot(c)];
get_residual(b,RB).
[];
get_residual(c,RC).
[tnot(a)];
get_residual(d,RD).
Fecho transitivo
:- auto_table.
edge(a,b).
edge(c,d).
edge(d,c).
reach(a).
reach(A) :edge(A,B),reach(B).
|?- reach(X).
X = a;
no.
|?- reach(c).
no.
|?-tnot(reach(c)).
yes.
• Devido à circularidade
a completação não
concluí not reach(c)
• SLDNF (e Prolog)
entram em loop
• XSB-Prolog trabalha
bem
Fecho transitivo (cont)
:- auto_table.
edge(a,b).
edge(c,d).
edge(d,c).
reach(a).
reach(A) :edge(A,B),reach(B).
:- auto_table.
edge(a,b).
edge(c,d).
edge(d,c).
reach(a).
reach(A) :reach(B), edge(A,B).
Em vez disto, poderiamos ter escrito
Semântica declarativa mais próximo da operacional
Recursão à esquerda tratada correctamente
A versão da direita até é mais eficiente
SLX e XSB
• Existe uma implementação do SLX usando
tabulação
• Essa implementação está baseada no XSBProlog
• Vem de base com o XSB-Prolog desde a
versão 2.0, cf:
http://xsb.sourceforge.net