From f3dc8a33f55eea85b09c08e57384a3f050b70255 Mon Sep 17 00:00:00 2001 From: Narysev Date: Sat, 13 Jun 2026 15:15:12 +0300 Subject: [PATCH 1/4] add report Sergej Naryshev --- Sergej_Narysev/Sergej_Narysev_report.tex | 205 ++++++++++++++++++ Sergej_Narysev/images/filters_combined.pdf | Bin 0 -> 15507 bytes .../images/forall_vs_exists_matrix.pdf | Bin 0 -> 14142 bytes .../images/forall_vs_exists_vector.pdf | Bin 0 -> 14877 bytes main.tex | 5 +- 5 files changed, 209 insertions(+), 1 deletion(-) create mode 100644 Sergej_Narysev/Sergej_Narysev_report.tex create mode 100644 Sergej_Narysev/images/filters_combined.pdf create mode 100644 Sergej_Narysev/images/forall_vs_exists_matrix.pdf create mode 100644 Sergej_Narysev/images/forall_vs_exists_vector.pdf diff --git a/Sergej_Narysev/Sergej_Narysev_report.tex b/Sergej_Narysev/Sergej_Narysev_report.tex new file mode 100644 index 0000000..c724abf --- /dev/null +++ b/Sergej_Narysev/Sergej_Narysev_report.tex @@ -0,0 +1,205 @@ +\documentclass[a4paper]{article} + +\usepackage[a4paper, top=8mm, bottom=8mm, left=8mm, right=8mm]{geometry} +\usepackage{float} +\usepackage{graphicx} + +\usepackage{polyglossia} +\setdefaultlanguage[babelshorthands=true]{russian} +\setotherlanguage{english} + +\usepackage{fontspec} +\setmainfont{FreeSerif} +\newfontfamily{\russianfonttt}[Scale=0.7]{DejaVuSansMono} + +\usepackage[tiny, compact]{titlesec} + +\usepackage{titling} +\setlength{\droptitle}{-1cm} +\pretitle{\begin{center}\begin{bfseries}\Large} +\posttitle{\par\end{bfseries}\end{center}} +\preauthor{\begin{center}\normalsize} +\postauthor{\par\end{center}\vspace{-1.8cm}} + +\usepackage{hyperref} +\usepackage{bookmark} +\usepackage{csquotes} +\usepackage{booktabs} +\usepackage{multirow} + +\title{Lamagraph: Разреженные матрицы на F\#} + +\author{Нарышев Сергей Иванович} + +\date{} + +\begin{document} + +\maketitle + +\begin{flushright} + Группа: \emph{2025.Б-72-мм} + + Кафедра: \emph{кафедра системного программирования} + + Научный руководитель: \emph{Григорьев Семён Вячеславович} + + Номер семестра практики: \emph{2} +\end{flushright} + +\section{Введение} + +В задачах анализа графов и обработки больших разрежённых матриц ключевую роль играет выбор эффективного внутреннего представления данных. Традиционные форматы вроде CSR (Compressed Sparse Row) обеспечивают высокую производительность статических операций, но плохо приспособлены к рекурсивным алгоритмам, характерным для функционального программирования. Альтернативный подход~--- использование деревьев квадрантов (quadtree), которые позволяют единообразно работать с данными на разных уровнях вложенности и естественным образом реализуют разрежённое хранение. + +Библиотека QTreeFSharp~--- это реализация разрежённых векторов и матриц на основе квадродеревьев на языке F\#. Она предоставляет базовый набор операций линейной алгебры и графовых алгоритмов в парадигме Graph\-BLAS. В рамках данной работы выполнялось расширение функциональности библиотеки: добавлены операции фильтрации и кванторные проверки, необходимые для реализации более сложных графовых алгоритмов (например, выделение подмножества вершин по условию или проверка свойств графа без полного перебора). + +\section{Цель и задачи} + +\textbf{Целью работы} является доработка репозитория QTreeFSharp путём реализации трёх групп операций над разрежёнными структурами данных: фильтрации по предикату, проверки существования элемента и проверки всеобщности. + +Для достижения цели были поставлены следующие задачи: +\begin{enumerate} + \item Изучить внутреннее устройство библиотеки QTreeFSharp: типы данных квадродеревьев, механизм конденсации, существующие рекурсивные операции. + \item Реализовать операцию \texttt{filter} для векторов и матриц, возвращающую новую структуру, содержащую только элементы, удовлетворяющие предикату. + \item Реализовать операции \texttt{exists} и \texttt{forall} с поддержкой короткого замыкания для векторов и матриц. + \item Написать набор модульных тестов для проверки корректности реализованных операций. + \item Провести сравнительный анализ производительности реализованных операций на плотных и разрежённых данных. +\end{enumerate} + +\section{Особенности реализации} + +\subsection{Схема работы с квадродеревьями} + +Векторы в библиотеке представлены бинарными деревьями: внутренний узел хранит два поддерева, лист~--- либо пустое значение (\texttt{Dummy}), либо пользовательские данные (\texttt{UserValue}). Матрицы используют двумерные квадродеревья с четырьмя потомками (NW, NE, SW, SE). Для обеспечения компактности применяется конденсация: если после операции все четыре потомка узла стали одинаковыми листьями, они сливаются в один. + +\subsection{Фильтрация} + +\texttt{filter} принимает структуру данных (вектор или матрицу) и функцию-предикат, после чего строит новую структуру, куда попадают только те элементы, для которых предикат вернул \texttt{true}. Пустые листы (\texttt{Dummy}) игнорируются. Рекурсивный спуск по дереву позволяет обрабатывать только занятые узлы, а конденсация на выходе обеспечивает компактность результата. Это особенно важно для разрежённых данных, где большая часть элементов не удовлетворяет предикату~--- итоговая структура также остаётся разрежённой. + +\subsection{Кванторные операции с коротким замыканием} + +\texttt{exists} проверяет, встречается ли хотя бы один элемент, удовлетворяющий предикату (\texttt{||} по всем значениям). Если такой элемент найден, дальнейший обход дерева прекращается. \texttt{forall} проверяет, что все элементы удовлетворяют предикату (\texttt{\&\&} по всем значениям)~--- при нахождении первого неподходящего элемента обход также завершается досрочно. Короткое замыкание реализовано на уровне рекурсивного обхода: если левое поддерево уже дало ответ, правое не просматривается. В худшем случае (предикат истинен для всех элементов в exists или ни для одного в forall) выполняется полный обход, что эквивалентно filter. + +\subsection{Тестовое покрытие} + +Для проверки корректности разработанных функций написаны модульные тесты (64 штуки). Они покрывают как штатные сценарии (фильтрация части элементов, exists/forall с подходящими и неподходящими предикатами), так и граничные случаи: пустые структуры, предикат, истинный для всех / ни для одного элемента, проверка досрочного завершения при коротком замыкании. + +\section{Экспериментальная оценка} + +\subsection{Условия проведения замеров} + +В качестве инструмента профилирования использовался BenchmarkDotNet, среда исполнения~--- .NET 10. Для каждой операции измерялись математическое ожидание времени выполнения (Mean) и среднеквадратичное отклонение (StdDev). + +Генерировались два набора синтетических данных: +\begin{itemize} + \item \textbf{Dense}~--- структуры, целиком заполненные единицами (максимальная нагрузка на квадродерево); + \item \textbf{Sparse}~--- структуры с небольшим числом ненулевых элементов: около 3 на вектор и примерно 10 на каждую строку матрицы. +\end{itemize} + +Тестирование проводилось для трёх размеров: 64, 256 и 1024. Для векторов размер означает длину, для квадратных матриц~--- количество строк и столбцов. + +\subsection{Бенчмарки filter} + +\begin{table}[H] +\centering +\caption{Результаты filter (среднее время, мкс)} +\label{tab:filter} +\begin{tabular}{lrrr} +\toprule +Метод & N=64 & N=256 & N=1024 \\ +\midrule +VectorDense & 2.8 & 11.5 & 57.1 \\ +VectorSparse & 1.1 & 4.6 & 19.7 \\ +MatrixDense & 272.8 & 24\,400 & 402\,544 \\ +MatrixSparse & 21.6 & 549 & 44\,189 \\ +\bottomrule +\end{tabular} +\end{table} + +Сравнение показывает, что разрежённые векторы обрабатываются быстрее плотных в 2.5--3 раза, разрежённые матрицы~--- в 9--12 раз. Это объясняется меньшим числом обходимых узлов квадродерева. + +\subsection{Бенчмарки exists и forall} + +\begin{table}[H] +\centering +\caption{Результаты exists (среднее время, нс)} +\label{tab:exists} +\begin{tabular}{lrrr} +\toprule +Метод & N=64 & N=256 & N=1024 \\ +\midrule +VectorDense & 527 & 2\,224 & 9\,440 \\ +VectorSparse & 247 & 947 & 3\,899 \\ +MatrixDense & 31\,292 & 579\,103 & 18\,688\,678 \\ +MatrixSparse & 3\,769 & 57\,734 & 1\,274\,995 \\ +\bottomrule +\end{tabular} +\end{table} + +\begin{table}[H] +\centering +\caption{Результаты forall (среднее время, нс)} +\label{tab:forall} +\begin{tabular}{lrrr} +\toprule +Метод & N=64 & N=256 & N=1024 \\ +\midrule +VectorDense & 556 & 2\,212 & 9\,207 \\ +VectorSparse & 258 & 978 & 4\,148 \\ +MatrixDense & 33\,393 & 625\,096 & 19\,155\,156 \\ +MatrixSparse & 4\,155 & 60\,387 & 1\,429\,950 \\ +\bottomrule +\end{tabular} +\end{table} + +На рис.~\ref{fig:forall_vect} и~\ref{fig:forall_mat} приведено визуальное сравнение exists и forall. + +\begin{figure}[H] +\centering +\includegraphics[width=0.92\textwidth]{images/forall_vs_exists_vector.pdf} +\caption{Сравнение exists/forall на векторах} +\label{fig:forall_vect} +\end{figure} + +\begin{figure}[H] +\centering +\includegraphics[width=0.92\textwidth]{images/forall_vs_exists_matrix.pdf} +\caption{Сравнение exists/forall на матрицах (N=64, 256)} +\label{fig:forall_mat} +\end{figure} + +\begin{figure}[H] +\centering +\includegraphics[width=0.92\textwidth]{images/filters_combined.pdf} +\caption{Производительность filter на различных размерах и типах данных} +\label{fig:filters} +\end{figure} + +\subsection{Обсуждение результатов} + +Разница между exists и forall находится в пределах погрешности, поскольку при выбранных условиях (предикат верен для всех или ни для одного элемента) короткое замыкание не срабатывает, и оба метода выполняют полный обход. На реальных данных с неравномерным распределением значений эффект от короткого замыкания будет заметнее. + +Разрежённое представление даёт существенный выигрыш во времени: для векторов~--- до 3 раз, для матриц~--- до 15 раз. Чем больше размер структуры, тем значимее становится разница, так как квадродерево эффективнее сжимает большие разрежённые данные. + +\section{Заключение} + +В ходе выполнения работы получены следующие результаты: + +\begin{itemize} + \item Реализованы операции \texttt{filter}, \texttt{exists} и \texttt{forall} для разрежённых векторов и матриц на основе квадродеревьев. + \item В \texttt{exists} и \texttt{forall} внедрено короткое замыкание, позволяющее завершать обход досрочно. + \item Написаны 64 модульных теста для проверки корректности реализованных функций. + \item Проведены бенчмарки, которые подтверждают эффективность разрежённого представления: выигрыш по сравнению с плотным составляет до 3 раз для векторов и до 15 раз для матриц. +\end{itemize} + +\begin{thebibliography}{99} +\bibitem{qtreefsharp} Репозиторий QTreeFSharp. URL: \url{https://github.com/Lamagraph/QTreeFSharp} +\bibitem{benchmarkdotnet} BenchmarkDotNet. URL: \url{https://benchmarkdotnet.org/} +\bibitem{fsharpdocs} F Sharp Programming. URL: \url{https://en.wikibooks.org/wiki/F_Sharp_Programming} +\bibitem{matplotlib} Matplotlib documentation. URL: \url{https://matplotlib.org/stable/contents.html} +\end{thebibliography} + +\section{Репозиторий} +\url{https://github.com/narysh/QTreeFSharp} + +\end{document} diff --git a/Sergej_Narysev/images/filters_combined.pdf b/Sergej_Narysev/images/filters_combined.pdf new file mode 100644 index 0000000000000000000000000000000000000000..2d444b8b8712dc8c04e7edc172d7d4254d99d559 GIT binary patch literal 15507 zcmc&*bzD^4(-#S)q>&I@6eI+;fhDE8yCj#8Wf52q1Vjl5>23u@5GBPRL_k15N>s`M zL6MRU33>0X`sgG3`#k>l5}&^psRYprQyWzB_L~w`-}OAPC6A z{tT70Gze_ue-;e_E85}gFdohzu%4YW+8YD|7z{wNvQ%iSBc4&>w+1R6SR4pWU;vxx z+Mhu?;6UQvZ*e8Kh{k~| zfnk+Y08!9>I1pIf9S}j`$EV_tPj!&>Z{k4rDu9<8FTEEUknX$qU<0(bhmV&7pbuVt z0}xmn?dWQ!;Nb_12myY@VGs}k4g*An1?LR9rEDt{|`q1~7mU+QGvSjThM)=Y_U&r}E2rW$`}#$OGChcfUpZ*ON}8 zqLKur^67jHIS=;jFQe;L?2lNPmhfGB({}jf&hnPJ6g;UocQxLM;XTKsb2i}=C6WbUoH6`(9D7?<**;^u8Ez2rb`_ zvCSLW9L{RY>(EVG?TW%3r1>!Q_SsbS)EsU#<636_U7m3iOg=J?3w-sWN}uer^^}|E zhQB$#5WUCvQiEOF+jdSXi~DQFk?uSRv&$WAnVCah^Jn^emCbG}c2I~nTRhwt`??Yy z5F*{n22Em@mhb3g_Ti{KH)J?%XAZxdY7_I-gqN265~|wg;V$zMc#_6wKBzWWDi#O3vx_Be_JT zEK$xEvkBDIT`VHsAc2+HhY|#ju}WoJ%tb2)i+z>s=CjINSz0u6R3pe|N4KycSM-}NioEMSAN`ZHE9vR} z%nP3=>mLe=ByU$Pr}w{f&3u0)*jlI>WpUL@z^cA3hhw^&3dyH&qo9@sR^15D_ZVyQE^!y46|LT|`FCZu@ZFGRb{e+nxWgFrH6z)k8D8d?DwY)4W^ zlSF(pj8;+@*@hPE3!1F>dMPUB=dixAXP(z;Uo{qjTvoNhNtTWZrdqxG$Q5_lobSk$ zBsx*s12Nx{jW%6q^{**rj$WU_VMYxtM!dXaI#qKNHMfryi3HWBJ)S>~G1?q=S3A_% z*4})X>S{H~nQSyp!=J_N^U){6xnJvx^&AuTncx&^9}}SEOZ2f^ ziq`N_ad$JEO}$kNdP=p{HdZl`Xlj(8nzwv9KVT`E%B#h_40m2rT#wNqD>?Sfv$A54 z_()UJ(E52zPCwhoulqxg)R$?~XfBUVoKo1O;AY#-q2^{4GB$&OP-Df|5Vrj0Boh79 zYE{8uxDi0q6CiU7*rerZKmI1R=J3)2VBJ3pR#syB9tq=vH6g?tClxTQd~;DN%0a6ZzIlT$9r zF=7>t`xwZ1<)Gv&+-wPb1_zHBA}SmsCC+&-S;XL5){%yEMVS{bG$uIBCAEtP>f|XMm_iqQ zqPy+rvn!D!?Y1(UOyfl~Z4dnW?+-(a(Q1g*6xT ztS48qo5bnBgBFASZ`fNrB~jAgD%K?vCjEWE=Y~x{h@hZAxdJQUwRzpy`ZY+yt81re zz>04=(|KUsstqd7lex)rl8UZ;d3r_PuuR#;2c4*F1kph~z2fKqb711+wI84Q7zRV~ zt4=N}V=`Y1%tbVO)vT$r6)G3EWwDKWMw=~OlY0~~ITI^A6ZYh)Y;=9HRx;T)s2ZwG z=Sn@-#JiNO1d5HyNY_M5RR4NYt=x;NQY6oSzsIt+I}xO7qz$sc@~^tXgcj@h-cL>k zABpEUj>mI90Lc$zM?f!lL<56Lz<$C#0_?#PEdgxwlks;9_!IhwApyMeAGk**L5h)- zhek0#C;#}+C|wSJrdD+K&TF%G>Kwuq{)~=PWX^+0CGC8E(|ySYUvE^8M7s&cT4t<8 zab1dTGF6xxg$8o2NGLGEt7fRm52d#5=MVIMzbNvGhwo;n9!G!p>SFxa*!5yRly0GU zL8(x9w+Z%AO33Fso`vRLLV7P8TD)_ProXeCK9*_H{Eys?SX>JN$#a+0fHA zel-&FM9e}2=!v8LTUqVyCdx+0LGr#jLx~WR*jimd8Qv|Mll}cx+qz-pH9U4IwBx4^ zHz()&$}t{h3vj!CIgW8sltt7vM!R6~bg(}9ai+~y7-!i57!%vKyQ%jvuL;4aYTw_G5-B zmCo3mA`_`+U~Nr~uxj2W%aqy&g`KO7e)ESOjt1^q0&{&NBIEDi{KrE18`H_eHsNI? z-PIanILoMTSJ!w|er@-DzJ}ZyJK37=DQFtb(9bw0MLd8#!$2rmp^Kwk`@JyuLjS$% zMcxP;)*_FkQZC|+mrR=~8yOL?@G$)k=nhBx#rhRVdgk5&p&_3y3857RUEq6lS3W_p ze;29fPuF%`Fw;Y=RvN8QSdZXaPhk-AH$;?rA75^z#Th(FWtwBkEqK+o>9Qg&KAoJ(Sf`{rIxKrr^tmzPIk^vT zQF1bgh_ah4f+yDFqRT~G`E(5D6O}1;TZYfbN@f=x_kpPoY9?tu|2lewzNlaGIjX$b z^8l;;eSNj{#6jf)!ph+Ki?g|RM7ggCIv5qc8dA`$O`oNJKS?VqDe`rvKi^q9KZ!7E zJlAtTgSMj8rT?f*?5jjikw*9cL$!O%MW!#DGt0RjXr7ywyk2!`-&vEwR7q@P_oOR! zZa5FVy&NE>`Nl`%e38_}$alBpj+^3EFuv?B?6R*soqJw%J=?C}$_{y*`IoCVO?E9$ ziK11n?#|0xXj_+~_P=02WQOob6uqEA+ZL-CMAyIb#M9f$&-E z9|FN468|lcjJ_t;0ZQ|Fi@E;PzM08hf0#h6+WcdYTZp@mc78d-8`Z*)$`jls0_R@B zw(l~qFIaD|H#o!3eHf{jS;+D`WJwu+aq*cmazyBD5_=+w+DlZ$`@srL0wZ8n5vt*vVICJG`Pdg`cYie zODq#~COu=IjOeU*U)z;qP8}Dz6wWm*ownW3dBC9|#GBRc&kwg)2sp2IY2lfsuNJo~ zV}nEFBU+V@5pNYnshL@Q0?_FHwXJlgi6v)Gi9cy<9bY6OC@v#xqZTy47&T1JtDg@Olw=YoO1_E;(878tojDQ zq`No@BF4v`8T?^<7~(IMgR;Jq7da2j3@RMF;Iwd9qSpx~D7Nl#+}|dtbHAfG?4zJz zPfGgD2@`YVM@7|HzWY`UoHa)&bGD0>Qo`J8R0OcMTb{E@HAR;VLRRR_rD@;+>z_MJ z^jGv!Q@s}y5a|i|nQyPx7E`3kgclUbkbmSjLVfD6Utwv4&UNO`2faHyQrrSp6N*m> zXMaZdLDLa2I>{?%mW85{-PG+l^K`>uHK!_BAM)JdoL))tm$bz$=?*%dNNgryr;-g2 zdVQkGOC;{Cs;-@~Xb^o+eMv0W$o}UQX=`r-Uay^gof44qxcO-P*0-b3<=E}3a_=jx znuypAf57sm?ck9AUbrIq9kD>H+p41ygIvT)tvXf=J;m<6&rc!QpK#wX(FjH!qE(Mz zm;`Aq4j^Ar?LIk16MV9h!TjL+$YUkP?vJ0o;3v5s%tP_UVd3WRT1uINTk93L&oyALZYjKOaBRL+UF3B0 z{i(qgJ9F~#9N`|cKww(4Fl(sMBx}~xJH7F9dUNRw9 z*OF&Xy|Jbc%$=;sga#xzPAl2*ovCsx-`xuMvRZdR)_BtB2oZDPkFWkP*IxymXHB#h zAvB8518y$tSF02ZyF~w??@KVBYmE}P>RS(W+(C@vsbj^Y;-#lc>@p?{gG&5E{NWPG zCq;}a2ju3~MwUsu1sL6l2t)*H!H|Ek&&%kc;z*%1GdollKo@EqhMAJ6JVSdfwzmKiYu-nt=lq3s zu;Puj6|-9ts%LZvuD_DQxk7cg!9GX)MS;FY%a}R?I$E_nh;>=VO!B$ieY*a<#VmCw zn+?2X$1N{?*ieH5XS_uw%t$j?&7>_cI7q)4j!Hq=$dZHldX|xWbJ6>a6!P3|pF2#LQVnJ3iTJFnz#W$m8ZfdPcqP`wux;P<~cN+X$jje*Vs|o?)AohFO`}ZdZ&#Ghb?H zd2XPI{*W3I!qATl%QJRzD#J+iX&qYI&`qYq2jlkXm9X*g-AVn@&^$VQX?B*qG66og zXQjcAi2oK!TVD#>3ZZ%JO?7&dWMFW~-+-Cx^!(#A1B+{lr&Q9E4RkbxXJgaJn(6L~ z1h(_tu2>!2T4H+g?n!^Lmd=htUba^2sAYa_6r~Rj>le-AV|;y&B4-7T)`Oq1ePUj< zdNGgivdJfL2)2az>veC1X@xiqdj{T6FgrKRDjcnUB+EHrddSy;<3ODheuf?O==gbkJq7mMM&4=dJFi{NtXjF5t_b&Zlc~N6)s3@j z-QI>fO-ZrJTH3`;3q4+rM8K%eNwR!tKSbM~nfvO#!DO7-yhz`?^YEc>r=iPE+HwQ4pPVCMt9v;=Bd~9Wu z{K@AVs|pyNkqEN;yc46foH`-0e?C)X*xev^<%H&qqm|F9vimpJ=g@Jq_OfrL*>eX; zPY)bN5RsDz=7fs<#dIs{)i6AP(99soRYq?+b5D8+=Ip$_xP%hrJw--oFw0FZJeFDs zsU0mWEv_4_%N)fd($&Uh$A;Ugd{#2^eEM8rW4e&B==oIh^n9%)*rd} zz{y65EQbaYXv1?I)%jg!$yz)8gL&$=Z-0Y4&0g12k;55im$Aa2`f4+>cer;`aB}rEx8cp(AdTBZtAl}7%xt!{&ithCy(*uYI@AH&0<8zxgIC` zgC?+SHS1Y;LR~|5oK}y0pvz&up3TuT^WBu%PefZ{ zumm`g`0pbiJ#{PqOX_-0Zd}@TllAp-9%c0D&0RNT_73$bCC|khb|5COQ)+BZOLlsE z)X=5J&(0M0U_eeG4|p(RH4>y3=pYB)oHMm7i>=j9R)9FarJpE^U2HoceE6okka6BK z_@?!nd$CFOBv((`i_5<>2(z|S$W;no2wLy1HlY>%)|ko(+D?#wW2TgQqC+Yr`nB+mzGqv%!z|mzr6! z({Gyf*C;9Tzqra4y|PR<^Ujdik{|**B>pCCi2+~-aB>u&yQnhiY(LMWjF0*I3_eik zNFFjhaLKi8)=47etQU}1w!Uy&2{Rs*49%d_S$kexm8fA6JENWY>HSdwso}bow`GU- zCviCKoj(LI^nv&b=hxOlVadM3O51&!X@T|5At2?oU3ax^3U$7b0)M|arKeL5>yJ)| zO&|iz;LUS>ETdlIb-B9&4h$|^5%v^`>v0m)Ur47YbXDV`>S~6hX|q?R*uHkvg+ElP zWUaYW9ShpRW*!*J9&V9C2GP1lVv>6;kK1@SX~Z1+l<*0yFPe2Oxjezk>TU>E>#^rd zy4d>c_j9+&UwvE^LQo_xAckb^O@y-8JtkZ9c5@w-weMMnOLJeYd;ET=!yqx$2zgZ} zTyi|wE_1aFqaG_%qVwGKBWzWsicgOU%QBOHvY4zy!Dgehz~ZXhsebEKBBmpPIG}$M zv1N3dXi1?5x16cKXANk=68sH}gRItfSw#(O%!Y={OjT8Btc)%tWjKtr-khb|7F(pG z3oUN)K50agI~1#Fi?yZan9;I;Mk#qGQ{61U!dxG~#+3X|I}{k?P1sK~N|hsrNi2k< z1VW6WU9uX6s@F})jkv~G(*G^J?sd_lU^^!W5vUBTfjzJk ziiG~RVTImRd%~NDbPv?WP->q!!e=iIfBrCSY~HDyo^rLrwpB^yesKP`*sVmDk)e(^}ysth&pvu`1+?NU&GC5r;pKQ zmi^&xlrx#O-m;pSuHqT?q1|801Z;~;l5-Ju($#lT%BMr?qWD|X@`W(-ae33D`TK>b zko-N~A5CtS#*~Q6VlElEayvIW?pii0^CZ=`-ZHpQ&3foGAMNrjmmC4ncZ-FaW%`gu zB{>>Ut-MtKfU{P|8#@Lt@|Egi)mJt(Z@8k<>RQ>w&)+>B*p?^4li28EJmou}m{HZS z&~rci{N|_5_376=%}N2rM)gu(azt{_FYkxFXz_hiM$;VpxZXK1zFbZV9T-VuVu&C< zI86L6T+HBm?44xU2F?d?D`HW1&9EOC|T@Jx|VN#UoNm6czQrKr=3;S?+_NSnH~l4JtA zH>#aqlc+UN>n)Z^u&0+O@*=!lDV3DM1wR}WET5bd^w6U2G#KFC2s*=-^#auz1-~(b z47-t+6lfea#Gh3DHu`}RKe^7!IB#ZEK6LM?vWu$Os`a71i1u)UfdcqY;AB|5eA7xufsZH9x8Ly2h$oz9dekaCszfiQOG$WVG(B|sv43n0|eR(Bv>q zi*QwSoF*oBqL*ic?#*N^S9{UG{3GSVj~*BKKK=k2M9e$GOmf#c@nh;*w;f z$|I|($tzk4<#uI91Z0Aepxs+!sYyErWX1;$xYMLpz8HN|&&WfvuKsxE#qceUoI?2B z);Ei}PIuxfNylYMwHpNmor_xs)qJ=8+t$DOH|&y}&b16BVn!mc5cL;35K_B?0XVYQ zHYDc@b1>fQa9ry9_E94FIPYXh6lFH8VgJ3T^?5L4B#tB+9 zkE@!T3%gvbO<{?--3Sg&T-Jr^<UCA=>NzKE z;s+8NRd~)pBxsqyr?NRAD={ju9JOcV4bye<8vB2*?SNO_DKsr635ECeNB$Q=Rft9g9 z?IONR^H+K3PZAYa$<@gT4HQ}8t12xCT6v$fa{vlHfi&baOXTgNEj8^2`JJ8ft_4^0h%`;Djt}jJ$>vjATgkU z5=b1MVS>bgy;2)62MC``8Gh@FyMR$KLY+n1ct|S zigst!&;%O;%gOBLB~UR7)bhGI$YY%`Xh3kVAr9?sg1^wV^CRd8m<{oJHSJGy49q96 z1p>uw|MMS?f`IV17eB6#i)S)?>yh{@w9*1{A~O4Qv&|K#}pTb08gSIAf!0* zf42u#y*RM6e)jjzC;YcIz`-9tC-n8t_y0>zU;&5$ZIM7cB=7>R|4$oWABTw(#-c(3 zMGg3CyfMW9x)=~D@$K-u2%th43AiL2D9-q&EnW}c{#QlK?+`=@1el(%?o>cf{9Xa9 zKy47A-UGPO0Rf#6XoesdK3M~3CLq|4m1+lq5rPL5;0Q2$oC3ae0Ko|E{L}XUs7aus zL9id=e0MQmRT1a}_ai)>0P3^}9tr<3q6^;32|TVKAgmCs+(3ZBgewdPP?>P$4gw~b zaD@fI38PT~9tTV=frj^Z_>Zy9;-dwD`YU1}evC$-{0JO`VW|LT1s?kn*uC+==_LeUqr~*?|sc3(auR@|too;76*|9v7y&xj*-CZv8 zsarvqx$3BuSK!)E?U-aF_rS*w$Vif&WbG=e40R9ac=6;rKEbTIncAi|BcAHh7B@W1 zti*#^>JHqcIh%fvr~j}=qwbop@6jSry|=A39vMy84+)4^2;_sW?xTP&&h&!W>!nSb z)z<4STZZ*ET#-4;!dB{F3X?&%g-0@q21m~#3%EUzlxEB2dADpi+lqVDwa1uBBW={) zGWojNGnwPk%AT1?4w6`fPnfr zcH&(-2@?xv2W7}1`Y$JV8r!cu9E|QUT+}s|uwo(Ec+8S3e~EluZS4BD2JS~-+HrTk zmDYe9&O9@2HjdPeX7}Q^AKI1Q(>*!bb#w1djr`rMeoQ3{`4@#g+WMMjlz^&@$A+Kx z(|z#BS=JJ?)|!7@I_ukcsO^&m0t#z=KrnhCmaaxf(r5$wvT~Adi)-pUPY3y} zu;S~Qjv~^c$R-^Z$&DD#tf%P2@uRJx4>30njDOh=4Udq&A8TCtjc1dK^IM$Ka`;0H zzYv+@WavB5LqlxR0+CUnGJ`UK|MIB4^8rlLy|Js!ZK9)Gfs zRJ%pZ^m1TgUB*n*`0btf=2dR*Yp99k-5b3#Gn?BaFs0KFB6j?_E&PH3dk~Mjnud|? z|3EyzhVu{L*$a1or`ZH|{2y@V&yN3Ur^Ji*_izWuVF;n&C$=F1cYqD|UvLLd$p`BS zfh#ByUPl4_gbct@8KJ9RkO5e4c=dk0K||2@XMp)n$ndB7|NoEyzk~m#4PIfqHkO2~ z{huw3VAG#k{xlWAA^&9yym5YV{q)ekISa8)&~1lB2*}1b=Az z%>B&Uo)gp^3l$>dld_w+eK2qdeG;m9{2k@K1n@+HLeA)dCwrOcldNU&9yV&6 zg4@~8Uu*c2uXe|PI0I+7X7VwrZQqW}TdGJr_=<~lOn$=0dByQVn1YWLN6KXX{_9&s z?~9+$`-%;&-KyPsK3(3qUBXfx{Pyl}YNW%x@M>wKdgQ}-;UcSB=P&G=`s6jc*9(7l zLKP^8kcI%;y9x}1{JtsvniTwc{%KWt=K9`?W4L?wWj z32;L27X)Vb|6~Rb`>#F`|C0^q>SvcgkH4>{U!wog=eIcii}>3<{fmf?B|kO)?pxnq zV*_itI^xq5!uw(d_>4%=!v}!R1m%C!H6wrP5v&NjtA$U-1b{Gd7UO}#xY~n!;i6Ee zC`1_Kg2SElmIQ;{|M^bT!^>Ha3Jj!Ajy?{+yI;RIJL~8KvbS?^1BUt81;9!ez|{k* zgnvm+KuHn?fr&xHpl~Q0fkKF#guwYB5PremEaT^ecA^4+qXZS?pC6DI5(%I#C(u7M zeCme(0bzg8pa=*a`uv*)7srRCKWV7Fd?;YX|KLMFAVkK%qso8v2iyRUKmVk`@xb!m ze1O`2jthan_R?TTi9g4HLSaCT`|tjsP>95z{Xro}AT{`tPYg&W|DeGjVt?ueObZ?- zM_UAu zwnzvbYyW!;Bz*52A(8mJ_YXday={SPW{+LOV0bA0@3vxa2>@{aK|>PZ6WeQ3al%2x zzuSt#@Y%y3G~`~Jii_=8FAxb}W&PP!0*23-{@tGhVvo;2B*Y~4v_(OHle<6Kq7X!A z$i3?TB~E0WLh)h!U$OuPIzVdq2MrEK{W(WKt<8 literal 0 HcmV?d00001 diff --git a/Sergej_Narysev/images/forall_vs_exists_matrix.pdf b/Sergej_Narysev/images/forall_vs_exists_matrix.pdf new file mode 100644 index 0000000000000000000000000000000000000000..e80fd6571a5644ce41e86057b9b4f0f3850db7fc GIT binary patch literal 14142 zcmc(Gc|4Tg7k{#pv1SdW5we8Y%?u&?zKty*4aO3N7_z3UCA+dyWGNL{S}cV^A$yiq zN{EzwOXc^>r0=IPpWnyp_s@^lyq^2q=iGbGIrrXk-se8&5j9fNkcP=1L83QbgKt!W zU|=ZN!|nv=&>=9y)Zdc;hN$96csCCxFvJM&MDPZ~0RkLYQ4vHSI*;#I0GV$x_g(~myPxbsa0G7;A1`}A z9y0$pFhrl=;DT52@B>DK0{^l|3>YB`1>1lis(?^HOK&jtC#5ox=mFfp$Yj4Og8cZG z=JW_eCz3N5wlSK9iyI&-7^2|@C_s&1@8Liov+PasBH-OYep&67`i6V3>~AVUBI3ii z4#|Y9CD6L<#O15ChE_(k3+_+3eIxOhJ5`txBhv$HWGwnBZ2CIp z+E?S-D&~jc*j7u$+^||s=$I95MPBQtbLG7T6m>n2VGF<+&$lk)Tz34$0;T& z!NZFT{7+*1rB#ex?k))hUkYhBv!ufPv{fGUmg9l*YH<=9Z30%#K>xbwd?&a=g9|k0r>>rwBqF%-{iR;bC z6iecmdF1Fu+_;G}0;1N>M$98(IocCLK0q+Odn?Z+-i$SyY1Z16*Hb-K9e#DEq82Yr zss?D~dfqr)ojx;8GyIZDO23+RcgtVlnQj# zkhp%VT{K3G?!sBrs_3`5tCvOm+i#*UiKLmb=!a)+aVJ$41*mg<b zdpxE~s1$4@uS>)K#H1Tdr{fc6v6$GjV;YO!USPGW1>OzeoDWnPq`%;Q zpv~qqk9^}}XEn)_-I_!zR(zR%_4!9{@g4VswVx)2vjwHHy}e?abnI(u6ixP=vgO&} zeDT#YFicK2d(*jWqB3;c*vU-n$p=W2a&;33Teh~gd%=fDEEjyzXx z`nEm<{YM=)sg2^NwJJ$Sxe%fVSj zZC+1EPUWE8Q{%nww+#v8HR(!9#+V<#Ab9hFbJ*`JTzd+N3gEV*8RE@Lk@F$Sm@P8B2}F@_mEg+yzNob@P#L$(-8GF4>JKOI7={ z)x=#dG0%wh9uv7NZ7%VOmN)jPx01>3Z;4Uzy4oGdV-Ihc^2K6XALze({O0LX0vxUv z*qgEPcDpdk+tQ>_tG*&h$*Iw-wugq-cYNzXORExRPi4L~W}nVfU#m*g6g)OQR?56q z-tig3bXB{|>0Pqz9y!>s0=Yt`|h_3T~^a(HY@UUDV zOFfgNN0t+2@dc@}$n*~nm<6PS0=gz+Eu5EzW4Mn@e<*$wsTFPc_4pG$IbDzFsGD`q zzNQ~+d)0kMG*ck)V*^vyf!$ekGQ6p%3ct(zBRBX@9Z?pjtuz__?(Vl(t=rT_Jh@=$ zvBTi539FN>bKJwLwJP`eK9;<&M2|eEvQ;YOMSA3f_$jQur| z+8SID+&rdX=8*e6UF1f+Yk7Xgfg6qcG|ge7h%cFIx-DFIwz|%Pi~<^ERmLcMgC3{s z@Qn;DtoD%zrKH>VR^IZOu@-xj|GpO?NiOXuvJ2ht0UOSg;xNcg1criRe|cDnry*Bb z0q*D*;qPwum$#8c0WRi0T#Z74JO`~1vudD0uJGV6Tb5Y5UUd8SS4ZAz^Gn_K=Wqbg zISnKgKNa`LDGYNhgJw5wFCRoc?|y=S8vEL1)Z!-51BFe)5~@=u^r)=N#>#e)2Y zW~KXtL<_@=_D8WayGNfrhrO zE9&=#y;(n68N0YWK8XDyKM!-~{z+%knQI9Zcj^Vy?1~K~T#F;!-`769=+9XeJOL@% zHFhDQZ10T+wlbJ~9DRGjHnRpN!+^isJ{r3f)*2Y=p*!ijYD_Sp=CRd=5(*+~wg-E9 ztiKtCmsSbkHCRRt^FB(>^;P2F-5uz9H!_Z6T!vf5B}PAQ_E?B9p)TEaEnJ{v2b^>F z4=QZ^4udw<2Nu2swmPa~7dIHYgU2!>rwdrEnI!Q@U~n+7QWCai6amd1$BO zbe12jt1bT(m8bhnG|HTa-;2!U+aUV7{Na@%4OSPc?-jHz*85Gf-X9LyHV4@|N`*%< zI{JT5okDB_nMc}ny?47jIaDeP%@&oH*6-%(C@t~PE%_dXrI1Yg%(5<`1NqW$lF2I1 z_@C+zNkLBc+__rhjU*9|=5UuOMZNY?Xx7|KM};jifc=Xt1ab>oOFF5|y%EYxKV2Nk zA_YDz+E<~RpxU#JQuSwRzABOKp;di|pi@wb6kWc^En_Q}^esao1YPX^;Z)-b++C5@ zd^?>%<@nmD%X!T_r3vq!zbSnfb<10LzKMl|dwhxWGiP>QU-MVz1vGjx`4UHsn&I#Z z#X^~GGmcYA?-4TebeO1;!bXV$%W=`A(k`L~Cew-P4C{?APAJM{76|*mwFh*Qbh}rF zFR&N&=yqdEAD!I6V|UkBYdLX1eTS4fr1s2I_DvbVD-!mm1$~1mhSjN442Z`mCB;R) z?(6}r)zjlh)A~~#J9JoXH#zt0Q;6+LJSkm|=-*Z89&?8Ci@>M(?Dx#wmc_3Y9iM(* zl6Nb|tYmhis_wk^Dca+ zud)1cxzK#w>aYw!^YZ$%!s+H^B_{vVI4Uzl4k7-YAt>g*SGR((F3}#w{A!J>_VBh( zqQ!!Mmbtq$~~lr6KUFV2i7% za>%PU211HTXBD`>&nAw#l^3on`l&QBlX#ts&+lcLX|dGSDlQWgcEON6mbcZu#Aj1;U;%jN_rIbr>52V4!!Tt zZa(&iBPI4;=i>BA-r78io5WFTDoP}W>3=B^E&Ja)O1-TH@UYD4-EU25cYR}F=2GXv zugfy%=E~2_f9`K!XVv0Fn)uNXh29;UNHf)ZQbW);aaAbxadRE(lQI)tA2+@gmcwRz zh>x2JPgF1t9EJREru2>FiA_-ESKgpw!!-Q^bN)E4y~n2OQgBDFs2PzUn&gp+Hr|urlrXtuWw{pzmY>lP zJSWe@-d~OeXEtf1A3rGMsvKj_loWA-5Boqkz}QHIFS}l3Qvc>F=M#(8t`-YY9qn|Q zePM=i_@-~)5RMb_Jc?HMxJk*n`Ey7((BjSF~wyGQ!aVi5-!9{S{EoegB7@I^V#N6f|ad}w4&(OnNAG)?q zBJ?7%!I$V$ZZDJUUdGtJi{bj3xU2O;$pZROY>-4#xVTP>3SMPEOBIy{=gooXCpNo2 zt10(X+H+2@p+M@szl3XY1uEmt_T~jaZzX3rCAVCq_f>8gCJF6rVq9;GjHhF&%FD_> zo1BdrR|^nNF?!U7orwbLDm<;>y6xo~G9%&~N!ORlasQe8+0T89%)Jsyj~xuQ+jQ%- zL6S`qxmgDiSR%3=w8fmK=$cynLxgI--S`20lDTZ8p+v&z7rVPWzg(WZH&B@eYjrzq z`Iy_jF)ho?`TE$LhxT4VgU}JDQQzrx{?geswuR%4AE>C43Z8>)B~(%eLZ!!GX0~kPXDZye9tdKjuB5z(yVoXw7V3*M;=Mr3)Q?YxYcDd^F{yc6M)QgO)h}j*FW3!cH*N>xClwI_EkZ7tB~3FVrtB!?QB%&sSZcG zo#yaNEt@GsLe0bWIK2+LAZK2`j$2v%BomTGXvuS&+{D9A{rjG~Etl^3-1}BZv`~IK z6=|tpBRCMG{C8kzq)i08VNK`3m9yIld0x%uFh(Eyy6&pZ*P>mnc5*f!59Wk8UW(0X z%uJ0xKX|sT?ZmYXH?U*qJt4PuRT$dSY|tIAPgz)%#8w+8t3aLJuzx6toozlK#apN> zX_nK5_-ga|PHd7L&ESR z))6Z{_OC~Js?^lQdN1#eUYKY5^wxyhlAwZNwh~XO#{k|A2-*S-XElbM?4~)@C9=N1 z+J<}2U?9h8vE!^u^OPgzqNf*tF`IfF7Q)Sj<-*b!4VJnq%M*2u#(vVjG&ZzPT>eE( zo6xwlWsHMoi!FF7rjB5-OO*{hV8Jr-SCM(f!Q>iTzVA`S^g*3=CRw%`&k znW8QmM97UKMj|EVhDS0}Cx|=b94;;)!DpPw>Z?1zRt#^T^hTvC!0Hwl+PRlxF{~sc?$z zo9rwjTiCS*?}Mhy*@LmV$BD<;`9J9$g`HRPP6id`5#cWP;P2G@kJ;zpaz5C7sFyEA zy`VWNDK8#sR&uaMik%hKkHOR1?YEr2DpqS6qqyfsYR#*n2O)SzC>4Z; zpn`^ADA<2*Y?NUYARY536g}_GE1h?d@nPU5!n$k{kIY`Rz_LY&GYWQ;XVDK;Or#d6Ai ze_}0iLbQZKEdRLl^Vj-G#ssrxjCT(CU6z;P_&no9au}S{^U=eT#+jc?hh)B8__}>a z3OYb#_Nc%VnCuqhQ#X=lRTW}>g^h?m{4im@ws>+TVEqnj@k@HEvXjg*q31IWS#u?Z zMlp{+@0}4;%;b*Yv1PEzOuHXRNHS&&n`W$#^J96l23?esCFS?XI^RE6rMfxNW@H2d|3@F)#+Gnl(u9tC@}(lRWcnO%l0L|;;4kM{fM@v z)WWN<^8?eoUuO9`*)%VqUu~8YNd@R25L-ZGsH7@)V2i7Jn>8>npG%DkXol_?{9bhW zLrEA7>f#DSLZ6@$8RV?vmTE0|S#JN4>Q;}^{VCsKx`Y!gz7;phy+62H+dpzG1#>_V zdlKh1RMH8Jw{U`2#EaWPmzmq?Gol$96>WV2KHv80Lhg+dtsZ`sL(}rOk#yl|2hY0f zg>jjaKBiwY?0A1Leo8;?t*EQ(f=;swYhNu9KVD>>oQ=dEs=RrzbTX{wyjY`FuB6*^ zT+ZZh?sh2sF7{g_3HUuH#Nu@~|EgWtqS3oFy*v zcDCSai81s+ah48DFXxhfpr^HPeM`Taa+&tK$_rn0^IZrjHBEfzfC}ND<{W9E#CjjI z3EzIzwDOjjj=QM=U&mUPCtr0uQVTRQt(E_hC7nfhemA_g(f2_K^P`ZuTBo4+QYAe? z&^am-Lk006;OH%EG2BnvJI?(LI9I6rp2NZ;k+gnK$lXmeR?0XZvp4qa+m&*a_Qq%R z_Y`)~VmU(MOBK^oh591{g-*O%9DKXe7V5i_f!3IeNS6+ilX{X~R<^qTqBgrMNyX|Y zZ9}_Wl0s1XN~O~)8m)&+MzbXtzSLq>5u~>ZqncWT#QS{`rQ_og9(qizxPHNv;1jzu zda+IC5&46t@cf*lAhYm6v82*B(f1t1=nbC7d2?xs5;_l;oLN+v3gjvu)fjj4iq{=b z_I_&{5E|%(igyY*WwaVkP7Ovy_H5{+diT4Q7NO-s-{A2IvyJH@G+Fof(+oagkHT9VYY zh!|;^zGlDwV0qLbF~j*XP4frqH1-FAVyMgq6(9`T!Z8m*w$ccC<}sIQ33A)sFxfKEU}iE6 zlI`m$d-`(aYEN=`pcaFY0}3AH8C71-bl^G{^Vy>}uXnx0jrlU&ckczuTiK@xq1<|m zcZDT~3mlEm)F$b=Wq;@tddc>Byn64`qWbwu?ihN*fR1`%8^dXR25J!4r;eH1N z14kgQreA=y%2q=Ja1~95_hfU8&Lv6P%oRwaOYfB#slsRqvo;VBFR&Tsl zYrenli?ZeU(cqi>!iV{-ddv*8_9SbqJhnMe9prNEPF%3G>KDJI2s2|2yR#ZQPfzft zG=I5WEInQD>YXODdnfm;q^mcpE%;w!K1cWE`b(EH%n%Fd9VZ0M@y=z+vsX0Zf|qt* zobl}S7U4Ro7ao28o}aiPGgg78#!X;Bkn1B8X)$b1CP$(gJ3`EoH}Xd;+g{Ge_$KQ) zTDhm{8fSfukCwl`# z{YI{fxP~s%T;EA#njS|z?4SO+x^UbXLXTtZ3xC

_EkWo!%%Q^fM`x~Q2>G2d4wQVHWL9-fSCm2Tj`3B;fbMbd zh>ARK`k9QH$KHIb6Jsq^!ryf5Pe|m86iZA>C5W^v^j({X6K*1kq}De3zTg^~Up?#!uWy~D3-IfQ7Iwd=n3zPRp@Re-2ydOe%% zcr(6?c0}Qpe!YZ*)3v4nE#Ghc&C9F)57%jqWm{2s*@C13j<(tN12ba4EhwsqMufJH9by-_3T1H>FTZnPw0cVQ8Ce#JzC+MJU{B})s-vgzz zT85DM3fD5qVjn5}8Eb4%2u<*Rk;Jqlnjg>mW#CO5&Bf8r!V+9q#UHrrQQh%oRVpWSW;H z>hh##n(xrW_`U*&>7~uef&IQOf2KQ8a+n}0cyGeblA5}nrh(}}HNpwJxsM5+=uOs~ zmp4h(8Se!~0D9EJZ`{D(P!NRNNR8la@8#l2^6&z~HnN>eeC$Y+Y%1~~z-hSw-W|wE z+SK>Y_9{Q~kfdQyI1DU}ltqAHXe<)QCPE;9Tqnv9`goF;3nf`e1_~v^7U2JXC34ad zz?~70Lj~k1Q8KDP5OpGuc0|sw`X{sNR}~1N=Hlo`0P>^A2~k!Qsk}Y$_CT%{aB$#B zPMmThI0E@sl%ki5lQRiS_Ad4w?(TRnkSPTTAb5FzAs$3PCekUOL~`~b5I_(|Ajb*} zadhzo>b(JW$#9-<(g*JbmIWHAfg$REG+;DkG^M9E$Km<3ulQ*EXEzO>?w>>!z4GRa3 z63HWwZ=~U5_^*oh)FM!n3#_9fzluPX8<2nJVy{eeaw7nuKukykcXM(5E(@D^nJLg0g^( z{52*L$SOnudl3P=LMOLH{dWB)CF6JJqy`35Pg!^BU>G^F1y-O2n3602l=Q(sXOubv zFq{l>fjSc~d}F2J!ElPz0BvkAIN3-66a+AwvX_7DAs{lL)Km5sd}BDumIKxn<%tWJ za;OfZSGoaf;b)yYd3#fy62X8yp_DwpfWSXXz!nA+O(}Z<8Ia@>a4PaY6M)zl^EXRC zIhX+01FYf3u-;_5LFt0L>5-IyL68lLvN1SdK{f`b*b1^ep|l{I58!1xrR)o)IDDXQ zpcl%(pr4ioSRQ18-*zzh>8~BUk?w#%!vUTDM>>oRPT%!0l=;E9#meAbos8%D=He0E zHUWb>KKb&?=ikL`zrgu=p({j5q2<%@$d9?p3sX8^;9r?KCLS6kQv)DbmWlX>XDcgUtL=Djynci9Fcd#S)+BMY43!G zSW1X8s^%I=N^#$Oq?5~05%of>Vh6$4vG=sO0`Px`M^N{A{S6f(bIeW}kgy5&4>}qy zVR5%e@N=DOsB6zXMYGL6RvHZKXABcGPgFT*)OM-Q`Oe*=$6SZ*EVWC4B)RhMo^Z); zZr{Jtr;|%*V7g{_6zX`d%rkYj|9%G^0vD9d=E|%4agTTMKHO)f)#$L<2?MY6Hcj4E z4t@|wC=__}11&Rx!tVkvfKWK7EYe5|_5ogI3YEQW`gF7$iK46Us+SVBXJ-;;bUOS2 z4!m^X4Q7p|!UTDh{#rr*_yF*4NI*+j$3)-oUyuM`kN*b*Hp2ka#(tm<12%QMB}YO= z8e4|}zzcC;%luzq0N{`QfB}F=1a}9#w=*Td8vM(l0w=1Jp8j#DsGmFepY2Eyce667 zJJe0m|NnQWFeqT;{}G2GFLkmc0v22ad`QI4_$A1NQMPFuG+KnbKA47F7JKwhD&a^e&wxL=ewdG zca~*nLkyMK(i-GEIArkp{P@Ne|9;=&SslyQeHCsz#WXy=>yQ=bLCd*)Wyg741A#rq z^mfmlr`c8~64tWH$U4yLS;ODIJH%7taxNYhs;t}j;JTkVVteUK89KkFb}!?acMx$` z?hWt23;AIUqLQ)NtBmQ+*F<*eit+`_8`hazee>Bt=CdwIe@&{6Y2JwG*pF(bURNEi z8#4K0653f$f}LQEDwpP&o=tdN*t`qL3+b1tG+k|30wARf;Nn44BY*cHt|kYE!eybdFa!*N#3G>wp$IW3R7~PG z&G>l{96R@m*89e<}ha`iazw3bGg1_rz zf$uyv)nS13_E%dp6wv%1b-)eqBKhw+#HMkfFf3W|f3<}JLCs%vFf18}{Xqu=LO|^I zXB`xa#cXPeMWQ#!0Yy=%!;;POA7cPR0EqmrIyjshI{irp#3`G`g`>y-_b)nGAeQ^P z4zo!%D1w}*^%osNmJCb(><@tkkojMANEmbz9TH$>6CH|5TQnJ2{y7E`14Kf9)uEu| z&GaW73bDB@3WeD;M<@&s*#6a47La&T9fFK){~SXWCA&$dvS{okd4VOlsVy2whV6g$ zhsIE;!;-^^Kj|>A&AP{+Hm?^971^**awzj>e^?k`P5-O|V)RXG2ngQ+!1os&kOKer zoC9q)=>P^S)4%5p218&sj|(W_pD{>Yco#Q<7v(!Q6PEx2U~|9_oQDV5TvCD$ZK9(G dm|`v|&fJ@X_aafu6AX?;!a<^<>V_Ji{{z4#6-)pC literal 0 HcmV?d00001 diff --git a/Sergej_Narysev/images/forall_vs_exists_vector.pdf b/Sergej_Narysev/images/forall_vs_exists_vector.pdf new file mode 100644 index 0000000000000000000000000000000000000000..8a8a440cf60a2898707acc9b1ae2c47623c039b8 GIT binary patch literal 14877 zcmc(Gc|27A_kR>J*@-B+vahp`8AA5#dz;YMWehQ7E7>C1WnYR!R79mLg|bB1vqYsr zqGXSfeD6$p*PHn~-X6bye&gYBU-xxi%Q@%uI_Esk>z*rOq^>CgmqkHDZoUF;R6^hY z3~;kK3E96NfSUQb+XGNFJPA*5a|ED9ct?9r00A~I0hE*=_Cz~!L+oE2G~I|K07+>8 zJz{8c(%zN?$o;z2@F8iLlJF#Z0QIZF2u~u}dk_IM`4$2-b;8>@6CDA}+EWiVTT^=y zU;$36t_hN2??VEh+O8l8s%uxZwW~H@`4>6xjSP_KCR6WW4^sDwe5i@Nr<<3DEyxd< zeiHzyZ*S*}S9S9NXM}-&7!(#jVqkzJ1gZuy1@`m=aKBor5Q%Q!9h}_kZ$XeB|CXGd zJ<*Zm1i;s3({v_)yaG^70w@4=ds{ahT4qSy)5vXI7c}a=j*WS>cRgcrR*e+mi@WaEt!w@;y~xIQ;m1UG z>-UM2i=N+ycbBzv`Dtx?*wBt1o#$4*TzG|NsX}y5SMrg`nF{U8EsZrktKWD8re5?j2dKy z)8ANj4t->(lusP@7R`h8T8uNj(;NJG`3YxJ^r8tb??=nKGr7m~S#OEfD~N`ASuu+; zI$y~$5oPk;8POYMF>Jmi^K`NkVg{`!Ba}3!cSLIGU?z7mo!G6tQP0mI^mL1F(j6m6 zziZkhky~8nx%0}ykhE7HYc+1aVomPRb-EL(Cr;~p2q~s!XU>}PF4 z_%H`z;m<38X#Q`_+f&`oD@-06(43D~`Dj-n5T!zLev(sFoXw?@TB>%VIrOTG3Ko9# zCcDk;vID`Bssk_VlBc!PUz#u=LL3@}l&{A>kJ`oX`ciP+&L)u`SmYUqd>$hmk`58f zO{(+)Xz($5K<=FWh*XV($!FISev-q9HHzES_6z`I1$ol&ALQzWmqi&Aem zEsbm4ZldTO){nzcs56jK!DI%dUF@7^5eF2kLJ3x6QE`5#y~d;W@x(2Gisum=LCwWo zW_u1VY4Z(uFkrIm_W5)m!Qpd^SAx5nuh_VSDR*@|V!^ViB~6%Is1H#Rz9*H7f#x%C zCo=k5a1=6j*ybU(>Kvs1TJ0h8jP7i(X8H3R-krgxh*A8{w1c*f9GVKADSr2$UJH5H zvFMX;iE)*i?c)P|ne%FW($x;C5)beMWr#X5Eb%Fh?@RlL&{@y#QQg= ziFGRRsakvE`zetif?{QsPwRW4_Qjs|?vuQBx8LZ;{EQP8zD@i@)NV<<{gu_@TV(YE z;S%jxmd-ZVyShVP;5+OtA4YXCRO-smMh-DzNA)kAPy8tnc3StC-zQmlyI18GSy?L` zXL}emRCsD{dhQ8ndmT0nj70>#TU@3GIZgXg^^(CMuF?H~?-|W8(t#Q#P6hq|0{mWQ zZ&Tz$YsRBh6Uzg*>a+4Y7k2|uC!WHiX?R!CY4-VDy848}K(Jx*{((TL9m1-a76Kvp zkRYbOR{Cb!q-YMvE$oSq6$cEqwc03}ZtIfy3cp9$fk`e=plPaaX!Y>-Kw;x>N8{b^ zj89DpiamPcB?>l7E}Va_VV@$LBk)O-eH}b#UW*SB5aBA%=e5bVu@L{Vf}~ ziY}UmEMJ10vaQP_qy|*vK?IAij}AumU(MynQw<^xc?86I7jml?=-LWv4Ht7Xgk5d6 z;Z)36c@u%^NqApt=&bN)LLFzB4souqD;v`&k`H6C77c$@uQq$H>TAR@ck0b6XVh<6 zwY)J`LG*nq3#9qPJhb3u_EqL=Y+KeYcHO&W%H8jxmqcwj~0(5hu(^3-nM6u)*!YqQyQ<$n53uljbTJ%i5g zu_KpR1O{K)>C-LFnb}q6tA6yA)cFx)HX^lX+BxdkId(HuTBqi9kNQKGSCxgFA5qcD z=aR2FhVE3;Y8R9$Gg@$HmYhzPmK|%BoC%LNKmILrDw@F7{nR`8woubKX1rDmpUdOw zY%%HKjP!#_x<|s4<8B9xUZ}PVZx-@@s^Brv7k7HZu2i(W*>@IUm6-Cgk8r-4BM|WY z)*==#s2(z{ncT`aH$MA7+xpp%@tyi~C50h7E+75NS#Ai)A3^gkh0>!|7hWsqi5$H< z<)AU@G7EkG!G9Ooo3FW}HNQ^rU1Wa-$6&C(ojt|rkt;1g&-lCH-w5Eh{A_9YZO74ezqNZdZSbax=q zMLOCd_3H)xpvbzzs*`Ww0lVk1svO9&PmmIpqy}2C0NpnQcYe#c$Nrtr^A_iRw{&@4$wWD8x+t0Gh+&s-xbJHs*8XiWwCoXdiI2D zBn?4EBw$pV~nPP(vMOPY1C<-rIOLcV}|6v$fQXz=fWF9`i^Effb zTbYArm%mH-`52Bd*`2b^QTn+vR)NO$HEGt%p}UJ25S+VyQX%VaM7Fj+aEMKi)mFhw zAuC&ASKXcu{bG?O*ya21WX@~vl&_qF)t%?P^MJP!wST+ARHn~X7i+#Ns!#WsYL+?@ zR|*a(JcH`%@`c_NuCusQdH-6=Laomf%Y(N8TV|pBqf}@l1GWDL(J4mPk!jqzs`rlF zokR7Gq4|Q!*VXbI9p$gQ+rD}qfG3koeatg2$@%l9nn)(9KIeO?KO_x3+jZ}1fhUSY zJeIw)R5|>Whhn4Fu5DDvB4g=wWFb+TP%W8+XRh@yCc3GjU}kCHtVqutl{mGoRkWHf zYvWakG`EA5`|WkERii`}FYT1ImQVPRE)ghKOfq?r#5u{CmD|(!-DzGqe|WI?MtP6*-mqg)5`CWvUJ<9 z;l=s&5~7PSktH(DA_k^Y@f!52^)F8<$!A;>@)J>ABj z!+g8JscWxdbWi*#nObBo`(4+lbDUpxf11mB&(wLeXmG*d>B?6HLK$``qb)_PWy!Jc z^?84c?kg`HzXFAG5pQlN3mqoS6TEr5@fjDJCOZqRX5e!#uFzE-{c<_~(5l4&S$nO^ zt5b?+8yA&#_?|VPvO?r&X59+OZNePLTr4GToNfO3OYBVj=N2#Ia`~)c#B+ScNhNnu zcTJ~P)Oo$NNx01sPAj`x`}wOp)7t9DWS1)Fk0JgZ`$cWm*U(c(IZ~+*M2@G{5rl+c z|6AP@jdh8(aHhd!uId9@K8>~eBE%~XPSwa1qVB++iYc4s-Ia!wiV7SOKm7vn;|@FT zwB-`-BS+-v_XD>-O{e>?STM$(n|bDl9*}$;F@F9rhV}EVw$U)d@cGBJN(n;ywT>iS zk3Pd5ZYh1#uvZ3($UJlSYKlDS>W#j@f|40UF5vn2F+y4Xs*;atJrjw?(f9)Yj@g|f ztcTj(0jZJcvEC=<_c=75eXe@CZr19=lEHmG9ZBKzE?+U^v1xxlqoC<$y54#MN*s@D zBOWqqj)uQh9Z>l$Drd*KzaM%3E;dpv!(Yy$_}k%k+;bhQ!{dgxf}?cdk|GPP1~JCO z22_4uN0DSv%HcG{iHVrD!wt8vh7tl^VY4Q!U5RcH&r=UqHt;)U^&X08H_1NU(FfhS zN}{JCd~)=g#e91Oq!qR9LXP-QPr99m=^xLmO9a7jK533)ZVf zv5x_|Gri~+kku#qm;$9**pF@>ir81QuYB0*tdBe`RFM9a?X*?7ODfJ^Du<`wC0+wp z2My~A3TGP7+btUQr6bDsYNbD4K_*e^QZyuJ_R=KM(kRz;@)7a!vg+U?yT^rh3mo!? z4)oRIkJ6Q7O1IgI2P8k1<_<9%<4zxcV>Eo)XflPbWwO+|y_Peie!Pf(shi*N{fuu{ zC0)k&D@%Hbtg(tTxPOA(ggRd2WSL#b>azcrg{rek=3{1isECVvHn2`yn^K-^s*xq-12^4XzP=}WNY}*mDonUuh-}S9>x2%frsUxOmihP58k=R5j z8S~O!<;kxDb2Ogf9IjLdq5@?Q=uP-4MI&6yRyfnA706lOoY&D=e+PC#{7T^NmP7&^ z5M5sJfFFH9>Vj;CR46E*VwK8oi@9Dq*lop?m2@a@}2l{)~@WCbZz)9 zYh=ZWOLodjQyo5%`SLbt4yLiYoch?lKDO^+xJx*j&V!S{#n1bnOEB9OS-$ve_`#rm zu}m)j>Jx4Kbwn?zZ=Q?z&C#eSlz1z>fNOU#^YB=M$pphuNw@sol+zlz_sa&k^Lp#U+7QO++udC z+*K#sxGQruLFC?OO1>Tc%XhODd;5e0L<08?4y5@;4Bxre(3jMH)$u|Wn?^-L)`JAO zr+3XFj0P>QK66(~j@}x_z0^VXZq7#}aSQ!@{Nj$-o1zi>9(rYRXXQw+bJeBCYj8kB z#KLN>24pM8N*Ilukk;5+bAtH=ZBDtc%~r2YV#=P+YPZznW8%4fdL^0BvJxyO(I;Gz zjS~B_y_7Ze!oUR&iSVpJkKZ_oxObGdK;Loy%pii}QB?7RUL7GfDc0ADJ5C2V!wqGR zgq_L5+w8`CRMnDqapv?7e9mQ|L!g%(^>A)AUZPp8ySOW4m-DMHdUD*sI=iu=stYNf zl)v2{>?9U{O1hdYV|4%C+dh_KSDOSyotTj~k3u!wUN~n620z;tuA<)m)OKX+F;9<& z?8n<)s5{+JXK`tYID7ml%VZAY0D9Cm^N9dYS?{vJa!wf%DJd8{kbnMUbJs-O_qHc5 z&;F#ja6C78+8`Em`AIwZ#8eI5Q483lS!tC5+Zyg)U zK~9vZ&o-jqJE`$hGp(j7dwo+E#Ud|)%ZDCmbD`BS<69xwtj7C!cT%B=3aCV&QU6Vp zzOe$a0md}w39))h)7v-eYr@5EHC2;ra_oxQ0nKC$69Zl8&(SH{9QvorJ>-df~TUSRYR7^iHJXVZ>+gz17fXyFPF&9Pge&d06Mr z*ali4e2rR{L-m3kUY-ibQ$2Eef?GP$cu%@x+{9Olqx>d-!nBS+gu)KC-ZD8Lqd_z6 zgp{C*N|f!6gs_vmxQ9Z1#zv~VS+&9w`ZouiPA(jGIXo}j*1AorC&VxY-|*uH(qUYI zTgd_+Ga*?s7lA_TI4!^P%TpHSuC%P4a+9%`BU3URQ;siLep=0*Ib(TQ`LV|FY${@; zf_rhBSX%vP6&5g>*)~;ea~ZgDV6_{i_;Izw+{G3O!((n13JPlN71>qHD3<6~Tb9fI zj7Eaj>kWq4Vq8>)b}CKtrK?HSyr^#8-qL4f8C~BOC+%aHZIoV3@MiUGwdxf@QK6Fx z5SH77T}C4A8^Mfjqi8tJbLT@oIM72R&L2PUsPICCs%%OQU1-u)2i`5tx>!2)_APLg z0U%OEI>H9YiHwlPZrztsmqfosRE@iZ3O!U{A8He!7Ik`*B9fljJJH}r&m9E@I1E(k zkq^4IRAe)YQ<<0wyhC6%Aqfp*T*5X%rf0rkm*4L8F?4g)hb^y??7NX!KoVW@?M0H! zK$PvfD6a4E>@6e3^Ky@)10)(k#dVrh@v40X)zGO3o@}^&e51?rsxo)wJrM$R*Q6i# zO1LE6L8srNZJZbIRCbbACgdo;uOOtG#TG;9Qww@f02hSCPCVLo}x+RpK*cs4TcIrKYCYr_XWa*1z4$HFB z7IXT%t)ay?P_X*Pji0clj71|&Ws-@0k*o8I%Vk;o{wmx!i`%J-R)oDD4j#>ztBuZn zWa}Z=4;ywI^`2VgE16kloj>6)LPeZZ02_QWXBQga*~JrpN!{O|RI4MU-8Zv2&;84g zLs-)(n&l3Nc84Nxm7RUkhU`My?Wv^Gn&DZ_nB;<-JEHw7^Q%i%-hZ z50&APcnx7&`<(sF_(z>kVUlF^;I*POzc5 zEM+67^1>w4(n2*$J#6~SVr!`g2k*{;sKDI)eQr%HILYKbbxZZpuj*!TArmS7D~-YJ zrm^|*6UA(Ki~55+jEtuq`EZ#_5pgC>IJzq@aYt@2P7Gy0YiMsBvEXIOG~YVfOmS*RWUdTuF?mmKAkT7`A;`J$ zvjg^$y9XF!HFVp}hnl~Y4@qS-_}Y25EMDhW^e6qK4?}y!6<$`=zb@vXP2h8&vVK&M z6#}&h<<~dD5x4z?zl^Ed44_FY5%XVxE>8AjHS>vf(| zW=vWA(YhyyC)oHt=^cY#Q1?uP;bAkid>0Cg6w%9ZQP|J>M#Fd^ zUQeWpk+A2twN2k8N=@B9A{Uv`rDxf}A`$3V7A9+~d0MIQfHjU2v(j{2_@qcNhgjYT znHR706O8T6pEKUu?{ir}nqzX>gJjn~q35NCCyg;RO$BDWng32ZBn|7MvU*ft3LLWu z{xpmfSkwfW2617r2Oh=ERToW6`>oz%DH@=&C_Tj_8+;*s|8cJP;Bcm~7v0kWN*Oz& zxUK0eGEyI$w@)x;44GoQBk#lfdKtDLFHr=!e<&|ldq-K=;)gnK)0eM@1r|c4HM-`M z=gbgUpC1dGYl$za1JdmdWk#uAP5UK=fx+Ub&}h~#d3TOU2-yy6Ye~-!hFs{I;`uVe z*UqYyBsWNfQz}3QiQEJtLnlMBq zKEO$bkaAq|vi!ayl`U>1`;vb|bqK{D{!vsf|6XdBw(t4nWUQzX?vx2(sJI;#d)N_i zCsy1Vw#d{t!eT`nw+&s%`EisFZ5IyL<7wZl1G!a#aJboZlUxfW~YY!T4G)^KtK9wbZia>9+C| zzwaMf7AFSV9;^GCn^h}($&|^oe^DOVUGM#{nCWp~O|@e{Y>Bd-eLw`2g`tA@kO;X= zsF=ww+dH=N2Y9Y_cO{#dTOwigzMv~XBwE@y56d4N^k%6{wYC0v?R`b|tvHUr*b=3* z6v5u}{(>jpE%d+HZVmHZN|)1|2uqU*k(X{tD=q!D?~*nfhNNn7Y-?SsUV>sk>(X7v zL7Ib)b{NeRV|i1G)Pzx<&W!5nVG{56N|cO^Nx13lXff#(SUPiZS9&+D;Q}(RA03*P zoe*Fi+Ao$+@;dUqgBYE`ix^KXEfM?n1I6bSR6qN3m5pkS5jr6*gWqxH>-<+?s%_dRfo(J-YC+!sH`=_~zJQulD!aP!o4+kH}H z;rqo5=SsB>JzS-+6%B}@vK~}`FnklooJh=FBiOkoTx!LrE&Lz0QaRE^QNx7D&4iY* z&&aMqeaZ|jGCdRPw@1U@{d*04^#GRV1C7lVPdYV=Z7wlw=TqXCc9;cVdb&!V4lG^m zN-Xm~NUv;%MufYEm(}hNE#zVfI(DorsfQXo4{Hj%;H*>xMGf?ACQ=qLt~v!q%AXYJG}%^P>~9-2 z5njGe^9{m#Tbu?+O2�i`_ILE+uFc=Q0Nx-qxF~8ev-;c}%>xCqhz~&V;2Wbf97R z`}5x)n=VWj^f_(pFZm?FydpwZgkJBS@l^-E&M{zE zRe>k%Tzb_LPhOVs56u-qKXh$RO5_O_NlZw`2{+I8Tpy3-L$551#SgFy7h&@wA5DI0`&8xjsnt54UK2la+rBje`_#tPquNKVN#7DqR+xX40+TMrC zsnr}yRMwRW7{qPDC8G74*}>5Lhbf&%sIB?;X1m#rpEWActo>PvTXF(Q%a4oWtiEvv zH|2&fB^0}h0f-mP_#Nm>^Ef@GnzA~_YtNl541%YR(J_U$#-r#NuJYO_|C5ZYRBdV9h2NL?H4h#uS_b14_#3?x09vm z&Ud*VX6?1{z|##77ISR^1Y4Qw!q?Z#1DKm z%gq#VZt9xi-9J9I_ZrkJX`^u9e;cr0nRb-)IjAb$)BaaU^N^m(VFM|3`;+)XUZ!}W zCs}eHo+LFVya#{;<*0{WyMZHM5bz+7NK&`=wDoXyC%Jh5@U=ucQ!g75C6SLj3Akeo z@UCDw+=j7#^;i9s0w)89A>e=v3WEgTayS&2$c99MX?Bz;^zkGQXG)%&EDS~lp5Wg< zC33zTNSzUwz6YkrQIh!}Pz@rO@kUPW`;%1oy9xqTcXn{F2UGLNxp)>7t~}lGwqTkd z7?-+}bM^@K4q)mZrRd@8=tKfgpe?p_b9Kc7pi)Bp>^}*GJ0wqF*cP3yuqnkO=nUV$wC!6QL(+DZc_WPyCpMCMy!ctb@f2<#5>tOHPW!AwV|CGmvj&5M;cmhIc>sOJ?BCI`X>+rd)!_pw6}`L`Q->NI2A# zWbb;2T+qk+PZ{m-1g=l*@gf(jr9?y}$a|6GxO^}(XZ&%rl$e`x=o zWpD$KpP@n1NNEFFfxp`#E&`VH0dO!%odJL#2U=jADS%kpsfPdr#g0IrcmP2* zS>RJ!07230-)acLU`o9`fLNR7*UkZV)vtPr#!+4)fSJA&y+p1}Nl{gB5h(4P0no}& zN(2C8no@EFK(;9*BAAf-tKAHHN*(7Kkzi*l%reianxuzJF;oxyNs< zUQ2>Of`;`!U7@9kzRMFB)5EdDOa1&h120Y;5)bRN^yp{!KzV z<);%tA9D&8xpKsnU&P*<5>2W(|3<*s#C6Q_N@)$f?u7bSo8u?diZ%m@L?>u#+$ce* zZCE{J;QpEN!NMQW7l*kV?)kW{T=;^xX7-a~PgvXKp7+DlXnTAM$%7y0TLsD8Y z_x(?vAN!yx$un2xeS9k4x4B%oVR?U?q_A~UJYmXd51($%jAM(p)Y-2m`)2R7KdlN} zSilSzxOVXv2?dlT&0H+>HyTtI#P{no?}WY?Us2z-|FX~n#k1{p@;lQ56{;w3a3bihjLEre;sq?Bg2E~pIdlYJEfL>+8 zl5XZq0*Qjbz?TxRQX?3m9DFx{Hi2PKMhD>|h*C2c=C;|>(J~Zz+Z~TuX(3y-9pa3R z2SyO!`v9IZERh>g1p2pq{o`8KqlkklI;Q%D{{uyUmir$Nu@ORmuf8d|KpjGC7Gj&!{4A{ky|xN6JBx6_v8+amw#*Ie>%YnR@L zwZAL)d2dm6YoMVDYigam8;2}jpATQ(?Az;oBC~C=&|C4wQ*7Ona=T1_x2>GCOAHru z4R-Ib(%Ut2fo4mMa7gnvMwY&A_bR^LU4ibJmvitY!794#4-0(`A!$pdOXc#as`(k0 zJp+jBIX680FXn~RiAY9ke`8E@x-Pt3SA^GZ&alSx>g!26*-2fJ{<3t=igFQ zf&aao|M@@$s-^-qg4*H%IC(XpDv1BxOco15Qm`eAT%a^Y{?EoBhW#@p>VGx^hx$Dv zIO5;?=@03D`1#8S{;B-S+5M>`+mhd$|5C1B9~41#o$bibpYr972|3D8bMpdmD24g8 z9AorfBSO`{uV%;rjyPyW+zDd0n0Ro~rECkfEwI6^%qe1B60Q^%&4u{A;fVfr%jz+0ZSn688n&Jma7ob{ z`M{C^@VdUZ4ZOjSNbsa(T{|S23{U^v7i_j+UKII_>$-L*u8~b9&ao763R@^4AaK-yd3V z7_t#sSBKrOmT-jJ2Kj*+O?I#U>I-i14f`4FyMbmn0=v;3fO@%pZ-BPsZ{A2AcxQsW z2jw$PQ)fSW&^7^36E`=qS*1WaZK4BsSORkN>+r#og!dp(%orSrLCQfyL^KRFA^!)L Ct5YBV literal 0 HcmV?d00001 diff --git a/main.tex b/main.tex index 73c5f6c..66e7544 100644 --- a/main.tex +++ b/main.tex @@ -52,4 +52,7 @@ \includepdf[pages=-, addtotoc={1, section, 1, {Арзамасцева Екатерина Андреевна, Оптимизация произведения Кронекера для библиотеки SuiteSparse:GraphBLAS}, arzamaszeva_ekaterina}] {Ekaterina_Arzamaszeva/Ekaterina_Arzamaszeva_report.pdf} -\end{document} \ No newline at end of file +\includepdf[pages=-, + addtotoc={1, section, 1, {Нарышев Сергей Иванович, Lamagraph: Разреженные матрицы}, naryshev_sergej}] +{Sergej_Narysev/Sergej_Narysev_report.pdf} +\end{document} From 020f55152514ea92a18735126ff5279d09437601 Mon Sep 17 00:00:00 2001 From: Narysev Date: Sat, 13 Jun 2026 15:26:16 +0300 Subject: [PATCH 2/4] fix report --- main.tex | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/main.tex b/main.tex index 66e7544..bd9dfad 100644 --- a/main.tex +++ b/main.tex @@ -3,7 +3,6 @@ \usepackage[en-US]{datetime2} \usepackage{polyglossia} -% Setup fonts. \usepackage{fontspec} \setmainfont{CMU Serif} \setsansfont{CMU Sans Serif} @@ -13,7 +12,6 @@ \setdefaultlanguage{russian} - \begin{document} Compiled: \DTMnow \tableofcontents @@ -53,6 +51,6 @@ addtotoc={1, section, 1, {Арзамасцева Екатерина Андреевна, Оптимизация произведения Кронекера для библиотеки SuiteSparse:GraphBLAS}, arzamaszeva_ekaterina}] {Ekaterina_Arzamaszeva/Ekaterina_Arzamaszeva_report.pdf} \includepdf[pages=-, - addtotoc={1, section, 1, {Нарышев Сергей Иванович, Lamagraph: Разреженные матрицы}, naryshev_sergej}] + addtotoc={1, section, 1, {Нарышев Сергей Иванович, Lamagraph: Разреженные матрицы на F\#}, naryshev_sergej}] {Sergej_Narysev/Sergej_Narysev_report.pdf} \end{document} From 505e83bc7b014430becf1c655f153b056fe3c9eb Mon Sep 17 00:00:00 2001 From: Narysev Date: Sun, 14 Jun 2026 14:38:46 +0300 Subject: [PATCH 3/4] fix after review --- Sergej_Narysev/Sergej_Narysev_report.tex | 40 +++++++----------------- 1 file changed, 11 insertions(+), 29 deletions(-) diff --git a/Sergej_Narysev/Sergej_Narysev_report.tex b/Sergej_Narysev/Sergej_Narysev_report.tex index c724abf..ef86dcf 100644 --- a/Sergej_Narysev/Sergej_Narysev_report.tex +++ b/Sergej_Narysev/Sergej_Narysev_report.tex @@ -49,17 +49,17 @@ \section{Введение} -В задачах анализа графов и обработки больших разрежённых матриц ключевую роль играет выбор эффективного внутреннего представления данных. Традиционные форматы вроде CSR (Compressed Sparse Row) обеспечивают высокую производительность статических операций, но плохо приспособлены к рекурсивным алгоритмам, характерным для функционального программирования. Альтернативный подход~--- использование деревьев квадрантов (quadtree), которые позволяют единообразно работать с данными на разных уровнях вложенности и естественным образом реализуют разрежённое хранение. +Ключевую роль при работе с разрежёнными матрицами и векторами играет выбор эффективного внутреннего представления данных. Традиционные форматы вроде CSR (Compressed Sparse Row) обеспечивают высокую производительность статических операций, но плохо приспособлены к рекурсивным алгоритмам, характерным для функционального программирования. Альтернативный подход~--- использование деревьев квадрантов (quadtree), которые позволяют единообразно работать с данными на разных уровнях вложенности и естественным образом реализуют разрежённое хранение. -Библиотека QTreeFSharp~--- это реализация разрежённых векторов и матриц на основе квадродеревьев на языке F\#. Она предоставляет базовый набор операций линейной алгебры и графовых алгоритмов в парадигме Graph\-BLAS. В рамках данной работы выполнялось расширение функциональности библиотеки: добавлены операции фильтрации и кванторные проверки, необходимые для реализации более сложных графовых алгоритмов (например, выделение подмножества вершин по условию или проверка свойств графа без полного перебора). +Библиотека QTreeFSharp~--- это реализация разрежённых векторов и матриц на основе деревьев квадрантов на языке F\#. Она предоставляет базовый набор операций линейной алгебры и алгоритмов анализа графов в парадигме Graph\-BLAS. В рамках данной работы выполнялось расширение функциональности библиотеки: добавлены операции фильтрации, проверки существования и всеобщности (\texttt{exists}, \texttt{forall}), необходимые для реализации более сложных графовых алгоритмов (например, выделение подмножества вершин по условию или проверка свойств графа без полного перебора). \section{Цель и задачи} -\textbf{Целью работы} является доработка репозитория QTreeFSharp путём реализации трёх групп операций над разрежёнными структурами данных: фильтрации по предикату, проверки существования элемента и проверки всеобщности. +\textbf{Целью работы} является доработка репозитория QTreeFSharp путём реализации трёх групп операций над разрежёнными структурами данных: фильтрации по предикату, проверки существования элемента, удовлетворяющего предикату, и проверки всеобщности. Для достижения цели были поставлены следующие задачи: \begin{enumerate} - \item Изучить внутреннее устройство библиотеки QTreeFSharp: типы данных квадродеревьев, механизм конденсации, существующие рекурсивные операции. + \item Изучить внутреннее устройство библиотеки QTreeFSharp: типы данных деревьев квадрантов, механизм конденсации, существующие рекурсивные операции. \item Реализовать операцию \texttt{filter} для векторов и матриц, возвращающую новую структуру, содержащую только элементы, удовлетворяющие предикату. \item Реализовать операции \texttt{exists} и \texttt{forall} с поддержкой короткого замыкания для векторов и матриц. \item Написать набор модульных тестов для проверки корректности реализованных операций. @@ -68,38 +68,26 @@ \section{Цель и задачи} \section{Особенности реализации} -\subsection{Схема работы с квадродеревьями} +Векторы в библиотеке представлены бинарными деревьями: внутренний узел хранит два поддерева, лист~--- \texttt{Dummy} (не содержит данных, дополняет дерево до размера степени двойки) или \texttt{UserValue}~--- \texttt{Some(x)} либо \texttt{None} (ноль, определённый реализацией). Матрицы используют двумерные деревья квадрантов с четырьмя потомками (NW, NE, SW, SE). Для обеспечения компактности применяется конденсация: если после операции все четыре потомка узла стали одинаковыми листьями, они сливаются в один. -Векторы в библиотеке представлены бинарными деревьями: внутренний узел хранит два поддерева, лист~--- либо пустое значение (\texttt{Dummy}), либо пользовательские данные (\texttt{UserValue}). Матрицы используют двумерные квадродеревья с четырьмя потомками (NW, NE, SW, SE). Для обеспечения компактности применяется конденсация: если после операции все четыре потомка узла стали одинаковыми листьями, они сливаются в один. - -\subsection{Фильтрация} - -\texttt{filter} принимает структуру данных (вектор или матрицу) и функцию-предикат, после чего строит новую структуру, куда попадают только те элементы, для которых предикат вернул \texttt{true}. Пустые листы (\texttt{Dummy}) игнорируются. Рекурсивный спуск по дереву позволяет обрабатывать только занятые узлы, а конденсация на выходе обеспечивает компактность результата. Это особенно важно для разрежённых данных, где большая часть элементов не удовлетворяет предикату~--- итоговая структура также остаётся разрежённой. - -\subsection{Кванторные операции с коротким замыканием} +\texttt{filter} принимает структуру данных (вектор или матрицу) и функцию-предикат, после чего строит новую структуру, куда попадают только те элементы, для которых предикат вернул \texttt{true}. \texttt{Dummy}-листы игнорируются. Рекурсивный спуск по дереву позволяет обрабатывать только занятые узлы, а конденсация на выходе обеспечивает компактность результата. Это особенно важно для разрежённых данных, где большая часть элементов не удовлетворяет предикату~--- итоговая структура также остаётся разрежённой. \texttt{exists} проверяет, встречается ли хотя бы один элемент, удовлетворяющий предикату (\texttt{||} по всем значениям). Если такой элемент найден, дальнейший обход дерева прекращается. \texttt{forall} проверяет, что все элементы удовлетворяют предикату (\texttt{\&\&} по всем значениям)~--- при нахождении первого неподходящего элемента обход также завершается досрочно. Короткое замыкание реализовано на уровне рекурсивного обхода: если левое поддерево уже дало ответ, правое не просматривается. В худшем случае (предикат истинен для всех элементов в exists или ни для одного в forall) выполняется полный обход, что эквивалентно filter. -\subsection{Тестовое покрытие} - Для проверки корректности разработанных функций написаны модульные тесты (64 штуки). Они покрывают как штатные сценарии (фильтрация части элементов, exists/forall с подходящими и неподходящими предикатами), так и граничные случаи: пустые структуры, предикат, истинный для всех / ни для одного элемента, проверка досрочного завершения при коротком замыкании. \section{Экспериментальная оценка} -\subsection{Условия проведения замеров} - В качестве инструмента профилирования использовался BenchmarkDotNet, среда исполнения~--- .NET 10. Для каждой операции измерялись математическое ожидание времени выполнения (Mean) и среднеквадратичное отклонение (StdDev). Генерировались два набора синтетических данных: \begin{itemize} - \item \textbf{Dense}~--- структуры, целиком заполненные единицами (максимальная нагрузка на квадродерево); + \item \textbf{Dense}~--- структуры, целиком заполненные единицами (максимальная нагрузка на дерево квадрантов); \item \textbf{Sparse}~--- структуры с небольшим числом ненулевых элементов: около 3 на вектор и примерно 10 на каждую строку матрицы. \end{itemize} Тестирование проводилось для трёх размеров: 64, 256 и 1024. Для векторов размер означает длину, для квадратных матриц~--- количество строк и столбцов. -\subsection{Бенчмарки filter} - \begin{table}[H] \centering \caption{Результаты filter (среднее время, мкс)} @@ -116,9 +104,7 @@ \subsection{Бенчмарки filter} \end{tabular} \end{table} -Сравнение показывает, что разрежённые векторы обрабатываются быстрее плотных в 2.5--3 раза, разрежённые матрицы~--- в 9--12 раз. Это объясняется меньшим числом обходимых узлов квадродерева. - -\subsection{Бенчмарки exists и forall} +Рост времени \texttt{filter} от N=256 к N=1024 составляет ≈5× для векторов (близко к $O(N)$) и ≈17× для плотной матрицы (близко к $O(N^2)$). Разрежённая матрица растёт медленнее, так как число ненулевых элементов линейно по N, а не квадратично. \begin{table}[H] \centering @@ -175,21 +161,17 @@ \subsection{Бенчмарки exists и forall} \label{fig:filters} \end{figure} -\subsection{Обсуждение результатов} - -Разница между exists и forall находится в пределах погрешности, поскольку при выбранных условиях (предикат верен для всех или ни для одного элемента) короткое замыкание не срабатывает, и оба метода выполняют полный обход. На реальных данных с неравномерным распределением значений эффект от короткого замыкания будет заметнее. - -Разрежённое представление даёт существенный выигрыш во времени: для векторов~--- до 3 раз, для матриц~--- до 15 раз. Чем больше размер структуры, тем значимее становится разница, так как квадродерево эффективнее сжимает большие разрежённые данные. +Результаты \texttt{exists} и \texttt{forall} практически совпадают: при выбранных условиях short-circuit не срабатывает (худший случай), поэтому время соответствует $O(N^2)$ на плотных матрицах и $O(N+nnz)$ на разрежённых. В лучшем случае (первый же элемент удовлетворяет \texttt{exists} или не удовлетворяет \texttt{forall}) сложность составит $O(1)$. Выигрыш разрежённого представления (до 3× для векторов, до 15× для матриц) согласуется с отношением числа узлов полного дерева к числу занятых листьев. \section{Заключение} В ходе выполнения работы получены следующие результаты: \begin{itemize} - \item Реализованы операции \texttt{filter}, \texttt{exists} и \texttt{forall} для разрежённых векторов и матриц на основе квадродеревьев. + \item Реализованы операции \texttt{filter}, \texttt{exists} и \texttt{forall} для разрежённых векторов и матриц на основе деревьев квадрантов. \item В \texttt{exists} и \texttt{forall} внедрено короткое замыкание, позволяющее завершать обход досрочно. \item Написаны 64 модульных теста для проверки корректности реализованных функций. - \item Проведены бенчмарки, которые подтверждают эффективность разрежённого представления: выигрыш по сравнению с плотным составляет до 3 раз для векторов и до 15 раз для матриц. + \item Бенчмарки подтвердили ожидаемую асимптотику: $O(N)$ для векторов, $O(N^2)$ для плотных матриц, $O(N+nnz)$ для разрежённых~--- выигрыш до $15\times$. \end{itemize} \begin{thebibliography}{99} From 74cbbb3bff7900cb8ada50d79e407610d6700289 Mon Sep 17 00:00:00 2001 From: Narysev Date: Mon, 15 Jun 2026 13:44:09 +0300 Subject: [PATCH 4/4] fix 2 report --- Sergej_Narysev/Sergej_Narysev_report.tex | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Sergej_Narysev/Sergej_Narysev_report.tex b/Sergej_Narysev/Sergej_Narysev_report.tex index ef86dcf..36fd3b4 100644 --- a/Sergej_Narysev/Sergej_Narysev_report.tex +++ b/Sergej_Narysev/Sergej_Narysev_report.tex @@ -57,7 +57,7 @@ \section{Цель и задачи} \textbf{Целью работы} является доработка репозитория QTreeFSharp путём реализации трёх групп операций над разрежёнными структурами данных: фильтрации по предикату, проверки существования элемента, удовлетворяющего предикату, и проверки всеобщности. -Для достижения цели были поставлены следующие задачи: +Для достижения цели были поставлены следующие задачи. \begin{enumerate} \item Изучить внутреннее устройство библиотеки QTreeFSharp: типы данных деревьев квадрантов, механизм конденсации, существующие рекурсивные операции. \item Реализовать операцию \texttt{filter} для векторов и матриц, возвращающую новую структуру, содержащую только элементы, удовлетворяющие предикату. @@ -96,15 +96,15 @@ \section{Экспериментальная оценка} \toprule Метод & N=64 & N=256 & N=1024 \\ \midrule -VectorDense & 2.8 & 11.5 & 57.1 \\ -VectorSparse & 1.1 & 4.6 & 19.7 \\ -MatrixDense & 272.8 & 24\,400 & 402\,544 \\ -MatrixSparse & 21.6 & 549 & 44\,189 \\ +VectorDense & 3 & 12 & 57 \\ +VectorSparse & 1 & 5 & 20 \\ +MatrixDense & 273 & 24\,400 & 402\,544 \\ +MatrixSparse & 22 & 549 & 44\,189 \\ \bottomrule \end{tabular} \end{table} -Рост времени \texttt{filter} от N=256 к N=1024 составляет ≈5× для векторов (близко к $O(N)$) и ≈17× для плотной матрицы (близко к $O(N^2)$). Разрежённая матрица растёт медленнее, так как число ненулевых элементов линейно по N, а не квадратично. +\texttt{filter} рекурсивно обходит все узлы дерева, поэтому ожидается линейный рост для векторов ($O(N)$) и квадратичный для плотных матриц ($O(N^2)$). При увеличении N с 256 до 1024 время выросло в $\approx$5$\times$ для векторов и $\approx$17$\times$ для плотной матрицы, что согласуется с ожиданием. Разрежённые структуры растут медленнее, так как число ненулевых элементов линейно по N. \begin{table}[H] \centering @@ -161,7 +161,7 @@ \section{Экспериментальная оценка} \label{fig:filters} \end{figure} -Результаты \texttt{exists} и \texttt{forall} практически совпадают: при выбранных условиях short-circuit не срабатывает (худший случай), поэтому время соответствует $O(N^2)$ на плотных матрицах и $O(N+nnz)$ на разрежённых. В лучшем случае (первый же элемент удовлетворяет \texttt{exists} или не удовлетворяет \texttt{forall}) сложность составит $O(1)$. Выигрыш разрежённого представления (до 3× для векторов, до 15× для матриц) согласуется с отношением числа узлов полного дерева к числу занятых листьев. +\texttt{exists} и \texttt{forall} в худшем случае (полный обход) имеют ту же асимптотику, что и filter: $O(N)$ для векторов, $O(N^2)$ для плотных матриц. Разница между ними находится в пределах погрешности. При срабатывании короткого замыкания (первый же подходящий элемент в exists или неподходящий в forall) сложность падает до $O(1)$. Выигрыш разрежённого представления (до 3$\times$ для векторов и до 15$\times$ для матриц) объясняется меньшим числом обходимых узлов. \section{Заключение} @@ -171,7 +171,7 @@ \section{Заключение} \item Реализованы операции \texttt{filter}, \texttt{exists} и \texttt{forall} для разрежённых векторов и матриц на основе деревьев квадрантов. \item В \texttt{exists} и \texttt{forall} внедрено короткое замыкание, позволяющее завершать обход досрочно. \item Написаны 64 модульных теста для проверки корректности реализованных функций. - \item Бенчмарки подтвердили ожидаемую асимптотику: $O(N)$ для векторов, $O(N^2)$ для плотных матриц, $O(N+nnz)$ для разрежённых~--- выигрыш до $15\times$. + \item Проведены бенчмарки, подтверждающие ожидаемую масштабируемость: рост времени соответствует полному обходу дерева ($O(N)$ для векторов, $O(N^2)$ для матриц); выигрыш разрежённого представления~--- до $15\times$. \end{itemize} \begin{thebibliography}{99}