可能无限域上的CLP(FD)标号

Question

作为对这个问题的后续，我为基于Prolog的语言布氏对数实现了自己的标记谓词brachylog_equals/2，它不一定会终止，但适用于无限域：

brachylog_equals(Z,Z) :-
    brachylog_equals_('init',10,Z).

brachylog_equals_(I,J,'integer':Z) :-
    fd_inf(Z,'inf'),
    fd_sup(Z,'sup')
    -> (
        (
            I = 'init'
            ;
            I \= 'init',
            abs(Z) #>= I
        ),
        abs(Z) #< J,
        label([Z])
        ;
        I2 is J,
        J2 is J*10,
        brachylog_equals_(I2,J2,'integer':Z)
    )
    ;
    fd_inf(Z,'inf')
    -> (
        (
            I = 'init'
            ;
            I \= 'init',
            Z #=< -I
        ),
        Z #> -J,
        label([Z])
        ;
        I2 is J,
        J2 is J*10,
        brachylog_equals_(I2,J2,'integer':Z)
    )
    ;
    fd_sup(Z,'sup')
    -> (
        (
            I = 'init'
            ;
            I \= 'init',
            Z #>= I
        ),
        Z #< J,
        label([Z])
        ;
        I2 is J,
        J2 is J*10,
        brachylog_equals_(I2,J2,'integer':Z)
    )
    ;
    label([Z]).

有关此代码的几个注意事项：

• 这个谓词应该在自动生成的Prolog代码中使用，因此它的名称并不描述它的函数，而是遵循约定。
• 'integer':Z而不是简单的Z只是为了遵守项目的其余部分(它用于检查其他谓词中的参数类型)

以下是我的担忧：

• 这是最惯用的解决办法吗？(也就是说，在变量具有无限界的情况下，对其施加一个有限界，并在发生回溯时递归地增加它？)
• 这在所有情况下都是正确的吗？(根据我测试的结果，但我想知道我是否错过了一些奇怪的域，它会在其中崩溃)
• 这在计算上有效吗？

当然，对代码样式(我知道它不尊重通常的惯例)或代码简化的评论也是欢迎的。

Answer 1

在讨论正确性、效率和替代方法之前，我首先有三个较小的建议来稍微简化谓词：

• I2似乎没有真正需要的地方，您总是可以简单地使用J。
• 对于J2，我将坚持使用CLP(FD)约束，比如：J2 #= J*10。
• 与(\=)/2不同，我建议使用dif/2。

这些更改使代码更易于阅读和更统一，并使我们能够更好地讨论其余的问题。