Shoggoth: A Formal Foundation for Strategic Rewriting

Xueying Qin, Liam O’Connor, Rob van Glabbeek, Peter Höfner, Ohad Kammar, Michel Steuwer

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Rewriting is a versatile and powerful technique used in many domains. Strategic rewriting allows programmers to control the application of rewrite rules by composing individual rewrite rules into complex rewrite strategies. These strategies are semantically complex, as they may be nondeterministic, they may raise errors that trigger backtracking, and they may not terminate.

Given such semantic complexity, it is necessary to establish a formal understanding of rewrite strategies and to enable reasoning about them in order to answer questions like: How do we know that a rewrite strategy terminates? How do we know that a rewrite strategy does not fail because we compose two incompatible rewrites? How do we know that a desired property holds after applying a rewrite strategy?

In this paper, we introduce Shoggoth: a formal foundation for understanding, analysing and reasoning about strategic rewriting that is capable of answering these questions. We provide a denotational semantics of System S, a core language for strategic rewriting, and prove its equivalence to our big-step operational semantics, which extends existing work by explicitly accounting for divergence. We further define a location-based weakest precondition calculus to enable formal reasoning about rewriting strategies, and we prove this calculus sound with respect to the denotational semantics. We show how this calculus can be used in practice to reason about properties of rewriting strategies, including termination, that they are well-composed, and that desired postconditions hold. The semantics and calculus are formalised in Isabelle/HOL and all proofs are mechanised.
Original languageEnglish
Article number3
Pages (from-to)61-89
Number of pages29
JournalProceedings of the ACM on Programming Languages
Volume8
Issue numberPOPL
DOIs
Publication statusPublished - 5 Jan 2024

Fingerprint

Dive into the research topics of 'Shoggoth: A Formal Foundation for Strategic Rewriting'. Together they form a unique fingerprint.

Cite this