Mercurial Mercurial > hg > regexp / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
utm/ROOT.ML
author zhang
Sat, 29 Sep 2012 12:38:12 +0000
changeset 370 1ce04eb1c8ad
child 371 48b231495281
permissions -rw-r--r--
Initial upload of the formal construction of Universal Turing Machine.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
370
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
     1
 
(*
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
     2
 
	turing_basic.thy : The basic definitions of Turing Machine.
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
     3
 
	uncomputable.thy : The existence of Turing uncomputable functions.
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
     4
 
	abacus.thy : The basic definitions of Abacus machine (An intermediate langauge underneath recursive functions) and
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
     5
 
	             the compilation of Abacus machines into Turing Machines.
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
     6
 
	recursive.thy : The basic defintions of Recursive Functions and the compilation of Recursive Functions into
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
     7
 
		     Abacus machines.
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
     8
 
	UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness.
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
     9
 
	UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
    10
 
	         initialization and termination processing Turing Machines.
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
    11
 
*)
1ce04eb1c8ad Initial upload of the formal construction of Universal Turing Machine.
zhang
parents:
diff changeset 
    12
 
  no_document use_thys ["turing_basic", "uncomputable", "abacus", "recursive", "UF", "UTM"]
regexp