turing.trig

# --------------
# Turing Machine
# --------------
#
# Turing completeness test case.
# See http://en.wikipedia.org/wiki/Prolog#Turing_completeness

@prefix list: <http://www.w3.org/2000/10/swap/list#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix var: <http://www.w3.org/2000/10/swap/var#>.
@prefix : <http://example.org/#>.

# interpreter for Turing machine
_:bng_1 log:isImpliedBy _:bng_2.

_:bng_1 {
    () :compute var:OutTape.
}

_:bng_2 {
    var:Machine :start var:I.
    (var:I () "#" ()) :find var:OutTape.
}

_:bng_3 log:isImpliedBy _:bng_4.

_:bng_3 {
    var:List :compute var:OutTape.
}

_:bng_4 {
    var:List list:firstRest (var:Head var:Tail).
    var:Machine :start var:I.
    (var:I () var:Head var:Tail) :find var:OutTape.
}

_:bng_5 log:isImpliedBy _:bng_6.

_:bng_5 {
    (var:State var:Left var:Cell var:Right) :find var:OutTape.
}

_:bng_6 {
    (var:State var:Cell var:Write var:Move) :tape var:Next.
    (var:Move var:Left var:Write var:Right var:A var:B var:C) :move true.
    (var:Next var:A var:B var:C) :continue var:OutTape.
}

_:bng_7 log:isImpliedBy _:bng_8.

_:bng_7 {
    (:halt var:Left var:Cell var:Right) :continue var:OutTape.
}

_:bng_8 {
    var:Left :reverse var:R.
    var:List list:firstRest (var:Cell var:Right).
    (var:R var:List) list:append var:OutTape.
}

_:bng_9 log:isImpliedBy _:bng_10.

_:bng_9 {
    (var:State var:Left var:Cell var:Right) :continue var:OutTape.
}

_:bng_10 {
    (var:State var:Left var:Cell var:Right) :find var:OutTape.
}

_:bng_11 log:isImpliedBy _:bng_12.

_:bng_11 {
    (:left () var:Cell var:Right () "#" var:L) :move true.
}

_:bng_12 {
    var:L list:firstRest (var:Cell var:Right).
}

_:bng_13 log:isImpliedBy _:bng_14.

_:bng_13 {
    (:left var:List var:Cell var:Right var:Tail var:Head var:L) :move true.
}

_:bng_14 {
    var:List list:firstRest (var:Head var:Tail).
    var:L list:firstRest (var:Cell var:Right).
}

_:bng_15 log:isImpliedBy true.

_:bng_15 {
    (:stop var:Left var:Cell var:Right var:Left var:Cell var:Right) :move true.
}

_:bng_16 log:isImpliedBy _:bng_17.

_:bng_16 {
    (:right var:Left var:Cell () var:L "#" ()) :move true.
}

_:bng_17 {
    var:L list:firstRest (var:Cell var:Left).
}

_:bng_18 log:isImpliedBy _:bng_19.

_:bng_18 {
    (:right var:Left var:Cell var:List var:L var:Head var:Tail) :move true.
}

_:bng_19 {
    var:List list:firstRest (var:Head var:Tail).
    var:L list:firstRest (var:Cell var:Left).
}

_:bng_20 log:isImpliedBy true.

_:bng_20 {
    () :reverse ().
}

_:bng_21 log:isImpliedBy _:bng_22.

_:bng_21 {
    var:List :reverse var:Reverse.
}

_:bng_22 {
    var:List list:firstRest (var:Head var:Tail).
    var:Tail :reverse var:R.
    (var:R (var:Head)) list:append var:Reverse.
}

# a Turing machine to add 1 to a binary number
:add1 :start 0.

(0 0 0 :right) :tape 0.
(0 1 1 :right) :tape 0.
(0 "#" "#" :left) :tape 1.
(1 0 1 :stop) :tape :halt.
(1 1 0 :left) :tape 1.
(1 "#" 1 :stop) :tape :halt.

# query
_:bng_23 log:query _:bng_23.

_:bng_23 {
    (1 0 1 0 0 1) :compute var:A1.
    (1 0 1 1 1 1) :compute var:A2.
    (1 1 1 1 1 1) :compute var:A3.
    () :compute var:A4.
}