module BitString. kind bool type. type t bool. type f bool. kind exp type. type e_eps exp. type e_ind (bool -> exp -> exp -> exp). type bnot (bool -> bool -> o). type append (list A -> list A -> list A -> o). type decode (exp -> list bool -> o). type encode (list bool -> exp -> o). bnot t f. bnot f t. append [] L L. append (X::J) K (X::L) :- append J K L. decode e_eps nil. decode (e_ind B E1 E2) S :- bnot B B', decode E1 S1, decode E2 S2, append (B::S1) (B'::S2) S. encode nil e_eps. encode S (e_ind B E1 E2) :- bnot B B', append (B::S1) (B'::S2) S, encode S1 E1, encode S2 E2.


[BitString] ?- encode (f :: f :: t :: t :: f :: t :: f :: t :: t :: f :: nil) X. The answer substitution: X = e_ind f (e_ind f e_eps e_eps) (e_ind f e_eps (e_ind f e_eps (e_ind t e_eps e_eps))) More solutions (y/n)? y The answer substitution: X = e_ind f (e_ind f e_eps e_eps) (e_ind f (e_ind t e_eps e_eps) (e_ind t e_eps e_eps)) More solutions (y/n)? y The answer substitution: X = e_ind f (e_ind f e_eps (e_ind t e_eps e_eps)) (e_ind f e_eps (e_ind t e_eps e_eps)) More solutions (y/n)? y The answer substitution: X = e_ind f (e_ind f e_eps (e_ind t e_eps (e_ind t e_eps e_eps))) (e_ind t e_eps e_eps) More solutions (y/n)? y The answer substitution: X = e_ind f (e_ind f e_eps (e_ind t (e_ind f e_eps e_eps) e_eps)) (e_ind t e_eps e_eps) More solutions (y/n)? y no (more) solutions


얼마전에 배운 개날먹 언어