]A Sampling-Aware Interpretation of Linear Logic: Syntax and Categorical Semantics

Pedro H. Azevedo de Amorim

Cornell University
P.O. Box 1212
New York

The usual resource interpretation of linear logic says that variables have to be used exactly once. However, there are models of linear logic where this interpretation is too restrictive.

In this work we show how in probabilistic models of linear logic the correct resource interpretation should be sampling, i.e. the linear arrow should be read as “the output may only sample once from its input”.

We accommodate this new interpretation by defining a multilanguage syntax and its categorical semantics that bridges the Markov kernel and linear logic interpretations of probabilistic programs.

§ INTRODUCTION

Probabilistic primitives have been a standard feature of programming languages since the 70s. At first, randomness was mostly used to program so called random algorithms, i.e. algorithms that require access to a source of randomness. Recently, however, with the rise of computational statistics and machine learning, randomness is also used to program statistical models and do inference on them.

Programming languages researchers have seen this rise in interest as an opportunity to further study the interaction of probability and programming languages, establishing it as an active subfield within the PL community.

One of its main challenges is giving semantics to programming languages that are both expressive in the regular PL sense as well as in its abilities to program with randomness. One particular difficulty is that the mathematical machineries used for probability theory, such as measure theory, do not interact well with higher-order functions.

In this work we focus on two classes of models of probabilistic programming — in its broad sense — that have found numerous applications: models based in linear logic and models based on Markov kernels. Out of the linear-logic-based semantics there are two that we highlight:

* Ehrhard et. al <cit.> have defined models of linear logic with probabilistic primitives and have used the translation of intuitionistic logic into linear logic $A \to B = !A \lto B$, where $!A$ is the exponential modality, to give semantics to a stochastic $\lambda$-calculus.

* Dahlqvist and Kozen <cit.> have defined an imperative, higher-order, linear language and added the type constructor $!A$ to accommodate non-linear programs.

Though their semantical models are very similar, their calculi lie on quite different foundations. By using the intuitionist logic translation into linear logic, Ehrhard et al. get a call-by-name (CBN) semantics for a functional language <cit.>. This semantics is not well-suited for practical purposes as it makes it impossible to reuse a value sampled from a distribution. Consider, for instance, the following program written in a language that has a fair coin primitive $\cdot \vdash \mathsf{coin} : \nat$:

\[\letin x {\mathsf{coin}} {(x, \neg x)}\]

Under a call-by-name semantics the program above is equivalent to $(\mathsf{coin}, \mathsf{coin})$, since it samples from $\mathsf{coin}$ each time $x$ is used. To get around this limitation the authors have introduced  a call-by-value (CBV) $\mathsf{let}$ operator, which would make the example program be interpreted as $\frac{1}{2}\delta_{(0,1)} + \frac{1}{2}\delta_{(1,0)}$, where $\delta_a$ is the point mass distribution at $a$. Unfortunately, from a semantical point of view, the existence of said operator relies on subtle mathematical constructions which complicate the semantics.

On the other hand, the calculus proposed by Dahlqvist and Kozen adopts a linear typing discipline and extends their type system with the exponential modality $!A$. Their language provides a conceptually elegant presentation of soft-conditioning based on the Kothe dual of vector spaces <cit.>.

While these linear-logic-based semantics have been proposed, semantics based on Markov kernels have also been shown to properly handle conditioning and higher-order functions <cit.>. In particular, the calculus interpreted using $\omega$-quasi Borel spaces <cit.> can soundly interpret recursive types, soft-conditioning, higher-order functions and provides a monadic interface for its probabilistic fragment.

Though both styles of semantics provide insights into how to interpret probabilistic programming languages (PPL), it is still too early to claim that we have a “correct” semantics which subsumes all of the existing ones. The approaches mentioned above both have their advantages and their drawbacks. A major advantage of the models based on linear logic mentioned above is that its morphisms are linear operators of norm $\leq 1$ – a formalism that has been extensively used to reason about stochastic processes. Indeed, Dahlqvist and Kozen <cit.> have used results from Ergodic theory to reason about the correctness of a Gibbs sampling algorithm written in their language. Because the quasi Borel formalism has only been recently discovered, there is still much work to be done when it comes to proving useful lemmas required for reasoning about programs. Even though it is a conservative extension of regular measure theory, it is still unclear which theorems hold in the higher-order setting.

That being said, there are also drawbacks to the linear logic approach. The syntactic linearity restriction imposes severe restrictions on the programming model and, as we mentioned above, making the exponential capable of reusing samples requires significant mathematical effort.

Therefore, it is essential to understand how these two families of semantics relate to each other. In this work we shed some light into the matter by showing how we can use both styles of semantics to interpret a linear calculus that does not suffer from some of the drawbacks mentioned above, while maintaining its rich reasoning principles. We believe that in the context of probabilistic programming, linear logic departs from its usual Computer Science ethos of enforcing syntactic invariants, and instead it provides a natural mathematical formalism in which to express ideas from probability theory, such as the soft-conditioning construction mentioned above.

We bridge the gap of these semantics by noting that the regular resource interpretation of linear logic, i.e. $A \lto B$ being equivalent to “by using one copy of $A$ I get one copy of $B$” is too restrictive an interpretation for probabilistic programming. Instead, we should think of usage as being equivalent to sampling. Therefore the linear arrow $A \lto B$ should be thought of as “by sampling from $A$ once I get $B$”.

From a programming languages perspective it is not completely straight forward to realize this new interpretation. The linear arrow expects its argument to be something that can be sampled from (e.g. a measure), but when we abstract over the argument, we want to think of it as if it were a value. This suggests that there are two different interpretations of variables.

We avoid this problem with a multilanguage approach: we have one language where variables roughly correspond to measures, one language where variables are values, and syntax that transports programs from the former language into the latter.

With this new interpretation of linearity, composition already corresponds to the CBV $\mathsf{let}$ used by Ehrhard et al while avoiding complicating the model. Furthermore, we get a more expressive language than that of Dahlqvist and Kozen, since we can reuse variables while still maintaining a resource interpretation of randomness.

Besides, since linear logic is at the center of our approach, we can use it to handle alternative computational interpretations of linear logic, such as session types. Indeed, there has been work done on using probabilistic session types to reason about channel communication in the presence of probabilities <cit.>. In this context we should use the usual resource interpretation of linear logic when handling the communication of processes, but the probabilistic resource interpretation when computing within a single process.

Our contributions are:

$\bullet$ We define a multi-language syntax that allows us to realize our “sampling as resource” interpretation of linear logic.

$\bullet$ We define its categorical semantics and prove certain interesting equations satisfied by it.

$\bullet$ We show that our construction is already present in existing models for probabilistic programming.

§ MATHEMATICAL PRELIMINARIES

We are assuming that the reader is familiar with basic notions of category theory such as categories and functors.

Transition matrices are one of the simplest abstractions used when modeling stochastic processes. Given two countable sets $A$ and $B$, the entry $(a, b)$ of a transition matrix is the probability of ending up in state $b \in B$ whenever you start from initial state $a \in A$.

The category $\cat{CountStoch}$ has countable sets as objects and transition matrices as morphisms. The identity morphism is the identity matrix and composition is given by matrix multiplication.

This category can only model discrete probabilistic processes. In order to generalize it we must use Markov kernels between measurable sets.

A measurable set is a pair $(A, \Sigma_A)$, where $A$ is a set and $\Sigma_A \subseteq \mathcal{P}(A)$ such that it contains the empty set, it is closed under complements and countable unions.

A function $f : (A, \Sigma_A) \to (B, \Sigma_B)$ is called measurable if for every $\mathcal{B} \in \Sigma_B$, $f^{-1}(\mathcal{B}) \in \Sigma_A$.

Let $(A, \Sigma_A)$ be a measurable space. A probability measure $(A, \Sigma_A)$ is a function $\mu : \Sigma_A \to [0, 1]$ such that $\mu(\emptyset) = 0$, $\mu(A) = 1$ and $\mu(\uplus_{i\in\nat} A_i) = \sum_{i\in\nat} \mu(A_i)$.

A measure space is a triple $(A, \Sigma_A, \mu)$, where $(A, \Sigma_A)$ is a measurable space and $\mu$ is a measure.

Let $(A, \Sigma_A)$ and $(B, \Sigma_B)$ be two measurable spaces. A Markov kernel is a function $f : A \times \Sigma_B \to [0, 1]$ such that

* For every $a \in A$, $f(a, -)$ is a probability measure.

* For every $\mathcal{B} \in \Sigma_B$, $f(-, \mathcal{B})$ is a measurable function.

An alternative definition of Markov kernel is that of Kleisli arrows for the Giry monad, also known as the probability monad.

The category $\cat{BorelStoch}$ has measurable sets as objects and Markov kernels as morphisms. The identity arrow is the function $id(a,\mathcal{A}) = 1$ if $a \in \mathcal{A}$ and $0$ otherwise. Composition is given by $(f \circ g)(a, \mathcal{C}) = \int f(-, \mathcal{C}) d(g(a, -))$.

The field of categorical probability was created in order to get a more conceptual understanding of these mathematical constructions. One of its cornerstone definitions is that of a Markov category:

A Markov category is a semicartesian symmetric monoidal category $(\cat{C}, \otimes, 1)$ in which every object $A$ comes equipped with a commutative comonoid structure, denoted by $\mathsf{copy} : X \to X \otimes X$ and $\mathsf{delete} : X \to 1$, where $\mathsf{copy}$ satisfies

\[
\mathsf{copy}_{X \otimes Y} = (id_X \otimes b_{Y, X} \otimes id_Y) \circ ( \mathsf{copy}_{X} \otimes  \mathsf{copy}_{Y}),
\]

where  $b_{Y, X}$ is the natural isomorphism $Y \otimes X \cong X \otimes Y$. The intuition behind $\mathsf{copy}_X$ is that it duplicates the input without introducing any randomness. The equation above says that duplicating over a product does not introduce any correlation between $X$ and $Y$.

$\cat{CountStoch}$ is a Markov category.

In this case the $\mathsf{copy}_X$ morphism is the matrix $X \times X \times X \to [0, 1]$ which is $1$ in the positions $(x, x, x)$ and $0$ elsewhere, and the $\mathsf{delete}$. morphism is the constant $1$ matrix indexed by $X$. Note that by composing $\mathsf{copy}$ with a measure (a morphism $\mu : 1 \to X$) you get a measure over pairs $(x, x)$ for every $x$ in the support of the measure $\mu$.

$\cat{BorelStoch}$ is a Markov category.

This category is the continuous generalization of $\cat{CountStoch}$. Its $\mathsf{copy}_X$ morphism is the Markov kernel $\mathsf{copy}_X : X \times \Sigma_X \otimes \Sigma_X \to [0, 1]$ such that $\mathsf{copy}_X(x, S \times T) = 1$ if $x \in S \cap T$ and $0$ otherwise. Its $\mathsf{delete}$ morphism is simply the function that given any element in $X$, returns the dirac measure over the singleton set — i.e. the monoidal unit.

Linear logic is a resource-aware logic that has found numerous applications in Computer Science. In particular, some of its models have been used to give semantics to probabilistic computation. We recall the categorical semantics of the multiplicative fragment of linear logic (MLL):

A category $\cat{C}$ is an MLL model if it is symmetric monoidal closed (SMCC).

We denote the monoidal product as $\otimes$ and the space of linear maps between objects $X$ and $Y$ as $X \lto Y$, $\mathsf{ev} : ((X \lto Y) \otimes X) \to Y$ is the counit of the monoidal closed adjunction and $\mathsf{cur} : \cat{C}(X \otimes Y, Z) \to \cat{C}(X, Y \lto Z)$ is the linear curryfication map. We use the triple $(\mathcal{C}, \otimes, \lto)$ to denote such models.

Let $(\cat{C}, \otimes_{\cat{C}}, 1_{\cat{C}})$ and $(\cat{D}, \otimes_{\cat{D}}, 1_{\cat{D}})$ be two monoidal categories. We say that a functor $F : \cat{C} \to \cat{D}$ is lax monoidal if there is a morphism $\epsilon : 1_{\cat{D}} \to F(1_{\cat{C}})$ and a natural transformation $\mu_{X, Y} : F(X) \otimes_{\cat{D}} F(Y) \to F(X \otimes_{\cat{C}} Y)$ making the diagrams in Figure <ref> commute.

(F(X) ⊗_D F(Y)) ⊗_D F(Z)                 F(X) ⊗_D (F(Y) ⊗_C F(Z))

F(X  ⊗_C Y) ⊗_D F(Z)                 F(X) ⊗_D F(Y ⊗_C Z)

F((X⊗_C Y) ⊗_C Z)                   F(X⊗_C (Y ⊗_C Z))

["μ⊗id", from=1-1, to=3-1]
["μ", from=3-1, to=5-1]
["α"', from=1-1, to=1-6]
["id ⊗μ"', from=1-6, to=3-6]
["μ"', from=3-6, to=5-6]
["F α", from=5-1, to=5-6]

1 ⊗_D F(X)           F(1) ⊗_D F(X)        F(X) ⊗_D 1           F(X) ⊗_D F(1)

F(X)           F(1 ⊗_C X)        F(X)           F(X ⊗_C 1)
["ϵ⊗id", from=1-1, to=1-4]
["l^D"', from=1-1, to=3-1]
["F(l^C)", from=3-4, to=3-1]
["μ", from=1-4, to=3-4]
["id⊗ϵ", from=1-6, to=1-9]
["μ", from=1-9, to=3-9]
["F(r^D)", from=3-9, to=3-6]
["r^D"', from=1-6, to=3-6]

Lax monoidal diagrams

If $\epsilon$ and $\mu_{X, Y}$ are isomorphisms we say that $F$ is strong monoidal.

One key observation of this paper is that there are many lax monoidal functors between Markov categories and models of linear logic that can interpret probabilistic processes.

§ SYNTAX

A recurring theme of linear logic models that can interpret probabilistic computation is that linear morphisms correspond to Markov kernels, which correspond to “sample-once” probabilistic processes. The connection to linearity in the algebraic sense comes when noting that every Markov kernel $A \to M B$ can, by integration, be seen as a linear function $M A \multimap M B$.

We want a syntax that reflects the fact that linearity corresponds to sampling, not variable usage. We achieve this by making use of a multi-language semantics that enables the programmer to transport programs defined in a Markov kernel-centric language to a linear, higher-order, language.

This approach contrasts with existing multi-language semantics where one of the languages is linear and is used to increase the expressivity of a non-linear language by, for instance, allowing it to have access to mutable state <cit.>. Our language flips this idea on its head: we define syntax so that we may increase the expressivity of a linear calculus.

Since many probabilistic programming constructs, such as soft-conditioning and Markov kernels, can be naturally interpreted in linear logic terms, we believe that our calculus allows the user to benefit from the insights linearity provides to PPL while unburdening them from worrying about syntactic restrictions.

We use standard notation from the literature: $\Gamma \vdash t : \tau$ means that program $t$ has type $\tau$ under context $\Gamma$, $\subst t x u$ means substitution of $u$ for $x$ in $t$ and $\subst t {\overrightarrow{x}} {\overrightarrow{u}}$ is the simultaneous substitution of the term list $\overrightarrow{u}$ for a variable list $\overrightarrow{x}$ in $t$.

We are going to use orange to represent MK programs and purple to represent LL programs. Both languages will be defined in the following sections.

§.§ A Markov Kernel Language

We need a language which can program Markov kernels. Since we are aiming at generality, we are assuming the least amount of structure possible. As such we will be working with the internal language of Markov categories, as presented in Figure <ref> and Figure <ref>. Note that we are implicitly assuming a set of primitives for the functions $\textcolor{orange}f$.

\begin{align*}
\textcolor{orange}{
\tau := 1 \smid \tau \times \tau}
\end{align*}

\begin{align*}
& \textcolor{orange}{t, u} \defined \textcolor{orange}{x} \smid \textcolor{orange}{\mathsf{unit}} \smid \textcolor{orange}{\letin x t u} \smid \textcolor{orange}{(t, u)} \smid \textcolor{orange}{\pi_1 t} \smid \textcolor{orange}{\pi_2 u} \smid \textcolor{orange}{f(M)}
\end{align*}

\begin{align*}
\textcolor{orange}{\Gamma} := \textcolor{orange}{\cdot} \smid \textcolor{orange}{x : \tau}, \textcolor{orange}{\Gamma}
\end{align*}

Syntax MK

[Var] Γ, x : τ ⊢x : τ

[Unit] Γ ⊢𝗎𝗇𝗂𝗍 : 1

[Let]Γ ⊢t : τ_1
Γ , x : τ_1 ⊢u : τΓ ⊢x t u : τ

[Primitive]Γ⊢M : τ_1
f :τ_1 →τ_2Γ⊢f(M) : τ_2

[Pair]Γ ⊢t : τ_1
Γ ⊢u : τ_2Γ ⊢(t, u) : τ_1 ×τ_2

[Proj1]Γ ⊢t : τ_1 ×τ_2 Γ ⊢π_1 t : τ_1

[Proj2]Γ ⊢t : τ_1 ×τ_2 Γ ⊢π_2 t : τ_2

Typing rules MK

Due to obvious reasons, every Markov category can interpret this language, as we show in Figure <ref>. However, as it stands, this language is not very expressive, as it does not have any probabilistic primitives nor does it have any interesting types since $1 \times 1 \cong 1$.

When working with concrete models (c.f. Section <ref>) we can extend it with more expressive types as well as with concrete probabilistic primitives. For instance, in the context of continuous probabilities we could add a $\R$ datatype and a $\cdot \vdash \mathsf{uniform} : \R$ uniform distribution primitive.

§.§ A Linear Language

Our second language is a linear simply-typed $\lambda$-calculus. Its main appeal is that it has higher-order functions.

\begin{align*}
\textcolor{npurple}{\tau} := \textcolor{npurple}{1} \smid \textcolor{npurple}{\tau \lto \tau} \smid \textcolor{npurple}{\tau \otimes \tau}
\end{align*}

\begin{align*}
& \textcolor{npurple}{t, u} \defined \textcolor{npurple}{x} \smid \textcolor{npurple}{\mathsf{unit}} \smid \textcolor{npurple}{\lamb x t} \smid \textcolor{npurple}{\app t u} \smid \textcolor{npurple}{t \otimes u} \smid \textcolor{npurple}{\letin {x\otimes y} t u}
\end{align*}

\begin{align*}
\textcolor{npurple}{\Gamma} := \textcolor{npurple}{\cdot} \smid \textcolor{npurple}{x : \tau}, \textcolor{npurple}{\Gamma}
\end{align*}

Syntax LL

The type system depicted in Figure <ref> follows the standard presentation of linear $\lambda$-calculi.

[Axiom] x : τ ⊢x : τ

[Unit] · ⊢𝗎𝗇𝗂𝗍 : 1

[Abstraction]Γ, x : τ_1 ⊢t : τ_2Γ ⊢x t : τ_1 τ_2

[Application]Γ_1 ⊢t : τ_1 τ_2
Γ_2 ⊢u : τ_1Γ_1, Γ_2 ⊢t u : τ_2

[Tensor]Γ_1 ⊢t : τ_1
Γ_2 ⊢u : τ_2Γ_1, Γ_2 ⊢t ⊗u : τ_1 ⊗τ_2

[LetTensor]Γ_1  ⊢t : τ_1 ⊗τ_2
Γ_2, x : τ_1, y : τ_2 ⊢u : τΓ_1,  Γ_2 ⊢x⊗y t u : τ

Typing rules LL

As it is the case of linear $\lambda$-calculi, every symmetric monoidal closed category gives semantics to this language. Once again, we are aiming at generality instead of expressivity. In a concrete setting it would be fairly easy to extend the calculus with a datatype $\nat$ for natural numbers and probabilistic primitives such as $\cdot \vdash \mathsf{coin} : \nat$.

§.§ Combining Languages

The main drawback of the linear calculus above is that the syntactic linearity restriction makes it harder to program in it, while the main drawback of the Markov language is that it does not allow for higher-order constructs. In this section we will show how we can combine both language so that we get a calculus with looser linearity restrictions while still being higher-order.

\begin{align*}
&\textcolor{orange}{\tau} \defined \textcolor{orange}{1} \smid \textcolor{orange}{\tau \times \tau}\\
&\textcolor{npurple}{\underline{\tau}} \defined \textcolor{npurple}{1} \smid \textcolor{npurple}{\M} \textcolor{orange}{\tau} \smid \textcolor{npurple}{\underline{\tau} \lto \underline{\tau}} \smid \textcolor{npurple}{\underline{\tau} \otimes \underline{\tau}}
\end{align*}

\begin{align*}
\textcolor{orange}{M, N} &\defined  \textcolor{orange}{x} \smid \textcolor{orange}{\mathsf{unit}} \smid \textcolor{orange}{\letin x M N} \smid \textcolor{orange}{f(M)} \\
& \smid \textcolor{orange}{ (M, N)} \smid \textcolor{orange}{\pi_1 M} \smid \textcolor{orange}{\pi_2 M}\\
\textcolor{npurple}{t, u} & \defined \textcolor{npurple}{x} \smid \textcolor{npurple}{unit} \smid \textcolor{npurple}{\lamb x t} \smid \textcolor{npurple}{\app t u} \smid \textcolor{npurple}{t \otimes u} \smid \textcolor{npurple}{\letin {x \otimes y} t u} \\
& |\, \sample {\textcolor{npurple}{t_i}} {\textcolor{orange}{x_i}} {\textcolor{orange}{M}}
\end{align*}

Syntax LL+MK

When looking at concrete models for these languages it is easy to see that the semantical interpretations of variables in both languages are completely different: in the MK language variables should be thought of as values, as the result of sampling from a distribution, whereas in the LL language, variables of ground type are measures. In order to bridge these language we must use the observation that Markov kernels — i.e. open MK terms — have a natural interpretation as linear maps between measure spaces — i.e. open LL term. The combined syntax for the language is depicted in Figure <ref>.

We now have a language design problem: we want to capture the fact that every open MK program is, semantically, also an open LL term. The naive typing rule is:

[]x_1 : τ_1, ⋯, x_n : τ_n ⊢_MK M : τx_1 : τ_1, ⋯, x_n : τ_n ⊢_LL 𝖬𝖪(M):τ

The problem with this rule is that it breaks substitution: the variables in the premise are MK variables whereas the ones in the conclusion are LL variables. One way around this would be defining a dual-context calculus for the LL language. In this case the context would be split between LL variables and MK variables and the rule would look like[note the empty context in the conclusion]:

[]x_1 : τ_1, ⋯, x_n : τ_n ⊢_MK M : τ·  ; x_1 : τ_1, ⋯, x_n : τ_n ⊢_LL 𝖬𝖪(M):τ

This fixes the issue of the previous version of the rule, we just have to state the substitution theorem a bit differently; variables in the LL context can only be substituted for by LL programs and the variables of the MK context can only be substituted for by MK programs. That being said, we want our syntax to reflect a common idiom of PPLs: we compute a distribution (an element of $\M \tau$), we sample from it and then use the result in a non-linear continuation. This is captured by the following syntax:

\[
\sample {\textcolor{npurple}{t_1, \cdots, t_{n}}} {\textcolor{orange}{x_1, \cdots, x_{n}}} {\textcolor{orange}{M}}
\]

Note that we are sampling from LL programs $t_i$ (possibly an empty list), outputting the results to MK variables $x_i$ and binding them to an MK program $M$. When clear from the context we simply use $\sample {t_i} {x_i} M$. Its corresponding typing rule is:

[Sample]x_1 : τ_1 ⋯x_n : τ_n ⊢_MK M : τ   Γ_i ⊢_LL t_i :  τ_i
0 ≤i < nΓ_1, ⋯, Γ_n ⊢_LL t_i x_i M :  τ

As the typing rule suggests, its semantics should be some sort of composition. However, as we are composing programs that are interpreted in different categories, we must have a way of translating MK programs into LL programs — as we will see in Section <ref> this translation must be functorial. The operational interpretation of this rule is that we have a set of measures $\{ \textcolor{npurple}{t_i}\}$ defined using the linear language — possibly using higher-order programs — we sample from them, bind the samples to the variables $\{\textcolor{orange}{x_i}\}$ in the MK language $\textcolor{orange}{M}$ where there are no linearity restrictions. Note that the rule above looks very similar to a monadic composition, though they are semantically different (cf. Section <ref>).

With this new syntax we can finally program in accordance with our new resource interpretation of linear logic, allowing us to write the program

\[ \sample {\textcolor{npurple}{\coin}} {\textcolor{orange}{x}} {\textcolor{orange}{(x = x)}},\]

which flips a coin once and tests the result for equality with itself, making it equivalent to $\mathsf{true}$.

This combined calculus enjoys the expected syntactic properties[To avoid visually polluting the proofs we will drop the color code in Theorem <ref> and Theorem <ref>].

Let $\Gamma, x : \underline{\tau_1} \vdash t : \underline{\tau}$ and $\Delta \vdash u : \underline{\tau_1}$ be well-typed terms, then $\Gamma, \Delta \vdash \subst t x u : \underline{\tau}$

To be more formal we would have to prove such a theorem for both the MK and LL type systems. However, since the MK calculus has been shown to satisfy these metatheoretic properties, we only focus on the LL case, in which case the proof follows by structural induction on the typing derivation $\Gamma, x : \underline{\tau_1} \vdash t : \underline{\tau}$:

* Axiom: Since $t = x$ then $\subst t x u = u$ and $\underline{\tau_1} = \underline{\tau}$.

* Abstraction: By hypothesis, $\Gamma, x : \underline{\tau_1}, y : \underline{\tau_2} \vdash t : \underline{\tau_3}$. Since we can assume wlog that $x \neq y$ and that $y \notin \Delta$, $\subst {\lamb y t} x u = \lamb y {\subst t x u}$. Therefore we can show that $\Gamma, \Delta \vdash \lamb y {\subst t x u} : \tau_2 \lto \tau_3$ by applying the rule Abstraction and by the induction hypothesis.

* Application: $\subst {\app {t_1} {t_2}} x u = \app {\subst {t_1} x u} {\subst {t_2} x u}$. Since the language LL is linear, only one of $t_1$ or $t_2$ will have $x$ as a free variable. By symmetry we can assume that $t_1$ has $x$ as a free variable and we can prove $\Gamma, \Delta \vdash \app {\subst {t_1} x u} {t_2} : \underline{\tau}$ by applying the rule Application and by the induction hypothesis.

* Sample: It is easy to prove that $\subst {(\sample t y M)} x u = \sample {(\subst t x u)} y M$

The following example illustrates how we can use the MK language to duplicate and discard linear variables.

The program which samples from a distribution $\textcolor{npurple}{t}$ and then returns a perfectly correlated pair is given by:

\[
\sample {\textcolor{npurple}{t}} {\textcolor{orange}{x}} {\textcolor{orange}{(x, x)}}
\]

Similarly, the program that samples from a distribution $\textcolor{npurple}{t}$ and does not use its sampled value is represented by the term

\[
\sample {\textcolor{npurple}{t}} {\textcolor{orange}{x}} {\textcolor{orange}{\mathsf{unit}}}
\]

Suppose that we have a Markov kernel given by an open MK term $\textcolor{orange}{x} : \textcolor{orange}{\nat} \vdash \textcolor{orange}{M} : \textcolor{orange}{\nat}$. If we want to encapsulate it as a linear program of type $\textcolor{npurple}{\M} \textcolor{orange}{\nat} \textcolor{npurple}{\lto} \textcolor{npurple}{\M} \textcolor{orange}{\nat}$ we can write:

\[
\textcolor{npurple}{\lambda \, meas\ldotp} (\sample {\textcolor{npurple}{meas}} {\textcolor{orange}{x}} {\textcolor{orange}{M}})
\]

The language defined by Dahlqvist and Kozen has types $\R^n$ for every $n \in \nat$ and interprets them as the set of measures over $\R^n$, making their syntax not well-equipped to manipulate elements of type $\R^n$ as if they were tuples. To do that it is necessary to add constants to their syntax corresponding to projection combinators. In contrast, in our combined language we can write the program $ \sample t x {\app {\pi_1} x }$ which samples from a distribution over pairs and returns only the first component.

Unfortunately there are some aspects of this language that still are restrictive. For instance, imagine that we want to write an LL program that receives two Markov kernels and a distribution over $\R$ as inputs, samples from the input measure, feeds the result to the Markov kernels, samples from them and adds the results. Its type would be

\[(\textcolor{npurple}\M \textcolor{orange}\nat \textcolor{npurple}\lto \textcolor{npurple}\M \textcolor{orange}\nat) \textcolor{npurple}\lto (\textcolor{npurple}\M \textcolor{orange}\nat \textcolor{npurple}\lto \textcolor{npurple}\M \textcolor{orange}\nat) \textcolor{npurple}\lto \textcolor{npurple}\M \textcolor{orange}\nat \textcolor{npurple}\lto \textcolor{npurple}\M \textcolor{orange}\nat\]

Even though the algorithm only requires you to sample once from each measure, it is still not possible to write it in the linear language.

We will show in Section <ref> how the type constructor $\textcolor{npurple}\M$ actually corresponds to an applicative functor <cit.>. Therefore, the limitation above is actually a particular case of a fundamental difference between programming with applicative functors and programming with monads.

In applicative style there are restrictions on the kinds of dependencies you can create between distributions since the continuation of the $\mathsf{sample}$ construction needs to be an MK program, making it impossible to typecheck the program:

\[
\sample t x {(\sample {(\app f x)} y {(\app {\app g x} y)})}
\]

That being said, if you have two open MK programs $\textcolor{orange}{x} : \textcolor{orange}{\nat} \vdash \textcolor{orange}{M_1} : \textcolor{orange}{\nat} $ and $\textcolor{orange}{x} : \textcolor{orange}{\nat} \vdash \textcolor{orange}{M_2} : \textcolor{orange}{\nat} $ you can write the following open MK program:

\[
\textcolor{orange}{\letin {y_1} {M_1} {(\letin {y_2} {M_2} {(y_1 + y_2)})}}
\]

We now have two languages that can interpret probabilistic primitives such as $\mathsf{coin}$. However, every primitive $\textcolor{orange}M$ in the MK language can be easily transported to an LL program by $\sample \_ \_ {\textcolor{orange}M}$. Therefore it makes sense to only add these primitives to the MK language.

\begin{align*}
\sem{\textcolor{npurple}{1}} &= 1_{\cat{C}}\\
\sem{\textcolor{npurple}{\underline{\tau_1} \otimes \underline{\tau_2}}} &= \sem{\textcolor{npurple}{\underline{\tau_1}}} \otimes \sem{\textcolor{npurple}{\underline{\tau_2}}}\\
\sem{\textcolor{npurple}{\underline{\tau_1} \lto \underline{\tau_2}}} &= \sem{\textcolor{npurple}{\underline{\tau_1}}} \lto \sem{\textcolor{npurple}{\underline{\tau_2}}}\\
\\
\sem{\textcolor{npurple}{\cdot}} &= 1_{\cat{C}}\\
\sem{\textcolor{npurple}{x} : \textcolor{npurple}{\underline{\tau}}, \textcolor{npurple}{\Gamma}} &= \sem{\textcolor{npurple}{\underline{\tau}}} \otimes \sem{\textcolor{npurple}{\Gamma}}\\
\end{align*}

[Axiom] τ τ

[Tensor]Γ_1 t_1 τ_1
Γ_2 t_2 τ_2 Γ_1, Γ_2 t_1 ⊗t_2 τ_1 ⊗τ_2

[LetTensor]Γ_1 t τ_1 ⊗τ_2
Γ_2 ⊗τ_1 ⊗τ_2 u τΓ_1 ⊗Γ_2 (id ⊗t); u τ

[Abstraction]Γ⊗τ_1 t τ_2Γ𝖼𝗎𝗋(t) τ_1 τ_2

[Application]Γ_1 t τ_1 τ2
Γ_2 u τ_1Γ_1⊗Γ_2 (t ⊗u); 𝖾𝗏 τ_2

Denotational semantics for LL

§ CATEGORICAL SEMANTICS

As it is the case with categorical interpretations of languages/logics, types and contexts are interpreted as objects in a category and every well-typed program/proof gives rise to a morphism in the category.

In our case, MK types $\textcolor{orange}{\tau}$ are interpreted as objects $\sem{\textcolor{orange}{\tau}}$ in a Markov category $(\cat{M}, \times)$ and well-typed programs $\textcolor{orange}{\Gamma} \vdash_{MK} \textcolor{orange}{M} : \textcolor{orange}{\tau}$ are interpreted as an $\cat{M}$ morphism $\sem{\textcolor{orange}{\Gamma}} \to \sem{\textcolor{orange}{\tau}}$, as shown in Figure <ref>. Similarly, LL types $\textcolor{npurple}{\underline{\tau}}$ are interpreted as objects $\sem{\textcolor{npurple}{\underline\tau}}$ in a model of linear logic $(\cat{C}, \otimes, \lto)$ and well-typed programs $\textcolor{npurple}{\Gamma} \vdash_{LL} \textcolor{npurple}{t} : \textcolor{npurple}{\underline\tau}$ are interpreted as a $\cat{C}$ morphism $\sem{\textcolor{npurple}{\Gamma}} \to \sem{\textcolor{npurple}{\underline{\tau}}}$, as shown in Figure <ref>.

\begin{align*}
\sem{\textcolor{orange}{1}} &= 1_{\cat{M}}\\
\sem{\textcolor{orange}{\tau_1 \times \tau_2}} &= \sem{\textcolor{orange}{\tau_1}} \times \sem{\textcolor{orange}{\tau_2}}\\
\\
\sem{\textcolor{orange}{\cdot}} &= 1_{\cat{M}}\\
\sem{\textcolor{orange}{x} : \textcolor{orange}{\tau}, \textcolor{orange}{\Gamma}} &= \sem{\textcolor{orange}{\tau}} \times \sem{\textcolor{orange}{\Gamma}}\\
\end{align*}

\[
\begin{tabular}{c}
\begin{mathpar}

\inferrule[Var]{ }{\Gamma \times \tau \xrightarrow{\mathsf{delete}\times id_\tau} 1 \times \tau \cong \tau}

\and

\inferrule[Pair]{\Gamma \xrightarrow{M} \tau_1 \\ \Gamma \xrightarrow{N} \tau_2}{\Gamma \xrightarrow{\mathsf{copy}} \Gamma \times \Gamma \xrightarrow{M \times N} \tau_1 \times \tau_2}

\and

\inferrule[Proj]{\Gamma \xrightarrow{M} \tau_1 \times \tau_2}{\Gamma \xrightarrow{M; (id_{\tau_1} \times \mathsf{delete})} \tau_1 \times 1 \cong \tau_1}

\and

\inferrule[Let]{\Gamma \xto{M} \tau_1 \\ \Gamma \times  \tau_1 \xto{N} \tau}{\Gamma \xto{\mathsf{copy}} \Gamma \times \Gamma \xto{(id_\Gamma \times M); N} \tau}

\and

\inferrule[Primitive]{\Gamma \xto{M} \tau_1 \\ \tau_1 \xto{f} \tau_2}{\Gamma \xto{M} \tau_1 \xto{f} \tau_2}

\end{mathpar}
\end{tabular}
\]

Denotational semantics for MK

To give semantics to the combined language is not as straightforward. The sample rule allows the programmer to run LL programs, bind the results to MK variables and use said variables in an MK continuation. The implication of this rule in our formalism is that our semantics should provide a way of translating MK programs into LL programs. In category theory this is usually achieved by a functor $\M$.

However, we can easily see that functors are not enough to interpret the sample rule. Consider what happens when you apply $\M$ to an MK program $\textcolor{orange}{N}$ with two free variables:

\[
\M\sem{\textcolor{orange}{N}} : \M(\tau_1 \otimes \tau_2) \to \M\tau
\]

To precompose it with two LL programs outputting $\M \tau_1$ and $\M \tau_2$ we need a morphism $\mu_{\tau_1, \tau_2} : \M\tau_1 \otimes \M\tau_2 \to \M(\tau_1 \times \tau_2)$. Furthermore, if $\textcolor{orange}{N}$ has three or more free variables, there would be several ways of applying $\mu$. Since from a programming standpoint it should not matter how the LL programs are associated, we require that $\mu_{\tau_1, \tau_2}$ makes the lax monoidality diagrams to commute. Under this assumption we may interpret the sample rule:

\[
\inferrule[Sample]{\tau_1 \times \cdots \times \tau_n \xto{N} \tau \\ \Gamma_i \xto{t_i} \M \tau_i}{\Gamma \xto{t_1 \otimes \cdots \otimes t_n} \M \tau_1 \otimes \cdots \otimes \M \tau_n \xto{\mu} \M (\tau_1 \times \cdots \times \tau_n)\xto{\M N} \M \tau}
\]

In case it only has one MK variable, the semantics is given by $\sem{\textcolor{npurple}{t}} ; \M\sem{\textcolor{orange}{N}}$ and in case it does not have any free variables the semantics is $\epsilon; \M\sem{\textcolor{orange}{N}}$.

The equational theories of the MK and LL languages are well-known. Something which is not obvious is understanding how they interact through their boundary. This is where $\M$ being a functor becomes relevant, since from functoriality it follows the two program equivalences:

Let $\textcolor{npurple}{t}$, $\textcolor{orange}{M}$ and $\textcolor{orange}{N}$ be well-typed programs,

\begin{align*}
& \sem{\app {(\lamb {\textcolor{npurple}{y}} {\sample {\textcolor{npurple}{y}} z N})} {(\sample {\textcolor{npurple}{t}} x M)}} = \\
& \sem{\sample {\textcolor{npurple}{t}} {\textcolor{orange}{x}} {(\textcolor{orange}{\letin y M N})}}
\end{align*}

\begin{align*}
&\sem{\app {(\lamb {\textcolor{npurple}{y}} {\sample {\textcolor{npurple}{y}} {\textcolor{orange}{z}} {\textcolor{orange}{N}}})} {(\sample {\textcolor{npurple}{t}} {\textcolor{orange}{x}} {\textcolor{orange}{M}})}} = \\
&\sem{\textcolor{npurple}{t}}; \M \sem{\textcolor{orange}{M}}; \M \sem{\textcolor{orange}{N}} = \sem{\textcolor{npurple}{t}}; \M(\sem{\textcolor{orange}{M}}; \sem{\textcolor{orange}{N}}) = \\
&\sem{\sample {\textcolor{npurple}{t}} {\textcolor{orange}{x}} {(\textcolor{orange}{\letin y M N}})}
\end{align*}

Let $\textcolor{npurple}{t}$ be a well-typed program,

\[
\sem{\sample {\textcolor{npurple}{t}} {\textcolor{orange}{x}} {\textcolor{orange}{x}}} = \sem{\textcolor{npurple}{t}}
\]

$ \sem{\sample {\textcolor{npurple}{t}} {\textcolor{orange}{x}} {\textcolor{orange}{x}}} = \sem{\textcolor{npurple}{t}}; \M(\sem {\textcolor{orange}{x}}) = \sem {\textcolor{npurple}{t}}; \M(id) = \sem {\textcolor{npurple}{t}}; id = \sem{\textcolor{npurple}{t}}$

Furthermore, we also have a modularity property that can be easily proven:

Let $\textcolor{npurple}{t}$, $\textcolor{orange}{M}$ and $\textcolor{orange}{N}$ be well-typed programs. If $\sem{\textcolor{orange}{M}} = \sem{\textcolor{orange}{N}}$ then

\[
\sem{\sample {\textcolor{npurple}{t}} {\textcolor{orange}{x}} {\textcolor{orange}{M}}} = \sem{\sample {\textcolor{npurple}{t}} {\textcolor{orange}{x}} {\textcolor{orange}{N}}}
\]

The expected compositionality of the semantics also holds:

Let $x_1 : \tau_1, \cdots, x_n : \tau_n \vdash t : \tau$ and $\Gamma_i \vdash t_i : \tau_i$ be well-typed terms. $\sem{\Gamma_1, \cdots, \Gamma_n \vdash \subst t {\overrightarrow{x_i}} {\overrightarrow{t_i}} : \underline{\tau}} = (\sem{\Gamma_1 \vdash t_1 : \underline{\tau_1}} \otimes \cdots \otimes \sem{\Gamma_n \vdash t_n : \underline{\tau_n }}); \sem{x_1 : \underline{\tau}_1, \cdots, x_n : \underline{\tau}_n  \vdash t : \underline{\tau}}$.

The proof follows by induction on the typing derivation of $t$.

* Axiom: Since $t = x$ then $\subst t x {t_0} = {t_0}$ and $\sem{\subst t x {t_0}} = \sem{t_0} = \sem{t_0}; id = \sem{t_0}; \sem{x}$.

* Unit: Since $t = x$ then $\subst t x {t_0} = {t_0}$ and $\sem{\subst t x {t_0}} = \sem{t_0} = \sem{t_0}; id = \sem{t_0}; \sem{x}$.

* Tensor: We know that $t = t_1 \otimes t_2$. Furthermore, from linearity we know that each free variable appears either in $t_1$ or in $t_2$. Without loss of generality we can assume that

\begin{align*}
&\subst {(t_1 \otimes t_2)} {x_1, \cdots , x_n} {u_1,\cdots , u_n} = \\
&(\subst {t_1} {x_1, \cdots, x_k} {u_1, \cdots, u_k}) \otimes (\subst {t_2} {x_{k+1}, \cdots, x_n} {u_{k+1}, , \cdots, u_n})
\end{align*}

We can conclude this case from the induction hypothesis and functoriality of $\otimes$.

* LetTensor: This case follows from the functoriality of $\otimes$ and the induction hypothesis.

* Abstraction: This case follows from unfolding the definitions, using the induction hypothesis and by naturality of $\mathsf{cur}$.

* Application and Sample: Analogous to the Tensor case.

u_1 ≡u_2t x u_1 ≡t x u_2

Substitution rule

From this theorem we can conclude:

The rule shown in Figure <ref> is sound with respect to the categorical semantics.

Lax monoidal functors, under the name applicative functors, are widely used in programming languages research. They are often used to define embedded domain-specific languages (eDSL) within a host language. This suggests that the Markov kernel language can be thought of as an eDSL inside a linear language.

We have just shown that $\M$ being lax monoidal is sufficient to give semantics to our combined language, but what would happen if it had even more structure? If it were also full it would be possible to add a reification command[The proposed rule breaks the substitution theorem, but it is possible to define a variant for it where this is not the case]:

\[
\inferrule{\M\Gamma \vdash t : \M \tau}{\Gamma \vdash \mathsf{reify}(t) : \tau }
\]

Where $\M\Gamma$ is notation for every variable in $\Gamma$ being of the form $\M\tau'$, for some $\tau'$. The semantics for the rule would be taking the inverse image of $\M$. As we will show in the next section, there are some concrete models where $\M$ is full and some other models where $\M$ is not full.

A property which is easier to satisfy is asking for $\M$ to be faithful. In this case the translation of the MK language into the LL language would be fully-abstract in the following sense:

Let $ \textcolor{orange}{x} : \textcolor{orange}{\tau_1} \vdash \textcolor{orange}{M} : \textcolor{orange}{\tau_2}$ and $ \textcolor{orange}{x} : \textcolor{orange}{\tau_1} \vdash\textcolor{orange}{ N} : \textcolor{orange}{\tau_2}$ be two well-typed MK programs. If $\M$ is faithful then $\sem{\sample {\textcolor{npurple}{x}} {\textcolor{orange}{x} } \textcolor{orange}{M}} = \sem{\sample {\textcolor{npurple}{x}} {\textcolor{orange}{x} } \textcolor{orange}{N}}$ implies $\sem {\textcolor{orange}{M}} = \sem {\textcolor{orange}{N}}$.

$\sem{\sample {\textcolor{npurple}{x}} {\textcolor{orange}{x} } \textcolor{orange}{M}} = \sem{\sample {\textcolor{npurple}{x}} {\textcolor{orange}{x} } \textcolor{orange}{N}} \implies id_{\textcolor{npurple}{\M}\textcolor{orange}{\tau_1}}; \M\sem{\textcolor{orange}{M}} = id_{\textcolor{npurple}{\M}\textcolor{orange}{\tau_1}}; \M\sem{\textcolor{orange}{N}} \implies \sem{\textcolor{orange}{M}} = \sem{\textcolor{orange}{N}}$.

§ CONCRETE MODELS

In this section we show how existing models for both discrete as well as continuous probabilities fit within our formalism.

§.§ Discrete Probability

For the sake of simplicity we will denote the monoidal product of $\cat{CountStoch}$ as $\times$.

The probabilistic coherence space model of linear logic has been extensively studied in the context of semantics of discrete probabilistic languages<cit.>.

A probabilistic coherence space (PCS) is a pair $(|X|, \Pcal (X))$ where $|X|$ is a countable set and $\Pcal (X) \subseteq |X| \to \R^+$ is a set, called the web, such that:

* $\forall a \in X\ \exists \varepsilon_a > 0\ \varepsilon_a \cdot \delta_a \in \mathcal P (X)$, where $\delta_a(a') = 1$ iff $a = a'$ and $0$ otherwise;

* $\forall a \in X\ \exists \lambda_a\ \forall x \in \mathcal P (X)\ x_a \leq \lambda_a$;

* $\mathcal P (X)^{\perp\perp} = \mathcal P (X)$, where $\mathcal P (X)^\perp = \set {x \in X \rightarrow \R^+} {\forall v \in \mathcal P(X)\ \sum_{a \in X}x_av_a \leq 1}$.

We can define a category $\cat{PCoh}$ where objects are probabilistic coherence spaces and morphisms $X \lto Y$ are matrices $f : |X| \times |Y| \to \R^+$ such that for every $v \in \Pcal{(X)}$, $(f\, v) \in \Pcal{(Y)}$, where $(f \, v)_b = \sum_{a \in |A|}f_{(a,b)}v_a$.

Let $(|X|, \Pcal{(X)})$ and $(|Y|, \Pcal{(Y)})$ be PCS, we define $X \otimes Y = (|X| \times |Y|, \set{x \otimes y}{ x \in \Pcal{(X)}, y \in \Pcal{(Y)}}^{\perp\perp})$, where $(x \otimes y)(a, b) = x(a)y(b)$

Let $X$ be a countable set, the pair $(X, \set{\mu : X \to \R^+}{\sum_{x \in X} \mu(x) \leq 1})$ is a PCS.

The first two points are obvious, as the Dirac measure is a subprobability measure and every subprobability measure is bounded above by the constant function $\mu_1(x) = 1$.

To prove the last point we use the — easy to prove — fact that $\Pcal{X} \subseteq \Pcal{X}^{\perp\perp}$. Therefore we must only prove the other direction. First, observe that, if $\mu \in \set{\mu : X \to \R^+}{\sum_{x \in X} \mu(x) \leq 1}$, then we have $\sum \mu(x)\mu_1(x) = \sum 1\mu(x) = \sum \mu(x) \leq 1$, $\mu_1 \in \set{\mu : X \to \R^+}{\sum_{x \in X} \mu(x) \leq 1}^\perp$.

Let $\tilde{\mu} \in \set{\mu : X \to \R^+}{\sum_{x \in X} \mu(x) \leq 1}^{\perp\perp}$. By definition, $\sum \tilde{\mu}(x) = \sum \tilde{\mu}(x)\mu_1(x) \leq 1$ and, therefore, the third point holds.

Let $X \to Y$ be a $\cat{CountStoch}$ morphism. It is also a $\cat{PCoh}$ morphism.

There is a lax monoidal functor $\M : \cat{CountStoch} \to \cat{PCoh}$.

The functor is defined using the lemmas above. Functoriality holds due to the functor being the identity on arrows. The lax monoidal structure is given by $\epsilon = id_{1}$ and $\mu_{X, Y} = id_{X \times Y}$

If $\mu \in \set{x \otimes y}{ x \in \M (X), y \in \M (Y)}^{\perp}$ then for every $x \in X$ and $y \in Y$, $\mu(x, y) \leq 1$.

If there were such indices such that $\mu(x_1, y_1) > 1$ then $\sum\sum \mu(x,y)(\delta_{x_1}\otimes\delta_{y_1})(x,y) > \mu(x_1, y_1) (\delta_{x_1}\otimes\delta_{y_1})(x_1,y_1) = \mu(x_1, y_1) > 1$, which is a contradiction.

Let $X$ and $Y$ be two countable sets, then

\begin{align*}
&\M X \otimes \M Y = \left( X \times Y, \set{\mu : X \times Y \to \R^+}{\sum_{x \in X} \sum_{y \in Y}\mu(x, y) \leq 1}\right ) = \\
&\M(X \times Y).
\end{align*}

By the lemma above it follows that if we have a joint probability distribution $\tilde{\mu}$ over $X \times Y$ and an element $\mu \in \set{x \otimes y}{ x \in \M (X), y \in \M (Y)}^{\perp}$ then $\sum \sum \mu(x, y)\tilde{\mu}(x,y) \leq \sum\sum \tilde{\mu}(x, y) \leq 1$.

Both $\epsilon$ and $\mu_{X, Y}$ are isomorphisms.

Since $\epsilon$ is the identity morphism, it is trivially an isomorphim. The morphisms $\mu_{X, Y}$ being an isomorphism is a direct consequence of the lemmas above.

The functor $\M$ is full.

Both results above can be directly used to enhance the syntax of the combined language. From Theorem <ref> we can conclude that elements of type $\M(\tau_1 \times \tau_2)$, by projecting their marginal distributions, can be manipulated as if they had type $\M\tau_1 \otimes \M \tau_2$. Something to note is that when we do this marginalization process we lose potential correlations between the elements of the pair.

Furthermore, Theorem <ref> says that every element $\M \nat \lto \M \nat$ can be reified to an open MK program $x : \nat \vdash M : \nat$, meaning that the program described in Section <ref> that adds two Markov kernels could be written in the LL language as well.

§.§ Continuous Probability

The category $\cat{RoBan}$ has regular ordered Banach spaces as objects and regular linear functions as morphisms.

There is a lax monoidal functor $\M : \cat{BorelStoch} \to \cat{RoBan}$.

The functor acts on objects by sending a measurable space to the set of signed measures over it, which can be equipped with a $\cat{RoBan}$ structure. On morphisms it sends a Markov kernel $f$ to the linear function $\M( f)(\mu) = \int f d \mu$.

The monoidal structure of $\cat{RoBan}$ satisfies the universal property of tensor products and, therefore, we can define the natural transformation $\mu_{X, Y} : \M(X) \otimes \M(Y) \to \M (X \times Y)$ as the function generated by the bilinear function $ \M(X); \M(Y) \lto \M (X \times Y)$ which maps a pair of distributions to its product measure. The map $\epsilon$ is, once again, equal to the identity function.

The commutativity of the lax monoidality diagrams follows from the universal property of the tensor product: it suffices to verify it for elements $\mu_A \otimes \mu_B \otimes \mu_C$.

Even though $\M$ looks very similar to the discrete case, the functor is not strong monoidal, which has a few consequences in how we write programs in the combined language, as we may only project out of a pair by using the MK language, as the program below illustrates:

\[
t = (\sample {\mathsf{rand}} x {(x, x+1)})
\]

If we want to get only the first component of the pair we must wrap $t$ around a new $\mathsf{sample}$ construct:

\[
\sample t y {(\pi_1\ y)}
\]

This lack of isomorphism is a well-known theorem from functional analysis. In practice it means that there are joint probability distributions (elements of $\M(A \times B)$) that cannot be represented as an element of the tensor $\M(A) \otimes \M(B)$, which is usually defined as a closure of product probability distributions, as illustrated by <cit.>.

§ BEYOND PROBABILITY

There are other models of linear logic where syntactic usage is too restrictive to capture linear morphisms. One such example is non-determinism, where linear morphisms $A \lto B$ should be seen as “by observing the non-deterministic value of $A$ once I get $B$”.

It is possible to adapt the syntax and categorical semantics presented in this paper to give semantics to a language for non-deterministic programming. For instance, consider the powerset $\mathcal P$ monad over the category $\cat{Set}$. Non-deterministic functions can me modeled by functions $A \to \Pcal{(B)}$ — i.e. morphisms in the Kleisli category for the powerset monad.

Furthermore it is a well-known result that the Kleisli category to the powerset monad is isomorphic to the category $\cat{Rel}$, which is a model of linear logic. In such a scenario there is an obvious lax monoidal functor $id_{\cat{Rel}}: \cat{Rel} \to \cat{Rel}$ and we could add the syntax $\mathsf{observe}\ t \ \mathsf{as } \ x \ \mathsf{in}\ u$ to the language as the non-deterministic variant of the $\mathsf{sample}$ syntax. In this particular case the non-deterministic calculus does not suffer from any of the drawbacks mentioned in the probabilistic case.

§ RELATED WORK

Session types are an alternative computational interpretation for linear logic. It is used to model distributed computation and has been recently extended to program with randomness <cit.>. They can be used to program finite state Markov chains. Unfortunately, the linearity syntactic restrictions reduces the expressivity of the calculus. One way they work around it is by extending the type system with a new family of additive connectives $A \oplus_p B$, where $p \in [ 0, 1] $. This approach, however, is not enough, as they can only model finite state systems and the probability transitions are static. Our semantics could solve these issues by defining a functional-message passing language <cit.> where the functional core would deal with the probabilistic aspects of the system and the message passing core would deal with the communication between agents.

Ehrhard et al. <cit.> have defined a model of linear logic which can be used to interpret a higher-order probabilistic programming language. They have used the CBN translation of intuitionistic logic into linear logic $A \to B = !A \multimap B$ to give semantics to their language. One consequence of such a semantics is that it is not possible to store a sampled valued, meaning that every use of a variable corresponds to a different sampling from a random variable, making it unfit for writing many useful programs. In order to mitigate this problem the authors extend their language with a CBV “let” syntax which allows to record a sampled valued through out the execution of the program. In order to give semantics to this new language they must modify their semantical domain. Our approach differs from theirs because we do not make use of the exponential in other to interpret seemingly non-linear programs, meaning that we can use their original, simpler, model to interpret our language.

Dahlqvist and Kozen <cit.> have defined a category of partially ordered Banach spaces and shown that it is a model of intuitionistic linear logic. An important difference from their approach and the one mentioned above is that they embrace linearity as part of their syntax. As we argued in this paper, we believe that the syntactic restriction of linearity they have used is not adequate for the purposes of probabilistic programming. Therefore, by using the techniques presented in this paper we can give semantics to a more expressive version of their language.

Quasi Borel spaces <cit.> are a conservative extension of $\cat{Meas}$ that are Cartesian closed category equipped with a commutative probability monad. The drawback of this model is that it is still not as well understood as their measure theoretic counterpart. A practical consequence of this fact is there are probability theorems that are useful when proving properties about stochastic processes and programs that may not be true in $\cat{QBS}$.

Recently, Geoffroy <cit.> has made progress in connecting linear logic and quasi Borel Spaces by showing that a certain subcategory of the Eillenberg-Moore category for the Giry monad in $\cat{QBS}$ is a model of classical linear logic.

This result has interesting implications to our work as we can instantiate our categorical semantics with their concrete model and have an MK language with higher-order features and allow for the sampling of higher-order functions in the LL language. It is an interesting research question to understand if the characterizations of soft-conditioning as linear duality could be used in this model as well.

The idea of having two distinct languages that are connected by a functorial layer is reminiscent of Call-by-Push-Value (CBPV), which has a type system for values and a type system for computations that are connected by an adjunction. There has been recent work on using a CBPV semantics to interpret probabilistic computation. In the first one, Ehrhard and Tasson <cit.> use the monoidal adjunction generated by the linear logic exponential $!$ in order to define a calculus that can interpret lazy and eager probabilistic computation. Goubault-Larrecq <cit.> has defined a CBPV domain semantics that mixes probability and non-determinism.

There are a couple of important differences between these calculi and our language. Namely, the adjunction manifests itself in CBPV by requiring a way of moving from the value computation and vice-versa. Our language only requires translations in one direction. As a consequence, our semantics require less structure than the CBPV one. Indeed, neither of the models presented in Section <ref> are CBPV models. Furthermore, in CBPV calculi variables are interpreted the same in both languages. In our combined language this is not the case.

§ CONCLUSION AND FUTURE WORK

In this paper we have presented a new syntax that is better suited for our“sampling as a resource” interpretation of linear logic. We have also defined its categorical semantics, shown how the equational theories of the languages interact and presented concrete models for it that can handle discrete as well as continuous probabilities.

Due to the modularity of the semantics, it is fairly standard to provide extensions to the language by extending each of the languages separately. For instance, recent work by Stein and Staton <cit.> have shown how to extend Markov categories so that they may also handle probabilistic conditioning. On the linear logic side of things, Dahlqvist et al. have shown how Bayesian inference can be defined using dual vector spaces.

An interesting question is understanding whether we can adopt their models to our language and understand how they would interact. Models of linear logic such as $\cat{PCoh}$ have also been used to give semantics to more expressive features of programming languages, such as recursive types.

Finally, this new resource interpretation of linear logic has deep connections to probabilistic independence. Under this new interpretation, the Tensor rule of linear logic says that in order to produce an element of type $\tau_1 \otimes \tau_2$ you have to sample from distinct sources of randomness (the elements of the disjoint contexts $\Gamma_1$ and $\Gamma_2$), guaranteeing probabilistic independence. For future work we would to further explore the connections between our new resource interpretation of linear logic and probabilistic independence.

Going a different direction, it would also be interesting to extend this approach to other effects. Syntactically it is easy to generalize our syntax to general effects, the main difficulty arises when considering models for these new calculi. We conjecture that game semantics would provide a natural setting to construct said models.

#1     #1DOI:0#1
#1     #1     #1     #1     #1#1          #1#1   #1#1

[Clerc, Danos, Dahlqvist, and GarnierClerc
et al2017]
authorpersonFlorence Clerc, personVincent
Danos, personFredrik Dahlqvist, and personIlias
Garnier. year2017.
Pointless learning. In booktitleInternational Conference on Foundations of Software Science and Computation
Structures (FoSSaCS).

[Dahlqvist and KozenDahlqvist and
authorpersonFredrik Dahlqvist and
personDexter Kozen. year2019.
Semantics of higher-order probabilistic programs
with conditioning. In booktitlePrinciples of Programming
Languages (POPL).

[Danos and EhrhardDanos and Ehrhard2011]
authorpersonVincent Danos and personThomas
Ehrhard. year2011.
Probabilistic coherence spaces as a model of
higher-order probabilistic computation.
journalInformation and Computation
volume209, number6 (year2011),

[Das, Wang, and HoffmannDas
et al2020]
authorpersonAnkush Das, personDi Wang,
and personJan Hoffmann. year2020.
Probabilistic Resource-Aware Session Types.
journalarXiv preprint arXiv:2011.09037

authorpersonThomas Ehrhard.
On the linear structure of cones. In
booktitleLogic in Computer Science (LICS).

[Ehrhard, Pagani, and TassonEhrhard
et al2017]
authorpersonThomas Ehrhard, personMichele
Pagani, and personChristine Tasson.
Measurable cones and stable, measurable functions:
a model for probabilistic higher-order programming. In
booktitlePrinciples of Programming Languages (POPL).

authorpersonTobias Fritz.
A synthetic approach to Markov kernels, conditional
independence and theorems on sufficient statistics.
journalAdvances in Mathematics
volume370 (year2020), pages107239.

authorpersonGuillaume Geoffroy.
titleExtensional Denotational Semantics of Higher-Order
Probabilistic Programs, Beyond the Discrete Case (unpublished).

authorpersonJean Goubault-Larrecq.
A probabilistic and non-deterministic
call-by-push-value language. In booktitleLogic in Computer
Science (LICS).

[Heunen, Kammar, Staton, and YangHeunen
et al2017]
authorpersonChris Heunen, personOhad
Kammar, personSam Staton, and personHongseok
Yang. year2017.
A convenient category for higher-order probability
theory. In booktitleLogic in Computer Science (LICS).

[Inverso, Hernán, Luca, Trubiani, and
TuostoInverso et al2020]
authorpersonOmar Inverso, personMelgratti
Hernán, personPadovani Luca, personCatia
Trubiani, and personEmilio Tuosto.
Probabilistic Analysis of Binary Sessions. In
booktitleCONCUR 2020.

[Maraist, Odersky, Turner, and WadlerMaraist
et al1999]
authorpersonJohn Maraist, personMartin
Odersky, personDavid N Turner, and personPhilip
Wadler. year1999.
Call-by-name, call-by-value, call-by-need and the
linear lambda calculus.
journalTheoretical Computer Science

[McBride and PatersonMcBride and
authorpersonConor McBride and personRoss
Paterson. year2008.
Applicative programming with effects.
journalJournal of functional programming
volume18, number1 (year2008),

authorpersonPaul-André Mellies.
Categorical semantics of linear logic.
journalPanoramas et syntheses
volume27 (year2009), pages15–215.

[Scherer, New, Rioux, and AhmedScherer
et al2018]
authorpersonGabriel Scherer, personMax New,
personNick Rioux, and personAmal Ahmed.
Fabulous Interoperability for ML and a Linear
Language. In booktitleInternational Conference on
Foundations of Software Science and Computation Structures (FoSSaCS).

[Stein and StatonStein and Staton2021]
authorpersonDario Stein and personSam
Staton. year2021.
Compositional Semantics for Probabilistic Programs
with Exact Conditioning. In booktitleLogic in Computer
Science (LICS).

[Tasson and EhrhardTasson and
authorpersonChristine Tasson and
personThomas Ehrhard. year2019.
Probabilistic call by push value.
journalLogical Methods in Computer Science

[Toninho, Caires, and PfenningToninho
et al2013]
authorpersonBernardo Toninho,
personLuís Caires, and personFrank Pfenning.
Higher-order processes, functions, and sessions: A
monadic integration. In booktitleEuropean Symposium on
Programming (ESOP).

[Vákár, Kammar, and
StatonVákár et al2019]
authorpersonMatthijs Vákár,
personOhad Kammar, and personSam Staton.
A domain theory for statistical probabilistic
programming. In booktitlePrinciples of Programming Languages


# Approaches to Identify Vulnerabilities to Misinformation: A Research Agenda

Nattapat Boonprakong<EMAIL_ADDRESS>University of
MelbourneAustralia ,  Benjamin Tag<EMAIL_ADDRESS>University of
MelbourneAustralia and  Tilman Dingler<EMAIL_ADDRESS>University of MelbourneAustralia

(2018)

###### Abstract.

Given the prevalence of online misinformation and our scarce cognitive
capacity, Internet users have been shown to frequently fall victim to such
information. As some studies have investigated psychological factors that make
people susceptible to believe or share misinformation, some ongoing research
further put these findings into practice by objectively identifying when and
which users are vulnerable to misinformation. In this position paper, we
highlight two ongoing avenues of research to identify vulnerable users:
detecting cognitive biases and exploring misinformation spreaders. We also
discuss the potential implications of these objective approaches: discovering
more cohorts of vulnerable users and prompting interventions to more
effectively address the right group of users. Lastly, we point out two of the
understudied contexts for misinformation vulnerability research as
opportunities for future research.

misinformation; vulnerable users; user profiling; cognitive bias

††copyright: acmcopyright††journalyear: 2022††doi:
10.1145/1122445.1122456††conference: CHI ’22: ACM CHI Conference on Human
Factors in Computing Systems; April 30–May 6, 2022; New Orleans,
LA††booktitle: CHI ’22: ACM CHI Conference on Human Factors in Computing
Systems, April 30–May 6, 2022, New Orleans, LA††price: 15.00††isbn:
978-1-4503-XXXX-X/18/06††ccs: Human-centered computing Human computer
interaction (HCI)

##  1\. Introduction

There is a sheer amount of misinformation circulating on the Internet
nowadays. Defined as false or misleading information, misinformation
misinforms people and bears many of the harmful effects to individuals and
society (Lewandowsky et al., 2017). More recently, misinformation has
undermined public health guidance about COVID-19 (Roozenbeek et al., 2020).
Through Internet users who consume online media, misinformation has been shown
to spread faster than factually accurate information (Vosoughi et al., 2018).
This phenomenon, where users believe and share misinformation without taking
deliberate considerations, can be attributed to not only the presence of
misinformation but also the psychological vulnerabilities of information
consumers (Freitas et al., 2013). Humans are not always rational (Simon,
1957); therefore, they are prone to make erroneous decisions, like
misinterpreting news or sharing unverified information.

There are two main actions regarding misinformation: believing and sharing. In
the literature, research has explored several user-side factors that govern
the susceptibility of people to believe online misinformation. Cognitive
biases–mental shortcuts we use to achieve faster but less deliberate
decisions– have been marked as factors that make people be gullible to false
or unverified information (Pantazi et al., 2021). Martel et al. (2020) have
shown that reliance on emotion indicates higher belief in false information.
Some research have shown that political partisans (Nikolov et al., 2021) or
those who are older than 65 years (Brashier and Schacter, 2020) are prone to
believing fake news. Roozenbeek et al. (2020) found that higher numeracy
skills and better trust in science are indicators of lower susceptibility to
misinformation.

On the other hand, some research has investigated why people share unverified
information online. Motivated by (DiFonzo and Bordia, 2007; Pennycook et al.,
2020), Karami et al. (2021) listed five motivational factors in spreading fake
news: uncertainty, anxiety, lack of control, relationship enhancement, and
social rank. Laato et al. (2020) found that trust in online information and
information overload are strong indicators of sharing unverified information.
Chen et al. (2015) suggested that people share misinformation because of
social factors, i.e., self-expression and socialization. In addition, Avram et
al. (2020) found that social engagement metrics (i.e., the number of likes or
shares) increased the tendency to share misinformative contents.

Based on the above-mentioned psychological findings, some research have put
these findings into practice by building computing systems that objectively
identify potential misinformation spreaders based on their online and offline
behaviours (Giachanou et al., 2020; Karami et al., 2021; Sülflow et al.,
2019). Unlike previous approaches that rely on self-report measures, these
approaches quantify how people behave with information and produce insights
about their specific behaviours regarding to misinformation. Through
behavioural and psycho-physiological measures, these approaches can explicitly
identify when and which users are prone to believe or spread misinformation.

Different individuals have different backgrounds and different levels of
cognitive capacity. Therefore, some information consumers may be more prone
than others to misinformation. Echoing the findings in Geeng et al. (2020)
that different design interventions may be effective for different users, the
objective approaches to identify vulnerable users would also provide a a guide
on which misinformation intervention should be deployed to which group of
users. Ultimately, interventions would be made more effective as they address
the right group of users.

In this position paper, we discuss empirical approaches to identifying people
who may be susceptible to misinformation: detecting cognitive biases and
profiling vulnerable users. We also highlight their implications of
identifying more cohorts of vulnerable users and prompting interventions to
address the right group of users. Lastly, we elaborate on challenges and
future avenues to investigate vulnerabilities to misinformation. We intend to
generate a fruitful discussion in this workshop about the need to explore
potential victims of misinformation, identify their vulnerabilities, and
employ the right interventions to address the right user cohorts.

##  2\. Approaches to Identifying Vulnerabilities to Misinformation

Various studies have investigated why people believe and share misinformation
on the Internet. However, most of the studies addressed such questions based
on self-report measures, e.g., questionnaires, which are prone to many
limitations such as subjectiveness. On the other hand, some research has
proposed objective approaches to identifying users who may be susceptible to
misinformation. Combining prior psychological findings and behavioural
measures, these research efforts explicitly identify which and when users tend
to believe and share misinformation. In this paper, we discuss two promising
approaches: detecting cognitive bias detection and profiling social media
users.

###  2.1. Cognitive Bias Detection

Humans possess limited cognitive capacity and employ cognitive biases as
mental shortcuts, which can lead to irrational judgements. One prominent
example is “confirmation bias” (also known as selective exposure) as a
tendency to seek solely information to supports one’s perspectives or
expectations, while ignoring other dissenting information (Nickerson, 1998).
Taking the advantage of social media platforms that inform users with contents
that reinforce their viewpoints, confirmation bias is easily seen on social
media platforms as many users tend to consume and spread content items that
match their belief without checking its veracity (Zollo and Quattrociocchi,
2018).

Addressing cognitive biases might be a feasible approach to identify when the
user is susceptible to misinformation. Methods to detect confirmation bias
have traditionally relied on self-reports (Clay et al., 2013), for example,
asking users about their news consumption habits (Garrett et al., 2013).
Recent approaches, on the other hand, have used behavioral measures to
objectively determine confirmation bias (e.g., time spent on reading news
articles). In addition, some research employed psycho-physiological signals as
objective measures of confirmation bias, like eye tracking (Marquart et al.,
2016; Sülflow et al., 2019) and electroencephalography (Moravec et al., 2018).

However, we note that research on cognitive bias detection has been limited.
While we have seen some research quantifying confirmation bias, little
attention has been paid to investigate the detection of other cognitive biases
that also help the spread of misinformation. The bandwagon effect, for
example, is a tendency to adapt certain behaviours (e.g., believing a news
piece) because many other people are doing the same. There have been some
research efforts in the context of information retrieval to detect such
phenomena (Harris, 2019); thus, it is promising to see the quantification of
bandwagon effects in the realm of online information consumption.

###  2.2. Profiling Vulnerable Users

Some ongoing research focused on empirical, objective approaches to profiling
potential fake news believers and spreaders by using data mining and machine
learning algorithms on real-world social media data. Shu et al. (2018b)
extracted social media user profiles into explicit features (metadata, for
example, the number of posts and the number of followers) and implicit
features (e.g., age, gender, personality) and used them to infer users who are
prone to believing fake news. Giachanou et al. (2020) combined linguistic and
the Big Five Personality scores in users’ tweets to classify Twitter users who
spread fake news. Karami et al. (2021) developed metrics to measure how likely
a Twitter user will spread false information. Informed by research in
psychology (DiFonzo and Bordia, 2007; Pennycook et al., 2020), they quantified
each user profile based on the five categories of motivational features:
uncertainty, emotions, lack of control, relationship enhancement, and social
rank. Furthermore, this problem led to a collective effort in a challenge at
the PAN at CLEF 2020 workshop111https://pan.webis.de/clef20/pan20-web/ where
several machine learning approaches to detect fake news spreaders were
proposed (Rangel et al., 2020).

##  3\. Future Implications: Designing for Different Vulnerabilities

In this section, we discuss future implications from each of the two presented
approaches to identifying those who are vulnerable to misinformation.

###  3.1. Cognitive Bias Reflection

The ability to detect cognitive biases implies that we can prompt users to
reflect on their susceptibility to misinformation. (or, in the case of
confirmation bias, information that confirms their opinion) Furthermore,
interventions could be employed to address users who are subject to cognitive
biases. On the other hand, we would be able to more accurately place
misinformation interventions on contents that induce users’ cognitive biases.
For instance, interface designers may place a warning message that prompts
users awareness (e.g., ”This content might reinforce your belief” (Rieger et
al., 2021)) or a nudge (e.g., recommending alternative contents to balance out
the viewpoints (Thornhill et al., 2019)) on online contents/posts/tweets that
pose cognitive biases and susceptibility to believe and spread misinformation.

Figure 1. t-SNE visualization of Twitter profiles from the PolitiFact dataset
and GossipCop dataset (Obtained from Karami et al. (2021))

t-SNE visualization of Twitter profiles from the PolitiFact dataset and
GossipCop dataset (Obtained from Karami et al. (2021))

###  3.2. Data-driven Identification of Vulnerable Users

Online behaviour data provide opportunities to model and profile users who may
be more susceptible to misinformation. Data-driven approaches could identify
more features associated with the users’ tendency to spread misinformation
online. Linguistic features, for example, might be able to tell the user’s age
cohort (Nguyen et al., 2013) or political orientation (Pennacchiotti and
Popescu, 2011).

Furthermore, with the abundance of features, we could perform clustering on
the feature vectors of user profiles to explore user groups that are
represented by clusters of data. Based on the t-SNE visualization of user
profiles in Karami et al. (2021) using PolitiFact and GossipCop datasets (Shu
et al., 2018a) (see Figure 1), we may be able to imply that there are some
fake news spreaders who exhibited some similarities with those who did not
share fake news because their data points are closely located on the
representation space. Further investigations would reveal the features of such
user groups and proper intervention methods to address them.

The identified vulnerabilities would also inform the design of misinformation
interventions that is personalised or targeted according to users’ behaviour
on platforms. At the same time, misinformation interventions would be made
more explainable to the users as interventions are attributed by the
vulnerabilities informed by the empirical results.

##  4\. Challenges: Understudied Context

Although approaches exist to detect potential consumers and spreaders
misinformation, there is more avenues for researchers to investigate
vulnerabilities to misinformation. In this section, we discuss two challenges:
visual-based media and instant messaging services. Visual information and
instant messaging are understudied contexts in misinformation research.
Therefore, we argue that more research is needed to address people’s
vulnerabilities to misinformation in the forms of visuals and private
messaging.

###  4.1. Visual-based Media

Visual information (i.e., images and videos) is one of the most prevalent
format of misinformation (Brennen et al., 2021) and it is more likely to
persist in our memory (Defeyter et al., 2009). However, there has been limited
research on visual misinformation (Saltz et al., 2021), including those in the
context of vulnerabilities to believe and disseminate visual misinformation.
In the following, We discuss challenges regarding to the two approaches
presented in this paper.

In the realm of cognitive bias detection, some research investigated
confirmation bias in viewing visual stimuli. Marquart et al. (2016) examined
users’ selective exposure to political advertisement posters via eye-tracking
data. The paper revealed significant effects of political predisposition on
time spent looking political ads. From this paper, we argue that gaze data are
promising means to identify patterns of visual information consumption. Gaze
patterns would reveal how users see, share, and interact with visual
misinformation on visual-based social media platforms, like Instagram, Tiktok,
Youtube, or Snapchat.

Additionally, there has been little research that investigate potential
spreaders of misinformation on visual-based platforms. Yet, Hussein et al.
(2020) investigated YouTube’s personalisation algorithm through search engine
audits and found that, while demographics (i.e., age, gender, and location)
did not affect the amount of misinformation presented, users with watch
history on misinformative topics (e.g., 9/11 or flat earth conspiracies)
tended to be exposed to more of such videos. We suggest that further
investigation is needed to assess the vulnerabilities of conspiracy video
consumers. We also argue that visual-based media pose some challenges for user
profile investigation. One prominent challenge is that the meaning conveyed by
visual information can be highly contextual (Saltz et al., 2021). For example,
one might share a video containing false claims with accurate user corrections
in a caption.

###  4.2. Instant Messaging

Instant messaging (IM) applications (for instance, WhatsApp, WeChat, and
Telegram) are one of the most used services on mobile phones. However, such
services are fertile grounds for the spread of misinformation and propaganda
(Bradshaw and Howard, [n. d.]; Garimella and Eckles, 2020). The role of IM
services on misinformation has been understudied and obtaining real-world data
has been difficult due to its private, encrypted nature.

We argue that cognitive biases exist in the interactions between users and
messages. Users may forward message contents that confirm their beliefs to
other users or chat groups. At the same time, some users may belong in one or
more chat groups, which consist of people of same interests, e.g., liberal or
conservative politics. In such cases, private group chats may be amplification
venues for contents that tell predominantly one side of every story. It is
therefore interesting to see the detection of cognitive biases in IM settings
and interventions that invite users to reflect themselves on, for example,
their information diet.

While there has been some studies that explored motivations in sharing fake
news on IM platforms (Herrero-Diz et al., 2020), there is little or no
research on approaches to objectively identify IM users who may be susceptible
to misinformation. Although data on IM platforms are hardly accessible, it is
encouraging to see many of the psychological aspects (for example, the pace of
communication and emotion expressed as a group) be taken into account when
designing systems that detect potential spreaders of misinformation.

##  5\. Concluding Remarks

Misinformation does its work in deceiving and misinforming users. However, the
question remains how people fall victim of misinformation. Various research
efforts have explored psychological factors involved; furthermore, some
ongoing research have brought these insights into practice. In this position
paper, we discuss two promising approaches to identify people’s
vulnerabilities towards believing and spreading misinformation. Through
cognitive bias detection and user profiling, we explore their implications in
(1) prompting misinformation interventions to effectively address the right
user groups and (2) identifying more vulnerable user cohorts. We also address
existing challenges in identifying users’ vulnerabilities in understudied
contexts like visual-based media and instant messaging services. In the end,
as different users possess different vulnerabilities, we suggest that the
ability to identify vulnerable users would allow interventions to effectively
address the right group of users.

## References

  * (1)
  * Avram et al. (2020) Mihai Avram, Nicholas Micallef, Sameer Patil, and Filippo Menczer. 2020.  Exposure to social engagement metrics increases vulnerability to misinformation.  _Harvard Kennedy School Misinformation Review_ (Jul 2020).  https://doi.org/10.37016/mr-2020-033
  * Bradshaw and Howard ([n. d.]) Samantha Bradshaw and Philip N Howard. [n. d.].  Challenging Truth and Trust: A Global Inventory of Organized Social Media Manipulation.  ([n. d.]), 26.  https://demtech.oii.ox.ac.uk/wp-content/uploads/sites/93/2018/07/ct2018.pdf
  * Brashier and Schacter (2020) Nadia M. Brashier and Daniel L. Schacter. 2020.  Aging in an Era of Fake News.  _Current Directions in Psychological Science_ 29, 3 (2020), 316–323.  https://doi.org/10.1177/0963721420915872 arXiv:https://doi.org/10.1177/0963721420915872  PMID: 32968336.
  * Brennen et al. (2021) J. Scott Brennen, Felix M. Simon, and Rasmus Kleis Nielsen. 2021\.  Beyond (Mis)Representation: Visuals in COVID-19 Misinformation.  _The International Journal of Press/Politics_ 26, 1 (2021), 277–299.  https://doi.org/10.1177/1940161220964780 arXiv:https://doi.org/10.1177/1940161220964780
  * Chen et al. (2015) Xinran Chen, Sei-Ching Joanna Sin, Yin-Leng Theng, and Chei Sian Lee. 2015.  Why Students Share Misinformation on Social Media: Motivation, Gender, and Study-level Differences.  _The Journal of Academic Librarianship_ 41, 5 (2015), 583–592.  https://doi.org/10.1016/j.acalib.2015.07.003
  * Clay et al. (2013) Russ Clay, Jessica M. Barber, and Natalie J. Shook. 2013\.  Techniques for Measuring Selective Exposure: A Critical Review.  _Communication Methods and Measures_ 7, 3-4 (2013), 147–171.  https://doi.org/10.1080/19312458.2013.813925 arXiv:https://doi.org/10.1080/19312458.2013.813925
  * Defeyter et al. (2009) Margaret Anne Defeyter, Riccardo Russo, and Pamela Louise McPartlin. 2009.  The picture superiority effect in recognition memory: A developmental study using the response signal procedure.  _Cognitive Development_ 24, 3 (2009), 265–273.  https://doi.org/10.1016/j.cogdev.2009.05.002
  * DiFonzo and Bordia (2007) Nicholas DiFonzo and Prashant Bordia. 2007.  _Rumor psychology: Social and organizational approaches._ American Psychological Association, Washington, DC, US.  https://doi.org/10.1037/11503-000 Pages: x, 292.
  * Freitas et al. (2013) Julian De Freitas, Brian A Falls, Omar S Haque, and Harold J Bursztajn. 2013.  Vulnerabilities to misinformation in online pharmaceutical marketing.  _Journal of the Royal Society of Medicine_ 106, 5 (2013), 184–189.  https://doi.org/10.1177/0141076813476679 arXiv:https://doi.org/10.1177/0141076813476679  PMID: 23761527.
  * Garimella and Eckles (2020) Kiran Garimella and Dean Eckles. 2020.  Images and Misinformation in Political Groups: Evidence from WhatsApp in India.  arXiv:2005.09784 [cs.SI]
  * Garrett et al. (2013) R. Kelly Garrett, Dustin Carnahan, and Emily K. Lynch. 2013\.  A Turn Toward Avoidance? Selective Exposure to Online Political Information, 2004–2008.  _Political Behavior_ 35, 1 (March 2013), 113–134.  https://doi.org/10.1007/s11109-011-9185-6
  * Geeng et al. (2020) Christine Geeng, Tiona Francisco, Jevin West, and Franziska Roesner. 2020.  Social Media COVID-19 Misinformation Interventions Viewed Positively, But Have Limited Impact.  arXiv:2012.11055 [cs.CY]
  * Giachanou et al. (2020) Anastasia Giachanou, Esteban A. Ríssola, Bilal Ghanem, Fabio Crestani, and Paolo Rosso. 2020\.  The Role of Personality and Linguistic Patterns in Discriminating Between Fake News Spreaders and Fact Checkers. In _Natural Language Processing and Information Systems_ , Elisabeth Métais, Farid Meziane, Helmut Horacek, and Philipp Cimiano (Eds.). Springer International Publishing, Cham, 181–192.
  * Harris (2019) Christopher G. Harris. 2019\.  Detecting Cognitive Bias in a Relevance Assessment Task Using an Eye Tracker. In _Proceedings of the 11th ACM Symposium on Eye Tracking Research & Applications_ (Denver, Colorado) _(ETRA ’19)_. Association for Computing Machinery, New York, NY, USA, Article 36, 5 pages.  https://doi.org/10.1145/3314111.3319824
  * Herrero-Diz et al. (2020) Paula Herrero-Diz, Jesús Conde-Jiménez, and Salvador Reyes de Cózar. 2020\.  Teens’ Motivations to Spread Fake News on WhatsApp.  _Social Media + Society_ 6, 3 (2020), 2056305120942879\.  https://doi.org/10.1177/2056305120942879 arXiv:https://doi.org/10.1177/2056305120942879
  * Hussein et al. (2020) Eslam Hussein, Prerna Juneja, and Tanushree Mitra. 2020\.  Measuring Misinformation in Video Search Platforms: An Audit Study on YouTube.  _Proc. ACM Hum.-Comput. Interact._ 4, CSCW1, Article 048 (may 2020), 27 pages.  https://doi.org/10.1145/3392854
  * Karami et al. (2021) Mansooreh Karami, Tahora H. Nazer, and Huan Liu. 2021\.  Profiling Fake News Spreaders on Social Media through Psychological and Motivational Factors.  _Proceedings of the 32st ACM Conference on Hypertext and Social Media_ (Aug 2021).  https://doi.org/10.1145/3465336.3475097
  * Laato et al. (2020) Samuli Laato, A. K. M. Najmul Islam, Muhammad Nazrul Islam, and Eoin Whelan. 2020.  Why do People Share Misinformation during the COVID-19 Pandemic?  _CoRR_ abs/2004.09600 (2020).  arXiv:2004.09600 https://arxiv.org/abs/2004.09600
  * Lewandowsky et al. (2017) Stephan Lewandowsky, Ullrich K.H. Ecker, and John Cook. 2017\.  Beyond Misinformation: Understanding and Coping with the “Post-Truth” Era.  _Journal of Applied Research in Memory and Cognition_ 6, 4 (2017), 353–369.  https://doi.org/10.1016/j.jarmac.2017.07.008
  * Marquart et al. (2016) Franziska Marquart, Jörg Matthes, and Elisabeth Rapp. 2016\.  Selective Exposure in the Context of Political Advertising: A Behavioral Approach Using Eye-Tracking Methodology.  _International Journal of Communication_ 10 (2016), 20.
  * Martel et al. (2020) Cameron Martel, Gordon Pennycook, and David G. Rand. 2020\.  Reliance on emotion promotes belief in fake news.  _Cognitive Research: Principles and Implications_ 5, 1 (Oct. 2020), 47.  https://doi.org/10.1186/s41235-020-00252-3
  * Moravec et al. (2018) Patricia Moravec, Randall Minas, and Alan R. Dennis. 2018\.  Fake News on Social Media: People Believe What They Want to Believe When it Makes No Sense at All.  _SSRN Electronic Journal_ (2018).  https://doi.org/10.2139/ssrn.3269541
  * Nguyen et al. (2013) Dong Nguyen, Rilana Gravel, Dolf Trieschnigg, and Theo Meder. 2013.  How Old Do You Think I Am? A Study of Language and Age in Twitter.  _Proceedings of the International AAAI Conference on Web and Social Media_ 7, 1 (June 2013), 439–448.  https://ojs.aaai.org/index.php/ICWSM/article/view/14381
  * Nickerson (1998) Raymond S. Nickerson. 1998\.  Confirmation Bias: A Ubiquitous Phenomenon in Many Guises.  _Review of General Psychology_ 2, 2 (1998), 175–220.  https://doi.org/10.1037/1089-2680.2.2.175 arXiv:https://doi.org/10.1037/1089-2680.2.2.175
  * Nikolov et al. (2021) Dimitar Nikolov, Alessandro Flammini, and Filippo Menczer. 2021.  Right and left, partisanship predicts (asymmetric) vulnerability to misinformation.  _Harvard Kennedy School Misinformation Review_ (Feb 2021).  https://doi.org/10.37016/mr-2020-55
  * Pantazi et al. (2021) Myrto Pantazi, Scott Hale, and Olivier Klein. 2021\.  Social and Cognitive Aspects of the Vulnerability to Political Misinformation.  _Political Psychology_ (2021).  https://doi.org/10.1111/pops.12797
  * Pennacchiotti and Popescu (2011) Marco Pennacchiotti and Ana-Maria Popescu. 2011.  A Machine Learning Approach to Twitter User Classification. In _Proceedings of the Fifth International Conference on Weblogs and Social Media, Barcelona, Catalonia, Spain, July 17-21, 2011_ , Lada A. Adamic, Ricardo A. Baeza-Yates, and Scott Counts (Eds.). The AAAI Press.  http://www.aaai.org/ocs/index.php/ICWSM/ICWSM11/paper/view/2886
  * Pennycook et al. (2020) Gordon Pennycook, Jonathon McPhetres, Yunhao Zhang, Jackson G. Lu, and David G. Rand. 2020.  Fighting COVID-19 Misinformation on Social Media: Experimental Evidence for a Scalable Accuracy-Nudge Intervention.  _Psychological Science_ 31, 7 (2020), 770–780.  https://doi.org/10.1177/0956797620939054 arXiv:https://doi.org/10.1177/0956797620939054  PMID: 32603243.
  * Rangel et al. (2020) Francisco Rangel, Anastasia Giachanou, Bilal Hisham Hasan Ghanem, and Paolo Rosso. 2020\.  Overview of the 8th author profiling task at pan 2020: Profiling fake news spreaders on twitter. In _CEUR Workshop Proceedings_ , Vol. 2696. Sun SITE Central Europe, 1–18.  https://riunet.upv.es/handle/10251/166528
  * Rieger et al. (2021) Alisa Rieger, Tim Draws, Mariët Theune, and Nava Tintarev. 2021\.  This Item Might Reinforce Your Opinion: Obfuscation and Labeling of Search Results to Mitigate Confirmation Bias. In _Proceedings of the 32nd ACM Conference on Hypertext and Social Media_ (Virtual Event, USA) _(HT ’21)_. Association for Computing Machinery, New York, NY, USA, 189–199.  https://doi.org/10.1145/3465336.3475101
  * Roozenbeek et al. (2020) Jon Roozenbeek, Claudia R Schneider, Sarah Dryhurst, John Kerr, Alexandra LJ Freeman, Gabriel Recchia, Anne Marthe Van Der Bles, and Sander Van Der Linden. 2020.  Susceptibility to misinformation about COVID-19 around the world.  _Royal Society open science_ 7, 10 (2020).  https://doi.org/10.1098/rsos.201199
  * Saltz et al. (2021) Emily Saltz, Claire R Leibowicz, and Claire Wardle. 2021\.  _Encounters with Visual Misinformation and Labels Across Platforms: An Interview and Diary Study to Inform Ecosystem Approaches to Misinformation Interventions_.  Association for Computing Machinery, New York, NY, USA.  https://doi.org/10.1145/3411763.3451807
  * Shu et al. (2018a) Kai Shu, Deepak Mahudeswaran, Suhang Wang, Dongwon Lee, and Huan Liu. 2018a.  FakeNewsNet: A Data Repository with News Content, Social Context and Dynamic Information for Studying Fake News on Social Media.  _arXiv preprint arXiv:1809.01286_ (2018).
  * Shu et al. (2018b) Kai Shu, Suhang Wang, and Huan Liu. 2018b.  Understanding User Profiles on Social Media for Fake News Detection. In _2018 IEEE Conference on Multimedia Information Processing and Retrieval (MIPR)_. 430–435.  https://doi.org/10.1109/MIPR.2018.00092
  * Simon (1957) Herbert A Simon. 1957\.  A behavioral model of rational choice.  _Models of man, social and rational: Mathematical essays on rational human behavior in a social setting_ (1957), 241–260.
  * Sülflow et al. (2019) Michael Sülflow, Svenja Schäfer, and Stephan Winter. 2019\.  Selective attention in the news feed: An eye-tracking study on the perception and selection of political news posts on Facebook.  _New Media & Society_ 21, 1 (Jan. 2019), 168–190.  https://doi.org/10.1177/1461444818791520
  * Thornhill et al. (2019) Calum Thornhill, Quentin Meeus, Jeroen Peperkamp, and Bettina Berendt. 2019.  A Digital Nudge to Counter Confirmation Bias.  _Frontiers in Big Data_ 2 (2019).  https://doi.org/10.3389/fdata.2019.00011
  * Vosoughi et al. (2018) Soroush Vosoughi, Deb Roy, and Sinan Aral. 2018.  The spread of true and false news online.  _Science_ 359, 6380 (2018), 1146–1151.  https://doi.org/10.1126/science.aap9559
  * Zollo and Quattrociocchi (2018) Fabiana Zollo and Walter Quattrociocchi. 2018.  _Misinformation Spreading on Facebook_.  Springer International Publishing, Cham, 177–196.  https://doi.org/10.1007/978-3-319-77332-2_10