Extract subsections on formal languages into a standalone section

bibliography/books.bib

@@ -175,6 +175,18 @@ @book{Erickson2019
   year = {2019}
 }
 
+@book{Farmer2023,
+  author = {William M. Farmer},
+  doi = {10.1007/978-3-031-21112-6},
+  isbn = {9783031211126},
+  language = {english},
+  publisher = {Springer International Publishing},
+  series = {Computer Science Foundations and Applied Logic},
+  title = {Simple Type Theory},
+  url = {http://dx.doi.org/10.1007/978-3-031-21112-6},
+  year = {2023}
+}
+
 @book{Fitzpatrick2008Euclid,
   author = {Euclid of Alexandria},
   isbn = {9780615179841},
@@ -522,18 +534,6 @@ @book{TroelstraSchwichtenberg2000
   year = {2000}
 }
 
-@book{Farmer2023,
-  author = {William M. Farmer},
-  doi = {10.1007/978-3-031-21112-6},
-  isbn = {9783031211126},
-  language = {english},
-  publisher = {Springer International Publishing},
-  series = {Computer Science Foundations and Applied Logic},
-  title = {Simple Type Theory},
-  url = {http://dx.doi.org/10.1007/978-3-031-21112-6},
-  year = {2023}
-}
-
 @book{VanDalen2004,
   author = {Dirk van Dalen},
   isbn = {978-3-540-20879-2},

bibliography/papers.bib

@@ -356,6 +356,18 @@ @misc{Unger1968
   year = {1968}
 }
 
+@article{WagnerFischer1974,
+  author = {Robert A. Wagner and Michael J. Fischer},
+  doi = {10.1145/321796.321811},
+  language = {english},
+  month = {1},
+  primaryclass = {Information Systems},
+  publisher = {Association for Computing Machinery (ACM)},
+  title = {The String-to-String Correction Problem},
+  url = {http://dx.doi.org/10.1145/321796.321811},
+  year = {1974}
+}
+
 @article{АлександровУрысон1950,
   author = {Павел Сергеевич Александров and Павел Самуилович Урысон},
   language = {russian},
@@ -367,3 +379,18 @@ @article{АлександровУрысон1950
   volume = {31},
   year = {1950}
 }
+
+@article{Левенштейн1965,
+  author = {Владимир Левенштейн},
+  issue = {4},
+  journal = {Доклады АН СССР},
+  language = {russian},
+  mathnet = {http://mi.mathnet.ru/dan31411},
+  mathscinet = {http://mathscinet.ams.org/mathscinet-getitem?mr=0189928},
+  pages = {845--848},
+  shortauthor = {Vlаdimir Levenshteyn},
+  title = {Двоичные коды с исправлением выпадений, вставок и замещений символов},
+  vol = {163},
+  year = {1965},
+  zmath = {https://zbmath.org/?q=an:0149.15905}
+}

code/src/grammars/parse_tree.py

@@ -95,7 +95,7 @@ def _insert_subtree_leftmost(tree: ParseTree, subtree: ParseTree):
     return False
 
 
-# This is alg:leftmost_derivation_from_parse_tree in the text
+# This is alg:parse_tree_to_leftmost_derivation in the text
 def derivation_to_parse_tree(derivation: Derivation) -> ParseTree:
     tree = None
 
@@ -115,7 +115,7 @@ def derivation_to_parse_tree(derivation: Derivation) -> ParseTree:
     return cast(ParseTree, tree)
 
 
-# This is alg:parse_tree_from_derivation in the text
+# This is alg:derivation_to_parse_tree in the text
 def parse_tree_to_derivation(tree: ParseTree) -> Derivation:
     assert isinstance(tree.payload, NonTerminal)
     queue: SimpleQueue[ParseTree] = SimpleQueue()

code/src/grammars/regular.py

@@ -37,7 +37,7 @@ def is_regular(grammar: Grammar):
     return is_left_linear(grammar) or is_right_linear(grammar)
 
 
-# This is alg:finite_automaton_from_regular_grammar in the text
+# This is alg:regular_grammar_to_automaton in the text
 def to_finite_automaton(grammar: Grammar) -> FiniteAutomaton:
     assert is_regular(grammar)
 
@@ -82,7 +82,7 @@ def to_finite_automaton(grammar: Grammar) -> FiniteAutomaton:
     return reverse_automaton(aut)
 
 
-# This is alg:right_linear_grammar_from_finite_automaton from the text
+# This is alg:finite_automaton_to_right_linear_grammar from the text
 def from_finite_automaton(aut: FiniteAutomaton) -> Grammar:
     det = determinize(aut)
     schema = GrammarSchema([

code/src/lang/distance.py

@@ -0,0 +1,26 @@
+from ..linalg.matrix import zeros
+
+
+def hamming(v: str, w: str):
+    return sum(a != b for a, b in zip(v, w))
+
+
+# This is alg:wagner_fisher in the text
+def fisher_wagner(v: str, w: str):
+    mtx = zeros(len(v) + 1, len(w) + 1)
+
+    for i in range(len(v) + 1):
+        mtx[(i, 0)] = i
+
+    for j in range(len(w) + 1):
+        mtx[(0, j)] = j
+
+    for i in range(1, len(v) + 1):
+        for j in range(1, len(w) + 1):
+            mtx[(i, j)] = min(
+                mtx[(i - 1, j)] + 1,
+                mtx[(i, j - 1)] + 1,
+                mtx[(i - 1, j - 1)] + (0 if v[i - 1] == w[j - 1] else 1)
+            )
+
+    return mtx[(len(v), len(w))]

code/src/lang/test_distance.py

@@ -0,0 +1,23 @@
+from .distance import hamming, fisher_wagner
+
+
+def test_hamming():
+    assert hamming('', '') == 0
+    assert hamming('test', 'test') == 0
+
+    # ex:def:levenshtein_distance/shift
+    assert hamming('ac', 'ba') == 2
+    assert hamming('abc', 'bca') == 3
+    assert hamming('abbc', 'bbca') == 3
+    assert hamming('abbbc', 'bbbca') == 3
+
+
+def test_fisher_wagner():
+    assert fisher_wagner('', '') == 0
+    assert fisher_wagner('test', 'test') == 0
+
+    # ex:def:levenshtein_distance/shift
+    assert fisher_wagner('ac', 'ba') == 2
+    assert fisher_wagner('abc', 'bca') == 2
+    assert fisher_wagner('abbc', 'bbca') == 2
+    assert fisher_wagner('abbbc', 'bbbca') == 2

code/src/linalg/matrix.py

@@ -205,16 +205,16 @@ def __matmul__(self, other: object):
         ])
 
 
-def eye(n: int):
+def eye(n: int, m: int):
     return Matrix([
-        [1 if i == j else 0 for j in range(n)]
+        [1 if i == j else 0 for j in range(m)]
         for i in range(n)
     ])
 
 
-def zeros(n: int):
+def zeros(n: int, m: int):
     return Matrix([
-        [0 for _ in range(n)]
+        [0 for _ in range(m)]
         for _ in range(n)
     ])
 

figures/thm__regular_pumping_lemma.tex

@@ -0,0 +1,9 @@
+\documentclass{classes/tikzcd}
+
+\begin{document}
+  \begin{tikzcd}[every arrow/.append style={dash}, column sep=small]
+                       &&                       &                            & \cdots \ar[rd, bend left]                   &                            &                       &&     \\
+                       &&                       & q_{i+1} \ar[ru, bend left] &                                             & q_{j-1} \ar[ld, bend left] &                       &&     \\
+    q_0 \ar[rr, "a_1"] && \cdots \ar[rr, "a_i"] &                            & q_i = q_j \ar[lu, bend left] \ar[rr, "a_j"] &                            & \cdots \ar[rr, "a_n"] && q_n
+  \end{tikzcd}
+\end{document}

notebook.tex

@@ -156,9 +156,12 @@
   \input{text/diagonalization.tex}
   \input{text/algebraic_dual_spaces.tex}
 
-  \input{text/mathematical_logic.tex}
+  \input{text/formal_language_theory.tex}
   \input{text/formal_languages.tex}
+  \input{text/regular_languages.tex}
   \input{text/syntax_trees.tex}
+
+  \input{text/mathematical_logic.tex}
   \input{text/boolean_functions.tex}
   \input{text/propositional_logic.tex}
   \input{text/first_order_logic.tex}

text/formal_language_theory.tex

@@ -0,0 +1 @@
+\section{Formal language theory}\label{sec:formal_language_theory}