A simple O(n^2) DFA minimization implementation in CHR

gistfile1.txt

% DFA minimization

:- use_module(library(chr)).

:- chr_constraint trans/3, state/1, same/2, different/2, final/1, non_final/1, state_order/2.

% A simple test DFA for arithmetic expressions
test :- 
	final(s3),
	trans('(', s1, s1),
	trans('(', s6, s1),
	trans('(', s5, s1),
	trans(')', s3, s3),
	trans(a, s6, s3),
	trans(a, s5, s3),
	trans(+, s3, s6),
	trans(*, s3, s5),
	trans(a, s1, s3).

lexical_before([],[]) :- false, !.
lexical_before([E1|_], [E2|_]) :- E1 < E2.
lexical_before([E1|List1], [E2|List2]) :- E1 = E2, lexical_before(List1, List2).
lexical_before([], [_|_]).
lexical_before(A,B) :-
	atom(A), atom(B),
	atom_codes(A,ACodes),
	atom_codes(B,BCodes),
	lexical_before(ACodes, BCodes).

% Duplicate removal
trans(A,B,C) \ trans(A,B,C) <=> true.
same(A,B) \ same(A,B) <=> true.
state(A) \ state(A) <=> true.
different(A,B) \ different(A,B) <=> true.
non_final(A) \ non_final(A) <=> true.

% Symmetric 
same(A,B) ==> same(B,A).
different(A,B) ==> different(B,A).

% Two states that are different cannot be the same
different(A,B) \ same(A,B) <=> true.

% Infer states
trans(_,A,B) ==> state(A), state(B).

% This will produce O(n^2) state_order contraints, but allow constant-time
% matching for other central rules
state(A), state(B) ==> lexical_before(A,B) | state_order(A,B).

% Assume all states are the same
state_order(A,B), state(A), state(B) ==> same(A,B).

% Assume all states are non_final
state(A) ==> non_final(A).

% If a state is final, then it cannot be non-final
final(A)  \ non_final(A) <=> true.

% If one state is final and another is not, they must be different
final(A), non_final(B) \ same(A,B) <=> different(A,B).
final(B), non_final(A) \ same(A,B) <=> different(A,B).

% separate any two states which has a transition on the same synbol to two states which are separated
%state_order(A,B), state_order(C,D),
trans(Symbol,A,B), trans(Symbol,C,D), different(B,D), same(A,C) <=> different(A,C).

% Use lexical order of states names to collapse states
state_order(A,B), same(A,B) \ trans(Symbol,B,C) <=> trans(Symbol, A, C).

% Use lexical order of states names to collapse states
state_order(A,B), same(A,B) \ trans(Symbol,C,B) <=> write(collaps2), nl, trans(Symbol, C, A).

% Clean-up store when done
trans(_,A,C), state_order(A,B) \ state(B) <=> true.
trans(_,A,C), state_order(A,B) \ state(B) <=> true.
same(_,_) <=> true.
different(_,_) <=> true.
state_order(_,_) <=> true.