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.

CPS transformation with affine types for call-by-value implicit polymorphism

Transformation of programs into continuation-passing style (CPS) reveals the notion of continuations, enabling many applications such as control operators and intermediate representations in compilers. Although type preservation makes CPS transformation more beneficial, achieving type-preserving CPS transformation for implicit polymorphism with call-by-value (CBV) semantics is known to be challenging. We identify the difficulty in the problem that we call scope intrusion. To address this problem, we propose a new CPS target language Λ open that supports two additional constructs for polymorphism: one only binds and the other only generalizes type variables. Unfortunately, their unrestricted use makes Λ open unsafe due to undesired generalization of type variables. We thus equip Λ open with affine types to allow only the type-safe generalization. We then define a CPS transformation from Curry-style CBV System F to type-safe Λ open and prove that the transformation is meaning and type preserving. We also study parametricity of Λ open as it is a fundamental property of polymorphic languages and plays a key role in applications of CPS transformation. To establish parametricity, we construct a parametric, step-indexed Kripke logical relation for Λ open and prove that it satisfies the Fundamental Property as well as soundness with respect to contextual equivalence.

Presuppositions, implicatures, and contextual equivalence

Maximize Presupposition! (MP), as originally proposed in Heim (Semantik: Ein internationales Handbuch der zeitgenössischen Forschung, pp. 487–535, 1991) and developed in subsequent works, offers an account of the otherwise mysterious unassertability of a variety of sentences. At the core of MP is the idea that speakers are urged to use a sentence ψ over a sentence ϕ if ψ contributes the same new information as ϕ, yet carries a stronger presupposition. While MP has been refined in many ways throughout the years, most (if not all) of its formulations have retained this characterisation of the MP-competition. Recently, however, the empirical adequacy of this characterisation has been questioned in light of certain newly discovered cases that are infelicitous, despite meeting MP-competition conditions. This has led some researchers to broaden the scope of MP, extending it to competition between sentences which are not contextually equivalent (Spector and Sudo in Linguistics and Philosophy 40(5):473–517, 2017) and whose presuppositions are not satisfied in the context (Anvari in Proceedings of Semantics and Linguistic Theory 28, pp. 711–726, 2018; Manuscript, IJN-ENS, 2019). In this paper, we present a body of evidence showing that these formulations of MP are sometimes too liberal, sometimes too restrictive: they overgenerate infelicity for a variety of felicitous cases while leaving the infelicity of minimally different cases unaccounted for. We propose an alternative, implicature-based approach stemming from Magri (PhD dissertation, MIT, 2009), Meyer (PhD dissertation, MIT, 2013), and Marty (PhD dissertation, MIT, 2017), which reintroduces contextual equivalence and presupposition satisfaction in some form through the notion of relevance. This approach is shown to account for the classical and most of the novel cases. Yet some of the latter remain problematic for this approach as well. We end the paper with a systematic comparison of the different approaches to MP and MP-like phenomena, covering both the classical and the novel cases. All in all, the issue of how to properly restrict the competition for MP-like phenomena remains an important challenge for all accounts in the literature.

Gradual type theory

Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. Sound gradually typed languages dynamically check types at runtime at the boundary between statically typed and dynamically typed modules. However, there is much disagreement in the gradual typing literature over how to enforce complex types such as tuples, lists, functions and objects. In this paper, we propose a new perspective on the design of runtime gradual type enforcement: runtime type casts exist precisely to ensure the correctness of certain type-based refactorings and optimizations. For instance, for simple types, a language designer might desire that beta-eta equality is valid. We show that this perspective is useful by demonstrating that a cast semantics can be derived from beta-eta equality. We do this by providing an axiomatic account program equivalence in a gradual cast calculus in a logic we call gradual type theory (GTT). Based on Levy’s call-by-push-value, GTT allows us to axiomatize both call-by-value and call-by-name gradual languages. We then show that we can derive the behavior of casts for simple types from the corresponding eta equality principle and the assumption that the language satisfies a property called graduality, also known as the dynamic gradual guarantee. Since we can derive the semantics from the assumption of eta equality, we also receive a useful contrapositive: any observably different cast semantics that satisfies graduality must violate the eta equality. We show the consistency and applicability of our axiomatic theory by proving that a contract-based implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual typing. The model is parameterized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.

On theories of names and references in formal languages and implications for functional and object-oriented programming

The long-standing problem of adequate formalization of local names in mathematical formulae and semantics of references in object-oriented languages taken “as is” without objects, is discussed. Reasons why the existing approaches cannot be considered suitable solutions, are explained. An introduction to the relatively recent works on the theories of names and references of the group headed by Andrew Pitts, is given. The notion of referential transparency, in which contextual equivalence is used instead of the usual equality of values, is analyzed. This is the main property, which these theories are based upon: it is preserved when a purely functional language is extended with names and references as data. It is argued that such referential transparency, along with many others, can be preserved for mutable objects that change to a limited extent. This leads to a model of computation between functional and object-oriented ones, allowing for a deterministic parallel implementation.

Contextual Equivalence for Signal Flow Graphs

We extend the signal flow calculus—a compositional account of the classical signal flow graph model of computation—to encompass affine behaviour, and furnish it with a novel operational semantics. The increased expressive power allows us to define a canonical notion of contextual equivalence, which we show to coincide with denotational equality. Finally, we characterise the realisable fragment of the calculus: those terms that express the computations of (affine) signal flow graphs.

A case study in programming coinductive proofs: Howe’s method

Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the property that similarity in the call-by-name lambda calculus is a pre-congruence using Howe’s method in the Beluga formal reasoning system. The development relies on three key ingredients: (1) we give a higher order abstract syntax (HOAS) encoding of lambda terms together with their operational semantics as intrinsically typed terms, thereby avoiding not only the need to deal with binders, renaming and substitutions, but keeping all typing invariants implicit; (2) we take advantage of Beluga’s support for representing open terms using built-in contexts and simultaneous substitutions: this allows us to directly state central definitions such as open simulation without resorting to the usual inductive closure operation and to encode very elegantly notoriously painful proofs such as the substitutivity of the Howe relation; (3) we exploit the possibility of reasoning by coinduction in Beluga’s reasoning logic. The end result is succinct and elegant, thanks to the high-level abstractions and primitives Beluga provides. We believe that this mechanization is a significant example that illustrates Beluga’s strength at mechanizing challenging (co)inductive proofs using HOAS encodings.

Mechanizing proofs with logical relations – Kripke-style

Proofs with logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe two case studies using the proof environmentBeluga: First, we explain the mechanization of the weak normalization proof for the simply typed lambda-calculus; second, we outline how to mechanize the completeness proof of algorithmic equality for simply typed lambda-terms where we reason about logically equivalent terms. The development of these proofs inBelugarelies on three key ingredients: (1) we encode lambda-terms together with their typing rules, operational semantics, algorithmic and declarative equality using higher order abstract syntax (HOAS) thereby avoiding the need to manipulate and deal with binders, renaming and substitutions, (2) we take advantage ofBeluga's support for representing derivations that depend on assumptions and first-class contexts to directly state inductive properties such as logical relations and inductive proofs, (3) we exploitBeluga's rich equational theory for simultaneous substitutions; as a consequence, users do not need to establish and subsequently use substitution properties, and proofs are not cluttered with references to them. We believe these examples demonstrate thatBelugaprovides the right level of abstractions and primitives to mechanize challenging proofs using HOAS encodings. It also may serve as a valuable benchmark for other proof environments.