Develop (check before developing whether such a thing already exists) an algebra where we can say that:
if you take a the formal specs of Turing machine f and an input x, and encode them with encoder C^1 for L^1, and provide them to L^1, and decode the output of L^1 with the inverse of the previous encoder, you must obtain the same as if you do the same but with L^2 and C^2.
Expressed something like:
(for all i,j) C^i^(-1)(C^i(f,x) + L^i) = C^j^(-1)(C^j(f,i) + L^j)
Concepts:
Informal definition, name: what a human agent needs to test a Tm
Turing machine. informal definition, and name.
set of formal models of Tms
each formal model allows the formal definition of arbitrary Tms.
From each informal definition we can obntain by human work many formal definitions.
Logic L, informal definition: works out the output of other Tms, or hangs
Needs other Tms encoded
To each L, a compiler C
oracles
Notation for: human agent, tm name, number, produce, formal model of tm, encode, encoded Tm,
Develop (check before developing whether such a thing already exists) an algebra where we can say that:
if you take a the formal specs of Turing machine f and an input x, and encode them with encoder C^1 for L^1, and provide them to L^1, and decode the output of L^1 with the inverse of the previous encoder, you must obtain the same as if you do the same but with L^2 and C^2.
Expressed something like:
(for all i,j) C^i^(-1)(C^i(f,x) + L^i) = C^j^(-1)(C^j(f,i) + L^j)
Concepts:
Informal definition, name: what a human agent needs to test a Tm
Turing machine. informal definition, and name.
set of formal models of Tms
each formal model allows the formal definition of arbitrary Tms.
From each informal definition we can obntain by human work many formal definitions.
Logic L, informal definition: works out the output of other Tms, or hangs
Needs other Tms encoded
To each L, a compiler C
oracles
Notation for: human agent, tm name, number, produce, formal model of tm, encode, encoded Tm,