Prolog : 可算無限の結果を網羅的に列挙したい


可算無限の結果すべてを列挙できるようなPrologの実装はあるのでしょうか？

例として自然数のペアを列挙するプログラムについて考えさせてください。  
もし、{(0,0), (0,1), (1,0), (0,2), (1,1), (2,0), ...}という順番で答えを列挙すれば、全てのペアを列挙できます。  
しかし、もし{(0,0), (0,1), (0,2), (0,3) ...}という以下のGNU
Prologと同じ順番で答えを列挙すると(1,1)のような結果を取り出すことができません。  
このような可算無限の結果を全て列挙するような研究、実装はあるのでしょうか？

[code]

    % cat nats.pl
    nat(0).
    nat(X1) :- nat(X), X1 is X + 1.
    
    pair_of_nats(X, Y) :- nat(X), nat(Y).
    % prolog
    GNU Prolog 1.3.0
    By Daniel Diaz
    Copyright (C) 1999-2007 Daniel Diaz
    | ?- ['nats.pl'].
    compiling /home/egi/prolog/nats.pl for byte code...
    /home/egi/prolog/nats.pl compiled, 4 lines read - 762 bytes written, 9 ms
    
    yes
    | ?- pair_of_nats(X,Y).
    
    X = 0
    Y = 0 ? ;
    
    X = 0
    Y = 1 ? ;
    
    X = 0
    Y = 2 ? ;
    
    X = 0
    Y = 3 ? 
    
[/code]




Prologは、その仕様として、解の探索をバックトラックを用いて深さ優先で行うことが定められています。そのため、Prologを自動定理証明系として見るとすると、Prologは完全性を持たないということになります。（つまり、求められない論理的帰結があるということです。）幅優先探索を行う処理系を作れば、それは完全性を持つことになります。([Prologの表示的意味論](https://github.com/suharahiromichi/doc/blob/master/cs_prolog_denotational_semantics.md))

_The Fun of Programming_ (Jeremy Gibbons and Oege de Moor
編、邦題『関数プログラミングの楽しみ』山下伸夫 訳)
第9章「論理プログラミングのためのコンビネータ」では、モナドを用いて論理プログラミングを実現する手法について述べていて、幅優先探索を行う技法についても言及があります。




Prologは、その仕様として、解の探索をバックトラックを用いて深さ優先で行うことが定められています。そのため、Prologを自動定理証明系として見るとすると、Prologは完全性を持たないということになります。（つまり、求められない論理的帰結があるということです。）幅優先探索を行う処理系を作れば、それは完全性を持つことになります。([Prologの表示的意味論](https://github.com/suharahiromichi/doc/blob/master/cs_prolog_denotational_semantics.md))

_The Fun of Programming_ (Jeremy Gibbons and Oege de Moor
編、邦題『関数プログラミングの楽しみ』山下伸夫 訳)
第9章「論理プログラミングのためのコンビネータ」では、モナドを用いて論理プログラミングを実現する手法について述べていて、幅優先探索を行う技法についても言及があります。

