I propose an operational semantics for concatenative languages.

In a concatenative language, expressions are made up of a sequence of
*terms*. The terms act on a piece of data I will call the *state*, and
the effect of an expression is the composition of the effects of its
terms. In this was any concatenative language forms a pre-category in
which objects are states, morphisms are expressions, the identity is
the empty expression, and the composition of any two morphisms is the
concatenation of their expressions.

The categorical axioms then correspond to trivial properties of
concatenation. Using the notation `[...]`

for lists, `++`

for
concatenation, `.`

for composition, and `id`

for the identity, we have

`(f . g) . h = (f ++ g) ++ h = f ++ (g ++ h) = f . (g . h)`

`id . f = [] ++ f = f = f ++ [] = f . id`

This model does not, however, enable reasoning about execution time or nontermination. Thus I propose a model in which terms not only have an effect on the state, but also produce a (possibly empty) sequence of terms to be executed immediately after them. In this model, a concatenative language consists of,

- A set of
*terms* - A set of
*states* - A function
`apply :: term -> state -> (state, [term])`

Evaluation is then defined as follows, using Haskell notation,

```
apply :: Term -> State -> (State, [Term])
eval :: [Term] -> State -> State
eval [] x = x
eval (t : ts) x = let (y, u) = apply t x in
eval (u ++ ts) y
```