Primitive recursive algebraic theories and program schemes

W. Kühnel, J. Meseguer, M. Pfender, I. Sols

Research output: Contribution to journalArticlepeer-review


We introduce primitive recursion as a generation process for arrows of algebraic theories in the sense of Lawvere and carry over important results on algebraic theories and functorial semantics to the enriched setting of “primitive recursive algebra”: Existence of free primitive recursive theories and of theories presented by operations and equations on primitive recursive functions; existence of free models presented by generators and equations. Finally semantical correctness of translations is reduced to correctness for the basic operations. There is a connection to the theory of program schemes: Program schemes involving primitive recursion correspond to arrows of a primitive recursive theory freely generated over a graph of basic operations. This theory T can be viewed as a programming language with “arithmetics” given by the basic operations and with DO-loops. A machine loaded with a compiler for T can be interpreted as a T-model in Lawvere's sense, preserving primitive recursion.

Original languageEnglish (US)
Pages (from-to)207-233
Number of pages27
JournalBulletin of the Australian Mathematical Society
Issue number2
StatePublished - Oct 1977
Externally publishedYes

ASJC Scopus subject areas

  • Mathematics(all)


Dive into the research topics of 'Primitive recursive algebraic theories and program schemes'. Together they form a unique fingerprint.

Cite this