[Infrastructures] rollback, turing, semantics, and reflection

[Daniel Hagerty]

 > I've always said rollbacks can't be made reliable for changes to UNIX
 > hosts, because it's self-modifying code and you might have broken your
 > rollback mechanism; i.e. the turing paper.  I think a transaction
 > rollback might be able to be made safe for most classes of network

    This is not a turing equivelence problem.  While we're at it,
could we please forget about the turing machines for real work and
stick to lambda calculus please?  They're equivelent, and the latter
is much more expressive.  Lambda calculus sees every day use today,
whereas turing is mostly used as a "prove equivelent to" model.

    Wikipedia's informal statement of the halting problem is:

      Given a description of an algorithm and its initial input,
      determine whether the algorithm, when executed on this input,
      ever halts (completes). The alternative is that it runs forever
      without halting.

    While we could write questions in this form, we obviously want to
avoid doing this, as it's been demonstrated as an inherently self
contradictory question.  Given "doctor, it hurts when I do this?" as
the first part of the joke, what's the reply?  Right.


    There are other ways we can write our questions where we avoid
these issues.  In particular, "meta-language"/"object-language"
splits, like the many forms of semantic approaches, can be used to
attack problems in this realm.  If the terms "meta language" and
"object language" don't work for you, you could also substitute
"compiler of my stuff" (for example, a C compiler) and "my stuff" (a C
program) for the respective terms.

    If halting was really that much of a problem, we couldn't make a
compiler ever work with non terminating statements, could we?  The C
program's compiled form may not halt when it's actually evaluated --
that may be the very point.  And if you're a sysadmin, that is almost
certainly the point as you get to bigger and bigger scopes of "the
program".  "Halt" means "pagers go off" and other bad things.

    Moving onto the initial cause of my reply, I'll speak more
concretely of this "rollback" concept you are alluding to.


    "Rollback" in the context of a SQL database is a mathematical
property of the system first, and an implementation detail second.

    In particular, the class of statements you may make that have the
rollback property are restricted to those within the correct level of
the semantic to support it (so called "Data Manipulation Language"
(DML) statements).  You can add "rollback" within the same level of
the language as the operations because of a well defined semantic,
with proper recursive closure over itself.  Alva Couch has done some
specific work in saying this kind of thing about our problems.

    The important point is that the math comes first, and
implementation comes second.  Trying to figure out the implementation
with no grasp on the math is a *lot* more work than figuring out the
math first and doing the implementation second.

    In practice, you do often figure out math and implementation at
the same time (necessity being the mother of invention), but focus on
the math side as the complexity level goes up.  Trust me.  I'm only
able to tell you all this now because I followed this advice at one
point.


    System administration languages are different from SQL DML.  Our
languages do not have well defined semantics in the traditional sense
of the term.  If we ask our machines to execute a two element compound
statement where the second element statement is a rollback, and the
first element statement turns the machine that is executing the
statement off in some fashion or another, then our rollback operation
will never be executed(1).  This isn't a matter of halting (failure to
produce a value by way of falling into an infinite loop of some sort),
it's "you destroyed the interpreter that produces the values, if not
interpreter', and interpreter'', and interpreter'''"

    This is not asking 'does this completely unqualified notion of
program halt?', this is asking 'does this somewhat qualified notion of
program destroy its environment?'  (where the ideas of qualifying the
program and its environment are closely related when it comes to being
able to answer such questions).

    You'll need two major ingredients to think about the problems
you're running into here.  Semantics, and reflection.

    Rollback can be done, but it probably doesn't mean what you think
it means; if your object language can destroy itself, rollback has to
happen in a meta language.

    The combination of semantics and reflection can allow you to
attack problems where the object language can potentially destroy
itself, and detect such statements.  But as you have hopefully grasped
by now, we're speaking of a tall order to get here.

    Part of the deep problem is that system administrations languages
have the potential to be "implicitly reflective": they can reason with
their own statements, but can do so in very oblique ways.  To give you
some idea of what a reflective statement is in another context, think
of Liar's paradoxes like "this statement is false" -- it's reflective,
but rather explictly so -- it says "this statement" which denotes the
statement itself.  It says "is false" which is a reflected concept
from the very logic in which we are trying to evaluate the
statement(2).  Liar's paradoxes are difficult to reason with in ways
that do not cause halting problems.  It can be done, but it's work,
especially as the obliqueness of reference increases.

    For example, while we can say statements that mean "turn the
computer executing this statement off" (where "this statement" is the
reflection), this is not typically what we say: a more common
expression of something that *could* mean "turn this computer off" is
"turn power outlet #25 off" where the computer executing this
statement happens to be connected to power outlet 25.  "remove power
from outlet #25" could be expressed in some relatively direct form, or
it could be an even more oblique form like "ssh to host 'powerbar' and
type 'remove power from outlet #25'".  If that isn't oblique enough
for you, the actual version of the statement that is implicitly
reflective could be "send mail to an operator and ask them to unplug a
randomly selected power outlet", and if the operator happens to pick
outlet 25....


    We've got a fair amount of work in front of us to produce the
general case tools for what we really want.  As I said, ad hoc
approaches do work.  If you ask me, I'd say that higher order signal
is beginning to appear in what we've managed to produce so far, and
"oh dear" is approximately the scope of the problem.  It's not
impossible to "solve", but just spewing out a "proof" and moving on
doesn't really express what's going on.

    I'm not sure how clear all of this really is, but it's probably
better than the previous pap I've written to try to express the full
scope of "oh dear".  I wish my writing were more concise, but I'm
working on it.  Forgive me for using you as experimental victims.

    I should address Brent's most recent mail, but "later".



(1) At the level we're interested in thinking about, a statement that
destroys the interpreter followed by any other statement is
semantically equivelent to a statement that destroys the interpreter
followed by no other statement.  We can substitute semantically
equivelent statements for one another with no actual consequences.  It
could also be said that statements like "halt; rollback" within a
single language are non-sequiturs.

(2) Reflection is one of the key properties of liar's paradoxes.  Such
statements reflect the statement under consideration in some fashion,
and they reflect the statement's value in the logic system under which
the statement is being evaluated.  A liar's paradox of a different
logic system that is still a liar's paradox could be "This statement
does not denote the liar's paradox." or "The following statement
participates in a compound statement that, considered as a whole,
denotes the liar's paradox.  The previous statement participates in a
compound statement that, considered as a whole, does not denote the
liar's paradox."