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
```