Concatenative Languages

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