turel.clj

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

(defn not-membero
  [x l]
  (conde [(emptyo l)]
         [(fresh [head tail]
          (conso head tail l)
          (!= head x)
          (not-membero x tail))]))

(defn turing-ruleo
  [rules state-in tape-in-val rule-out]
  (fresh [rule rules-rest write-val dir state-new]
         (conso rule rules-rest rules)
         (conde [(== [state-in tape-in-val write-val dir state-new] rule)
                 (== rule-out [write-val dir state-new])]
                [(turing-ruleo rules-rest state-in tape-in-val rule-out)])))

(defn turing-directiono
  [dir tape-in tape-out]
  (fresh [tape-in-l tape-in-val tape-in-r]
         (== [tape-in-l tape-in-val tape-in-r] tape-in)
         (conde [(== dir :r)
                 (fresh [tape-new-l tape-new-val tape-new-r]
                        (conde [(== tape-in-val :_)
                                (emptyo tape-in-l)
                                (emptyo tape-new-l)]
                               [(conso tape-in-val tape-in-l tape-new-l)])
                        (conde [(firsto tape-in-r tape-new-val)
                                (resto tape-in-r tape-new-r)]
                               [(== tape-new-val :_)
                                (emptyo tape-in-r)
                                (emptyo tape-new-r)])
                        (== tape-out [tape-new-l tape-new-val tape-new-r]))]
                [(== dir :l)
                 (fresh [tape-new-l tape-new-val tape-new-r]
                        (conde [(== tape-in-val :_)
                                (emptyo tape-in-r)
                                (emptyo tape-new-r)]
                               [(conso tape-in-val tape-in-r tape-new-r)])
                        (conde [(firsto tape-in-l tape-new-val)
                                (resto tape-in-l tape-new-l)]
                               [(== tape-new-val :_)
                                (emptyo tape-in-l)
                                (emptyo tape-new-l)])
                        (== tape-out [tape-new-l tape-new-val tape-new-r]))]
                [(== dir :n)
                 (== tape-out tape-in)])))

; note: tape is a 3-tuple [[tape-left...] tape-val [tape-right...]]
; tape-left and tape-right are vectors
; tape-left is inverted, so a value of [[:0 :1] :0 [:1 :1]] actually
; represents the tape [:1 :0 :0 :1 :1]

(defn turing-machineo
  [rules accept-states state-in tape-in state-out tape-out]
  (fresh [tape-in-l tape-in-val tape-in-r
          write-val dir state-new
          tape-new]
         (conde [(== state-out state-in)
                 (== tape-out tape-in)
                 (membero state-in accept-states)]
                [(== tape-in [tape-in-l tape-in-val tape-in-r])
                 (not-membero state-in accept-states)
                 (turing-ruleo rules state-in tape-in-val [write-val dir state-new])
                 (turing-directiono dir [tape-in-l write-val tape-in-r] tape-new)
                 (turing-machineo rules accept-states state-new tape-new state-out tape-out)])))

; this is a nice little binary incrementer

(def rules
  [[1 :0 :1 :r 2]
   [1 :_ :1 :r 2]
   [1 :1 :0 :l 1]
   [2 :0 :0 :r 2]
   [2 :1 :1 :r 1]
   [2 :_ :_ :l 3]])

(run 5 [q]
  (fresh [state-out tape-out]
    (turing-machineo rules [3] 1 [[:1 :0 :1] :1 []] state-out tape-out)
    (== q [state-out tape-out])))

(run 5 [q]
  (fresh [state-out tape-out]
    (turing-machineo rules [3] 1 [[] :0 []] state-out tape-out)
    (== q [state-out tape-out])))

(run 5 [q]
  (fresh [state-out tape-out]
    (turing-machineo rules [3] 1 [[] :1 []] state-out tape-out)
    (== q [state-out tape-out])))

; generate a machine that flips :0 to :1

(run 1 [q]
  (fresh [rules accept-states state-in state-out]
    (turing-machineo rules accept-states state-in [[] :0 []] state-out [[] :1 []])
    (== q [rules accept-states state-in state-out])))

; flip :0 to :1, then move right

(run 5 [q]
  (fresh [rules accept-states state-in state-out]
    (== accept-states [1])
    (turing-machineo rules accept-states state-in [[] :0 []] state-out [[:1] :_ []])
    (== q [rules accept-states state-in state-out])))

; moving and writing

(run 1 [q]
  (fresh [rules accept-states state-in state-out]
    (== accept-states [1])
    (turing-machineo rules accept-states state-in [[] :0 []] state-out [[:1] :0 []])
    (== q [rules accept-states state-in state-out])))

; generate a hello world machine

(run 1 [q]
  (fresh [rules]
    (turing-machineo rules [42] 1 [[] :_ []] 42 [[] :o []])
    (turing-machineo rules [42] 1 [[] :o []] 42 [[] :l [:o]])
    (turing-machineo rules [42] 1 [[] :l [:o]] 42 [[] :l [:l :o]])
    (turing-machineo rules [42] 1 [[] :l [:l :o]] 42 [[] :e [:l :l :o]])
    (turing-machineo rules [42] 1 [[] :e [:l :l :o]] 42 [[] :h [:e :l :l :o]])
    (turing-machineo rules [42] 1 [[] :h [:e :l :l :o]] 42 [[] :_ [:h :e :l :l :o]])
    (== q rules)))

; generate another one, this time without hints
; unfortunately it is waaaaaaay too slow
; and for some reason it does not terminate :-(
; causes an OutOfMemoryError where java runs out of heap space

#_(run 1 [q]
  (turing-machineo q [42] 1 [[] :_ []] 42 [[] :_ [:l :l :o]]))

; which is really confusing, because it works just fine for this rule set

(def hello-rules
  [[1 :_ :o :l 2]
   [2 :_ :l :l 3]
   [3 :_ :l :l 42]])

(run 1 [q]
  (turing-machineo hello-rules [42] 1 [[] :_ []] 42 [[] :_ [:l :l :o]]))

; now, let's try to generate the rules for a binary increment machine
; guess what?! this appears to be a general algorithm!

(run 5 [q]
  (fresh [rules]
    (turing-machineo rules [3] 1 [[]         :0 []] 3 [[]         :1 []])
    (turing-machineo rules [3] 1 [[]         :1 []] 3 [[:1]       :0 []])
    (turing-machineo rules [3] 1 [[:1]       :0 []] 3 [[:1]       :1 []])
    (turing-machineo rules [3] 1 [[:1]       :1 []] 3 [[:0 :1]    :0 []])
    (turing-machineo rules [3] 1 [[:0 :1]    :0 []] 3 [[:0 :1]    :1 []])
    (turing-machineo rules [3] 1 [[:0 :1]    :1 []] 3 [[:1 :1]    :0 []])
    (turing-machineo rules [3] 1 [[:1 :1]    :0 []] 3 [[:1 :1]    :1 []])
    (turing-machineo rules [3] 1 [[:1 :1]    :1 []] 3 [[:0 :0 :1] :0 []])
    (== q rules)))

; another increment try, with more hints

(run 1 [q]
  (fresh [rules]
    (turing-machineo rules [3] 1 [[]         :0 []] 3 [[]         :1 []])
    (turing-machineo rules [3] 1 [[]         :1 []] 3 [[:1]       :0 []])
    (turing-machineo rules [3] 1 [[:1]       :0 []] 3 [[:1]       :1 []])
    (turing-machineo rules [3] 1 [[:1]       :1 []] 3 [[:0 :1]    :0 []])
    (turing-machineo rules [3] 1 [[:0 :1]    :0 []] 3 [[:0 :1]    :1 []])
    (turing-machineo rules [3] 1 [[:0 :1]    :1 []] 3 [[:1 :1]    :0 []])
    (turing-machineo rules [3] 1 [[:1 :1]    :0 []] 3 [[:1 :1]    :1 []])
    (turing-machineo rules [3] 1 [[:1 :1]    :1 []] 3 [[:0 :0 :1] :0 []])
    (turing-machineo rules [3] 1 [[:0 :0 :1] :0 []] 3 [[:0 :0 :1] :1 []])
    (turing-machineo rules [3] 1 [[:0 :0 :1] :1 []] 3 [[:1 :0 :1] :0 []])
    (turing-machineo rules [3] 1 [[:1 :0 :1] :0 []] 3 [[:1 :0 :1] :1 []])
    (turing-machineo rules [3] 1 [[:1 :0 :1] :1 []] 3 [[:0 :1 :1] :0 []])
    (turing-machineo rules [3] 1 [[:0 :1 :1] :0 []] 3 [[:0 :1 :1] :1 []])
    (turing-machineo rules [3] 1 [[:0 :1 :1] :1 []] 3 [[:1 :1 :1] :0 []])
    (turing-machineo rules [3] 1 [[:1 :1 :1] :0 []] 3 [[:1 :1 :1] :1 []])
    (== q rules)))