Weak Similarity in Higher-Order Mathematical Operational Semantics

TL;DR

This paper extends the framework of higher-order abstract GSOS to include weak similarity, proving it to be a congruence and connecting it to known concepts like Abramsky's applicative similarity.

Contribution

It establishes a congruence theorem for weak similarity in higher-order operational semantics, using advanced categorical techniques.

Findings

Weak similarity is shown to be a congruence in the higher-order setting.

The work connects weak similarity to Abramsky's applicative similarity.

Develops new categorical techniques for relation liftings and higher-order GSOS laws.

Abstract

Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky's applicative similarity for the lambda-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe's method.