  We investigate representations of imperative programs as constrained Horn
clauses. Starting from operational semantics transition rules, we proceed by
writing interpreters as constrained Horn clause programs directly encoding the
rules. We then specialise an interpreter with respect to a given source program
to achieve a compilation of the source language to Horn clauses (an instance of
the first Futamura projection). The process is described in detail for an
interpreter for a subset of C, directly encoding the rules of big-step
operational semantics for C. A similar translation based on small-step
semantics could be carried out, but we show an approach to obtaining a
small-step representation using a linear interpreter for big-step Horn clauses.
This interpreter is again specialised to achieve the translation from big-step
to small-step style. The linear small-step program can be transformed back to a
big-step non-linear program using a third interpreter. A regular path
expression is computed for the linear program using Tarjan's algorithm, and
this regular expression then guides an interpreter to compute a program path.
The transformation is realised by specialisation of the path interpreter. In
all of the transformation phases, we use an established partial evaluator and
exploit standard logic program transformation to remove redundant data
structures and arguments in predicates and rename predicates to make clear
their link to statements in the original source program.
