In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, a computation history is a sequence of steps taken by an
abstract machine
An abstract machine is a computer science theoretical model that allows for a detailed and precise analysis of how a computer system functions. It is analogous to a mathematical function in that it receives inputs and produces outputs based on pre ...
in the process of computing its result. Computation histories are frequently used in
proofs
Proof most often refers to:
* Proof (truth), argument or sufficient evidence for the truth of a proposition
* Alcohol proof, a measure of an alcoholic drink's strength
Proof may also refer to:
Mathematics and formal logic
* Formal proof, a co ...
about the capabilities of certain machines, and particularly about the
undecidability of various
formal languages
In logic, mathematics, computer science, and linguistics, a formal language consists of string (computer science), words whose symbol (formal), letters are taken from an alphabet (formal languages), alphabet and are well-formedness, well-formed ...
.
Formally, a computation history is a (normally
finite
Finite is the opposite of infinite. It may refer to:
* Finite number (disambiguation)
* Finite set, a set whose cardinality (number of elements) is some natural number
* Finite verb, a verb form that has a subject, usually being inflected or marke ...
) sequence of configurations of a formal
automaton
An automaton (; plural: automata or automatons) is a relatively self-operating machine, or control mechanism designed to automatically follow a sequence of operations, or respond to predetermined instructions.Automaton – Definition and More ...
. Each configuration fully describes the status of the machine at a particular point. To be valid, certain conditions must hold:
* the first configuration must be a valid initial configuration of the automaton and
* each transition between adjacent configurations must be valid according to the transition rules of the automaton.
In addition, to be complete, a computation history must be finite and
* the final configuration must be a valid terminal configuration of the automaton.
The definitions of "valid initial configuration", "valid transition", and "valid terminal configuration" vary for different kinds of formal machines.
A
deterministic
Determinism is a philosophical view, where all events are determined completely by previously existing causes. Deterministic theories throughout the history of philosophy have developed from diverse and sometimes overlapping motives and consi ...
automaton has exactly one computation history for a given initial configuration, though the history may be infinite and therefore incomplete.
Finite State Machines
For a
finite state machine
A finite-state machine (FSM) or finite-state automaton (FSA, plural: ''automata''), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number o ...
, a configuration is simply
the current state of the machine, together with the remaining input. The first configuration must be the initial state of
and the complete input. A transition from a configuration
to
a configuration
is allowed if
for
some input symbol
and if
has a transition from
to
on input
. The final
configuration must have the empty string
as its remaining
input; whether
has accepted or rejected the input depends
on whether the final state is an accepting state.
Turing Machines
Computation histories are more commonly used in reference to
Turing machines
A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
. The configuration of a single-tape Turing machine consists of the contents of the tape, the position of the read/write head on the tape, and the current state of the associated state machine; this is usually written
where
is the current state of the machine, represented in some
way that's distinguishable from the tape language, and where
is
positioned immediately before the position of the read/write head.
Consider a Turing machine
on input
. The first
configuration must be
, where
is the initial state of the Turing machine. The machine's state in the final
configuration must be either
(the accept state) or
(the reject state). A configuration
is a valid successor
to configuration
if there's a transition from the state in
to the state in
which manipulates the
tape and moves the read/write head in a way that produces the result in
.
Decidability results
Computation histories can be used to show that certain problems for
pushdown automata
In the theory of computation, a branch of theoretical computer science, a pushdown automaton (PDA) is
a type of automaton that employs a stack.
Pushdown automata are used in theories about what can be computed by machines. They are more capab ...
are
undecidable. This is because the language of
non-accepting computation histories of a Turing machine
on input
is a
context-free language
In formal language theory, a context-free language (CFL) is a language generated by a context-free grammar (CFG).
Context-free languages have many applications in programming languages, in particular, most arithmetic expressions are generated by ...
recognizable by a
non-deterministic pushdown automaton.
We encode a Turing computation history
as the
string
, where
is the encoding of configuration
, as discussed above, and where
every other configuration is written in reverse. Before reading a particular
configuration, the pushdown automaton makes a non-deterministic choice
to either ignore the configuration or read it completely onto the stack.
* If the pushdown automaton decides to ignore the configuration, it simply reads and discards it completely and makes the same choice for the next one.
* If it decides to process the configuration, it pushes it completely onto the stack, then verifies that the next configuration is a valid successor according to the rules of
. Since successive configurations are always written in opposite orders, this can be done by, for each tape symbol in the new configuration, popping off a symbol from the stack and checking if they're the same. Where they disagree, it must be accountable for by a valid transition of
. If, at any point, the automaton decides that the transition is invalid, it immediately enters a special accept state which ignores the rest of the input and accepts at the end.
In addition, the automaton verifies that the first configuration is the correct
initial configuration (if not, it accepts) and that the state of the final
configuration of the history is the accept state (if not, it accepts). Since
a non-deterministic automaton accepts if there's any valid way for it to accept,
the automaton described here will discover if the history is not a valid
accepting history and will accept if so, and reject if not.
This same trick cannot be used to recognize ''accepting'' computation histories
with an NPDA, since non-determinism could be used to skip past a test that would
otherwise fail. A linear-bounded Turing machine is sufficient to recognize
accepting computation histories.
This result allows us to prove that
, the language
of pushdown automata which accept all input, is undecidable. Suppose
we have a decider for it,
. For any Turing machine
and input
, we can form the pushdown automaton
which accepts non-accepting computation histories for that
machine.
will accept if and only if there are no
accepting computation histories for
on
; this
would allow us to decide
, which we know to be undecidable.
References
{{reflist
Theory of computation