More turing machines (still not compiling)

[helm.git] / matita / matita / lib / turing / universal.ma

diff --git a/matita/matita/lib/turing/universal.ma b/matita/matita/lib/turing/universal.ma
index 357e3548862ca51b992a6ce7eb4d00bfc058d177..8f9e58be064b542b74f1f10721979a20b8ff653a 100644 (file)
--- a/matita/matita/lib/turing/universal.ma
+++ b/matita/matita/lib/turing/universal.ma
@@ -1,3 +1,10 @@
+include "turing/turing.ma".
+
+axiom Q : FinSet.
+axiom q0 : Q. axiom q1 : Q. axiom q2 : Q. axiom q3 : Q. axiom q4 : Q. axiom q5 : Q. 
+axiom q6 : Q. axiom q7 : Q. axiom q8 : Q. axiom q9 : Q. axiom q10 : Q. axiom q11 : Q. 
+axiom q12 : Q. axiom q13 : Q. axiom q14 : Q. axiom q15 : Q. axiom q16 : Q.
+
 (* 
 Simboli:
 0 1 *0 *1 # | ,
@@ -24,9 +31,9 @@ Input:
 
 Output:
 
- ls # current # ... | input , output , D | ... # rs  (rimuove le marcature)
-    ^
- SUCCESS
+ ls # current # ... | input , output , D | ... # rs  (rimuove le marcature e si sposta sull'output)
+                              ^
+                           SUCCESS
 
       *                                    *
  ls # current # ... | input , output , D | ... # rs (sposta la marcatura alla tupla successiva)
@@ -35,14 +42,14 @@ Output:
 
 STATO 0:
   #/R --> 1
-
+  
 STATO 1:
   \forall c != *z. c/L --> 1
   \forall x. *x/x/R --> 2(x)
 
 STATO 2(x):
-  \forall y. y/*y/R --> 2
-  #/R --> 2
+  \forall y. y/*y/R --> 3(x)
+  #/R --> 3(x)
 
 STATO 3(x):
   \forall y.\forall c != *y. c/R --> 3(x)
@@ -62,7 +69,7 @@ STATO 6:
 
 STATO 7:
   \forall c != #. c/L --> 7
-  #/L
+  #/L -→ 8
 
 STATO 8:
   \forall c != #. c/L --> 8
@@ -72,7 +79,48 @@ STATO 8:
 STATO 9:
   \forall x. x/*x/L --> FAILURE
 
+*)
+
+match s with
+[ q0 ⇒ match c with
+  [ grid ⇒ 〈q1,〈#,R〉〉
+  | _ ⇒ 〈qsink,〈c,N〉〉 ]
+| q1 ⇒ match c with
+  [ mark x ⇒ 〈q2 x,〈bit x,R〉〉
+  | _ ⇒ 〈q1,〈c,L〉〉 ]
+| q2 x ⇒ match c with
+  [ bit y ⇒ 〈q3 x,〈mark y,R〉〉
+  | grid ⇒ 〈q3 x,〈grid,R〉〉
+  | _ ⇒ 〈qsink,〈c,N〉〉 ]
+| q3 x ⇒ match c with
+  [ mark y ⇒ match bool_eqb x y with
+    [ true ⇒ 〈q4,〈bit y,R〉〉
+    | false ⇒ 〈q5,〈bit y,R〉〉 ]
+  | _ ⇒ 〈q3 x,〈c,R〉〉 ]
+| q4 ⇒ match c with
+  [ comma ⇒ 〈qSuccess,〈comma,R〉〉
+  | bit x ⇒ 〈q1,〈mark x,L〉〉
+  | _ ⇒ 〈qsink,〈c,N〉〉 ]
+| q5 ⇒ match c with
+  | bar ⇒ 〈q6,〈bar,R〉〉
+  | _ ⇒ 〈q5,〈c,R〉〉
+| q6 ⇒ match c with 
+  [ bit x ⇒ 〈q7,〈mark x,L〉〉
+  | _ ⇒ 〈qsink,〈c,N〉〉 ]
+| q7 ⇒ match c with
+  [ grid ⇒ 〈q8,〈grid,L〉〉
+  | _ ⇒ 〈q7,〈c,L〉〉 ]
+| q8 ⇒ match c with
+  [ grid ⇒ 〈q9,〈grid,R〉〉 
+  | mark x ⇒ 〈q8,〈bit x,L〉〉 
+  | _ ⇒ 〈q8,〈c,L〉〉 ]
+| q9 ⇒ match c with
+  [ bit x ⇒ 〈qFailure,〈mark x,L〉〉 
+  | _ ⇒ 〈qsink,〈c,N〉〉 ]
+| qsink ⇒ 〈qsink,〈c,N〉〉 ]
 
+  
+(*
 ==============================
 MACCHINA PER COPIA NUOVO STATO IN CURRENT
 ==============================
@@ -90,7 +138,7 @@ Output:
 
 STATO 0:
   \forall x. x/*x/L --> 1
-
+  
 STATO 1:
   [01,|]/L --> 1
   #/L --> 2
@@ -124,8 +172,54 @@ STATO 8:
 
 STATO 9:
   stato finale
-
-
+*)
+match s with
+ [ q0 ⇒ match c with
+   [ bit x ⇒ 〈q1,〈mark x,L〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q1 ⇒ match c with
+   [ bit x ⇒ 〈q1,〈c,L〉〉
+   | comma ⇒ 〈q1,〈c,L〉〉
+   | bar ⇒ 〈q1,〈c,L〉〉
+   | grid ⇒ 〈q2,〈c,R〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q2 ⇒ match c with
+   [ bit x ⇒ 〈q2,〈c,L〉〉
+   | grid ⇒ 〈q3,〈c,R〉〉 
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q3 ⇒ match c with
+   [ bit x ⇒ 〈q4,〈mark x,R〉〉
+   | grid ⇒ 〈q8,〈c,R〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q4 ⇒ match c with
+   [ bit x ⇒ 〈q4,〈c,R〉〉
+   | comma ⇒ 〈q4,〈c,R〉〉
+   | bar ⇒ 〈q4,〈c,R〉〉
+   | grid ⇒ 〈q4,〈c,R〉〉
+   | mark x ⇒ 〈q5 x,〈bit x,R〉〉 ]
+ | q5 x ⇒ match c with
+   [ grid ⇒ 〈q6 x,〈c,R〉〉
+   | bit y ⇒ 〈q7 x,〈mark y,L〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q6 x ⇒ match c with
+   [ bit D ⇒ 〈q7 x,〈mark D,L〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q7 x ⇒ match c with
+   [ bit y ⇒ 〈q7 x,〈c,L〉〉
+   | comma ⇒ 〈q7 x,〈c,L〉〉
+   | bar ⇒ 〈q7 x,〈c,L〉〉
+   | grid ⇒ 〈q7 x,〈c,L〉〉
+   | mark y ⇒ 〈q3,〈bit x,R〉〉 ]
+ | q8 ⇒ match c with
+   [ bit y ⇒ 〈q8,〈c,R〉〉
+   | comma ⇒ 〈q8,〈c,R〉〉
+   | bar ⇒ 〈q8,〈c,R〉〉
+   | grid ⇒ 〈q8,〈c,R〉〉
+   | mark D ⇒ 〈q9,〈bit D,L〉〉 ]
+ | q9 ⇒ ? (* successo *)
+ ]
+
+(*
 ==================================
 MACCHINE PER SPOSTARE LA "TESTINA"
 ================================
@@ -184,8 +278,20 @@ STATO 3:
 
 STATO 4:
   stato finale
+*)
 
-
+match s with
+ [ q0 ⇒ match c with
+   [ bit x ⇒ 〈q1 x,〈c,L〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q1 x ⇒ match c with
+   [ grid ⇒ 〈q3,〈bit x,R〉〉
+   | _ ⇒ 〈q2 c,〈bit x,R〉〉 ]
+ | q2 d ⇒ 〈q0,〈d,L〉〉
+ | q3 ⇒ 〈q4,〈grid,L〉〉
+ | q4 ⇒ (* finale *) ].
+
+(*
 MACCHINA B
 ----------
 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua destra.
@@ -216,8 +322,20 @@ STATO 3:
 
 STATO 4:
   stato finale
+*)
 
-
+match s with
+[ q0 ⇒ match c with
+  [ bit x ⇒ 〈q1 x,〈c,R〉〉
+  | _ ⇒ 〈qsink,〈c,N〉〉]
+| q1 x ⇒ match c with
+  [ grid ⇒ 〈q3,〈bit x,L〉〉
+  | _ ⇒ 〈q2 c,〈bit x,L〉〉 ]
+| q2 d ⇒ 〈q0,〈d,R〉〉
+| q3 ⇒ 〈q4,〈grid,L〉〉 
+| q4 ⇒ (* finale *) ].
+
+(*
 MACCHINA C
 ----------
 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
@@ -246,3 +364,13 @@ STATO 3:
   stato finale
 
 *)
+
+match s with 
+[ q0 ⇒ match c with
+  [ bit x ⇒ 〈q1 x,〈c,R〉〉
+  | _ ⇒ 〈qsink,〈c,N〉〉 ]
+| q1 x ⇒ match c with
+  [ grid ⇒ 〈q3,〈grid,L〉〉
+  | _ ⇒ 〈q2 c,〈bit x,L〉〉
+| q2 d ⇒ 〈q0,〈c,R〉〉
+| q3 ⇒ (* finale *) ].