We use the concept of a distributive law of a monad over a copointed endofunctor to define and develop a reformulation and mild generalisation of Turi and Plotkin's notion of an abstract operational rule. We make our abstract definition and give a precise analysis of the relationship between it and Turi and Plotkin's definition. Following Turi and Plotkin, our definition, suitably restricted, agrees with the notion of a set of $GSOS$-rules, allowing one to construct both an operational model and a canonical, internally fully abstract denotational model. Going beyond Turi and Plotkin, we construct what might be seen as large-step operational semantics from small-step operational semantics and we show how our definition allows one to combine distributive laws, in particular accounting for the combination of operational semantics with congruences.
Category theory for operational semantics
LENISA, Marina;
2004-01-01
Abstract
We use the concept of a distributive law of a monad over a copointed endofunctor to define and develop a reformulation and mild generalisation of Turi and Plotkin's notion of an abstract operational rule. We make our abstract definition and give a precise analysis of the relationship between it and Turi and Plotkin's definition. Following Turi and Plotkin, our definition, suitably restricted, agrees with the notion of a set of $GSOS$-rules, allowing one to construct both an operational model and a canonical, internally fully abstract denotational model. Going beyond Turi and Plotkin, we construct what might be seen as large-step operational semantics from small-step operational semantics and we show how our definition allows one to combine distributive laws, in particular accounting for the combination of operational semantics with congruences.File | Dimensione | Formato | |
---|---|---|---|
watanabe.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
Non pubblico
Dimensione
259.22 kB
Formato
Adobe PDF
|
259.22 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.