Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a lambda-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations -- a recently introduced notion of higher-order distance between programs -- both pure and effectful, bringing them back to a common picture with traditional ones.
The author has recently introduced an abstract algebraic framework of analogical proportions within the general setting of universal algebra. This paper studies analogical proportions in the boolean domain consisting of two elements 0 and 1 within his framework. It turns out that our notion of boolean proportions coincides with two prominent models from the literature in different settings. This means that we can capture two separate modellings of boolean proportions within a single framework which is mathematically appealing and provides further evidence for the robustness and applicability of the general framework.
We study the extent to which it is possible to approximate the optimal value of a Unique Games instance in Fixed-Point Logic with Counting (FPC). Formally, we prove lower bounds against the accuracy of FPC-interpretations that map Unique Games instances (encoded as relational structures) to rational numbers giving the approximate fraction of constraints that can be satisfied. We prove two new FPC-inexpressibility results for Unique Games: the existence of a $(1/2, 1/3 + \delta)$-inapproximability gap, and inapproximability to within any constant factor. Previous recent work has established similar FPC-inapproximability results for a small handful of other problems. Our construction builds upon some of these ideas, but contains a novel technique. While most FPC-inexpressibility results are based on variants of the CFI-construction, ours is significantly different. We start with a graph of very large girth and label the edges with random affine vector spaces over $\mathbb{F}_2$ that determine the constraints in the two structures. Duplicator's strategy involves maintaining a partial isomorphism over a minimal tree that spans the pebbled vertices of the graph.
When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of $\lambda$-calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on $\lambda$-terms known as $\simeq_\sigma$-equivalence, in both the intuitionistic (due to Regnier) and classical (due to Laurent) cases. The purpose of this paper is to uncover a strong bisimulation behind $\simeq_\sigma$-equivalence, as formulated by Laurent for Parigot's $\lambda\mu$-calculus. This is achieved by introducing a relation $\simeq$, defined over a revised presentation of $\lambda\mu$-calculus we dub $\Lambda M$. More precisely, we first identify the reasons behind Laurent's $\simeq_\sigma$-equivalence on $\lambda\mu$-terms failing to be a strong bisimulation. Inspired by Laurent's \emph{Polarized Proof-Nets}, this leads us to distinguish multiplicative and exponential reduction steps on terms. Second, we enrich the syntax of $\lambda\mu$ to allow us to track the exponential operations. These technical ingredients pave the way towards a strong bisimulation for the classical case. We introduce a calculus $\Lambda M$ and a relation $\simeq$ that we show to be a strong bisimulation with respect to reduction in $\Lambda M$, ie. two $\simeq$-equivalent terms have the exact same reduction semantics, a result which fails for Regnier's $\simeq_\sigma$-equivalence in $\lambda$-calculus as well as for Laurent's […]
Quantum based systems are a relatively new research area for that different modelling languages including process calculi are currently under development. Encodings are often used to compare process calculi. Quality criteria are used then to rule out trivial or meaningless encodings. In this new context of quantum based systems, it is necessary to analyse the applicability of these quality criteria and to potentially extend or adapt them. As a first step, we test the suitability of classical criteria for encodings between quantum based languages and discuss new criteria. Concretely, we present an encoding, from a language inspired by CQP into a language inspired by qCCS. We show that this encoding satisfies compositionality, name invariance (for channel and qubit names), operational correspondence, divergence reflection, success sensitiveness, and that it preserves the size of quantum registers. Then we show that there is no encoding from qCCS into CQP that is compositional, operationally corresponding, and success sensitive.
