【目標】述語 単位行列/2 を“うまく”定義する。
【出典】http://codetter.com/?p=902
「添字」を考えて、単位行列 E_n := [ δ_i,j ]_n×n として定義する。
数値を用いると is によって双方向性を失ってしまうので、ペアノ自然数 s(N) を用いる。
ペアノ自然数と数値を相互に単一化させる述語 natural/2 に、めんどくさい条件分岐を押し付けることで、定義を簡潔にする試み。
【目標】述語 単位行列/2 を“うまく”定義する。
【出典】http://codetter.com/?p=902
「添字」を考えて、単位行列 E_n := [ δ_i,j ]_n×n として定義する。
数値を用いると is によって双方向性を失ってしまうので、ペアノ自然数 s(N) を用いる。
ペアノ自然数と数値を相互に単一化させる述語 natural/2 に、めんどくさい条件分岐を押し付けることで、定義を簡潔にする試み。
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, ... と順次成功する