frame-automata.tex

% SPDX-License-Identifier: CC-BY-4.0
% Copyright 2018 Toni Dietze
\documentclass[beamer]{standalone}
\input{preamble.tex}
\begin{document}
%         1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7
\timeline{+ + + + + + + + + + + + + + + - -}{tlFSAandTA}
\timeline{- - - - - - - + + + + + + + + + +}{tlTAandUTA}
\timeline{+ + + + + + + + - - - - - - - - -}{tlString}
\timeline{+ + + + + + + - - - - - - - - - -}{tlFSA}
\timeline{- + + + + + + - - - - - - - - - -}{fsaRunA}
\timeline{- - + + + + + - - - - - - - - - -}{fsaRunB}
\timeline{- - - + + + + - - - - - - - - - -}{fsaRunC}
\timeline{- - - - + + + - - - - - - - - - -}{fsaRunD}
\timeline{- - - - - + + - - - - - - - - - -}{fsaRunE}
\timeline{- - - - - - + - - - - - - - - - -}{fsaRunF}
\timeline{- - - - - - - + - - - - - - - - -}{tlRaise}
\timeline{- - - - - - - + + + + + + + + - -}{tlTA}
\timeline{- - - - - - - - + + + + + + + - -}{tlTAb}
\timeline{- - - - - - - - + - - - - - - - -}{tlTreeA}
\timeline{- - - - - - - - - + + + + + + + -}{tlTreeB}
\timeline{- - - - - - - - - - - - - - - - +}{tlTreeC}
\timeline{- - - - - - - - - - - - - - - + +}{tlUTA}
\timeline{- - - - - - - - - - - - - - - + -}{tlUTAa}
\timeline{- - - - - - - - - - + + + + - - -}{tlFormalDefs}
\timeline{- - - - - - - - - - + - - - - - -}{tlFormalTA}
\timeline{- - - - - - - - - - - + - - - - -}{tlFormalWTA}
\timeline{- - - - - - - - - - - - + - - - -}{tlRunWeighted}
\timeline{- - - - - - - - - - - - - + - - -}{tlDefProbabilistic}
\timeline{- - - - - - - - - - - + + + - - -}{tlWeights}
\begin{standaloneframe}[t]{\jobname}
\begin{columns}[T]
\column{0.45\linewidth}
	\only<\tlFSA>{%
		\begin{tikzpicture}[x=1em, y=1em, overlay, shift={(4em, -15em)}]
			\node[state] (1) at (0, 0) {\(\nt{A}\)};
			\node[state] (2) at (6, 0) {\(\nt{B}\)};
			\draw[<-] (1) -- ++(-3,  0);
			\draw[->] (1) edge[out= 60, in=120] node[above] {\(a\)} (2);
			\draw[->] (2) edge[out=240, in=300] node[below] {\(b\)} (1);
			\draw[->] (2) -- ++(3, 0);
		\end{tikzpicture}%
	}%
	\only<\tlTA>{%
		\begin{tikzpicture}[x=1em, y=1em, overlay, shift={(4em, -15em)}]
			\node[state] (1) at ( 0,  0) {\(\nt{A}\)};
			\node[state] (2) at ( 6,  0) {\(\nt{B}\)};
			\node[trans] (a) at ( 3,  2) {};
			\node[trans] (b) at ( 3, -2) {};
			\node[trans] (f) at ( 9,  0) {};
			\node[above=0 of a] {\(a\)};
			\node[below=0 of b] {\(b\)};
			\node[above=0 of f] {\(⊥\)};
			\draw[<-] (1) -- ++(-3,  0);
			\draw     (1) edge[out= 60, in=180] (a);
			\draw[->] (a) edge[out=  0, in=120] (2);
			\draw<\tlTAb>
			     [->] (a) edge[bend right] (2);
			\draw     (2) edge[out=240, in=  0] (b);
			\draw[->] (b) edge[out=180, in=300] (1);
			\draw     (2) -- (f);
		\end{tikzpicture}%
	}%
	\setlength\abovedisplayskip{0pt}%
	\begin{align*}
		\oalt<\tlFSA>[r]%
			{\text{initial: }}%
			{\oalt[r]<\tlFormalDefs>%
				{\oalt[r]<\tlFormalTA>%
					{I\colon}%
					{ι\colon}%
				}%
				{\text{root: }}%
			}%
		\nt{A}
		&&& \only<\tlWeights>{\hspace{-4em} ↦ 1}
	\\[1em]
		\oalt[r]<\tlFormalDefs>%
			{\oalt[r]<\tlFormalTA>%
				{Δ\colon}%
				{δ\colon}%
			}%
			{\text{trans.: }}
		\nt{A} & \xrightarrow{\invisible<\tlFormalDefs>{a}}
			\otemporal<\tlUTAa>[l]%
			{\oalt<\tlTAb>[l]%
				{\oalt<\tlFormalDefs>[l]%
					{a(\nt{B}, \nt{B})}%
					{\nt{B}\,\nt{B}}%
				}%
				{\nt{B}}%
			}%
			{\tikz[baseline = (current bounding box.center)]{\node[draw, rounded corners]{\tikz{
				\node[state, inner sep = 0.2em] (p0) at (  0, 0) {};
				\node[state, inner sep = 0.2em] (p1) at (2em, 0) {};
				\node[state, inner sep = 0.2em] (p2) at (4em, 0) {};
				\draw[<-] (p0) -- ++(-1em, 0);
				\draw[->] (p2) -- ++( 1em, 0);
				\draw[->] (p0) -- node[above, tight] {\(\nt{B}\)} (p1);
				\draw[->] (p1) -- node[above, tight] {\(\nt{B}\)} (p2);
			}};}}%
			{\tikz[baseline = (current bounding box.center)]{\node[draw, rounded corners]{\tikz{
				\node[state, inner sep = 0.2em] (p) {};
				\draw[<-] (p) -- ++(-1em, 0);
				\draw[->] (p) -- ++( 1em, 0);
				\draw[->] (p) edge[loop above] node[right, tight] {\(\nt{B}\)} ();
			}};}}
		&& \only<\tlWeights>{\hspace{-4em} ↦ 1}
	\\
		\nt{B} & \xrightarrow{\invisible<\tlFormalDefs>{b}}
			\oalt<\tlFSAandTA>[l]%
			{\oalt<\tlFormalDefs>[l]%
				{b(\nt{A})}%
				{\nt{A}}%
			}%
			{\tikz[baseline = (current bounding box.center)]{\node[draw, rounded corners]{\tikz{
				\node[state, inner sep = 0.2em] (p1) {};
				\node[state, inner sep = 0.2em] (p2) at (2em, 0) {};
				\draw[<-] (p1) -- ++(-1em, 0);
				\draw[->] (p2) -- ++( 1em, 0);
				\draw[->] (p1) -- (p2) node[midway, above, tight] {\(\nt{A}\)};
			}};}}
		&& \only<\tlWeights>{\hspace{-4em} ↦ 0.5}
	\\
		\visible<\tlFSA>{\text{final: }} \nt{B}
	&
		\visible<\tlTAandUTA>{\xrightarrow{\invisible<\tlFormalDefs>{⊥}}
			\oalt<\tlTA>[l]%
			{\oalt<\tlFormalDefs>[l]%
				{⊥()}%
				{ε}%
			}%
			{\tikz[baseline = (current bounding box.center)]{\node[draw, rounded corners]{\tikz{
				\node[state, inner sep = 0.2em] (p) {};
				\draw[<-] (p) -- ++(-1em, 0);
				\draw[->] (p) -- ++( 1em, 0);
			}};}}
		&& \only<\tlWeights>{\hspace{-4em} ↦ 0.5}
		}
	\end{align*}
\column{0.55\linewidth}
	\alt<\tlFormalDefs>{%
		\only<\tlFormalTA>{%
			\begin{block}{tree automaton (ta)}
				tuple \(\mathscr{A} = (Q, Σ, I, Δ)\) where
				\begin{itemize}
				\item
					\(Q\) alphabet \hfill (\emph{states})
				\item
					\(Σ\) ranked alphabet \hfill (\emph{terminals})
				\item
					\(I ⊆ Q\) alphabet \hfill (\emph{root states})
				\item
					\(Δ\) is a finite set of \emph{transitions} of form \(A_0 → σ(A_1, \dots, A_k)\) where \(k ∈ ℕ\), \(σ ∈ Σ^{(k)}\), \(A_i ∈ Q\).
				\end{itemize}
			\end{block}
		}%
		\only<\tlFormalWTA>{%
			\begin{block}{weighted tree automaton (wta)}
				tuple \(ℳ = (\mathscr{A}, ι, δ)\) where
				\begin{itemize}
				\item
					\(\mathscr{A} = (Q, Σ, I, Δ)\) is a ta
				\item
					\(ι\colon I → ℝ_{≥ 0}\) \hfill (\emph{root weights})
				\item
					\(δ\colon Δ → ℝ_{≥ 0}\) \hfill (\emph{transition weights})
				\end{itemize}
			\end{block}
		}%
		\only<\tlRunWeighted>{%
			\centering
			\begin{tikzpicture}
				\node (t) {\(a\)}
					child { node {\(⊥\)}
						edge from parent node[left] {\(\nt{B}\)}
					}
					child { node {\(⊥\)}
						edge from parent node[right] {\(\nt{B}\)}
					};
				\node[above right=0 of t.north] {\(\nt{A}\)};
				\node[left=1em of t] {\(t\), \(r\):};
			\end{tikzpicture}
			\begin{align*}
				⟦ℳ⟧(t, r) = {}& ι(\nt{A})
			\\	{} ⋅ {}& δ(\nt{A} → a(\nt{B}, \nt{B}))
			\\	{} ⋅ {}& δ(\nt{B} → ⊥)
			\\	{} ⋅ {}& δ(\nt{B} → ⊥)
			\end{align*}
			\[
				⟦ℳ⟧(t) = ∑_{r} ⟦ℳ⟧(t, r)
			\]
		}%
		\only<\tlDefProbabilistic>{%
			\begin{block}{probabilistic wta (pta)}
				\begin{itemize}
				\item
					root weights sum up to \(1\)
				\item
					weights of transitions with same left-hand-side sum up to \(1\)
				\item
					weights of all trees sum up to \(1\)
				\end{itemize}
			\end{block}
			\begin{block}{Observation}
				If \(ℳ\) is a probabilistic wta,
				\\ then \(⟦ℳ⟧\) is a probability distribution.
			\end{block}
		}%
	}{%
		\hfill%
		\begin{tikzpicture}
		[ anchor = base
		, ampersand replacement = \&
		, row sep = -0.75em
		, graphs/tree graph/.style =
			{ number nodes
			, branch right = 2em
			, grow down
			, math nodes
			, edge quotes = {auto, inner sep = 0.15em, node font = \small}
			}
		]
			\matrix[anchor=base west, visible=<\tlString>] at (0, -1em) {
			\&   \node (s1) {\(a\)};
			\&\& \node (s2) {\(b\)};
			\&\& \node (s3) {\(a\)};
			\&\& \node (s4) {\(b\)};
			\&\& \node (s5) {\(a\)};
			\\   \node[visible={<\fsaRunA>}] (0) {\(\nt{A}\)};
			\&\& \node[visible={<\fsaRunB>}] (1) {\(\nt{B}\)};
			\&\& \node[visible={<\fsaRunC>}] (2) {\(\nt{A}\)};
			\&\& \node[visible={<\fsaRunD>}] (3) {\(\nt{B}\)};
			\&\& \node[visible={<\fsaRunE>}] (4) {\(\nt{A}\)};
			\&\& \node[visible={<\fsaRunF>}] (5) {\(\nt{B}\)};
			\\};

			\begin{scope}[->, > = Computer Modern Rightarrow, line width = 0.4pt]
				\draw <\fsaRunB> (0) -- (1);
				\draw <\fsaRunC> (1) -- (2);
				\draw <\fsaRunD> (2) -- (3);
				\draw <\fsaRunE> (3) -- (4);
				\draw <\fsaRunF> (4) -- (5);
			\end{scope}

			\begin{scope}[visible={<\tlRaise>}]
				% \node (t) {}
				% 	child { node (t1) {\(a\)}
				% 	child { node (t2) {\(b\)}
				% 	child { node (t3) {\(a\)}
				% 	child { node (t4) {\(b\)}
				% 	child { node (t5) {\(a\)}
				% 	child { node (t6) {\(⊥\)}
				% 	  edge from parent node[left] {\(\nt{B}\)}
				% 	} edge from parent node[left] {\(\nt{A}\)}
				% 	} edge from parent node[left] {\(\nt{B}\)}
				% 	} edge from parent node[left] {\(\nt{A}\)}
				% 	} edge from parent node[left] {\(\nt{B}\)}
				% 	} edge from parent[draw=none] node[left] {\(\nt{A}\)}
				% 	};
				\graph[tree graph] {
					"" --[draw=none] a [>"\(\nt{A}\)"']
					-- b [>"\(\nt{B}\)"']
					-- a [>"\(\nt{A}\)"']
					-- b [>"\(\nt{B}\)"']
					-- a [>"\(\nt{A}\)"']
					-- ⊥ [>"\(\nt{B}\)"']
				};
			\end{scope}

			\begin{scope}[gray, visible={<\tlRaise>}]
				\draw (s1) edge[bend left] (a 2);
				\draw (s2) edge[bend left] (b 3);
				\draw (s3) edge[bend left] (a 4);
				\draw (s4) edge[bend left] (b 5);
				\draw (s5) edge[bend left] (a 6);
			\end{scope}

			\begin{scope}[visible={<\tlTreeA>}]
				\graph[tree graph] {
					"" --[draw=none] a [>"\(\nt{A}\)"'] --
						{ b [>"\(\nt{B}\)"'] -- a [>"\(\nt{A}\)"'] --
							{ b [>"\(\nt{B}\)"'] -- a [>"\(\nt{A}\)"'] --
								{ ⊥ [>"\(\nt{B}\)"']
								, ⊥ [>"\(\nt{B}\)"]
								}
							, ⊥ [>"\(\nt{B}\)"']
							}
						, ⊥ [>"\(\nt{B}\)"]
						}
				};
			\end{scope}
			\begin{scope}[visible={<\tlTreeB>}]
				\graph[tree graph] {
					"" --[draw=none] a [>"\(\nt{A}\)"'] --
						{ b [>"\(\nt{B}\)"'] -- a [>"\(\nt{A}\)"'] --
							{ b [>"\(\nt{B}\)"'] -- a [>"\(\nt{A}\)"'] --
								{ ⊥ [>"\(\nt{B}\)"']
								, ⊥ [>"\(\nt{B}\)"]
								}
							, b [>"\(\nt{B}\)"'] -- a [>"\(\nt{A}\)"'] --
								{ ⊥ [>"\(\nt{B}\)"']
								, ⊥ [>"\(\nt{B}\)"]
								}
							}
						, ⊥ [>"\(\nt{B}\)"]
						}
				};
			\end{scope}
			\begin{scope}[visible={<\tlTreeC>}]
				\graph[tree graph] {
					"" --[draw=none] a [>"\(\nt{A}\)"'] --
						{ b [>"\(\nt{B}\)"'] -- a [>"\(\nt{A}\)"'] --
							{ b [>"\(\nt{B}\)"'] -- a [>"\(\nt{A}\)"'] --
								{ ⊥ [>"\(\nt{B}\)"']
								, ⊥ [>"\(\nt{B}\)"]
								}
							, b [>"\(\nt{B}\)"'] -- a [>"\(\nt{A}\)"'] --
								{ ⊥ [>"\(\nt{B}\)"']
								, ⊥ [>"\(\nt{B}\)"]
								}
							, b [>"\(\nt{B}\)"] -- a [>"\(\nt{A}\)"'] --
								{ ⊥ [>"\(\nt{B}\)"']
								, ⊥ [>"\(\nt{B}\)"]
								}
							}
						, ⊥ [>"\(\nt{B}\)"]
						}
				};
			\end{scope}
		\end{tikzpicture}
	}
\end{columns}
\end{standaloneframe}
\end{document}