Wednesday, January 25, 2012

Finite State Machines in core.logic

This is an implementation of Finite State Machines in Clojure using core.logic. They are a good starting point for computational linguistics and illustrate several features of core.logic, such as various ways of defining new relations, pattern matching and also the invertibility of relations.

It is not an introduction to core.logic. To learn the basics, I would recommend the Logic Starter.

(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))
view raw fsm.clj hosted with ❤ by GitHub

2 comments:

  1. Awesome! Reading about logic programming is always enlightening - thanks for this.

    One teeny weeny bug: in the formal comment of the state machine you define the first transition fn as `delta(ok, a) = a;` when it probably should be `delta(ok, a) = ok;`

    ReplyDelete
  2. Good spot, fixed. Glad to hear somebody actually reading the Maths :).

    ReplyDelete