It is not an introduction to core.logic. To learn the basics, I would recommend the Logic Starter.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(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)) |
Awesome! Reading about logic programming is always enlightening - thanks for this.
ReplyDeleteOne 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;`
Good spot, fixed. Glad to hear somebody actually reading the Maths :).
ReplyDelete