fix ADT description

build.gradle.kts

@@ -121,7 +121,7 @@ kotlin {
         // Markovian deps
         implementation("org.jetbrains.kotlinx:kotlinx-coroutines-core:1.8.1")
 
-        implementation("org.jetbrains.lets-plot:platf-awt-jvm:4.3.3")
+        implementation("org.jetbrains.lets-plot:platf-awt-jvm:4.4.0")
         implementation("org.jetbrains.lets-plot:lets-plot-kotlin-jvm:4.7.3")
 
 //  https://arxiv.org/pdf/1908.10693.pdf
@@ -153,7 +153,7 @@ kotlin {
 
         // TODO: Replace LogicNG with KoSAT?
         // https://github.com/UnitTestBot/kosat
-        implementation("org.logicng:logicng:2.5.0")
+        implementation("org.logicng:logicng:2.5.1")
 
         val multikVersion = "0.2.3"
         implementation("org.jetbrains.kotlinx:multik-core:$multikVersion")

latex/popl2025/popl.tex

@@ -1029,7 +1029,7 @@
     L(p) = 1 + p L(p) \phantom{addspace} P(a) = \Sigma + V L\big(V^2P(a)^2\big)
   \end{equation}
 
-  Depicted in Fig.~\ref{fig:ptree} is a partial $\mathbb{T}_2$, where red nodes are \texttt{root}s and blue nodes are \texttt{children}. The shape of type $\mathbb{T}_2$ is congruent with an acyclic CFG in Chomsky Normal Form, i.e., $\mathbb{T}_2\cong\mathcal{G}'$, so assuming the CFG recognizes a finite language, as is the case for $G_\cap'$, then it can be translated directly. Since the RHS of CNF productions must each be nonterminals, we define $P(a)$ as $\Sigma + L\big(V^2P(a)^2\big)$, otherwise, we could write $\Sigma + VL\big(P(a)^2\big)$ to allow productions containing mixed $\Sigma$ and $V$.
+  Depicted in Fig.~\ref{fig:ptree} is a partial $\mathbb{T}_2$, where red nodes are \texttt{root}s and blue nodes are \texttt{children}. The shape of type $\mathbb{T}_2$ is congruent with an acyclic CFG in Chomsky Normal Form, i.e., $\mathbb{T}_2\cong\mathcal{G}'$, so assuming the CFG recognizes a finite language, as is the case for $G_\cap'$, then it can be translated directly. Since the RHS of CNF productions must be nonterminals, we define $P(a)$ as $\Sigma + V L\big(V^2P(a)^2\big)$, otherwise, we could write $\Sigma + VL\big(P(a)^2\big)$ to allow productions containing mixed $\Sigma$ and $V$.
 
   It is also possible to construct $\mathbb{T}_2$ for infinite languages by using the matrix fixpoint technique. If the CFG is cyclic, we can slice the language, $\mathcal{L}(G)\cap \Sigma^n$, and solve the fixpoint for each slice $n \in [2, n]$. Given a porous string $\sigma: \underline\Sigma^n$ representing the slice, we construct $\mathbb{T}_2$ from the bottom-up, and read off structures from the top-down. Here, we define first upper diagonal $\hat\sigma_r = \Lambda(\sigma_r)$ as: