Lógica, unificação e execução em Prolog

Com os factos pai(tomas,ana) e pai(ana,leo), podemos concluir que Tomás é avô de Leo. Prolog representa os casos conhecidos como factos e a passagem de pai a avô como uma regra. Uma consulta pede os valores para os quais a relação se prova.

Factos, regras e queries

pai(tomas, ana).
pai(ana, leo).
pai(leo, rui).
avo(X, Z) :- pai(X, Y), pai(Y, Z).

A última é uma regra, lida “X é avô de Z se X é pai de Y e Y é pai de Z”. As maiúsculas são variáveis (por preencher); as minúsculas são átomos (valores concretos).

De regra a cláusula de Horn

A regra avo(X, Z) :- pai(X, Y), pai(Y, Z). corresponde à cláusula avo(X,Z) v -pai(X,Y) v -pai(Y,Z): a cabeça é verdadeira ou alguma condição é falsa.

Antes de cada resolução, renomeia as variáveis da cláusula copiada, por exemplo avo(X1, Z1) :- pai(X1, Y1), pai(Y1, Z1). Sem renomeação, duas utilizações da mesma regra partilhariam variáveis que deviam ser independentes.

O símbolo _ é uma variável anónima nova em cada ocorrência. par(_,_) aceita par(a,b); par(X,X) exige o mesmo termo nas duas posições e recusa par(a,b).

Unificação

Antes de procurar, o motor precisa de casar termos. Unificar dois termos é encontrar uma substituição que os torna iguais, ou seja procuramos a mais geral, que não fixe valores desnecessários:

• pai(ana, X) com pai(ana, leo) unifica com {X/leo}.
• pai(X, leo) com pai(ana, leo) unifica com {X/ana}.
• pai(X, leo) com pai(tomas, ana) falha: leo nunca iguala ana, e nenhuma substituição muda átomos.

Resolução SLD passo a passo

Para responder ?- avo(ana, X)., o motor constrói uma árvore de procura. Segue o ramo de sucesso:

1. A query unifica com a cabeça da regra avo(X', Z'), com {X'/ana, Z'/X}. Restam os subobjetivos pai(ana, Y), pai(Y, X).
2. pai(ana, Y) unifica com o facto pai(ana, leo): {Y/leo}. Resta pai(leo, X).
3. pai(leo, X) unifica com pai(leo, rui): {X/rui}. Não resta nada: sucesso, e a resposta compõe as substituições, X = rui.

Se pedires mais soluções (;), o motor faz retrocesso: volta ao último ponto com alternativas por explorar. Quando o programa diz false onde esperavas resposta, desenha a árvore: ela mostra o ramo que morreu e a cláusula em falta.

pai(tomas, ana).
pai(ana, leo).
pai(leo, rui).
avo(X, Z) :- pai(X, Y), pai(Y, Z).

main :- avo(ana, X), writeln(X).

Árvore SLD com falha e alternativa

Acrescenta à família um filho sem descendentes, antes de Ana:

pai(tomas, ines).
pai(tomas, ana).
pai(ana, leo).
pai(leo, rui).
avo(X,Z) :- pai(X,Y), pai(Y,Z).

Na consulta avo(tomas,N), a regra renomeada dá o resolvente pai(tomas,Y1), pai(Y1,N). O primeiro facto liga Y1=ines, mas o objetivo restante pai(ines,N) falha. O motor desfaz essa ligação e tenta o facto seguinte, que liga Y1=ana. Agora pai(ana,N) dá N=leo.

O ramo falhado não muda os factos nem fixa Y1 para a tentativa seguinte; um traço completo regista este ponto de retrocesso com a alternativa escolhida.

Negação por falha

\+ Objetivo sucede quando o objetivo não se prova:

?- \+ pai(rui, _).
true.

Não há facto com rui como pai e não há regras que permitam provar esse objetivo. A tentativa falha finitamente e a negação sucede. Se acrescentarmos pai(rui,sofia), a mesma negação passa a falhar: o resultado depende da base de conhecimento disponível.

Termos e variáveis de cada cláusula

Um termo pode ser uma variável, uma constante ou uma estrutura f(t1,...,tn). O nome f e o número de argumentos identificam o functor; pessoa(ana) não unifica com pessoa(ana,20). Um termo sem variáveis é ground. O universo de Herbrand reúne termos ground que podemos construir com os símbolos do programa; não é uma lista de valores da memória.

Em p(X) :- q(X,Y)., o Y é local àquela utilização da cláusula, pelo que cada utilização renomeia todas as variáveis para variáveis frescas.

Para unificar par(X,f(X)) com par(a,Y), a primeira posição dá X=a; propagamos essa ligação e a segunda dá Y=f(a). Para unificar par(X,X) com par(a,b), a primeira posição dá X=a e a segunda exige a=b; falha, porque não podemos escolher uma ligação diferente para cada ocorrência do mesmo X.

Ocorre a variável dentro do termo?

Na unificação de termos finitos, X=f(X) deve falhar: substituir X pelo termo faria a variável ocorrer dentro de si própria. Esta verificação é o occurs check. O =/2 de SWI-Prolog aceita em geral estruturas cíclicas, chamadas rational trees. unify_with_occurs_check(X,f(X)) rejeita a criação desse ciclo. Num exercício teórico que pede a unificação de Herbrand, usa a regra dos termos finitos; não concluas que o resultado do = de uma implementação resolve automaticamente esse exercício.

O que a estratégia de procura decide

SLD resolve um objetivo positivo escolhendo uma cláusula cuja cabeça unifica e substituindo o objetivo pelo corpo dessa cláusula. Prolog costuma escolher o objetivo mais à esquerda e explorar cláusulas de cima para baixo, em profundidade. Uma prova pode existir num ramo posterior e nunca ser encontrada porque um ramo anterior é infinito.

p :- p. antes de p. mostra o problema: a primeira tentativa volta a chamar p indefinidamente. Trocar as cláusulas permite encontrar uma primeira resposta, mas pedir todas volta a entrar no ramo infinito, ou seja não basta haver um caso base algures; a estratégia tem de conseguir chegar a ele.

Uma cláusula de Horn tem no máximo um literal positivo. Uma cláusula definida tem exatamente um, representado pela cabeça. Esta restrição permite organizar a resolução orientada a objetivos a partir da lógica estudada em MD, mas não garante que a procura termine.

A negação por falha também precisa de uma falha finita, pelo que se g divergir, \+ g não confirma a negação.