<p>I'm considering employing linear logic (or more specifically, MALL) as the typesystem for my programming language. Recall that linear logic is defined with four binary connectives: Multiplicative conjunction <span class="math-container">$\otimes$</span>, additive disjunction <span class="math-container">$\oplus$</span>, additive conjunction <span class="math-container">$\&amp;$</span>, and multiplicative disjunction <span class="math-container">$⅋$</span>.</p>
<p><span class="math-container">$\otimes$</span> is easy. The type <span class="math-container">$P \otimes Q$</span> consists of pairs of a value typed <span class="math-container">$P$</span> and a value typed <span class="math-container">$Q$</span>. Though, this interpretation has few consequences:</p>
<ul>
<li><p><span class="math-container">$P \otimes Q$</span> cannot be implicitly casted into <span class="math-container">$Q \otimes P$</span>. For consider the type <span class="math-container">$\mathrm{Int} \otimes \mathrm{Int}$</span>. After shuffling the two values involved, we wouldn't be able to know which is which now.</p>
</li>
<li><p>The identity element <span class="math-container">$1$</span> of <span class="math-container">$\otimes$</span> can be safely interpreted as the empty tuple. Furthermore, <span class="math-container">$1$</span> can be treated to have zero size in the memory. As a consequence, <span class="math-container">$P \otimes 1$</span> (and <span class="math-container">$1 \otimes P$</span> also) can be implicitly casted into <span class="math-container">$P$</span>, and vice versa.</p>
</li>
</ul>
<p><span class="math-container">$\oplus$</span> is also easy; it is the union of <span class="math-container">$P$</span> and <span class="math-container">$Q$</span>, using one of the involved types itself as the tag.</p>
<ul>
<li><p>By employing C-esque <code>union</code>, unlike multiplicative conjunction, <span class="math-container">$P \oplus Q$</span> can be implicitly casted into <span class="math-container">$Q \oplus P$</span>.</p>
</li>
<li><p><span class="math-container">$P$</span> (and <span class="math-container">$Q$</span> also) can be implicitly casted into <span class="math-container">$P \oplus Q$</span>. The converse doesn't hold.</p>
</li>
<li><p><span class="math-container">$P \oplus P$</span> can be implicitly casted into <span class="math-container">$P$</span>.</p>
</li>
<li><p>The identity element <span class="math-container">$0$</span> of <span class="math-container">$\oplus$</span> is the uninhabited type. <span class="math-container">$0$</span> can be implicitly casted into an arbitrary type, and every successful production of a value in <span class="math-container">$0$</span> shall result in panicking.</p>
</li>
</ul>
<p><span class="math-container">$\&amp;$</span> is quite harder to be understood. The key feature is that, unlike <span class="math-container">$P \otimes Q$</span>, taking <span class="math-container">$P$</span> from <span class="math-container">$P \&amp; Q$</span> results in dropping the <span class="math-container">$Q$</span>, and taking <span class="math-container">$Q$</span> from <span class="math-container">$P \&amp; Q$</span> results in dropping the <span class="math-container">$P$</span>. So <span class="math-container">$P \&amp; Q$</span> should not be understood as having a distinctive memory model, but should be understood as letting the interpreter decide which type to express.</p>
<ul>
<li><p><span class="math-container">$P \&amp; Q$</span> can be implicitly casted into <span class="math-container">$Q \&amp; P$</span>.</p>
</li>
<li><p><span class="math-container">$P \&amp; Q$</span> can be implicitly casted into <span class="math-container">$P$</span>, or into <span class="math-container">$Q$</span>. The interpreter shall decide which one it shall cast into, or lazily leave it undecided when possible.</p>
</li>
<li><p><span class="math-container">$P$</span> can be implicitly casted into <span class="math-container">$P \&amp; P$</span>.</p>
</li>
<li><p>The identity element <span class="math-container">$\top$</span> of <span class="math-container">$\&amp;$</span> can be understood as a deallocated storage; every type can be implicitly casted into <span class="math-container">$\top$</span>, which shall destroy the involved value.</p>
</li>
</ul>
<p>But what about <span class="math-container">$⅋$</span>? As far as I've understood, the key feature is that, dropping <span class="math-container">$P$</span> from <span class="math-container">$P ⅋ Q$</span> shall result in taking <span class="math-container">$Q$</span>, and dropping <span class="math-container">$Q$</span> from <span class="math-container">$P ⅋ Q$</span> shall result in taking <span class="math-container">$P$</span>. How should its semantics be understood in the perspective of a logic programming language?</p>

<types><type-inference><linear-types>
How is multiplicative disjunction understood in a logic programming language?
CC BY-SA 4.0
2024-07-29T17:39:08.313Z
Here's are interesting question & answers: https://math.stackexchange.com/questions/50340/what-is-the-intuition-behind-the-par-operator-in-linear-logic
Erik Eidt
CC BY-SA 4.0
2024-12-16T05:26:36.983Z
Post-comment: The cast to $\top$ doesn't destroy anything; rather, it leaves the value intact. It only conceals the type.
Dannyu NDos
<p>Multiplicative conjunction is conjunction in the usual logic-programming sense. If the goal is <span class="math-container">$A \otimes B$</span> and the context is <span class="math-container">$C$</span>, the judgement is <span class="math-container">$C \vdash A \otimes B$</span>, and you can decompose this into proving <span class="math-container">$C_1 \vdash A$</span> and then <span class="math-container">$C_2 \vdash B$</span>, where <span class="math-container">$C \cong C_1, C_2$</span>.</p>
<p>To avoid the nondeterminism of choosing how to partition the resources in <span class="math-container">$C$</span>, it’s a typical optimisation in linear logic programming to supply all of <span class="math-container">$C$</span> when trying to produce <span class="math-container">$A$</span>, and consider whatever was consumed to be <span class="math-container">$C_1$</span>; then the remainder <span class="math-container">$C_2$</span> is passed along to try to produce <span class="math-container">$B$</span>.</p>
<p>Additive disjunction is choice in the usual sense. To prove <span class="math-container">$C \vdash A \oplus B$</span>, you can try to prove <span class="math-container">$C \vdash A$</span>, then if that fails (effectively producing 0), backtrack and try to prove <span class="math-container">$C \vdash B$</span>.</p>
<p>Additive conjunction is dual to additive disjunction, so a <em>goal</em> of <span class="math-container">$A \mathbin{\&amp;} B$</span> is equivalent to having <span class="math-container">$A^\bot \oplus B^\bot$</span> in the <em>context</em>. This is also a search, but instead of checking multiple ways to satisfy one goal, it’s checking multiple goals against one context.</p>
<p>You can think of a program in LLP as a duplicable additive conjunction of all the rules: <code>head1 :- body1. … headN :- bodyN.</code> = <span class="math-container">$!((B_1 \multimap H_1) \mathbin{\&amp;} \ldots \mathbin{\&amp;} (B_n \multimap H_n))$</span>. In other words: any number of times, try to apply one of the rules by matching its head against the current goals, and adding its body as a subgoal.</p>
<p>When you have a multiplicative disjunction <span class="math-container">$A \mathbin{⅋} B$</span> as a goal, this is a “fork” where you can start trying to satisfy multiple goals simultaneously. The goals aren’t <em>contradictory</em>, but they are <em>mutually incompatible</em> in the sense that, if you focus on one of them to prove, you still have the obligation to deal with the other one.</p>
<p>One interpretation of the state <span class="math-container">$C \vdash A \mathbin{⅋} B$</span> is as a choice, <span class="math-container">$(C \otimes B^\bot \multimap A) \mathbin{\&amp;} (C \otimes A^\bot \multimap B)$</span>, based on commutativity of <span class="math-container">$⅋$</span>. You would try to prove <span class="math-container">$A$</span> under the assumption that it can produce <span class="math-container">$B$</span> somehow to refute the <span class="math-container">$B^\bot$</span>, and if that fails, you’d try it the other way around.</p>
<p>Another interpretation is to spawn two parallel tasks, where each may produce a result or join the other by sending a message to it and quitting—returning <span class="math-container">$\bot$</span>, which is the unit of <span class="math-container">$⅋$</span>. So an implication <span class="math-container">$A \multimap B$</span> is a parallel pair <span class="math-container">$A^\bot \mathbin{⅋} B$</span> where maybe the <span class="math-container">$A^\bot$</span> side consumes an input and sends it to the <span class="math-container">$B$</span> task to compute a result, or maybe the <span class="math-container">$B$</span> task produces a thunk that, when forced, awaits input from the <span class="math-container">$A$</span> task, but the <span class="math-container">$B$</span> can never be used to compute the <span class="math-container">$A$</span> because the tasks are disjoint.</p>
<p>A few good places to learn more are <a href="https://www.cs.bham.ac.uk/%7Eudr/papers/directional.pdf" rel="nofollow noreferrer">A Typed Foundation for Directional Logic Programming</a><sup>(PDF)</sup> and <a href="http://www.cs.bham.ac.uk/%7Eudr/papers/acceptors.pdf" rel="nofollow noreferrer">Acceptors as Values: Functional Programming in Classical Linear Logic</a><sup>(PDF)</sup> by Uday Reddy, and <a href="https://www.cs.cmu.edu/%7E./fp/courses/15317-s23/" rel="nofollow noreferrer">Frank Pfenning’s lecture notes</a> on linear logic.</p>

CC BY-SA 4.0
2024-07-30T00:36:02.567Z
2024-07-30T02:41:39.730Z
2024-07-30T02:41:39.730Z
Jon Purdy
# How is multiplicative disjunction understood in a logic programming language?
Posted by: username_0 on 2024-07-29
I'm considering employing linear logic (or more specifically, MALL) as the typesystem for my programming language. Recall that linear logic is defined with four binary connectives: Multiplicative conjunction $\otimes$, additive disjunction $\oplus$, additive conjunction $\&$, and multiplicative disjunction $⅋$.

$\otimes$ is easy. The type $P \otimes Q$ consists of pairs of a value typed $P$ and a value typed $Q$. Though, this interpretation has few consequences:

* $P \otimes Q$ cannot be implicitly casted into $Q \otimes P$. For consider the type $\mathrm{Int} \otimes \mathrm{Int}$. After shuffling the two values involved, we wouldn't be able to know which is which now.
* The identity element $1$ of $\otimes$ can be safely interpreted as the empty tuple. Furthermore, $1$ can be treated to have zero size in the memory. As a consequence, $P \otimes 1$ (and $1 \otimes P$ also) can be implicitly casted into $P$, and vice versa.

$\oplus$ is also easy; it is the union of $P$ and $Q$, using one of the involved types itself as the tag.

* By employing C-esque `union`, unlike multiplicative conjunction, $P \oplus Q$ can be implicitly casted into $Q \oplus P$.
* $P$ (and $Q$ also) can be implicitly casted into $P \oplus Q$. The converse doesn't hold.
* $P \oplus P$ can be implicitly casted into $P$.
* The identity element $0$ of $\oplus$ is the uninhabited type. $0$ can be implicitly casted into an arbitrary type, and every successful production of a value in $0$ shall result in panicking.

$\&$ is quite harder to be understood. The key feature is that, unlike $P \otimes Q$, taking $P$ from $P \& Q$ results in dropping the $Q$, and taking $Q$ from $P \& Q$ results in dropping the $P$. So $P \& Q$ should not be understood as having a distinctive memory model, but should be understood as letting the interpreter decide which type to express.

* $P \& Q$ can be implicitly casted into $Q \& P$.
* $P \& Q$ can be implicitly casted into $P$, or into $Q$. The interpreter shall decide which one it shall cast into, or lazily leave it undecided when possible.
* $P$ can be implicitly casted into $P \& P$.
* The identity element $\top$ of $\&$ can be understood as a deallocated storage; every type can be implicitly casted into $\top$, which shall destroy the involved value.

But what about $⅋$? As far as I've understood, the key feature is that, dropping $P$ from $P ⅋ Q$ shall result in taking $Q$, and dropping $Q$ from $P ⅋ Q$ shall result in taking $P$. How should its semantics be understood in the perspective of a logic programming language?
**Tags:** types type-inference linear-types
> **Comments:**
> **username_1**: Here's are interesting question & answers: https://math.stackexchange.com/questions/50340/what-is-the-intuition-behind-the-par-operator-in-linear-logic  
> **username_0**: Post-comment: The cast to $\top$ doesn't destroy anything; rather, it leaves the value intact. It only conceals the type.  
---
## 1 answers
### Answer by username_2 on 2024-07-30. Score: 3 | Accepted answer
Multiplicative conjunction is conjunction in the usual logic-programming sense. If the goal is $A \otimes B$ and the context is $C$, the judgement is $C \vdash A \otimes B$, and you can decompose this into proving $C\_1 \vdash A$ and then $C\_2 \vdash B$, where $C \cong C\_1, C\_2$.

To avoid the nondeterminism of choosing how to partition the resources in $C$, it’s a typical optimisation in linear logic programming to supply all of $C$ when trying to produce $A$, and consider whatever was consumed to be $C\_1$; then the remainder $C\_2$ is passed along to try to produce $B$.

Additive disjunction is choice in the usual sense. To prove $C \vdash A \oplus B$, you can try to prove $C \vdash A$, then if that fails (effectively producing 0), backtrack and try to prove $C \vdash B$.

Additive conjunction is dual to additive disjunction, so a *goal* of $A \mathbin{\&} B$ is equivalent to having $A^\bot \oplus B^\bot$ in the *context*. This is also a search, but instead of checking multiple ways to satisfy one goal, it’s checking multiple goals against one context.

You can think of a program in LLP as a duplicable additive conjunction of all the rules: `head1 :- body1. … headN :- bodyN.` = $!((B\_1 \multimap H\_1) \mathbin{\&} \ldots \mathbin{\&} (B\_n \multimap H\_n))$. In other words: any number of times, try to apply one of the rules by matching its head against the current goals, and adding its body as a subgoal.

When you have a multiplicative disjunction $A \mathbin{⅋} B$ as a goal, this is a “fork” where you can start trying to satisfy multiple goals simultaneously. The goals aren’t *contradictory*, but they are *mutually incompatible* in the sense that, if you focus on one of them to prove, you still have the obligation to deal with the other one.

One interpretation of the state $C \vdash A \mathbin{⅋} B$ is as a choice, $(C \otimes B^\bot \multimap A) \mathbin{\&} (C \otimes A^\bot \multimap B)$, based on commutativity of $⅋$. You would try to prove $A$ under the assumption that it can produce $B$ somehow to refute the $B^\bot$, and if that fails, you’d try it the other way around.

Another interpretation is to spawn two parallel tasks, where each may produce a result or join the other by sending a message to it and quitting—returning $\bot$, which is the unit of $⅋$. So an implication $A \multimap B$ is a parallel pair $A^\bot \mathbin{⅋} B$ where maybe the $A^\bot$ side consumes an input and sends it to the $B$ task to compute a result, or maybe the $B$ task produces a thunk that, when forced, awaits input from the $A$ task, but the $B$ can never be used to compute the $A$ because the tasks are disjoint.

A few good places to learn more are [A Typed Foundation for Directional Logic Programming](https://www.cs.bham.ac.uk/%7Eudr/papers/directional.pdf)(PDF) and [Acceptors as Values: Functional Programming in Classical Linear Logic](http://www.cs.bham.ac.uk/%7Eudr/papers/acceptors.pdf)(PDF) by Uday Reddy, and [Frank Pfenning’s lecture notes](https://www.cs.cmu.edu/%7E./fp/courses/15317-s23/) on linear logic.
---
