Notação sucessora Prolog produz resultado incompleto e loop infinito

Eu começo a aprender Prolog e primeiro aprendi sobre a notação sucessora.

E é aqui que descubro a escrita dos axiomas de Peano no Prolog.

Veja a página 12 do PDF :

sum(0, M, M). sum(s(N), M, s(K)) :- sum(N,M,K). prod(0,M,0). prod(s(N), M, P) :- prod(N,M,K), sum(K,M,P). 

Eu coloquei as regras de multiplicação no Prolog. Então eu faço a consulta:

 ?- prod(X,Y,s(s(s(s(s(s(0))))))). 

O que significa encontrar o fator de 6 basicamente.

Aqui estão os resultados.

 X = s(0), Y = s(s(s(s(s(s(0)))))) ? ; X = s(s(0)), Y = s(s(s(0))) ? ; X = s(s(s(0))), Y = s(s(0)) ? ; infinite loop 

Este resultado tem dois problemas:

  1. Nem todos os resultados são mostrados, observe que o resultado X = 6, Y = 1 está faltando.
  2. Ele não pára a menos que eu Ctrl + C, em seguida, escolha abortar.

Então … minhas perguntas são:

  1. Por que é que? Eu tentei mudar “prod” e “sum” ao redor. O código resultante me fornece todos os resultados. E mais uma vez, por que isso? Ainda assim, faz um loop morto.
  2. COMO resolver isso?

Eu li a outra resposta em loop infinito. Mas eu apreciaria alguém responder baseando-se neste cenário. Isso me ajuda muito.

Se você quiser estudar as propriedades de terminação em profundidade, programas usando aritmética sucessora são um object de estudo ideal: você sabe a priori o que eles devem descrever, para que você possa se concentrar nos detalhes mais técnicos. Você precisará entender várias noções.

Terminação universal

A maneira mais fácil de explicá-lo é considerar o Goal, false . Isso termina se o Goal terminar universalmente. Ou seja: olhar para os rastreadores é a maneira mais ineficaz – eles mostram apenas um único caminho de execução. Mas você precisa entender todos de uma vez! Também nunca olhe para as respostas quando você quer uma terminação universal, elas só irão distraí-lo. Você já viu isso acima: você tem três respostas corretas e corretas, só então o seu programa faz um loop. Então é melhor “desligar” as respostas com false . Isso remove toda a distração.

Fatia de falha

A próxima noção que você precisa é de uma fatia de falha . Pegue um programa lógico monotônico puro e inclua alguns gols false . Se a fatia de falha resultante não terminar (universalmente), também o programa original não será. Em seu exemplo, considere:

 prod (0, M, 0): - falso .
 prod (s (N), M, P): -
     prod (N, M, K), falso,
     sum (K, M, P) .

Essas metas false ajudam a remover adornos irrelevantes em seu programa: A parte restante mostra claramente, por que prod(X,Y,s(s(s(s(s(s(0))))))). não termina. Ele não termina, porque esse fragment não se importa com P jeito nenhum! Você está esperando que o terceiro argumento ajude a fazer o prod/3 terminar, mas o fragment mostra que é tudo em vão, já que P não ocorre em nenhum objective. Não há necessidade de rastreadores tagarela.

Muitas vezes não é tão fácil encontrar fatias de falhas mínimas. Mas uma vez que você encontrou um, é quase trivial determinar suas propriedades de terminação ou não de terminação. Depois de algum tempo, você pode usar sua intuição para imaginar uma fatia e depois usar sua razão para verificar se essa fatia é relevante ou não.

O que é tão notável sobre a noção de uma falha é esta: Se você quer melhorar o programa, você tem que modificar seu programa na parte visível no fragment acima! Contanto que você não mude, o problema persistirá. Uma fatia de falha é, portanto, uma parte muito relevante do seu programa.

Inferência de terminação

Essa é a última coisa que você precisa: Um inferenciador de terminação (ou analisador) como o cTI ajudará você a identificar rapidamente a condição de terminação. Olhe para as condições inferidas de terminação de prod/3 e o melhorado prod2/3 aqui !


Edit: E desde que esta foi uma pergunta de casa eu não postei a solução final. Mas para deixar claro, aqui estão as condições de terminação obtidas até agora:

     prod (A, B, C) termina em b (A), b (B).
     prod2 (A, B, C) termina em b (A), b (B);  b (A), b (C) .

Então o novo prod2/3 é estritamente melhor que o programa original!

Agora, cabe a você encontrar o programa final. Sua condição de rescisão é:

    prod3 (A, B, C) termina em b (A), b (B), b (C).

Para começar, tente encontrar a fatia de falha para prod2(A,B,s(s(s(s(s(s(0))))))) ! Esperamos que isso termine, mas ainda não. Então pegue o programa e adicione manualmente false objectives! A parte restante mostrará a chave!

Como uma dica final: você precisa adicionar uma meta extra e um fato.


Edit: A pedido, aqui está a fatia de falha para prod2(A,B,s(s(s(s(s(s(0))))))) :

 prod2 (0, _, 0): - falso .
 prod2 (s (N), M, P): -
    sum (M, K, P),
    prod2 (N, M, K), falso .

 sum (0, M, M).
 sum (s (N), M, s (K)): - falso ,
     sum (N, M, K) .

Por favor, observe a definição significativamente simplificada de sum/3 . Diz apenas: 0 mais qualquer coisa é qualquer coisa. Não mais. Como conseqüência, até mesmo o mais especializado prod2(A,0,s(s(s(s(s(s(0))))))) irá fazer um loop enquanto prod2(0,X,Y) termina elegantemente …

A primeira pergunta (POR QUÊ) é bastante fácil de detectar, especialmente se souber sobre recursion à esquerda . sum(A,B,C) liga-se a A e B quando C está ligado, mas o programa original prod (A, B, C) não usa essas ligações e, em vez disso, recorre com A, B e não ligado.

Se nós trocarmos sum, prod nós obtemos 2 ligações úteis da sum para a chamada recursiva:

 sum(M, K, P) 

Agora M está ligado e será usado para finalizar a recursion à esquerda. Podemos trocar N e M, porque sabemos que o produto é comutativo.

 sum(0, M, M). sum(s(N), M, s(K)) :- sum(N, M, K). prod3(0, _, 0). prod3(s(N), M, P) :- sum(M, K, P), prod3(M, N, K). 

Note que se nós trocarmos M, K (isto é, sum (K, M, P)), quando prod3 é chamado com P desconhecido nós novamente temos um loop não terminador, mas em sum.

 ?- prod3(X,Y,s(s(s(s(s(s(0))))))). X = s(s(s(s(s(s(0)))))), Y = s(0) ; X = s(s(s(0))), Y = s(s(0)) ; X = s(s(0)), Y = s(s(s(0))) ; X = s(0), Y = s(s(s(s(s(s(0)))))) ; false. 

OT estou perplexo com o relatório cTI: prod3 (A, B, C) termina_se b (A), b (B), b (A), b (C).