(... on hopefully better understood/known semantics cousin topics)
Well, T-diagrams are of course nothing new for those of us who read at some point books like the Dragon Book, to introduce compiler boot strapping, cross-compiling, sub-languages compiling, optimizing compilers built from non-optimizing ones, etc.
It's just that, below, we try to leverage in quite an unusual fashion the meaning we allow them to carry when we describe the processing of formalisms in chains of language transforms/rewritings, etc
Here below, you can see it as a usage of the notation "put on steroids", sort of, to discuss/ask (at some point) about much more (too much, for the notation?) abstract matters than just the usual, more technique-oriented depictions of compilers/translators construction.
Take this last remark as it only is : a warning that it's still, indeed, fairly speculative here below...
E : a programming language, e.g., Eiffel
C : another, e.g., the C prog. language
e2c : a translator (compiler) from Eiffel to C, implemented in C, etc.
c2x : a translator (assembler) from C to a processor architecture;
x : a processor architecture, e.g., x86
I : some input data, in some serialization format
O : output
P : name of a program instance
E e2c C E e2c C
C C x x
x
I P O I P O
E E e2c C C
x
(I P O and I P O are some arbitrary programs, supposedly taking I as input and giving output O, written in Eiffel and C, resp.)
E C
I P O I P O
C C c2x x x
x
I P O I P/l O
x x T T
T
T on the right side (arm) : let's read it "Executes..." or "Looks for the truth about..."
T at the bottom (legs) of T diagrams : let's read it "Has terminated with input I, output O", or "Has proved something from I to O"
If we accept Church-Turing thesis : P/l is then quite naturally(?) seen as the single semantics, expressed in the adhoc programming language of P,
when P terminates, taking input I and giving output O
Then, let I P O or I P/l O denote the same thing : P/l, in its shortest form of moniker (the semantics of P)
l T
(Where "l" --L lower case-- is there to remind us Church's lambda calcul)
Either : I P O is P/l, from the point of view : the semantics of P *formalized* (in a finite form)
l
Or, also : I P/l O is P/l from the point of view : seeing the semantics of P as P which terminates with output O, from input I
T
(In I P/l O also noted I P O, "P/l" in the center is to remind us it's the result of a logical construction process using another formalization "l")
T l
And, then, more generally, even :
I P O I P/l O
l l T T
T
I P O I P O
C C C/l l l
T
At this point, we already know about an easy (and interesting, because much studied) observation already : some programs terminates whatever is their input; others terminates only for some inputs,
and others are just "so full of bugs" that whatever the input, they will end up in an infinite loop. What does that mean semantically?
We can try answer this later. For now, let's start with this question :
What is C C/l l (or, C {C} l) by the way?
T l
We recognize the (arbitrary, human-made up, ad hoc, etc) semantics of the prog. language C, "{C}", expressed in formalization/theory "l"
Ok, but then, which meaning can we give, to that newcomer around, l T, in :
T
I P O I P/l O
l l T T
T
or in, even :
C {C} l C C/l l
l l T T
T
?
After staring at it long enough in those (pseudo-maths, I reckon) formulas l T really looks like (a/the?) (universal?) Turing machine(s), no?
T
Now, if our intuition happens to be well-enough founded, is it *a* specific Turing machine or *the* UTM ?
Unclear, but anyway, if it really seems like some sort of Turing machine, it's also found in a somewhat unusual context :
there, we're in the binding of the formalism C/l/l, human-invented, with all its possible conforming implementations of provers/verifiers : C/T/l
Let's be even more audacious! (and let's hope "audacious" won't mean "reckless", though...)
Question : is there maybe something more profound that actually "builds" (or "forms") Turing machines at the theoretical level itself?
Or are they merely *ad hoc* artefacts of man's mathematics/computer science as it evolves? (historically Alan Turing's creation, anyway);
Put differentely : could we have somewhat *predicted* their invention, through some formula, soon or late?
That's the (crazy?) idea here, now :
it's maybe that there's a "Godel operator" underneath TM's (!) ..let's try to represent it with the same notation here,
though at a different (higher) abstraction level :
Recap, first; isn't Godel's incompleteness theorems' essence in the following :
"Any system the axiomatic of which can be listed automatically is either incomplete or inconsistent" ?
If it is, then, we can go on with trying to write and give a meaning/point of view about another breed of T diagrams
(another "breed" at this meta mathematical level, this time anyway, while the T diagrams given for the Turing machine(s) were still mostly at
today's usual mathematics usage level) :
ZF+C (?) ZFC T
ZF ZF .T. T
G
Here just above, it would be :
if we assume ZF consistent, and we axiomatize ZFC using ZF (merely by very construction : accept ZFC as ZF and C both accepted; i.e., ZFC "=" ZF + C),
then resulting ZFC is *maybe* consistent, and *for sure* incomplete (since we had to add C to ZF to build ZFC and C wasn't in ZF)
Also, note : here above, T on the right arm means "maybe consistent"; T on the bottom (leg) means "built";
and (whatever noun) on the left arm is the name of the theory we're talking about; and, G at the bottom is Godel's incompleteness statements,
seen as the (meta mathematical) operator we had the idea of, above.
Finally, in this context here .T. on the right arm of the G-legged thing is just denoting we're applying that so-called meta-maths "Godel operator"
on its left arm's input theory, to build a new one.
We can also see here this G-legged "builder" as a formal reification of Godel's incompleteness theorems' truthfulness we decided to accept;
while, obviously, "(?)" merely tags our very questioning about the status of the theory we're building there.
Thus, now for the counter-example expression of Godel's proof that trying to axiomatize automatically a theory in itself forcibly gives an inconsistent theory,
we could go with, for instance :
0 (?) BT 0
BT BT .T. T
G
Where : "BT" = "some Bad Theory"; "0" on the left : we start with no axiom available at all and try to find them all, in BT alone...
... then, Godel tells us that the result is a BT, completely built, but totally useless, since inconsistent
(inconsistency being marked by "0" on the right arm)
Let's go back to our Turing machine and try put things together :
How to read the following ?
l T l T
m m .T. T
G
(in the idea of re using l T later on to learn/discover(?) more about prog. languages, programs, their semantics, etc)
T
We could propose :
An attempt at formalizing a semantic expressed in mathematics (there, "m" = "ZFC" for example) can be leveraged to create, using that "Godel operator",
a "Turing machine" (l T) which, *maybe* (and only *maybe* !) can terminate (for some or all inputs)
T
Then, such a resulting Turing machine (keeping in mind we're in the PoV of a use case of what I call "the Godel operator") can also be seen as a sort of
"super theorem" / theory that *might* happen to be "true" / consistent (in regards to its underlying axiomatic "m").
But.. wait! What was our starting point, btw? We had a program written in some programming language to start with, right?
.. and the fact is... it was PRE-existent ! I mean, some human had to write the source code first, before we bother thinking about how all this can
(or cannot) come to an end..
So, it "looks like" that a given program, written in a given programming language
(a language the formal, clear semantics of which has been defined somewhere and is indirectly reductible to ZFC or..., etc)
and in such a way that it (at least, *sometimes*) terminates with some output (be it the empty string or a null pointer, etc) well, with anything,
but that it can terminate anyway, is ... just a "new", but somewhat "hidden", theorem proved in "m" !
By "hidden" I mean: unless we can actually "exhibit" explicitly, either later or upfront, the equivalent I P O program,
l
by using some of those automatic automatic proof checkers/verifiers, that work with the help of the C {C} l "standard" semantic definition of prog. lang. "C"
l
(more precisely: this C/l/l is, the agreed upon, "official" semantics of the programming language C, formalized, by design/construction, in "l")
Now, we can maybe answer the former question we had above, through this T-diagrams "looking glass" :
a) A program that always terminates : this looks like the process/discovery of a consequence of ZFC
(or whatever other mathematics "m" agreed upon to axiomatize the theory, formalized in "l", of the program "P",
via an indirection with "P" 's implementation language's definition, also in "l").
(Note: for once not fuzzy, here, let's mean "consequence" in its strict, normal logician sense of one theory being the consequence of another.)
Even the 'print "Hello world!"' (with or without input, always terminating) for dummies is like a mere consequence of ZFC, there, by the way,
because the computer architecture with its assembly language, the high level prog. language's semantics (with english-like syntax), etc,
are just intermediary "layers" all made concrete in an ad hoc manner by us (in our tangible universe), building upon, and giving sense to ZFC only
(our today's maths as we see them).
b) A program that always (for all inputs) loops infinitely looks like an inconsistent theory (the blatant inconsistency of which is given by the computer's behavior)
c) A program that loops infinitely only for some input : looks like the process/discovery of theorem(s) of ZFC, already known or not,
explicitable or not (depending on the advancement or the technology of proof checkers) for which the computer gives us counter-example applications
when hypothesis requirement are not met (thus, the cases of infinite loops); otherwise, when it terminates, it's a clue about sufficient input/hypothesis
In a sense, programs always terminating independently of their input don't really teach us anything new in ZFC (mathematics), then.
That's so naturally verified with "Hello world" programs, for instance : what do you learn (in your brain) really new, aside the syntax, when you see a
"Hello world" program in a language you see for the first time?
Sure, you get clues about the "flavour" of the syntax; or the "flavour" of how I/O instructions integrates with the former, with dedicated concrete syntax
keywords for that purpose or not, etc.. but what about the *underlying* axiomatic assumed by the *underlying* type system of the language?
If you see no variable and/or function declaration that seems to implement some form, even minimal, of " Output = Function(Input) " transition in the overall program,
you learn nothing (other than syntactic aspects) about the language's very theory underneath (functional, imperative, etc), first, and *a fortiori*
even less about the language's true expressiveness, since you don't have a non-trivial "theory" sample provided by the program..
Of course, that doesn't mean such programs, be they trivial '"hello world"'-like or not trivial at all, are not useful in a practical perspective!
(we only meant here that they are maybe less informative on what we can deduce from, e.g. ZFC axiomatics, itself -- thus, maybe less useful to talk about theoretical aspects)
Note that one tough problem, to say the least (*), since it seems unsolvable (and very likely is) remains completely as it is known today, though;
and by these observations here above we're saying absolutely nothing new about it, anyway.
While, conversely.. programs we can *observe* terminating in some cases only and looping infinitely in others.. are maybe "telling us" new things about
what maths (based on ZFC or other axiomatics) can breed (?)...
Hmm... At this point, *any* (+/-) feedback from real experts, authoritative academics, on my speculations here, the way I came to them, or just whether it's reasonably sensical/worth digging or not...
... is, well, much, warmly welcome !
(*) http://en.wikipedia.org/wiki/Halting_problem
[EDIT 12/24/09 05:03PM EST]
Oh yes, a few personal notes on "Nothingness", "Infinite Loops", "Inconsistency", etc :
In the T diagrams above, the programs ones, one might choose to represent the construction of bogus programs (totally bogus, or only for some input)
which end stuck in infinite loops, like this, for instance :
I P O I O
C C (?)
T
(Where "(?)" means "NOT SURE it will terminate" and the right-most "O"-equipped arm is the ouput you *hope* to get)
And, when it's time to run the kid and it's bad news about it :
I P O I 0
x x (!)
T
(Where "(!)" means does not terminate; note the right-most "0"-equipped arm that tells you, you won't get anything useful out of this execution...)
Well, why not, after all, it's just (yet another) couple little extensions to our notation, which seems to remain consistent with the "spirit" of the reflection.
But then :
I'm not so sure what is the "official" position of logicians of authority on the matter, but as I see it, and by analogy with my experience with actual type systems
of the few, concrete, programming languages/runtime platforms I know about, here's how I visualize/think it :
An inconsistent theory : is one where you can end up proving anything, and even in direct contradiction with your second to last proof, immediately, or any time
(that is possibly, much, much later, which is even worse);
then, as I see it,
"being ABLE to SUPPOSEDLY-'prove' anything"
is really equivalent to :
"being UNABLE to ACTUALLY-'prove' anything"
It's similar to those (often OO-flavoured) type systems with some notion of conformance between types (whatever it is, contract-based, or etc).
In some (ever since the earliest I know of, anyway) definitions of Eiffel, for instance, while ALL types would, by construction of the T.S. 'conform'
to the special class type 'ANY' (or 'Object' in other languages, etc), NO type can ever conform to 'NONE' (or 'void' in other languages, etc).
But, the latter, special type 'NONE'/'void'/etc, whatever you call it, is usually the only one :
a) providing this single, only possible value for itself : 'null' or 'nothing' (roughly tagging the fact, by convention : "hey, no data, here!");
b) also, for reference class type (not value types), by convention/common design practise of those T.S., it is decided to define that latter type as the "bottom"
of the type system and conformance relation, because --de facto-- the 'null'/'nothing' value can be assigned to ANY other reference class type variable,
or actual argument, usually.
'NONE'/'void' is then that one very special builtin type that can implicitly 'conform' to all other possible present and future types imaginable & reified
in the language's type system runtime support.
Here, one possible analogy between always infinitely looping-programs (or seen as "way too often"), special types like 'NONE'/'void', and absurd theories is then coming to the surface:
Truth is, we have long ago accepted the idea that we just can't do anything constructive with those guys; the program will loop forever and it's the only information that you can get out of it, after launching it,
usually empirically (or, if not empirically, if you can prove it will loop forever beforehand, well, it's unlikely you'll bother launching it then,
unless you're that bored!)
Assigning null or reading null to/in a variable is, similarly, us accepting the idea, that, for a while, until it gets non-null, you're not going to consider that variable
as holding ANY form of useful 'data', I mean, when thinking 'data' as some form of non-trivial 'state' information, anyway.
(then, when/if the variable/language entity gets non-null later, the rationale for your program's choice of getting a reified view of its type that relies on
either a static- or dynamic type checking is not exactly the same topic discussed... hmm! or, is it the very same by a different bias, actually?!).
Last updated December 24, 2009; 05:03PM EST
© Cyril Jandia 2008, 2009. All rights reserved.