A relational theory of effects and coeffects

Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent, usage-sensitive computations, especially when combined with computational effects. From a semantic perspective, effectful and coeffectful languages have been studied mostly by means of denotational semantics and almost nothing has been done from the point of view of relational reasoning. This gap in the literature is quite surprising, since many cornerstone results — such as non-interference , metric preservation , and proof irrelevance — on concrete coeffects are inherently relational. In this paper, we fill this gap by developing a general theory and calculus of program relations for higher-order languages with combined effects and coeffects. The relational calculus builds upon the novel notion of a corelator (or comonadic lax extension ) to handle coeffects relationally. Inside such a calculus, we define three notions of effectful and coeffectful program refinements: contextual approximation , logical preorder , and applicative similarity . These are the first operationally-based notions of program refinement (and, consequently, equivalence) for languages with combined effects and coeffects appearing in the literature. We show that the axiomatics of a corelator (together with the one of a relator) is precisely what is needed to prove all the aforementioned program refinements to be precongruences, this way obtaining compositional relational techniques for reasoning about combined effects and coeffects.

Reasoning about “reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recursion

Metareasoning can be achieved in probabilistic programming languages (PPLs) using agent models that recursively nest inference queries inside inference queries. However, the semantics of this powerful, reflection-like language feature has defied an operational treatment, much less reasoning principles for contextual equivalence. We give formal semantics to a core PPL with continuous distributions, scoring, general recursion, and nested queries. Unlike prior work, the presence of nested queries and general recursion makes it impossible to stratify the definition of a sampling-based operational semantics and that of a measure-theoretic semantics—the two semantics must be defined mutually recursively. A key yet challenging property we establish is that probabilistic programs have well-defined meanings: limits exist for the step-indexed measures they induce. Beyond a semantics, we offer relational reasoning principles for probabilistic programs making nested queries. We construct a step-indexed, biorthogonal logical-relations model. A soundness theorem establishes that logical relatedness implies contextual equivalence. We demonstrate the usefulness of the reasoning principles by proving novel equivalences of practical relevance—in particular, game-playing and decisionmaking agents. We mechanize our technical developments leading to the soundness proof using the Coq proof assistant. Nested queries are an important yet theoretically underdeveloped linguistic feature in PPLs; we are first to give them semantics in the presence of general recursion and to provide them with sound reasoning principles for contextual equivalence.

Are You There?

The chapter targets the disruptive impact of the pandemic on learning environments and explores the responsive features it revealed about human resilience, creativity, and culture. By using the relational reasoning method, the chapter analyzes similarities and discrepancies between technological and human communication patterns to enhance digital learning. Furthermore, insights from synchronous and hybrid teaching experience exemplify how a relational and reflective learning approach helps us thrive as humans, as cultural selves, and enhance our skills as sovereign agents in any given environment, be it natural or virtual.

Not Just About Faces in Context: Face–Context Relation Moderates the Impact of Contextual Threat on Facial Trustworthiness

Recent work showed that the attribution of facial trustworthiness can be influenced by the surrounding context in which a face is embedded: contexts that convey threat make faces less trustworthy. In four studies ( N = 388, three preregistered) we tested whether face–context integration is influenced by how faces and contexts are encoded relationally. In Experiments 1a to 1c, face–context integration was stronger when threatening stimuli were attributable to the human action. Faces were judged less trustworthy when shown in threatening contexts that were ascribable (vs. non-ascribable) to the human action. In Experiment 2, we manipulated face–context relations using instructions. When instructions presented facial stimuli as belonging to the “perpetrators” of the threatening contexts, no difference with the control (no-instructions) condition was found in face–context integration. Instead, the effect was reduced when faces were presented as “victims.” We discussed the importance of considering relational reasoning when studying face–context integration.