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.

翻译：高阶抽象GSOS是图里语和普洛特金语数学操作语义框架最近延伸至高阶语言的延伸。 框架内所有规格的基本守规特性是其操作模式的相似性是相同的。 在目前的工作中,我们为微弱的相似性制定了相应的一致理论,这表明它即刻地与众所周知的概念如Abramsky对羊羔计算法的辅助相似性等概念相适应。 在前进的道路上,我们开发了在抽象类别一级具有独立利益的几种技术,包括混合变异分子和更高等级的GSOS法律的关系提升,以及Howe方法。