Machine semantics

The semantics of a machine are understood as the interplay of operational semantics with the input and output coding of a real or abstract computing machine , so that the result of a calculation can be determined without any doubt. It thus represents a typical application for formal semantics in theoretical computer science and is used in particular for proofs of correctness in the analysis of machines.

The operational semantics defines how the machine behaves at a given point in time, i.e. it specifies the step-by-step processing of data using a program . How this program looks and how it is implemented in individual work steps is part of the operational semantics. The input coding defines how the machine receives data from outside and how this is represented internally. The output coding defines which data is to be interpreted as a result in which way at the end of a calculation. This can be formalized as follows:

Be a program through which the step-by-step processing of input data is clearly defined within the framework of the respective machine model based on the operational semantics of the machine. Also let EC be the input coding and AC the output coding. Then the semantics of the machine M is a function with ${\displaystyle f_{P}}$ ${\displaystyle f_{M}:\subseteq X\rightarrow Y}$

${\displaystyle f_{M}:=AC\circ f_{P}\circ EC}$

Example: The machine program can be specified as a flow chart or program text in a programming language . A start state must now be defined in which the input data are fed to the machine. Depending on the machine model, this data could, for example, be transferred to a special register ( register machine ) or to a special input belt ( Turing machine ) so that the machine can now start processing the flowchart or program text and access this data. By processing the flowchart, the machine eventually goes into a hold state. It must now be determined how this final state of the machine is to be interpreted in terms of a calculation result. Such an interpretation can be the content of a certain register of a register machine or the tape inscription on a certain side of the read / write head of a Turing machine.