# Enriched Lawvere Theories for Operational Semantics

## TL;DR

This paper introduces enriched Lawvere theories as a flexible framework for modeling operational semantics of formal systems, enabling translation between different semantic forms and unifying models through the Grothendieck construction.

## Contribution

It extends Lawvere theories to enriched settings, allowing detailed descriptions of operational semantics and providing a categorical approach to relate various semantic models.

## Key findings

- Enriched Lawvere theories effectively model operational semantics.
- The Grothendieck construction unifies models across contexts.
- Application to SKI-combinator calculus demonstrates practical utility.

## Abstract

Enriched Lawvere theories are a generalization of Lawvere theories that allow us to describe the operational semantics of formal systems. For example, a graph enriched Lawvere theory describes structures that have a graph of operations of each arity, where the vertices are operations and the edges are rewrites between operations. Enriched theories can be used to equip systems with operational semantics, and maps between enriching categories can serve to translate between different forms of operational and denotational semantics. The Grothendieck construction lets us study all models of all enriched theories in all contexts in a single category. We illustrate these ideas with the SKI-combinator calculus, a variable-free version of the lambda calculus.