非決定性の述語 単位行列/2 (「添字」を用いるバージョン) | Codetter（こーどったー）

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
natural(0).
natural(s(N)) :- natural(N).
natural(0, 0).
natural(s(N), X) :- number(X), !, X > 0, X1 is X - 1, natural(N, X1).   % N によって変項 X を単一化させる場合
natural(s(N), X) :- var(X), !, integer_itetate(X, 1), natural(s(N), X). % 両方変項の場合
natural(s(N), X) :- natural_acc(N, X, 1), !.    % X によって変項 N を単一化させる場合
natural_acc(0, X, X).
natural_acc(s(N), X, Acc) :- Acc1 is Acc + 1, natural_acc(N, X, Acc1).
integer_itetate(X, X).
integer_itetate(X, L) :- L1 is L + 1, integer_itetate(X, L1).
mylength_n([], 0).
mylength_n([Head|Tail], s(N)) :- mylength_n(Tail, N).
at_n([Val|_], 0, Val).
at_n([_|List], s(N), Val) :- at_n(List, N, Val).
insertAt_n(List, 0, Val, [Val|List]).
insertAt_n([X|List], s(N), Val, [X|Tail]) :- insertAt_n(List, N, Val, Tail).
零リスト([]).
零リスト([0|T]) :- 零リスト(T).
単位行列_n(0, []).
単位行列_n(s(N), LL) :- 単位行列_n(s(N), LL, 0).    % 行番号によってループする
単位行列_n(N, [], N).
単位行列_n(N, [Row|RowT], M) :-
    mylength_n(Row, N), insertAt_n(RowRems, M, 1, Row), 零リスト(RowRems),
    単位行列_n(N, RowT, s(M)).
    
単位行列(X, LL) :- natural(N, X), 単位行列_n(N, LL).    % インターフェイス
?- 単位行列(2, [[1, 0], [0, 1]]).   %=> yes
?- 単位行列(N, [[1, 0], [0, 1]]).   %=> N = 2 ; ... (無限ループに陥る)
?- 単位行列(2, LL). %=> LL = [[1,0],[0,1]] ; no
?- 単位行列(N, LL). %=> N = 0, 1, 2, ... と順次成功する
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX