更紧凑的定义 [英] More compact definition

问题描述

给定word/1,

word(W) :-绝对(AB)，AB = W.绝对([]).abs([AB|ABs]) :-绝对(AB)，ab(AB).ab(a)ab(b).?- 字(W).W = [];W = [a];W = [b];W = [a,a];W = [b,a];W = [a,b];W = [b,b];W = [a,a,a];W = [b,a,a];W = [a,b,a];W = [b,b,a];W = [a,a,b];W = [b,a,b];W = [a,b,b];W = [b,b,b];W = [a,a,a,a]...

word/1 的更紧凑的定义看起来如何，否则与 w.r.t.终止和解决方案集，公平性，具有以下约束:

1. 不使用像 (=)/2 这样的内置函数.

2. 不使用像 (',')/2 或 (;)/2 或 call/1 这样的控制结构>.

3. 对 word/1 使用一个事实、一个递归规则和一个规则.

也许更简单的是要求条款 F1 ... F4 in:

word(W) :-p(F1).p(F2).p(F3) :-p(F4).

记录:这里利用的属性与单个二进制子句终止的不可判定性密切相关.赞美去:

Philippe Devienne、Patrick Lebègue、Jean-Christophe Routier 和 Jörg Würtz.一个二进制 horn 子句就足够了 STACS '94.

解决方案

我想出的解决方案是:

<预>字(W) :-p([[]|Ls], Ls, W).p([W|_], _, W).p([W0|Ws], [[a|W0],[b|W0]|Ls], W) :-p(Ws, Ls, W).

示例查询和答案:

<预>?- 字(W).W = [] ;W = [a] ;W = [b] ;W = [a, a] ;W = [b, a] ;W = [a, b] ;W = [b, b] ;W = [a, a, a] ;W = [b, a, a] ;W = [a, b, a] ;W = [b, b, a] ;W = [a, a, b] ;W = [b, a, b] ;W = [a, b, b] ;W = [b, b, b] ;W = [a, a, a, a] ;W = [b, a, a, a] ;等等.

我正在使用差异列表来逐步实现我希望顶层报告的解决方案.

Given word/1,

word(W) :-
   abs(ABs),
   ABs = W.

abs([]).
abs([AB|ABs]) :-
   abs(ABs),
   ab(AB).

ab(a).
ab(b).

?- word(W).
   W = []
;  W = [a]
;  W = [b]
;  W = [a,a]
;  W = [b,a]
;  W = [a,b]
;  W = [b,b]
;  W = [a,a,a]
;  W = [b,a,a]
;  W = [a,b,a]
;  W = [b,b,a]
;  W = [a,a,b]
;  W = [b,a,b]
;  W = [a,b,b]
;  W = [b,b,b]
;  W = [a,a,a,a]
...

how does a more compact definition of word/1 look like, otherwise identical w.r.t. termination and the set of solutions, fairness, with the following constraints:

1. No use of built-ins like (=)/2.

2. No use of control constructs like (',')/2 or (;)/2, or call/1.

3. Uses one fact, one recursive rule, and one rule for word/1.

Maybe simpler is to ask for the terms F1 ... F4 in:

word(W) :-
   p(F1).

p(F2).
p(F3) :-
   p(F4).

For the record: The property exploited here is closely related to the undecidability of termination of a single binary clause. Praise goes to:

Philippe Devienne, Patrick Lebègue, Jean-Christophe Routier, and Jörg Würtz. One binary horn clause is enough STACS '94.

解决方案

The solution I have come up with is:

word(W) :-
        p([[]|Ls], Ls, W).

p([W|_], _, W).
p([W0|Ws], [[a|W0],[b|W0]|Ls], W) :-
        p(Ws, Ls, W).

Sample query and answer:

?- word(W).
W = [] ;
W = [a] ;
W = [b] ;
W = [a, a] ;
W = [b, a] ;
W = [a, b] ;
W = [b, b] ;
W = [a, a, a] ;
W = [b, a, a] ;
W = [a, b, a] ;
W = [b, b, a] ;
W = [a, a, b] ;
W = [b, a, b] ;
W = [a, b, b] ;
W = [b, b, b] ;
W = [a, a, a, a] ;
W = [b, a, a, a] ;
etc.

I am using a difference list to incrementally materialize the solutions I want the toplevel to report.

这篇关于更紧凑的定义的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！