Formalizing a minimal subset of concatenative languages

I've read a bit about concatenative languages and how they can be modeled, but they seem to take a mostly informal tone. I'd like to change that, so I wrote the beginnings of a formalism on a tiny subset of concatenative languages. It's available here (the important parts are in monospaced font after an introduction). This is heavily based on existing work, which I reference. The main thing I'm wondering about is, how can I make this mathematically rigorous and prove that the combinators over, dip and drop form a Turing-complete language? Or, if not, how would I prove a counterexample?

Well, the question of Turing-completeness may be a bit academic. Another issue of concern relates to type systems. If a set of type rules is defined on a language, how can it be shown that those rules are consistent with the operational semantics? I think a minimal set of combinators would be an optimal base for a correct type system, but I'm not sure.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Embedding another formalism

You may show the turing completeness by showing how to embed another calculus that is known to be turing complete. For instance, you might choose to implement the S and K Combinators of Combinatory Logic using the combinators you mentioned.