Almost done

3or4or6/6.org

@@ -39,7 +39,7 @@ Implement a Turing machine interpreter using $\chi$.
 
 The interpreter should be a closed $\chi$ expression. If we denote this expression by run, then it should satisfy the following property (but you do not have to prove that it does):
 + For every Turing machine tm and input string $xs \in \text{List}\ \{0, 1\}$ the following equation should hold:
-  \[ \llbracket \text{apply}\ (\text{apply}\ \text{\textit{run}}\ \ulcorner \text{tm} \urcorner) \ulcorner xs \urcorner \rrbracket = \ulcorner \llbracket \text{tm} \rrbracket \text{xs} \urcorner \]
+  \[ \llbracket \text{apply}\ (\text{apply}\ \text{\textit{run}}\ \ulcorner \text{tm} \urcorner) \ulcorner xs \urcorner \rrbracket = \ulcorner \llbracket \text{tm} \rrbracket\ \text{xs} \urcorner \]
 (The $\llbracket \_ \rrbracket$ brackets to the left stand for the $\chi$ semantics, and the $\llbracket \_ \rrbracket$ brackets to the right stand for the Turing machine semantics.)
 
 Turing machines should be represented in the following way:
@@ -57,7 +57,7 @@ The input and output strings should use the usual representation of lists, with
 Please test that addition, implemented as in Tutorial 5, Exercise 6 (with 0 instead of #), works as it should when run on your Turing machine interpreter. A testing procedure that you can use is included in the wrapper module (documentation).
 
 ** Answer
-
+See =Turing.hs=
 * (2p)
 Prove that every Turing-computable partial function in $\mathbb{N} \rightharpoonup \mathbb{N}$ is also $\chi$ computable. You can assume that the definition of “Turing-computable” uses Turing machines of the kind used in the previous exercise.
 

3or4or6/Interpreter/Turing.hs

@@ -1,4 +1,87 @@
--- | 
+{-# Language LambdaCase, Strict #-}
 
 module Interpreter.Turing where
 
+import Chi
+import Interpreter.Haskell -- from assignment 3
+
+equalExp :: Exp
+equalExp = parse
+  "rec equal = \\m. \\n. case m of \
+  \ { Zero()  -> case n of { Blank() -> False(); Zero() -> True();  Suc(n) -> False() } \
+  \ ; Suc(m)  -> case n of { Blank() -> False(); Zero() -> False(); Suc(n) -> equal m n } \
+  \ ; Blank() -> case n of { Blank() -> True();  Zero() -> False(); Suc(n) -> False() } \
+  \ }"
+
+lookupExp :: Exp
+lookupExp =
+  subst (Variable "equal") equalExp $ parse
+  "\\s. \\head. rec lookup = \\rules. case rules of \
+  \ { Nil() -> Done() \
+  \ ; Cons(x,xs) -> case x of \
+  \   { Rule(s1, x1, s2, x2, d) -> case equal s s1 of \
+  \     { True()  -> case equal head x1 of \
+  \       { True()  -> Trip(s2,x2,d)\
+  \       ; False() -> lookup xs \
+  \       } \
+  \     ; False() -> lookup xs \
+  \     } \
+  \   }\
+  \ } \
+  \ "
+
+joinExp :: Exp
+joinExp = parse
+  "rec join = \\xs. \\ys. case xs of \
+  \ { Nil() -> ys \
+  \ ; Cons(x,xs) -> join xs Cons(x,ys) \
+  \ }"
+
+appendExp :: Exp
+appendExp = parse
+  "rec append = \\xs. \\ys. case xs of \
+  \ { Nil() -> ys \
+  \ ; Cons(x,xs) -> Cons(x,append xs ys) \
+  \ }"
+
+reverseExp :: Exp
+reverseExp =
+  subst (Variable "append") appendExp $ parse
+  "rec reverse = \\xs. case xs of \
+  \ { Nil() -> Nil() \
+  \ ; Cons(x,xs) -> append xs Cons(x,Nil())\
+  \ }"
+
+removeLastBlanksExp :: Exp
+removeLastBlanksExp = parse
+  "rec removeLastBlanks = \\xs. case xs of \
+  \ { Nil() -> Nil() \
+  \ ; Cons(x,xs) -> case x of \
+  \   { Blank() -> removeLastBlanks xs \
+  \   ; Zero()  -> Cons(x,xs) \
+  \   ; Suc(n)  -> Cons(x,xs) \
+  \   } \
+  \ }\
+  \ "
+
+runExp :: Exp
+runExp =
+  subst (Variable "removeLastBlanks") removeLastBlanksExp .
+  subst (Variable "reverse") reverseExp .
+  subst (Variable "join") joinExp .
+  subst (Variable "lookup") lookupExp $ parse
+  "(rec run = \\rev. \\tm. \\tape. case tm of \
+  \ { TM(state,deltas) -> case tape of \
+  \   { Nil() -> run rev TM(state,deltas) Cons(Blank(), Nil()) \
+  \   ; Cons(head,xs) -> case lookup state head deltas of \
+  \     { Done() -> join rev (reverse (removeLastBlanks (reverse tape))) \
+  \     ; Trip(s2, x2, d) -> case d of \
+  \       { L() -> case rev of \
+  \         { Nil() -> run Nil() TM(s2,deltas) Cons(x2,xs) \
+  \         ; Cons(y,ys) -> run ys TM(s2,deltas) Cons(y,Cons(x2,xs)) \
+  \         } \
+  \       ; R() -> run Cons(x2,rev) TM(s2,deltas) xs \
+  \       } \
+  \     } \
+  \   } \
+  \ }) Nil()"

3or4or6/chi.cabal

@@ -26,6 +26,7 @@ library
     PrintChi
     Interpreter.Haskell
     Interpreter.Self
+    Interpreter.Turing
   hs-source-dirs:
     .