gerrit / prolog-cafe / 199d14f3309e089912c2aabde0391a61e2bdad02 / . / examples / benchmarks / holmer / fast_mu.pl

% | |

% The MU-puzzle | |

% from Hofstadter's "Godel, Escher, Bach" (pp. 33-6). | |

% written by Bruce Holmer | |

% | |

% To find a derivation type, for example: | |

% theorem([m,u,i,i,u]). | |

% Also try 'miiiii' (uses all rules) and 'muui' (requires 11 steps). | |

% Note that it can be shown that (# of i's) cannot be a multiple | |

% of three (which includes 0). | |

% Some results: | |

% | |

% string # steps | |

% ------ ------- | |

% miui 8 | |

% muii 8 | |

% muui 11 | |

% muiiu 6 | |

% miuuu 9 | |

% muiuu 9 | |

% muuiu 9 | |

% muuui 9 | |

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |

main :- theorem([m,u,i,i,u]). | |

% First break goal atom into a list of characters, | |

% find the derivation, and then print the results. | |

theorem(G) :- | |

length(G, GL1), | |

GL is GL1 - 1, | |

derive([m,i], G, 1, GL, Derivation, 0). | |

% nl, print_results([rule(0,[m,i])|Derivation], 0). | |

% derive(StartString, GoalString, StartStringLength, GoalStringLength, | |

% Derivation, InitBound). | |

derive(S, G, SL, GL, D, B) :- | |

% B1 is B + 1, | |

% write('depth '), write(B1), nl, | |

derive2(S, G, SL, GL, 1, D, B). | |

derive(S, G, SL, GL, D, B) :- | |

B1 is B + 1, | |

derive(S, G, SL, GL, D, B1). | |

% derive2(StartString, GoalString, StartStringLength, GoalStringLength, | |

% ScanPointer, Derivation, NumRemainingSteps). | |

derive2(S, S, SL, SL, _, [], _). | |

derive2(S, G, SL, GL, Pin, [rule(N,I)|D], R) :- | |

lower_bound(SL, GL, B), | |

R >= B, | |

R1 is R - 1, | |

rule(S, I, SL, IL, Pin, Pout, N), | |

derive2(I, G, IL, GL, Pout, D, R1). | |

rule([m|T1], [m|T2], L1, L2, Pin, Pout, N) :- | |

rule(T1, T2, L1, L2, Pin, Pout, 1, i, N, X, X). | |

% rule(InitialString, FinalString, InitStrLength, FinStrLength, | |

% ScanPtrIn, ScanPtrOut, StrPosition, PreviousChar, | |

% RuleNumber, DiffList, DiffLink). | |

% The difference list is used for doing a list concatenate in rule 2. | |

rule([i], [i,u], L1, L2, Pin, Pout, Pos, _, 1, _, _) :- | |

Pos >= Pin, | |

Pout is Pos - 2, | |

L2 is L1 + 1. | |

rule([], L, L1, L2, _, 1, _, _, 2, L, []) :- | |

L2 is L1 + L1. | |

rule([i,i,i|T], [u|T], L1, L2, Pin, Pout, Pos, _, 3, _, _) :- | |

Pos >= Pin, | |

Pout is Pos - 1, | |

L2 is L1 - 2. | |

rule([u,u|T], T, L1, L2, Pin, Pout, Pos, i, 4, _, _) :- | |

Pos >= Pin, | |

Pout is Pos - 2, | |

L2 is L1 - 2. | |

rule([H|T1], [H|T2], L1, L2, Pin, Pout, Pos, _, N, L, [H|X]) :- | |

Pos1 is Pos + 1, | |

rule(T1, T2, L1, L2, Pin, Pout, Pos1, H, N, L, X). | |

% print_results([], _). | |

% print_results([rule(N,G)|T], M) :- | |

% M1 is M + 1, | |

% write(M1), write(' '), print_rule(N), write(G), nl, | |

% print_results(T, M1). | |

% | |

% print_rule(0) :- write('axiom '). | |

% print_rule(N) :- N =\= 0, write('rule '), write(N), write(' '). | |

% | |

lower_bound(N, M, 1) :- N < M. | |

lower_bound(N, N, 2). | |

lower_bound(N, M, B) :- | |

N > M, | |

Diff is N - M, | |

P is Diff/\1, % use and to do even test | |

(P =:= 0 -> | |

B is Diff >> 1; % use shifts to divide by 2 | |

B is ((Diff + 1) >> 1) + 1). | |

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |