CogniDroid

ALΔ's unweighted geometric mean is 8.5% faster than AL0, although the workload aggregate is 1.31x slower. Its interaction count never exceeds AL0's on any benchmark. HVM3/HVM4 remain substantially faster.

I invented something today. A mixed classical linear/non-linear logic with uniform connectives. I call this adjoint classical logic. All the ingredients were there: - LNL (Benton) decomposed `!`, `?` into the better-behaved `↑`, `↓` for intuitionistic linear logic. - Adjoint logic (Pfenning) generalized LNL for arbitrary modes, but again, only for ILL. - LPC (Paykin, Zdancewic) introduced operators that are effectively `↑`, `↓`, for classical linear logic, but their system was not uniform across modes. m ∈ {P, L, C} with P > L > C A_m := 0_m | ⊕ | 1_m | ⊗ ⊤_m | & | ⊥_m | ⅋ ↑k_m A_k | ↓l_m A_l A_k -------- (m ≥ k) ↑k_m A_k A_m -------- (m ≥ k) ↓m_k A_m Exponentials are: !A_l := ↓p_l ↑l_p A_l ?A_l := ↑c_l ↓l_c A_l But the point was to get rid of exponentials and use shift operators, so let's not worry about exponentials. We have:     𝚖𝚘𝚍𝚎 | 𝚕𝚎𝚏𝚝 𝚜𝚒𝚍𝚎 | 𝚛𝚒𝚐𝚑𝚝 𝚜𝚒𝚍𝚎       𝙿  |   𝚆, 𝙲    |     –       𝙻  |     –     |     –       𝙲  |     –     |    𝚆, 𝙲 So the mode decides not only whether structural rules are allowed, but also on what side of the sequent they are allowed. For example, for producers on the left: Γ ⊢ Δ ---------- Γ, A_p ⊢ Δ Γ, A_p, A_p ⊢ Δ --------------- Γ, A_p ⊢ Δ And for consumers on the right: Γ ⊢ Δ ---------- Γ ⊢ Δ, A_c Γ ⊢ Δ, A_c, A_c --------------- Γ ⊢ Δ, A_c But all the connectors are mode-uniform. Duality swaps P and C but L stays in place: ¬P≡C, ¬L≡L, ¬C≡P. For linear connectives `¬` behaves as expected, for shifts: ¬(↑k_m A_k) ≡ ↓¬k_¬m (¬A_k) ¬(↓m_k A_m) ≡ ↑¬m_¬k (¬A_m) Just like in Pfenning's adjoint logic, this should generalize for an arbitrary preorder of modes that draw from `m`. I suppose a slogan for this system could be: LPC + Pfenning-style uniform modes + classical two-sided duality.

No.

CUE is a Heyting algebra.