Mercurial Mercurial > hg > tm / 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.
ROOT1.ML
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 10 Jan 2013 08:27:42 +0000
changeset 22 cb8754a0568a
parent 2 26b17f2d583e
permissions -rw-r--r--
update
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     1
 
(*
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     2
 
	turing_basic.thy : The basic definitions of Turing Machine.
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     3
 
	uncomputable.thy : The existence of Turing uncomputable functions.
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     4
 
	abacus.thy : The basic definitions of Abacus machine (An intermediate langauge underneath recursive functions) and
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     5
 
	             the compilation of Abacus machines into Turing Machines.
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     6
 
	rec_def.thy: The basic definitions of Recursive Functions.
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     7
 
	recursive.thy : The compilation of Recursive Functions into
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     8
 
		     Abacus machines.
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     9
 
	UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness.
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    10
 
	UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    11
 
	         initialization and termination processing Turing Machines.
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    12
 
*)
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    13
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    14
 
no_document
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    15
 
use_thys ["turing_basic",
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    16
 
          "uncomputable",
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    17
 
          "abacus",
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    18
 
          "rec_def",
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    19
 
          "recursive",
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    20
 
          "UF",
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    21
 
          "UTM"];
26b17f2d583e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    22
 












26b17f2d583e
updated



Christian Urban <christian dot urban at kcl dot ac dot uk>


parents: 

diff
changeset




    23














26b17f2d583e
updated



Christian Urban <christian dot urban at kcl dot ac dot uk>


parents: 

diff
changeset




    24


use_thys ["Paper"]















tm