diff --git a/build.gradle.kts b/build.gradle.kts index e1a29507..7c882212 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -140,6 +140,7 @@ kotlin { // implementation(files("$projectDir/libs/mpj-0.44.jar")) implementation(files("$projectDir/jautomata-0.0.1-SNAPSHOT.jar")) + implementation("dk.brics:automaton:1.12-4") implementation("org.sosy-lab:common:0.3000-529-g6152d88") implementation("org.sosy-lab:java-smt:4.1.1") diff --git a/latex/popl2025/popl.pdf b/latex/popl2025/popl.pdf index 2001a9b9..08a1442a 100644 Binary files a/latex/popl2025/popl.pdf and b/latex/popl2025/popl.pdf differ diff --git a/latex/popl2025/popl.tex b/latex/popl2025/popl.tex index cd77599f..21b38d73 100644 --- a/latex/popl2025/popl.tex +++ b/latex/popl2025/popl.tex @@ -937,120 +937,119 @@ Constructively, let $+, *: \mathcal{M}\times \mathcal{M} \rightarrow \mathcal{M}$ be the automata operators corresponding to language union and concatenation satisfying $\mathcal{L}(A_1 + A_2) = \mathcal{L}(A_1)\cup\mathcal{L}(A_2)$, and $\mathcal{L}(A_1 * A_2) = \mathcal{L}(A_1)\times\mathcal{L}(A_2)$. This can be implemented using the standard textbook construction, recalling that NFA are closed under these operations. $\Lambda^* \circ S$ would then yield an NFA recognizing $\Sigma^n\cap\mathcal{L}(G)$, which can be determinized and decoded using k-best paths to obtain the top-k maximum likelihood repairs. - - \definecolor{R}{RGB}{202,65,55} - \definecolor{G}{RGB}{151,216,56} - \definecolor{W}{RGB}{255,255,255} - \definecolor{X}{RGB}{65,65,65} - - \newcommand{\TikZRubikFaceLeft}[9]{\def\myarrayL{#1,#2,#3,#4,#5,#6,#7,#8,#9}} - \newcommand{\TikZRubikFaceRight}[9]{\def\myarrayR{#1,#2,#3,#4,#5,#6,#7,#8,#9}} - \newcommand{\TikZRubikFaceTop}[9]{\def\myarrayT{#1,#2,#3,#4,#5,#6,#7,#8,#9}} - \newcommand{\BuildArray}{\foreach \X [count=\Y] in \myarrayL% - {\ifnum\Y=1% - \xdef\myarray{"\X"}% - \else% - \xdef\myarray{\myarray,"\X"}% - \fi}% - \foreach \X in \myarrayR% - {\xdef\myarray{\myarray,"\X"}}% - \foreach \X in \myarrayT% - {\xdef\myarray{\myarray,"\X"}}% - \xdef\myarray{{\myarray}}% - } - \TikZRubikFaceLeft - {LA}{W}{W} - {W}{LB}{LC} - {LD}{W}{W} - \TikZRubikFaceRight - {W}{LK}{W} - {LC}{W}{LG} - {W}{LH}{W} - \TikZRubikFaceTop - {LA}{W}{LI} - {W}{W}{LJ} - {W}{LK}{W} - \BuildArray - \pgfmathsetmacro\radius{0.1} - \tdplotsetmaincoords{55}{135} - - \showcellnumberfalse - - \bgroup - \newcommand\ddd{\Ddots} - \newcommand\vdd{\Vdots} - \newcommand\cdd{\Cdots} - \newcommand\lds{\ldots} - \newcommand\vno{\varnothing} - \newcommand{\ts}[1]{\textsuperscript{#1}} - \newcommand\non{1\ts{st}} - \newcommand\ntw{2\ts{nd}} - \newcommand\nth{3\ts{rd}} - \newcommand\nfo{4\ts{th}} - \newcommand\nfi{5\ts{th}} - \newcommand\nsi{6\ts{th}} - \newcommand\nse{7\ts{th}} - \newcommand{\vs}[1]{\shup\sigma_{#1}} - \newcommand\rcr{\rowcolor{black!15}} - \newcommand\rcw{\rowcolor{white}} - \newcommand\pcd{\cdot} - \newcommand\pcp{\phantom\cdot} - \newcommand\ppp{\phantom{\nse}} - - \begin{wrapfigure}{r}{0.32\textwidth} - \vspace{-0.5cm} - \begin{minipage}[r]{4cm} - \begin{align*} - o &\rightarrow \hiliD{so} \mid \hiliC{rs} \mid \hiliB{rr}\hspace{0.5pt} \mid \hiliA{oo}\\ - r &\rightarrow \hiliE{so} \mid \hiliH{ss}\hspace{0.4pt}\mid \hiliF{rr}\hspace{0.5pt} \mid \hiliK{os}\\ - s &\rightarrow \hiliL{so} \mid \hiliG{rs} \mid \hiliJ{or} \mid \hiliI{oo} - \end{align*} - \end{minipage} -% \mathcal{J} = \begin{pmatrix} -% \pder{o}{o} & \pder{o}{r} & \pder{o}{s}\\ -% \pder{r}{o} & \pder{r}{r} & \pder{r}{s}\\ -% \pder{s}{o} & \pder{s}{r} & \pder{s}{s} -% \end{pmatrix} - \hspace{-0.1cm}\begin{minipage}[r]{4cm} - \scalebox{0.8}{\begin{tikzpicture} - \clip (-3,-2.5) rectangle (3,2.5); - \begin{scope}[tdplot_main_coords] - \filldraw [canvas is yz plane at x=1.5] (-1.5,-1.5) rectangle (1.5,1.5); - \filldraw [canvas is xz plane at y=1.5] (-1.5,-1.5) rectangle (1.5,1.5); - \filldraw [canvas is yx plane at z=1.5] (-1.5,-1.5) rectangle (1.5,1.5); - \foreach \X [count=\XX starting from 0] in {-1.5,-0.5,0.5}{ - \foreach \Y [count=\YY starting from 0] in {-1.5,-0.5,0.5}{ - \pgfmathtruncatemacro{\Z}{\XX+3*(2-\YY)} - \pgfmathsetmacro{\mycolor}{\myarray[\Z]} - \draw [thick,canvas is yz plane at x=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle; - \ifshowcellnumber - \node[canvas is yz plane at x=1.5,shift={(\X+0.5,\Y+0.5)}] {\Z}; - \fi - \pgfmathtruncatemacro{\Z}{2-\XX+3*(2-\YY)+9} - \pgfmathsetmacro{\mycolor}{\myarray[\Z]} - \draw [thick,canvas is xz plane at y=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle; - \ifshowcellnumber - \node[canvas is xz plane at y=1.5,shift={(\X+0.5,\Y+0.5)},xscale=-1] {\Z}; - \fi - \pgfmathtruncatemacro{\Z}{2-\YY+3*\XX+18} - \pgfmathsetmacro{\mycolor}{\myarray[\Z]} - \draw [thick,canvas is yx plane at z=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle; - \ifshowcellnumber - \node[canvas is yx plane at z=1.5,shift={(\X+0.5,\Y+0.5)},xscale=-1,rotate=-90] {\Z}; - \fi - } - } - \draw [decorate,decoration={calligraphic brace,amplitude=10pt,mirror},yshift=0pt, line width=1.25pt] - (3,0) -- (3,3) node [black,midway,xshift=-8pt, yshift=-14pt] {\footnotesize $V_x$}; - \draw [decorate,decoration={calligraphic brace,amplitude=10pt},yshift=0pt, line width=1.25pt] - (3,0) -- (0,-3) node [black,midway,xshift=-16pt, yshift=0pt] {\footnotesize $V_z$}; - \draw [decorate,decoration={calligraphic brace,amplitude=10pt},yshift=0pt, line width=1.25pt] - (0,-3) -- (-3,-3) node [black,midway,xshift=-8pt, yshift=14pt] {\footnotesize $V_w$}; - \end{scope} - \end{tikzpicture}} - \end{minipage} - \caption{CFGs are hypergraphs witnessed by a rank-3 tensor, whose nonempty inhabitants indicate CNF productions.\vspace{-10pt}} - \end{wrapfigure} +% \definecolor{R}{RGB}{202,65,55} +% \definecolor{G}{RGB}{151,216,56} +% \definecolor{W}{RGB}{255,255,255} +% \definecolor{X}{RGB}{65,65,65} +% +% \newcommand{\TikZRubikFaceLeft}[9]{\def\myarrayL{#1,#2,#3,#4,#5,#6,#7,#8,#9}} +% \newcommand{\TikZRubikFaceRight}[9]{\def\myarrayR{#1,#2,#3,#4,#5,#6,#7,#8,#9}} +% \newcommand{\TikZRubikFaceTop}[9]{\def\myarrayT{#1,#2,#3,#4,#5,#6,#7,#8,#9}} +% \newcommand{\BuildArray}{\foreach \X [count=\Y] in \myarrayL% +% {\ifnum\Y=1% +% \xdef\myarray{"\X"}% +% \else% +% \xdef\myarray{\myarray,"\X"}% +% \fi}% +% \foreach \X in \myarrayR% +% {\xdef\myarray{\myarray,"\X"}}% +% \foreach \X in \myarrayT% +% {\xdef\myarray{\myarray,"\X"}}% +% \xdef\myarray{{\myarray}}% +% } +% \TikZRubikFaceLeft +% {LA}{W}{W} +% {W}{LB}{LC} +% {LD}{W}{W} +% \TikZRubikFaceRight +% {W}{LK}{W} +% {LC}{W}{LG} +% {W}{LH}{W} +% \TikZRubikFaceTop +% {LA}{W}{LI} +% {W}{W}{LJ} +% {W}{LK}{W} +% \BuildArray +% \pgfmathsetmacro\radius{0.1} +% \tdplotsetmaincoords{55}{135} +% +% \showcellnumberfalse +% +% \bgroup +% \newcommand\ddd{\Ddots} +% \newcommand\vdd{\Vdots} +% \newcommand\cdd{\Cdots} +% \newcommand\lds{\ldots} +% \newcommand\vno{\varnothing} +% \newcommand{\ts}[1]{\textsuperscript{#1}} +% \newcommand\non{1\ts{st}} +% \newcommand\ntw{2\ts{nd}} +% \newcommand\nth{3\ts{rd}} +% \newcommand\nfo{4\ts{th}} +% \newcommand\nfi{5\ts{th}} +% \newcommand\nsi{6\ts{th}} +% \newcommand\nse{7\ts{th}} +% \newcommand{\vs}[1]{\shup\sigma_{#1}} +% \newcommand\rcr{\rowcolor{black!15}} +% \newcommand\rcw{\rowcolor{white}} +% \newcommand\pcd{\cdot} +% \newcommand\pcp{\phantom\cdot} +% \newcommand\ppp{\phantom{\nse}} +% +% \begin{wrapfigure}{r}{0.32\textwidth} +% \vspace{-0.5cm} +% \begin{minipage}[r]{4cm} +% \begin{align*} +% o &\rightarrow \hiliD{so} \mid \hiliC{rs} \mid \hiliB{rr}\hspace{0.5pt} \mid \hiliA{oo}\\ +% r &\rightarrow \hiliE{so} \mid \hiliH{ss}\hspace{0.4pt}\mid \hiliF{rr}\hspace{0.5pt} \mid \hiliK{os}\\ +% s &\rightarrow \hiliL{so} \mid \hiliG{rs} \mid \hiliJ{or} \mid \hiliI{oo} +% \end{align*} +% \end{minipage} +%% \mathcal{J} = \begin{pmatrix} +%% \pder{o}{o} & \pder{o}{r} & \pder{o}{s}\\ +%% \pder{r}{o} & \pder{r}{r} & \pder{r}{s}\\ +%% \pder{s}{o} & \pder{s}{r} & \pder{s}{s} +%% \end{pmatrix} +% \hspace{-0.1cm}\begin{minipage}[r]{4cm} +% \scalebox{0.8}{\begin{tikzpicture} +% \clip (-3,-2.5) rectangle (3,2.5); +% \begin{scope}[tdplot_main_coords] +% \filldraw [canvas is yz plane at x=1.5] (-1.5,-1.5) rectangle (1.5,1.5); +% \filldraw [canvas is xz plane at y=1.5] (-1.5,-1.5) rectangle (1.5,1.5); +% \filldraw [canvas is yx plane at z=1.5] (-1.5,-1.5) rectangle (1.5,1.5); +% \foreach \X [count=\XX starting from 0] in {-1.5,-0.5,0.5}{ +% \foreach \Y [count=\YY starting from 0] in {-1.5,-0.5,0.5}{ +% \pgfmathtruncatemacro{\Z}{\XX+3*(2-\YY)} +% \pgfmathsetmacro{\mycolor}{\myarray[\Z]} +% \draw [thick,canvas is yz plane at x=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle; +% \ifshowcellnumber +% \node[canvas is yz plane at x=1.5,shift={(\X+0.5,\Y+0.5)}] {\Z}; +% \fi +% \pgfmathtruncatemacro{\Z}{2-\XX+3*(2-\YY)+9} +% \pgfmathsetmacro{\mycolor}{\myarray[\Z]} +% \draw [thick,canvas is xz plane at y=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle; +% \ifshowcellnumber +% \node[canvas is xz plane at y=1.5,shift={(\X+0.5,\Y+0.5)},xscale=-1] {\Z}; +% \fi +% \pgfmathtruncatemacro{\Z}{2-\YY+3*\XX+18} +% \pgfmathsetmacro{\mycolor}{\myarray[\Z]} +% \draw [thick,canvas is yx plane at z=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle; +% \ifshowcellnumber +% \node[canvas is yx plane at z=1.5,shift={(\X+0.5,\Y+0.5)},xscale=-1,rotate=-90] {\Z}; +% \fi +% } +% } +% \draw [decorate,decoration={calligraphic brace,amplitude=10pt,mirror},yshift=0pt, line width=1.25pt] +% (3,0) -- (3,3) node [black,midway,xshift=-8pt, yshift=-14pt] {\footnotesize $V_x$}; +% \draw [decorate,decoration={calligraphic brace,amplitude=10pt},yshift=0pt, line width=1.25pt] +% (3,0) -- (0,-3) node [black,midway,xshift=-16pt, yshift=0pt] {\footnotesize $V_z$}; +% \draw [decorate,decoration={calligraphic brace,amplitude=10pt},yshift=0pt, line width=1.25pt] +% (0,-3) -- (-3,-3) node [black,midway,xshift=-8pt, yshift=14pt] {\footnotesize $V_w$}; +% \end{scope} +% \end{tikzpicture}} +% \end{minipage} +% \caption{CFGs are hypergraphs witnessed by a rank-3 tensor, whose nonempty inhabitants indicate CNF productions.\vspace{-10pt}} +% \end{wrapfigure} In the distributional setting, suppose we have a PCFG, $G$, such that $|\mathcal{L}(G)|<\infty$. This induces a distribution $F_G: \mathcal{L}(G) \rightarrow \mathbb{R}$ which can be bisimulated by a weighted automaton (WA), $A$, where $F_A: \mathcal{L}(A) \rightarrow \mathbb{R}$ such that $F_G \sim F_A$, i.e., sampling paths through $A$ yields members of $\mathcal{L}(G)$ equal probability as sampling the PCFG from the top, down. A key issue with this approach is that $|P_G| \ll |\delta_A|$ for bisimilar $G, A$, and renormalizing the transition weights can be computationally infeasible for large $\delta_A$. diff --git a/src/jvmTest/kotlin/ai/hypergraph/kaliningraph/automata/WFSATest.kt b/src/jvmTest/kotlin/ai/hypergraph/kaliningraph/automata/WFSATest.kt index 18a85e0f..be203bd4 100644 --- a/src/jvmTest/kotlin/ai/hypergraph/kaliningraph/automata/WFSATest.kt +++ b/src/jvmTest/kotlin/ai/hypergraph/kaliningraph/automata/WFSATest.kt @@ -4,22 +4,27 @@ import Grammars import Grammars.shortS2PParikhMap import ai.hypergraph.kaliningraph.graphs.LabeledGraph import ai.hypergraph.kaliningraph.parsing.* +import ai.hypergraph.kaliningraph.visualization.alsoCopy import ai.hypergraph.markovian.mcmc.MarkovChain import net.jhoogland.jautomata.* import net.jhoogland.jautomata.Automaton import net.jhoogland.jautomata.operations.* import net.jhoogland.jautomata.semirings.RealSemiring +import kotlin.random.Random import kotlin.test.* -import kotlin.time.measureTimedValue +import kotlin.time.* +typealias BAutomaton = dk.brics.automaton.Automaton +typealias JAutomaton = Automaton class WFSATest { + /* ./gradlew jvmTest --tests "ai.hypergraph.kaliningraph.automata.WFSATest.testWFSA" */ @Test fun testWFSA() { - val a: Automaton = + val a: JAutomaton = EditableAutomaton(RealSemiring()).apply { val s1: Int = addState(1.0, 0.0) // Create initial state (initial weight 1.0, final weight 0.0) val s2: Int = addState(0.0, 1.0) // Create final state (initial weight 0.0, final weight 1.0) @@ -34,7 +39,22 @@ class WFSATest { .also { println("Took ${it.duration} to decode ${it.value.size} best strings") } } - fun Automaton.toDot(processed: MutableSet = mutableSetOf()) = +/* + ./gradlew jvmTest --tests "ai.hypergraph.kaliningraph.automata.WFSATest.testBRICS" +*/ + @Test + fun testBRICS() { + val ab = BAutomaton.makeString("a").concatenate(BAutomaton.makeString("b")) + val aa = BAutomaton.makeString("a").concatenate(BAutomaton.makeString("a")) + val a = ab.union(aa) + val ag = List(6) { a }.fold(a) { acc, automaton -> acc.concatenate(automaton) } + + println(ag.getFiniteStrings(-1)) + println() + println(BAutomaton.minimize(ag.also { it.determinize() }).toDot()) + } + + fun JAutomaton.toDot(processed: MutableSet = mutableSetOf()) = LabeledGraph { val stateQueue = mutableListOf() initialStates().forEach { stateQueue.add(it) } @@ -70,7 +90,7 @@ class WFSATest { * previous n-1 transitions, i.e., q' ~ argmax_{q'} P(q' | q_{t-1}, ..., q_{t-n+1}) */ - fun Automaton.randomWalk(mc: MarkovChain, topK: Int = 1000): Sequence { + fun JAutomaton.randomWalk(mc: MarkovChain, topK: Int = 1000): Sequence { val init = initialStates().first() val padding = List(mc.memory - 1) { null } val ts = transitionsOut(init).map { (it as BasicTransition).label() }.map { it to mc.score(padding + it) } @@ -85,27 +105,48 @@ class WFSATest { val toRepair = "NAME : NEWLINE NAME = STRING NEWLINE NAME = NAME . NAME ( STRING ) NEWLINE" val radius = 2 val pt = Grammars.seq2parsePythonCFG.makeLevPTree(toRepair, radius, shortS2PParikhMap) + fun Char.toUnicodeEscaped() = "\\u${code.toString(16).padStart(4, '0')}" + + val ctbl = Grammars.seq2parsePythonCFG.terminals.associateBy { Random(it.hashCode()).nextInt().toChar() } + val stbl = Grammars.seq2parsePythonCFG.terminals.associateBy { Random(it.hashCode()).nextInt().toChar().toUnicodeEscaped() } + fun Σᐩ.replaceAll(tbl: Map) = tbl.entries.fold(this) { acc, (k, v) -> acc.replace(k, v) } + println("Total trees: " + pt.totalTrees.toString()) val maxResults = 10_000 val ptreeRepairs = measureTimedValue { pt.sampleStrWithoutReplacement().distinct().take(maxResults).toSet() } measureTimedValue { - pt.propagator>( - both = { a, b -> if (a == null) b else if (b == null) a else Concatenation(a, b) }, - either = { a, b -> if (a == null) b else if (b == null) a else Union(a, b) }, + pt.propagator( + both = { a, b -> if (a == null) b else if (b == null) a else a.concatenate(b) }, + either = { a, b -> if (a == null) b else if (b == null) a else a.union(b) }, unit = { a -> if ("ε" in a.root) null - else EditableAutomaton(RealSemiring()).apply { - val s1 = addState(1.0, 0.0) - val s2 = addState(0.0, 1.0) - addTransition(s1, s2, a.root, 1.0) - } + else BAutomaton.makeChar(Random(a.root.hashCode()).nextInt().toChar()) +// EditableAutomaton(RealSemiring()).apply { +// val s1 = addState(1.0, 0.0) +// val s2 = addState(0.0, 1.0) +// addTransition(s1, s2, a.root, 1.0) +// } } ) // ?.also { println("\n" + Operations.determinizeER(it).toDot().alsoCopy() + "\n") } // .also { println("Total: ${Automata.transitions(it).size} arcs, ${Automata.states(it).size}") } - .let { Automata.bestStrings(it, maxResults).map { it.label.joinToString(" ") }.toSet() } +// .let { WAutomata.bestStrings(it, maxResults).map { it.label.joinToString(" ") }.toSet() } + ?.also { println("Original automata had ${it + .let { "${it.numberOfStates} states and ${it.numberOfTransitions} transitions"}}") } + ?.also { + measureTimedValue { BAutomaton.minimize(it) } + .also { println("Minimization took ${it.duration}") }.value +// .also { it.toDot().replaceAll(stbl).alsoCopy() } + .also { + // Minimal automata had 92 states and 707 transitions + println("Minimal automata had ${ + it.let { "${it.numberOfStates} states and ${it.numberOfTransitions} transitions" } + }") + } + } + .let { it?.getFiniteStrings(-1) ?: emptySet() } }.also { // // Print side by side comparison of repairs // repairs.sorted().forEach { @@ -117,7 +158,7 @@ class WFSATest { // } assertEquals(it.value.size, ptreeRepairs.value.size) - it.value.forEach { + it.value.map { it.map { ctbl[it] }.joinToString(" ") }.forEach { // println(levenshteinAlign(toRepair, it).paintANSIColors()) assertTrue(levenshtein(toRepair, it) <= radius) assertTrue(it in Grammars.seq2parsePythonCFG.language)