What is logical relations?

2023-03-24 :: research, notes, academia

I have long struggled to understand what a logical relation is. This may come as a surprise, since I have used logical relations a bunch in my research, apparently successfully. I am not afraid to admit that despite that success, I didn’t really know what I was doing—I’m just good at pattern recognition and replication. I’m basically a machine learning algorithm.

So I finally decided to dive deep and figure it out: what is a logical relation?

As with my previous note on realizability, this is a copy of my personal notebook on the subject, which is NOT AUTHORITATIVE, but maybe it will help you.

Here’s my working definition of a logical relation:

A realizability semantic model,
built of predicates over syntax,
that reflects judgments and structures from semantics to syntax.

Point 1 is subtle; it implies that the logical relation is both a model, and a realizability semantics. Unfortunately, I still don’t know what a model is, so I’m going to have work with the following probably wrong oversimplification: the logical relation must take (syntactically) equal terms to (semantically) equal terms. Which notion of syntactic equality though? I’m not sure, and I’m going to ignore it for now.

Point 2 is actually more specific than necessary. We don’t need to predicates over syntax specifically, but really over some base model. It’s easier for me to think of this as “syntax”, though.

Point 3 is quite difficult to make precise without making a lot of this more precise in a mathematical framework. Jon Sterling gave me the following helpful definition:

A logical relation on a model M (viewed as a category) is then a model that is constructed in the following way:

Choose some functor R : M —> E where E is a sufficiently structured category (e.g. the category of sets, or something else!). The most basic example of a functor R is the “global sections functor” M —> Set, which sends every type in M to the set of closed elements of that type. This is exactly the usual “non-Kripke logical relations"; to get Kripke logical relations, you replace Set with a functor category (presheaf category) and choose a more interesting functor R.

Now define a new category G, as a category whose objects are pairs of an object A of M, together with a subobject of R(A). A morphism in G from (A,A’) to (B, B’) is given by a morphism (f : A -> B) that sends elements satisfying A’ to elements satisfying B’.

You have to show that the category G is actually a model of your language (e.g. show that it has function spaces, booleans, whatever). Doing so is the FTLR.

Note that there are some ways to generalize the situation above, but this is basically what logical relations are.

Point 3 is also is more specific than necessary; “syntax” can be generalized to be “base model”.

Despite the complexity, we can see point 3 in action in some examples below.

What are logical relations, historically?

tait1967 - Intensional interpretations of functionals of finite type I

Logical relations are sometimes called “Tait’s Method”, dating back to Tait, as far as I can tell.

In this paper, Tait proves that System T with bar induction is a conservative extension of intuitionistic analysis U_1, which is intuitionistic arithmetic plus quantification over functions plus the axiom (schema) of choice plus bar induction. This conservative extension property is the semantic property of interest. The proof starts with a proof that T without bar induction is a conservative extension of just intuitionistic arithmetic (no choice or bar induction).

To do this, Tait develops a type-indexed predicate over System T terms (without bar induction), providing a U_0 term for all T terms of each type. These predicates M_t, C_t, and E_t are (I think) what we refer to as a logical relation. In particular, the C_t relation provides the interpretation of T values of type t, M_t seems to deal with variables, and E_t seems to be a binary relation defining semantics (“weak α-definitional equality”) of terms.

Theorem V (page 205) uses this logical relation to prove that, for all semantics values at the same type, (weak α-) definitional equality is decidable: they either are or are not related in E_t. This seems to be the key point: the definitional equality is reflected out of the semantics of terms, so it can apply to the syntax of terms.

This use of logical relation seems to also be a realizability semantics, since it it assigns syntactic types to a collection of semantics terms, by induction over syntactic types, where the realizers are a subset of all possible semantics terms.

However, it seems to be more than a realizability semantics, too. What seems very important in this paper is that the semantics preserves structure, namely definitional equality. Perhaps implicitly though, other pieces are important. For example, T functions are interpreted as U functions, although it’s not clear to me that this is critical.

This is in contrast to Kleene’s (kleene1945) realizability, which did not seem concerned with structure, but only the existence of the realizers.

plotkin1973 - Lambda-definability and logical relations

Plotkin seems to be responsible for the name, and perhaps rediscovering logical relations in the context of programming languages.

Plotkin helpfully gives us a definition of “logical”, as well, and it seems quite importantly related to part 3 of my working definition. Plotkin defines a relation R as logical if it is:

a subset of any D_k from the carrier any D∞ model (this seems to correspond to “admissible relations” in modern logical relations parlance);
the relation is preserved by functions in D. That is, the relation holds on a function f in D_k iff for all arguments x, R(x) implies R (f x) (extended to the n-ary case for n-ary relations).

This suggests that it is important the logical relation is somehow interpreting syntactic structures as semantic structures, as in the case of Tait’s model interpreting syntactic functions as semantic functions. More generally, we likely want this property of all structures in the languages: syntactic pairs are interpreted as semantic pairs, etc. Jon’s category theoretical definition seems to generalize Plotkin’s definition nicely.

This denotational logical relation also shows us a logical relation that is not defined over syntax. Instead, it is a relation over some arbitrary non-trivial D∞ model. The author mentions that since they can interpret syntax in a D∞ model, they informally treat the logical relation as over syntax sometimes, which I suppose could be made formal easily enough.

How is “logical relations” used in PL?

ahmed2006 - Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types

In this paper, Ahmed is concerned with syntactic logical relations for recursive and quantified types, in particular for reasoning about contextual equivalence. Likely due to Ahmed’s work, this kind of syntactic logical relation seems to be what most people mean or think when they say “logical relation”, although that may be changing.

The desired property of the logical relation then is that two related semantic terms should be contextually equivalent in the syntax. That is, the logical relation reflects (from semantics to syntax) equivalence.

Strangely (for a realizability model), this particular syntactic logical relation also reflects typing: semantic terms in the relation are also guaranteed to be well-typed in the syntax. In contrast, some uses of “logical relations” enable semantics terms to be syntactically ill-typed. Such logical relations might be better called realizability models, although they do something reflect some structure, so perhaps reflecting typability is not a critical point of reflecting structure.

Ahmed in the introduction points out an interesting distinction: that logical relations can be either denotational, or syntactic. Syntactic logical relations model syntax as sets of syntactic values such that some property holds over that syntax. By contrast, denotational logical relations model syntax as some denotational object, Syntactic logical relations are useful for proving properties of the operational semantics directly. Denotational models instead model syntax as denotational objects, such as, e.g., sets of set-theoretic functions over elements of a D∞ model in plotkin1973. This is useful for easily proving meta-theoretical properties by reflecting properties of the denotation into the syntax, but not necessarily about the operational semantics directly.

For example, Tait uses a “denotational logical relation” into intuitionistic analysis to prove that definitional equality of System T is decidable—the definition of definitional equality, in the model, and its proof of decidability, are reflected back into the syntax; this requires no operational semantics at all. Plotkin uses a denotational logical relation, into domain theory, to show that certain λ-calculus constructs are or are not definable—existence of a term in the logical relation is reflected into the syntax as a definable expression. Neither of these is a syntactic logical relation; the semantic values never mention syntactic values directly.

Ahmed uses a “syntactic logical relation” to prove something about the operational semantics, namely, to prove contextual equivalence (an operational notion), indirectly. Direct proofs of contextual equivalence are difficult. So instead, a semantic proof of equivalence is reflected back into the syntax as ta proof of contextual equivalence. This requires structuring the logical relation into a denotation of sets of syntactic terms that evaluate in the operational semantics, so that being in the relation tells us something about evaluation in the operational semantics, which tells us something about contextual equivalence.

abel2018 - Decidability of conversion for type theory in type theory

Abel et al. define a syntactic logical relation for typed, reducible (and equivalent) terms, to prove decidability of conversion for type theory. Here, the use of syntactic logical relation is important for proving a particular conversion algorithm over the syntax is decidable.

The interesting feature of this logical relation is the generalization from a model inductively defined over types, to inductively defined over judgments. This demonstrates a weakness in my working definition of logical relation and realizability, since I defined “realizability” in terms of models inductively defined over types.

timany2022 - A Logical Approach to Type Soundness

This paper is interesting because it uses a syntactic logical relation that intentionally does not reflect typing, as many syntactic logical relations cdo. Semantically valid terms are not necessarily syntactically valid. In other ways, it looks very much like a logical relation: syntactic pairs are semantic pairs, sums sums, functions functions, etc.

The key property this paper is interested in is type safety: all well-typed terms are well-defined in the operational semantics, i.e., they evaluate to values or well-defined errors or fail to terminate, but importantly, do not get stuck. “in the operational semantics” is important to understanding why this is a syntactic logical relation; it must model terms as sets of syntactic values to reason about the operational semantics given in the paper.

However, one could imagine proving a slightly different form of type safety with a denotational logical relation. Giving a logical relation into an arbitrary model with a well-defined notion of evaluation would be implicitly a proof of type safety: that there exists a model that is type safe. The ability to reflect from semantics to syntax provides a mechanism for constructing that evaluation over syntax. So while the denotational logical relation provides no direct proof about the operational semantics, it may provide a mechanism for a type-safe-by-construction operational semantics. (This reflecting evaluation out of the semantics seems very related to the idea of normalization-by-evaluation, but I’m not clear on this.)