Rn and Gn Logics

  • Claus Hintermeier
  • Hélene Kirchner
  • Peter D. Mosses


This paper proposes a simple, set-theoretic framework providing
expressive typing, higher-order functions and initial models at
the same time. Building upon Russell's ramified theory of types, we develop
the theory of Rn-logics, which are axiomatisable by an order-sorted
equational Horn logic with a membership predicate, and of Gn-logics,
that provide in addition partial functions. The latter are therefore more
adapted to the use in the program specification domain, while sharing
interesting properties, like existence of an initial model, with Rn-logics.
Operational semantics of Rn-/Gn-logics presentations is obtained through
order-sorted conditional rewriting.
How to Cite
Hintermeier, C., Kirchner, H., & Mosses, P. (1996). Rn and Gn Logics. BRICS Report Series, 3(51). https://doi.org/10.7146/brics.v3i51.20054