Converting between Combinatory Reduction Systems and Big Step Semantics

  • Hanne Gottliebsen
  • Kristoffer H. Rose
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5700)


We make a connection between higher-order rewriting in the form of combinatory reduction systems (CRS) and logic-based operational semantics in the form of big step semantic (BSS) specifications. We show how sets of CRS rewrite rules can be encoded as BSS, and how BSS (including natural semantics) can be encoded as CRS. The connections permit the use of proper variables and substitution in both formalisms.


Normal Form Induction Hypothesis Inference Rule Free Variable Function Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Benaissa, Z.-E.-A., Lescanne, P., Rose, K.H.: Modeling sharing and recursion for weak reduction strategies using explicit substitution. In: Kuchen, H., Swierstra, S.D. (eds.) PLILP 1996. LNCS, vol. 1140, pp. 393–407. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  2. 2.
    Despeyroux, J.: Proof of Translation in Natural Semantics. In: Symposium on Logic in Computer Science (LICS 1986), pp. 193–205 (1986)Google Scholar
  3. 3.
    Gottliebsen, H.: Combinatory Reduction Systems and Natural Semantics. Master’s thesis, DAIMI, Aarhus University (1998)Google Scholar
  4. 4.
    Kahn, G.: Natural Semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  5. 5.
    Klop, J.W.: Combinatory Reduction Systems. Mathematisch Centrum, Amsterdam (1980)zbMATHGoogle Scholar
  6. 6.
    Klop, J.W.: Term Rewriting Systems. In: Handbook of Logic in Computer Science, vol. 2, pp. 1–116. Clarendon Press, Oxford (1992)Google Scholar
  7. 7.
    Marchiori, M.: On deterministic conditional rewriting, MIT Laboratory for Computer Science, vol. 405, Computation Structures Group Memo (1997)Google Scholar
  8. 8.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96, 73–155 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Mosses, P.D.: SIS–semantics implementation system. Technical Report Daimi MD-30, Computer Science Department, Aarhus University (out of print) (1979)Google Scholar
  10. 10.
    Mosses, P.D.: Action semantics. Cambridge University Press, New York (1992)CrossRefzbMATHGoogle Scholar
  11. 11.
    Ohlebush, E.: Transforming Conditional Rewrite Systems with Extra Variables into Unconditional Systems. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705. Springer, Heidelberg (1999)Google Scholar
  12. 12.
    Plotkin, G.D.: A structural approach to operational semantics. Technical Report FN-19, DAIMI, Aarhus Universitet (1981)Google Scholar
  13. 13.
    Rose, K.H.: CRSX: Combinatory Reduction Systems with Extensions. SourceForge (2007–2009),
  14. 14.
    Rose, K.H.: Explicit Substitution - Tutorial & Survey. Lecture Series LS-96-3, BRICS, Aarhus Universitet (1996)Google Scholar
  15. 15.
    Rosu, G.: From Conditional to Unconditional Rewriting. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 218–233. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Serbanuta, T., Rosu, G., Meseguer, J.: A Rewriting Logic Approach to Operational Semantics. Information and Computation 207(2) (2009)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Hanne Gottliebsen
    • 1
  • Kristoffer H. Rose
    • 2
  1. 1.Brorsonsgade 8, 1.thCopenhagen VDenmark
  2. 2.IBM Thomas J. Watson Research CenterUSA

Personalised recommendations