fsm.clj

(ns fsm
  (:refer-clojure :exclude [==])
  (:use [clojure.core.logic]))

;; Encoding a Finite State Machine and recognizing strings in its language in Clojure core.logic

;; We will encode the following FSM:
;;
;;  (ok) --+---b---> (fail) 
;;   ^     |
;;   |     |
;;   +--a--+

;; Recall that formally a finite state machine is a tuple
;; A = (Q, Sigma, delta, q0, F)
;;
;; where
;; Q is the state space             | Q = {ok, fail}
;; Sigma is the input alphabet      | Sigma = {a, b}
;; delta is the transition function | delta(ok, a) = ok; delta(ok, b) = fail; delta(fail, _) = fail
;; q0 is the starting state         | q0 = ok
;; F are the accepting states       | F = {ok}

;; To translate this into core.logic, we need to define these variables as relations.

;; Relation for starting states
;; start(q0) = succeeds

(defrel start q)
(fact start 'ok)

;; Relation for transition states
;; delta(x, character) = y => transition(x, character, y) succeeds

(defrel transition from via to)
(facts transition [['ok 'a 'ok]
                   ['ok 'b 'fail]
                   ['fail 'a 'fail]
                   ['fail 'b 'fail]])

;; Relation for accepting states
;; x in F => accepting(x) succeeds

(defrel accepting q)
(fact accepting 'ok)

;; Finally, we define a relation that succeeds whenever the input
;; is in the language defined by the FSM

(defn recognize
  ([input]
     (fresh [q0]                                ; introduce a new variable q0
            (start q0)                          ; assert that it must be the starting state
            (recognize q0 input)))
  ([q input]
     (matche [input]                            ; start pattern matching on the input
        (['()]
           (accepting q))                       ; accept the empty string (epsilon) if we are in an accepting state
        ([[i . nput]]
           (fresh [qto]                         ; introduce a new variable qto
                  (transition q i qto)          ; assert it must be what we transition to from q with input symbol i
                  (recognize qto nput))))))     ; recognize the remainder

;; Running the relation:
(run* [q] (recognize '(a a a)))
;; => (_.0)
;;
;; Strings in the language are recognized.

(run* [q] (recognize '(a b a)))
;; => ()
;;
;; Strings outside the language are not.

;; Here's our free lunch, relational recognition gives us generation:
(run 3 [q] (recognize q))
;; => (() (a) (a a))