トップページ：初学者向けCHRの使い方まとめ

例題目録 †

↑

boolean.pl †

コード

:- module(boolean, 
[boolean/1, and/3, or/3, xor/3, neg/2, imp/2, labeling/0, 
    half_adder/4, full_adder/5]).
:- use_module( library(chr)).

%% Deprecated syntax used for SICStus 3.x
%handler boolean.
%constraints boolean/1, and/3, or/3, xor/3, neg/2, imp/2, 
%   labeling/0, half_adder/4, full_adder/5.

%% Syntax for SWI / SICStus 4.x
:- chr_type bool ---> 0 ; 1.

:- chr_constraint
    boolean(?bool),
    and(?bool,?bool,?bool), 
    or(?bool,?bool,?bool), 
    xor(?bool,?bool,?bool),
    neg(?bool,?bool), 
    imp(?bool,?bool),
    labeling,
    half_adder(?bool,?bool,?bool,?bool),
    full_adder(?bool,?bool,?bool,?bool,?bool).


boolean(0) <=> true.
boolean(1) <=> true.

labeling \ boolean(A) <=> A=0 ; A=1.


%% and/3 specification
%%and(0,0,0).
%%and(0,1,0).
%%and(1,0,0).
%%and(1,1,1).

and(0,_,Y) <=> Y=0.
and(_,0,Y) <=> Y=0.
and(1,X,Y) <=> Y=X.
and(X,1,Y) <=> Y=X.
and(X,Y,1) <=> X=1,Y=1.
and(X,X,Z) <=> X=Z.
and(X,Y,A) \ and(X,Y,B) <=> A=B.
and(X,Y,A) \ and(Y,X,B) <=> A=B.

labeling \ and(A,B,C) <=> label_and(A,B,C).

label_and(0,_,0).
label_and(1,X,X).


%% or/3 specification
%%or(0,0,0).
%%or(0,1,1).
%%or(1,0,1).
%%or(1,1,1).

or(0,X,Y) <=> Y=X.
or(X,0,Y) <=> Y=X.
or(X,Y,0) <=> X=0,Y=0.
or(1,_,Y) <=> Y=1.
or(_,1,Y) <=> Y=1.
or(X,X,Z) <=> X=Z.
or(X,Y,A) \ or(X,Y,B) <=> A=B.
or(X,Y,A) \ or(Y,X,B) <=> A=B.

labeling \ or(A,B,C) <=> label_or(A,B,C).

label_or(0,X,X).
label_or(1,_,1).


%% xor/3 specification
%%xor(0,0,0).
%%xor(0,1,1).
%%xor(1,0,1).
%%xor(1,1,0).

xor(0,X,Y) <=> X=Y.
xor(X,0,Y) <=> X=Y.
xor(X,Y,0) <=> X=Y.
xor(1,X,Y) <=> neg(X,Y).
xor(X,1,Y) <=> neg(X,Y).
xor(X,Y,1) <=> neg(X,Y).
xor(X,X,Y) <=> Y=0.
xor(X,Y,X) <=> Y=0.
xor(Y,X,X) <=> Y=0.
xor(X,Y,A) \ xor(X,Y,B) <=> A=B.
xor(X,Y,A) \ xor(Y,X,B) <=> A=B.

labeling \ xor(A,B,C) <=> label_xor(A,B,C).

label_xor(0,X,X).
label_xor(1,X,Y) :- neg(X,Y).


%% neg/2 specification
%%neg(0,1).
%%neg(1,0).

neg(0,X) <=> X=1.
neg(X,0) <=> X=1.
neg(1,X) <=> X=0.
neg(X,1) <=> X=0.
neg(X,X) <=> fail.
neg(X,Y) \ neg(Y,Z) <=> X=Z.
neg(X,Y) \ neg(Z,Y) <=> X=Z.
neg(Y,X) \ neg(Y,Z) <=> X=Z.

%% Interaction with other boolean constraints
neg(X,Y) \ and(X,Y,Z) <=> Z=0.
neg(Y,X) \ and(X,Y,Z) <=> Z=0.
neg(X,Z) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Z,X) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Y,Z) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(Z,Y) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(X,Y) \ or(X,Y,Z) <=> Z=1.
neg(Y,X) \ or(X,Y,Z) <=> Z=1.
neg(X,Z) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Z,X) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Y,Z) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(Z,Y) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(X,Y) \ xor(X,Y,Z) <=> Z=1.
neg(Y,X) \ xor(X,Y,Z) <=> Z=1.
neg(X,Z) \ xor(X,Y,Z) <=> Y=1.
neg(Z,X) \ xor(X,Y,Z) <=> Y=1.
neg(Y,Z) \ xor(X,Y,Z) <=> X=1.
neg(Z,Y) \ xor(X,Y,Z) <=> X=1.
neg(X,Y) , imp(X,Y) <=> X=0,Y=1.
neg(Y,X) , imp(X,Y) <=> X=0,Y=1.

labeling \ neg(A,B) <=> label_neg(A,B).

label_neg(0,1).
label_neg(1,0).


%% imp/2 specification (implication)
%%imp(0,0).
%%imp(0,1).
%%imp(1,1).

imp(0,_) <=> true.
imp(X,0) <=> X=0.
imp(1,X) <=> X=1.
imp(_,1) <=> true.
imp(X,X) <=> true.
imp(X,Y),imp(Y,X) <=> X=Y.

labeling \ imp(A,B) <=> label_imp(A,B).

label_imp(0,_).
label_imp(1,1).


%% half_adder/4: add bits X and Y, result in S and carry in C
%% X+Y = S+2*C
half_adder(X,Y,S,C) <=>
    xor(X,Y,S), and(X,Y,C).


%% full_adder/5: add bits X, Y and Ci, result in S and carry in Co
%% X+Y+Ci = S+2*Co
full_adder(X,Y,Ci,S,Co) <=>
    half_adder(X,Y,S1,Co1), half_adder(Ci,S1,S,Co2), or(Co1,Co2,Co).

このプログラムは、各種の論理関数(boolean,and,or,xor,neg,imp,半加算器、全加算器)をシミュレートすることができ、入力に矛盾が無いことを確認しつつ、正しく解ける時の変数についての制約として得られたことを出力してくる。 例えば

and(0,1,A), xor(1,1,B).

という入力に対しては、

and(0,_,A) <=> A=0.
xor(1,X,Y) <=> neg(X,Y).
neg(1,X) <=> X=0.

という3つのルールから

A=0, B=0.

という出力が得られる。

neg(A,A).

という入力に対しては、

neg(X,X) <=> fail.

というルールのみが発火するため

no.

という結果(解なし)が得られる。

また、

neg(A,B), or(A,B,C), labeling.

という制約を入力すれば、

labeling \ or(A,B,C) <=> label_or(A,B,C).

というルールで生成されたlabel_or制約が

label_or(0,X,X).
label_or(1,_,1).

という制約と矛盾しないように変数の値を選択されることになるため、出力は

A = 0, B = 1, C = 1, labeling.
A = 1, B = 0, C = 1, labeling.

の二通りになる。(SWI-prologはすべての解を網羅するため)

labeling制約がない場合、CHRの機能だけではどのルールも発火しないはずだが、SWI-prologは解を網羅して分かったC = 1を使って

C = 1, neg(A,B).

を出力してくる。

↑

equations_gauss.pl †

コード

:- module(equations_gauss, [eq/2, {}/1]).
:- use_module(library(chr)).
:- use_module(library(lists)).
user:library_directory('.').
:- use_module(library(var_order)).

:- op(600,xfx,eq).

%% Deprecated syntax used for SICStus 3.x
%handler gauss.
%constraints eq/2, {}/1.

%% Syntax for SWI / SICStus 4.x
:- chr_constraint eq/2, {}/1.

%% Poly eq Const, where Poly is list of monomials Coefficient*Variable
%%    eq/2

%% curly brackets as wrapper to avoid name clash with built-in =
%%    {}/1   


%% split system of equations
split @     {E, F} <=> {E}, {F}.

%% convert arbitrary polynomial equation to eq-notation
normalize @ {A = B} <=> globalize([A-B]), 
    normpoly([A-B] eq 0, Poly eq Const), Poly eq Const.


%% 0=C
zero @      [] eq C <=> zero(C).

%% normalize first coefficient to 1
norm1 @     [A*X|P] eq C <=> notzero(A-1) | 
    multpoly(1/A,P eq C,P2 eq C2), [1*X|P2] eq C2.

%% const on left side (because of bound variable)
bound @     P eq C <=> select(A*X, P, P0), number(X) | C0 is C-A*X, P0 eq C0.

%% A*X = C  =>  bind variable
bind @      [A*X] eq C <=> var(X) | X is C/A.


%% Gaussian elimination 
elimate @   [A*X|P] eq C \ Q eq D <=>
    select(B*X, Q, Q1) |
    multpoly(-B/A, P eq C, E),
    addpoly(E, Q1 eq D, Q0 eq D0), 
    Q0 eq D0.


%% Auxiliary predicates

%% stable variable order based on chr/ordering by C. Holzbaur (var_order.pl)
%% compare variables with var_compare
ord_lss(X,Y) :- var_compare(<,X,Y).
%% otherwise use Prolog standard order
ord_lss(X,Y) :- nonvar(Y), X @< Y.


%% numerical stabilty
notzero(A) :- abs(A) >  0.000001.
zero(A)    :- abs(A) =< 0.000001.

%% safe_is(X,Exp): X is Exp; fails, if Exp is not an arith. expression
safe_is(X,Exp) :- on_exception(_, X is Exp, fail).


%% normalize polynomial equation
normpoly([X] eq C, [1*X] eq C) :- var(X), !.
normpoly([X] eq C, [1*X] eq C) :- simple(X), \+ number(X).
normpoly([A] eq C, [] eq C0) :- number(A), C0 is C-A.
normpoly([A,B|P] eq C, E0) :- 
    normpoly([A] eq 0,E1), normpoly([B|P] eq C,E2), addpoly(E1,E2,E0).
normpoly([+A] eq 0, E0) :- 
    normpoly([A] eq 0, E0).
normpoly([-A] eq 0, E0) :- 
    normpoly([A] eq 0, E1), multpoly(-1, E1, E0).
normpoly([A+B] eq C, E0) :- 
    normpoly([A] eq C,E), normpoly([B] eq 0,F), addpoly(E,F,E0).
normpoly([A-B] eq C, E0) :- normpoly([A] eq C,E), normpoly([B] eq 0,F),
    multpoly(-1,F,F1), addpoly(E,F1,E0).
normpoly([A*X] eq 0, E0) :-
    safe_is(A1,A), normpoly([X] eq 0, E), multpoly(A1,E,E0).
normpoly([X*A] eq 0, E0) :-
    safe_is(A1,A), normpoly([X] eq 0, E), multpoly(A1,E,E0).
normpoly([X/A] eq 0, E0) :-
    safe_is(A1,1/A), normpoly([X] eq 0, E), multpoly(A1,E,E0).
normpoly([A] eq C, P0 eq C0) :- 
    C\==0, normpoly([A] eq 0, P0 eq C1), C0 is C+C1.


%% addpoly(E,F, E0): add polynomial equations
%% requires: polynomials ordered + duplicate free; retains properties
addpoly(P eq C, [] eq D, P eq C0) :- !, C0 is C+D.
addpoly([] eq C, Q eq D, Q eq C0) :- !, C0 is C+D.
addpoly([A*X|P] eq C, [B*Y|Q] eq D, E0) :- X==Y, !,
    A1 is A+B, addpoly(P eq C, Q eq D, P1 eq C1),
    (zero(A1) -> E0 = P1 eq C1 ; E0 = [A1*X|P1] eq C1).
addpoly([A*X|P] eq C, [B*Y|Q] eq D, [A*X|P0] eq C0) :- ord_lss(X,Y), !,
    addpoly(P eq C, [B*Y|Q] eq D, P0 eq C0).
addpoly([A*X|P] eq C, [B*Y|Q] eq D, [B*Y|P0] eq C0) :- ord_lss(Y,X), !,
    addpoly([A*X|P] eq C, Q eq D, P0 eq C0).
   
%% multpoly(M,E, E0): multiply polynomial equation with scalar
multpoly(M, [] eq C, [] eq C0) :- C0 is M*C. 
multpoly(M, [A*X|P] eq C, E0) :- 
    A1 is M*A, multpoly(M,P eq C,P1 eq C1),
    (zero(A1) -> E0 = P1 eq C1 ; E0 = [A1*X|P1] eq C1).

こちらはガウスの消去法により連立一次方程式を解くSolverである。

%% Auxiliary predicates

以降の記述はSWI-prologの述語(CHRで言う伝播規則のような動作をするルールのような何か、とにかく別言語の記法)であり、このSolverはPrologの動作に大きく依存している。ここで行う動作解説はCHRに関するものであり、また動作もPrologの知識に属するものなため、Auxilliary predicatesの内容(AP)による変化は結果を簡単に記述する以外は説明しない。興味がある場合は自分でprologの勉強をしてほしい。

入力例1として、

{2+2*X+4*Y+2*Z=0, 4+2*X+4*Y+4*Z=0, 1+2*X+3*Z=0}.

を与える。 この入力はまず、splitルールによって

{2+2*X+4*Y+2*Z=0},
{4+2*X+4*Y+4*Z=0},
{1+2*X+3*Z=0}.

と変換される。その後、normalizeルール及びAPによって

[2*X,4*Y,2*Z] eq -2,
[2*X,4*Y,4*Z] eq -4,
[2*X,3*Z] eq -1.

となり、eliminateルールとAPによって

[2*X,4*Y,2*Z] eq -2,
[2*Z] eq -2,
[2*X,3*Z] eq -1.

に変換されて、bindルール及びprologのライブラリにあるis/2 (第一引数が第二引数と等しいとtrue)により、Z = -1.0で束縛される。制約は

[2*X,4*Y,2*Z] eq -2,
[2*X,3*Z] eq-1.

となり、boundルールによってZ項は右辺に移項され、

[2*X,4*Y] eq 0,
[2*X] eq 2.

となる。再びbindルール及びboundルールが発火して、X=1.0で束縛されるとともに、制約が

[4*Y] eq -2.

となる。当然これもbindルールで変換され、Y=-0.5で束縛される。 結果、束縛された変数である

X=1.0, Y=-0.5, Z=-1.0.

が解として出力される。このようにしてこのSolverは連立一次方程式を解く。

↑

interval.pl †

コード

:- module(interval, [(::)/2, le/2, eq/2, ne/2, add/3, mult/3, int/1, bool/1, 
    split0/1, split/1, label/1]).
:- use_module( library(chr)).

% for domain constraints
:- op( 700,xfx,'::').
:- op( 600,xfx,':').
% for inequality constraints
:- op( 700,xfx,le).
:- op( 700,xfx,ne).
:- op( 700,xfx,eq). 

%% Deprecated syntax used for SICStus 3.x
%handler interval.
%constraints 

%% Syntax for SWI / SICStus 4.x
:- chr_constraint

% X::Min:Max - X is between the numbers Min and Max, inclusively
% X must always be an unbound variable(!), and Min and Max evaluable
% (i.e. ground) arithmetic expressions (or numbers)
    (::)/2, 
    le/2, eq/2, ne/2, add/3, mult/3,
% int(X) says that X is an integer (default is a real)
    int/1,
% bool(X) says that X is a boolean (default is a real)
    bool/1,

    split0/1,
    split/1,
    label/1,    % repeated split/1

    browse/1.   % watch how domain of X evolves


% Auxiliary -----------------------------------

browse(X), X::A:B ==> write((X::A:B)),nl.

% define the smallest intervals you want to get:
% the smaller, the more precise, the longer the computation
small(A:B) :- A+2.0e-05>=B. 

% is zero part of A:B ?
withzero(A:B) :- A=<0, 0=<B.


% Intersection  -------------------------------

redundant @ X::A:B \ X::C:D <=>
        (C=<A, B=<D ; A<B,small(A:B), C<D,small(C:D)) | true.

intersect @ X::A:B , X::C:D <=>
        X::max(A,C):min(B,D).


% Special Cases  -------------------------------

failure @ _::A:B <=> A>B | fail.

compute @ X::A:B <=> \+ (number(A),number(B)) | C is A, D is B, X::C:D.

integer @ int(X), X::A:B ==> \+ (integer(A),integer(B)) | 
      C is integer(ceiling(A)), D is integer(floor(B)), X::C:D.

bool @ bool(X), X::_:B ==> B<1 | X::0:0.
bool @ bool(X), X::A:_ ==> A>0 | X::1:1.
bool @ bool(X) ==> X::0:1.


% Inequality -------------------------------

(le) @ X le Y, X::A:_, Y::_:D ==> Y::A:D, X::A:D.
(eq) @ X eq Y, X::A:B, Y::C:D ==> Y::A:B, X::C:D.
(ne) @ X ne Y, X::A:A, Y::A:A <=> fail.

(ne_int) @ int(X) \ X ne Y, X::A:B <=> A=Y | X::A+1:B.
(ne_int) @ int(X) \ X ne Y, X::A:B <=> B=Y | X::A:B-1.
(ne_int) @ int(X) \ Y ne X, X::A:B <=> A=Y | X::A+1:B.
(ne_int) @ int(X) \ Y ne X, X::A:B <=> B=Y | X::A:B-1.


% Addition X+Y=Z -------------------------------

add @ add(X,Y,Z), X::A:B, Y::C:D, Z::E:F ==>
        X::E-D:F-C, Y::E-B:F-A, Z::A+C:B+D.


% Multiplication X*Y=Z -------------------------------

mult_z @ mult(X,Y,Z), X::A:B, Y::C:D ==> 
         M1 is A*C, M2 is A*D, M3 is B*C, M4 is B*D,
         Z::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),max(M3,M4)).

mult_y @ mult(X,Y,Z), X::A:B, Z::E:F ==>
         \+ withzero(A:B) |
         M1 is E/A, M2 is E/B, M3 is F/A, M4 is F/B,
         Y::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),max(M3,M4)).
mult_x @ mult(Y,X,Z), X::A:B, Z::E:F ==>
         \+ withzero(A:B) |
         M1 is E/A, M2 is E/B, M3 is F/A, M4 is F/B,
         Y::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),max(M3,M4)).

mult_xyz @ mult(X,Y,Z), X::A:B, Y::C:D, Z::E:F ==>
         withzero(A:B), withzero(C:D), \+ withzero(E:F) |
         (A*C<E -> D>0, X::E/D:B ; true),
         (B*D<E -> C<0, X::A:E/C ; true),
         (F<A*D -> C<0, X::F/C:B ; true),
         (F<B*C -> D>0, X::A:F/D ; true).


% Labeling --------------------------------------------------------

label @ split0(X), X::A:B <=> \+ small(A:B), A<0,0<B |
           (X::A:0 ; X::0:B). 

label @ split(X), X::A:B <=> \+ small(A:B) |
           Half is (A+B)/2,
           (X::A:Half ; X::Half:B).

label @ label(X), X::A:B <=> \+ small(A:B) |
           Half is (A+B)/2,
           (X::A:Half ; X::Half:B), 
           label(X).

これは数値に幅のある整数または実数の変数を扱うSolverである。 例えば、1~3まであり得るXと2~4まであり得るYの和X+Yは3~7まであり得るというような計算を処理することになる。 以下、入力例とその場合の動作である。

input
X::3:5, X::2:4.

intersectルールにより、 二つの制約は X::max(3,2):min(5,4) 則ち X::3:4 に書き換えられ出力される。

input
X le Y, X::3:5, Y::2:4.

le/2はless or equalを表す制約で、X=<Yの意味になる。 今回は伝播規則(le)が発火して、

Y::3:4, X::3:4

という制約が新たに生成される。 ここでintersectルールまたはrebundantルールが発火し、

X::3:4, X::3:5

という制約は

X::3:4

に書き換えられる。 また、

Y::3:4, Y::2:4

という制約も同じ2つのルールのどちらかによって

Y::3:4

に書き換えられる。 従って出力は

X le Y, X::3:4, Y::3:4

となる。

input
add(X,Y,Z), X::2:5, Y::3:4, Z::1:7

addは X+Y=Z の関係を表す制約である。

この入力に対しては伝播規則addが発火し、

X::1-4:7-3, Y::1-5:7-2, Z::2+3:4+5

則ち

X:: -3:4, Y:: -4:5, Z::5:9

という制約を生成する。 これが元々あった制約群と合わせてintersectルールまたはrebundantルールによって X::2:4, Y::3:4, Z::5:7 となる。 数値が変化したためもう一度addルールは発火するが、結局intersectルールまたはrebundantルールが発火して生成された制約は消去される。これ以上は伝播規則の性質によりaddルールは発火しない。従って出力は add(X,Y,Z), X::2:4, Y::3:4, Z::5:7 となる。

mult(X,Y,Z), X:: -2:3, Y:: -3:4, Z:: -12: -9.

multはX*Y=Zの関係を表す制約である。 半角スペースが入っているのは - が :: と結合して違う名前の制約扱いされないようにである。

この入力に対して4つの伝播規則mult_z, mult_y, mult_xが一度ずつ発火する。 mult_zにより、

M1=-2*-3=6, M2=-2*4=-8, M3=3*-3=-9, M4=3*4=12

を使って

Z:: -9:12

が生成され、 mult_yにより、

M1=-12/-2=6, M2=-12/3=-4, M3=-9/-2=4.5, M4=-9/3=-3

を使って

Y:: -4:6

が生成され、 mult_xにより、

M1=-12/-3=4, M2=-12/4=-3, M3=-9/-3=3, M4=-9/4=-2.25

を使って

X:: -3: 4

が生成される。 mult_xyzはwithzero制約がないので発火しない。 ここからintersectルールまたはrebundantルールによって、

X:: -2:3, X:: -3:4,
Y:: -3:4, Y:: -4:6,
Z:: -12: -9, Z:: -9:12,

という制約は

X:: -2:3, Y:: -3:4, Z:: -9: -9

に単純化される。これが出力となる。

input
A::(-3):3, B::(-3):3, C::4:4, mult(A,B,C), A eq B, label(A).

label/1はprologのライブラリにある述語でもあり、引数に与えられた変数に何か値が代入されていればtrueとなる。

3番目のlabelルールにより、Aの範囲は上限・下限の平均値でわけたどちらかから選択される。 また、(eq)ルールとintersectまたはrebundantルールが実行されればBの範囲はAに合わせられることになる。 その前後でmult(A,B,C)が発火し、結果Cが4を含まない範囲であるという制約が生成されればバックトラックが発生してAの範囲を選び直すことになる。 それを繰り返してでA,Bの範囲が狭まっていく。 これだけだと無限ループになるが、ある程度範囲が狭くなると述語

small(A:B) :- A+2.0e-05>=B

が成功し、3番目のlabelルールが発火しなくなって止まる。 何回繰り返しているかは不明確なのでここでは省略する。

トップ   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS