# Answer Set Programming for Regular Inference
## Appendix B The Complete Example of an ASP Program for NFA Induction  
Suppose we are given \(\Sigma=\{a,b\}\), \(S_{+}=\{a\}\), \(S_{-}=\{b\}\), and \(k=2\). After grounding rules (5)-(24) we get a program \(\Pi\) in a Clasp format (symbol :- denotes left arrow, symbol not denotes default negation, and symbol lambda denotes the empty word \(\varepsilon\)):  
``` symbol(a). symbol(b). prefix(lambda). prefix(a). prefix(b). positive(a). negative(b). join(lambda,a,a). join(lambda,b,b). q(0). q(1). delta(0,a,0):-not not_delta(0,a,0). delta(1,a,0):-not not_delta(1,a,0). delta(0,b,0):-not not_delta(0,b,0). delta(1,b,0):-not not_delta(1,b,0). delta(0,a,1):-not not_delta(0,a,1). delta(1,a,1):-not not_delta(1,a,1). delta(0,b,1):-not not_delta(0,b,1). delta(1,b,1):-not not_delta(1,b,1). not_delta(0,a,0):-not delta(0,a,0). not_delta(1,a,0):-not delta(1,a,0). not_delta(0,b,0):-not delta(0,b,0). not_delta(1,b,0):-not delta(1,b,0). not_delta(0,a,1):-not delta(0,a,1). not_delta(1,a,1):-not delta(1,a,1). not_delta(0,b,1):-not delta(0,b,1). not_delta(1,b,1):-not delta(1,b,1). x(lambda,0):-not not_x(lambda,0). x(a,0):-not not_x(a,0). x(b,0):-not not_x(b,0). x(lambda,1):-not not_x(lambda,1). x(a,1):-not not_x(a,1). x(b,1):-not x(b,1). not_x(lambda,0):-not x(lambda,0). not_x(a,0):-not x(a,0). not_x(b,0):-not x(b,0). not_x(lambda,1):-not x(lambda,1). not_x(a,1):-not x(a,1). not_x(b,1):-not x(b,1). x(a,0):-delta(1,a,0),x(lambda,1). x(a,1):-delta(1,a,1),x(lambda,1). x(b,0):-delta(1,b,0),x(lambda,1). x(b,1):-delta(1,b,1),x(lambda,1). x(a,0):-delta(0,a,0),x(lambda,0). x(a,1):-delta(0,a,1),x(lambda,0). x(b,0):-delta(0,b,0),x(lambda,0). x(b,1):-delta(0,b,1),x(lambda,0). :-x(a,0),0):=count{0,delta(0,a,0):x(lambda,0),delta(0,a,0); 0,delta(1,a,0):delta(1,a,0):delta(1,a,0),x(lambda,1)}. :-x(a,1),0):-count{0,delta(0,a,1):x(lambda,0),delta(0,a,1); 0,delta(1,a,1):x(lambda,1),delta(1,a,1)}. :-x(b,0),0)=count{0,delta(0,b,0):x(lambda,0),delta(0,b,0); 0,delta(1,b,0):x(lambda,1),delta(1,b,0)}. :-x(b,1),0)=count{0,delta(0,b,1):x(lambda,0),delta(0,b,1); 0,delta(1,b,1):x(lambda,1),delta(1,b,1)}. final(0):-not not_final(0). final(1):-not not_final(1). not_final(0):-not final(0). :-0>=#count{0,final(0):final(0),x(a,0);0,final(1):final(1),x(a,1)}. :-final(0),x(b,0). :-final(1),x(b,1). :-x(lambda,1). :-not x(lambda,0). has_state(lambda):-x(lambda,0). has_state(a):-x(a,0). has_state(b):-x(b,0). has_state(lambda):-x(lambda,1). has_state(a):-x(a,1). has_state(b):-x(b,1). :-not has_state(lambda). :-not has_state(a). :-not has_state(b). One of the answer sets \(X\) is:

q(0) q(1) prefix(lambda) prefix(a) prefix(b) symbol(a) symbol(b) negative(b) positive(a) join(lambda,a,a) join(lambda,b,b) x(lambda,0) not_x(lambda,1) has_state(lambda) not_delta(0,a,0) not_delta(1,a,0) delta(0,b,0) not_delta(1,b,0) delta(0,a,1) not_delta(1,a,1) not_delta(0,b,1) not_delta(1,b,1) not_x(a,0) x(b,0) x(a,1) not_x(b,1) not_final(0) final(1) has_state(a) has_state(b)

Note that the above answer set corresponds to a 2-state automaton having non-final state \(q_{0}\) and final state \(q_{1}\) (see predicates not_final(0) and final(1)), and the following transitions \(q_{0}\in\delta(q_{0},b)\), \(q_{1}\in\delta(q_{0},a)\) (defined by predicates delta(0,b,0) and delta(0,a,1)). It can be easily verified that \(\Pi^{X}=P\) is the positive program:

symbol(a). symbol(b). prefix(lambda). prefix(a). prefix(b). positive(a). negative(b). join(lambda,a,a). join(lambda,b,b). q(0). q(1). delta(0,b,0). delta(0,a,1). not_delta(0,a,0). not_delta(1,a,0). not_delta(1,b,0). not_delta(1,a,1). not_delta(0,b,1). not_delta(1,b,1). x(lambda,0). x(b,0). x(a,1). not_x(a,0). not_x(lambda,1). not_x(b,1). x(a,0). x(a,0).-delta(1,a,0),x(lambda,1). x(a,1).-delta(1,a,1),x(lambda,1). x(b,0):-delta(1,b,0),x(lambda,1). x(b,1):-delta(1,b,1),x(lambda,1). x(a,0):-delta(0,a,0),x(lambda,0). x(a,1):-delta(0,a,1),x(lambda,0). x(b,0):-delta(0,b,0),x(lambda,0). x(b,1):-delta(0,b,1),x(lambda,0). final(1). not_final(0). has_state(lambda):-x(lambda,0). has_state(a):-x(a,0). has_state(b):-x(b,0). has_state(lambda):-x(lambda,1).