Functorial semantics of rewrite theories

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

This paper develops a close analogy between Lawvere's functorial semantics of equational theories [21], and a similar 2-functorial semantics for rewrite theories, which specify concurrent systems and whose models are "true concurrency" models of such systems. This has the advantage of unifying within a single 2-functorial framework both models and rewrite theory morphisms. Such morphisms are used in Maude to "put rewrite theories together" in different constructions, including parameterized rewrite theory specifications.

Original languageEnglish (US)
Title of host publicationFormal Methods in Software and Systems Modeling
Subtitle of host publicationEssays Dedicated to Hartmut Ehrig on the Occasion of His 60th Birthday
EditorsHans-Joerg Kreowski, Ugo Montanari, Fernando Orejas, Grzegorz Rozenberg, Gabriele Taentzer
Pages220-235
Number of pages16
StatePublished - Dec 1 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3393 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Semantics
Morphisms
Maude
Equational Theory
Concurrent Systems
Concurrency
Specifications
Analogy
Model
Specification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Meseguer, J. (2005). Functorial semantics of rewrite theories. In H-J. Kreowski, U. Montanari, F. Orejas, G. Rozenberg, & G. Taentzer (Eds.), Formal Methods in Software and Systems Modeling: Essays Dedicated to Hartmut Ehrig on the Occasion of His 60th Birthday (pp. 220-235). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3393 LNCS).

Functorial semantics of rewrite theories. / Meseguer, José.

Formal Methods in Software and Systems Modeling: Essays Dedicated to Hartmut Ehrig on the Occasion of His 60th Birthday. ed. / Hans-Joerg Kreowski; Ugo Montanari; Fernando Orejas; Grzegorz Rozenberg; Gabriele Taentzer. 2005. p. 220-235 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3393 LNCS).

Research output: Chapter in Book/Report/Conference proceedingChapter

Meseguer, J 2005, Functorial semantics of rewrite theories. in H-J Kreowski, U Montanari, F Orejas, G Rozenberg & G Taentzer (eds), Formal Methods in Software and Systems Modeling: Essays Dedicated to Hartmut Ehrig on the Occasion of His 60th Birthday. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3393 LNCS, pp. 220-235.
Meseguer J. Functorial semantics of rewrite theories. In Kreowski H-J, Montanari U, Orejas F, Rozenberg G, Taentzer G, editors, Formal Methods in Software and Systems Modeling: Essays Dedicated to Hartmut Ehrig on the Occasion of His 60th Birthday. 2005. p. 220-235. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Meseguer, José. / Functorial semantics of rewrite theories. Formal Methods in Software and Systems Modeling: Essays Dedicated to Hartmut Ehrig on the Occasion of His 60th Birthday. editor / Hans-Joerg Kreowski ; Ugo Montanari ; Fernando Orejas ; Grzegorz Rozenberg ; Gabriele Taentzer. 2005. pp. 220-235 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inbook{6c3f47a3510648b3baae2db11e224cad,
title = "Functorial semantics of rewrite theories",
abstract = "This paper develops a close analogy between Lawvere's functorial semantics of equational theories [21], and a similar 2-functorial semantics for rewrite theories, which specify concurrent systems and whose models are {"}true concurrency{"} models of such systems. This has the advantage of unifying within a single 2-functorial framework both models and rewrite theory morphisms. Such morphisms are used in Maude to {"}put rewrite theories together{"} in different constructions, including parameterized rewrite theory specifications.",
author = "Jos{\'e} Meseguer",
year = "2005",
month = "12",
day = "1",
language = "English (US)",
isbn = "3540249362",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "220--235",
editor = "Hans-Joerg Kreowski and Ugo Montanari and Fernando Orejas and Grzegorz Rozenberg and Gabriele Taentzer",
booktitle = "Formal Methods in Software and Systems Modeling",

}

TY - CHAP

T1 - Functorial semantics of rewrite theories

AU - Meseguer, José

PY - 2005/12/1

Y1 - 2005/12/1

N2 - This paper develops a close analogy between Lawvere's functorial semantics of equational theories [21], and a similar 2-functorial semantics for rewrite theories, which specify concurrent systems and whose models are "true concurrency" models of such systems. This has the advantage of unifying within a single 2-functorial framework both models and rewrite theory morphisms. Such morphisms are used in Maude to "put rewrite theories together" in different constructions, including parameterized rewrite theory specifications.

AB - This paper develops a close analogy between Lawvere's functorial semantics of equational theories [21], and a similar 2-functorial semantics for rewrite theories, which specify concurrent systems and whose models are "true concurrency" models of such systems. This has the advantage of unifying within a single 2-functorial framework both models and rewrite theory morphisms. Such morphisms are used in Maude to "put rewrite theories together" in different constructions, including parameterized rewrite theory specifications.

UR - http://www.scopus.com/inward/record.url?scp=36849010650&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=36849010650&partnerID=8YFLogxK

M3 - Chapter

AN - SCOPUS:36849010650

SN - 3540249362

SN - 9783540249368

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 220

EP - 235

BT - Formal Methods in Software and Systems Modeling

A2 - Kreowski, Hans-Joerg

A2 - Montanari, Ugo

A2 - Orejas, Fernando

A2 - Rozenberg, Grzegorz

A2 - Taentzer, Gabriele

ER -