Сист 7

Теперь переходим к содержанию.

Мы будем вспоминать математическую логику, чтобы понимать, как работает SMT-солвер, а не просто смотреть на портянки кода на языке SMT-LIB. Для того чтобы понимать теоретическую базу под SMT, надо понимать теоретическую базу логики первого порядка, а именно: что такое сигнатура и алгебраическая структура.

Сигнатура первого порядка включает в себя функциональные символы, предикатные символы и константные символы, для каждого из которых задана арность. Задали сигнатуру — автоматически задали язык первого порядка, состоящий из термов, формул и кванторов. Подробно останавливаться на этом не будем, но важно обсудить, что в такой сигнатуре могут жить конкретные алгебраические структуры.

Алгебраическая структура в первую очередь начинается с множества-носителя. Сигнатура и структура никак не пересекаются, в сигнатуре не может быть элементов структуры, но для них должна быть задана интерпретация: куда отображаются функциональные символы, предикатные символы и константы.

Каждому функциональному символу ставится в соответствие соответствующая операция на носителе. Предикатному символу ставится в соответствие отношение на носителе, а константному символу — элемент носителя. Так задается интерпретация в структуре.

Понятие теории в контексте рассматриваемой темы задается через формулы языка, а именно предложения. Вспоминаются ранее изученные рабочие теории вроде групп, колец, полей и порядков.

Для арифметики Пресбургера предполагаемая модель, или структура (model), ради которой все и было придумано — это натуральные числа с нулем. Лектор отмечает, что это проговаривается не просто так, поскольку в СМТ-солверах это будет использоваться в качестве основы. При этом символ сложения используется как операция, и это тот же самый символ.

Арифметику Пресбургера можно описать через набор аксиом (например, порядка пяти штук), но можно поступить проще. Основное свойство арифметики Пресбургера заключается в том, что она является полной теорией. Проще всего построить полную теорию следующим образом: берется модель и рассматриваются все формулы, которые в этой модели истинны, что и дает полную теорию. Если мы знаем, что арифметика Пресбургера описывает соответствующую структуру, то вот она и есть. Для поставленных задач удобно смотреть именно так: выбрать структуру, взять все присущие ей формулы и сказать, что построена арифметика.

С алгоритмической, программистской точки зрения такая полная теория обладает очень важным полезным свойством — она разрешима. Разрешимость теории как множества означает, что существует алгоритм, которому можно на вход подать формулу, и он посмотрит и скажет, принадлежит ли эта формула теории. Если принадлежит, то она автоматически истинна в этой модели и во всех других моделях теории, а если не принадлежит — она в этой модели однозначно ложна. Таким образом, обсуждаются программистские свойства, позволяющие совершать полезные вычисления.

И еще чем бывает арифметика Пеано, как она устроена, какая у нее сигнатура. Можно добавить порядок, структура такая же. Арифметика Пеано — это вот такая штука... [неясный фрагмент] я беру модель, стандартную модель, и говорю: рассмотрю все формулы, истинные в стандартной модели арифметики Пеано. Показать, что если я рассмотрю теорию модели, я получу эту теорию, [неясный фрагмент]. Но я напишу — это не арифметика Пеано, это [неясный фрагмент]. Значит, о чем-то это нужно, и для того чтобы... а вот вопрос в реальности: программистам нужна именно эта теория, а не Пеано. Как видно, у этой теории есть название, ее можно назвать... здесь будет не она, это называется не [неясный фрагмент] арифметика [возможная ошибка распознавания: не арифметика Пресбургера или аналогичная], и мы их подробно разберем, когда поговорим о... [неясный фрагмент] только-только когда мы вспоминаем базовый курс матводики, который был у всех, который все радостно сдали...

Арифметика Пеано описывается [неясный фрагмент] набором аксиом, и собственно все. Так вот, давайте поговорим, вот эта теория — она разрешима или нет? Понятно, что она полна просто потому, что эта теория модели она разрешима, то есть что значит: существует алгоритм, которому мы на вход подаем формулу в такой сигнатуре, и она говорит, истинна она или нет. На самом деле хороший вопрос: есть какие-то более фундаментальные свойства, которые мы проходили, которые мешают ей быть разрешимой? Подробно мы с вами их не разбирали, но я вкратце упоминал, что мешает ей быть разрешимой. Как назвать теорему? Близко, но не совсем. Гёдель говорит, что у нас арифметика Пеано, как она есть, она не полна, если она непротиворечива. Это теорема Тарского... [неясный фрагмент] и неразрешима... [неясный фрагмент] теорема [неясный фрагмент] Тарского. Так что у нас есть арифметика Пресбургера, арифметика Пеано, есть арифметика Робинсона — ну вот это...

Обязательно нужно разобрать парочку примеров. Понятно, что произошло: я просто взял не натуральные числа, взял сейчас напрямую [неясный фрагмент].

[неясный фрагмент] описывают геометрию. Это обычно привычная знакомая вам геометрия: помните, нам всякие треугольники рисовали, отрезки, теоремы доказывать, подобие треугольников и так далее. Все эти задачи, все теоремы записать на этом языке — есть алгоритм, который их разрешает. Но, к сожалению, алгоритм работает за какое-то безумное время, там, по-моему, башня экспонент, тут точно не буду говорить и не уверен. И короче, вот геометрия вся эта школьная, вы знаете, она вырождается вот сюда, здесь все разрешено, то есть задач неразрешимых в геометрии, которые выражаются в таком языке, не бывает. В этом смысле геометрия очень такая простая, что мы тоже будем работать, я не помню, рассказывали ли на матлогике, ну вот сейчас будет пригодиться, вспомнили или нет.

[неясный фрагмент] рассматривает вещественные [числа]. Понятное дело, что вещественное число мы не запишем, вот приходится [работать] с тем, что есть. Рациональные числа в этом смысле гораздо хуже, чем вещественные. [неясный фрагмент] вещественные разрешимы, а рациональные нет, потому что мы можем написать вот так, и [такие] уравнения [неясный фрагмент] называются диофантовы, и внезапно выясняется, что мы не можем его решить. Помните результат Матиясевича, десятая проблема Гильберта и все такое? Вот с рациональными здесь все очень плохо. А в вещественных... [неясный фрагмент] поможет избавиться от знаменателей, там все получится. Так, какая за этим [неясный фрагмент]

Стоит теория, теория называется MSFOL (Many-Sorted First-Order Logic). Вот те языки первого порядка, которые мы изучали до этого, это FOL (First-Order Logic), а MSFOL — это multi-sorted first-order logic. Что это значит и зачем это надо? Если в обычных языках домен был всегда один, одно множество, то здесь нет, здесь у нас может быть несколько доменов, и функции действуют как-то между ними.

Каноническим примером является линейное пространство. Мы знаем, что всякие группы, кольца, поля, упорядоченные множества идеально ложатся на структуру первого порядка. А с линейным пространством ситуация выглядит не так просто, потому что с одной стороны у нас есть векторы как элементы, а с другой стороны — элементы поля. И операции, которые мы совершаем, задействуют и элементы поля, и векторы. Например, если вспомнить правила дистрибутивности, то один плюсик относится к пространству, а другие элементы — это числа. Возникает вопрос: а что тогда взять за носитель? Кто у нас является носителем?

Есть несколько способов с этим бороться. Один из них лектор уже рассказывал ранее, и теперь предлагает студентам вспомнить и рассказать, как он работает, и как мы пытаемся линейное пространство запихнуть в структуру первого порядка. В диалоге со студентами отмечается, что здесь никто не говорит, что пространство обязательно конечномерно, рассматривается бесконечномерное пространство.

Канонический способ борьбы с этой сложностью заключается в следующем. Мы заводим операцию плюсик, которая определена на векторах, а в качестве операций умножения на скаляр — точнее, их семейства — для каждого элемента поля мы заводим отдельную унарную операцию умножения. Вот так у нас получается бесконечная сигнатура, которая к тому же еще и от поля зависит. И если мы так сделаем, то подобные соотношения просто выражаются через эти операции: одна операция и другая операция. То есть у нас число является элементом поля [неясный фрагмент] [возможная ошибка распознавания: при сомнении других тогда мы запишем такую вспомнили пышки ок когда делать помощью мансо].

Тут давайте мы просто скажем, что у нас есть объекты двух типов, двух сортов: отдельно чиселки — элементы поля, и отдельная — векторы. Как это будет выглядеть в сигнатуре? Мы заводим семейство сортов — пока это просто какие-то символы, бесконечный счетный или произвольный набор, главное, чтобы он был непустым, чтобы нам было с чем работать. При интерпретации они попадают в какие-то множества, в домены. То есть сорт — это просто символ, а при интерпретации они попадают в множество. В нашем случае у нас два сорта: числа и векторы.

Дальше у нас есть функциональные символы. С каждым функциональным символом, как мы помним, связана арность — его местность. Дополнительно скажем, что каждому символу мы налепим тип. То есть у плюсика у нас будет такой тип: он действует из $V \times V$ в $V$ (если это сложение векторов). Еще раз: есть плюсик полей, он как действует? Он берет два элемента поля и складывает их, давая элемент поля. А еще у нас есть умножение вектора на элемент поля, оно действует так: из поля и вектора в вектор.

Когда мы их интерпретируем в честные операции, у нас получается, что эта операция должна действовать из соответствующих доменов. То есть домен $D_1$, домен $D_2$, и выходит, что это векторы и поле. По сути, получается такой язык первого порядка с типами.

Что-то аналогичное делается здесь: мы заводим разные объекты, сорта, и наворачиваем типы. Только в отличие от ML, у нас типы здесь очень простые, мы не комбинируем их сложным образом. Если мы возьмем несколько векторов и их сложим, должен получиться снова вектор. Функциональные символы у нас работают внутри термов, мы не порождаем сложные типы со множеством комбинаций, всё проще.

SMT теоретически строится на модели теории. У нас есть какой-то набор заранее заготовленных теорий, которые чем-то очень напоминают те, что мы вначале писали. Если их выписать, то мы рассматриваем целые числа — это носитель, операции «плюс», сравнение, и в качестве констант возьмем те же целые числа, потому что так проще, и на самом деле вот так обычно с этим и работают. Это очень похоже на арифметику Пресбургера, только на целых числах, и она называется LIA — Linear Integer Arithmetic (линейная арифметика целых чисел).

Мы пишем какую-то формулу в сигнатуре, которая соответствует модели. Там есть какие-то свободные переменные, и мы спрашиваем товарища SMT-солвера: «Существует такой набор переменных, который эту формулу делает истинной?». На что он говорит: «Да, есть» или «Нет, нет». Эта теория разрешима, теория этой модели будет разрешимой, поэтому алгоритм существует. Когда солвер говорит «да», он не просто отвечает утвердительно, он еще предъявляет конкретный набор примеров. Например, мы говорим товарищу SMT: «Дай мне, пожалуйста, такой $x$, чтобы $x + \dots$», и он выдает откуда-то, например, пяткерку. Можно взять более сложные вещи, но с такой арифметикой пока ничего не было.

Возникает вопрос: почему она называется «линейной»? Про арифметику Пресбургера такого не говорят, а здесь говорят. Линейность — это однородность и аддитивность. Аддитивность здесь понятна, потому что мы складываем. А где прячется однородность? Студенты предлагают варианты: умножение на коэффициенты. Возникает вопрос, какие коэффициенты и откуда они берутся, откуда константы берутся, а умножать на них нельзя, запрещено. Для однородности нужно умножение. И собственно, однородность она прямо говорит про умножение. Давайте посмотрим на термы, как устроены термы, переменные. А теперь давайте это всё приведем к общему члену, добавим, например, $2y$ и получим $2x + 3z$. Является ли это линейным выражением, линейной комбинацией? Да, это линейная комбинация над $x, y, z$ и единичкой. На самом деле никакого умножения на двойку в этой теории нету, это просто сокращенная запись, но в реальности мы работаем с этим. Писать по-другому грустно, все пишут так, поэтому она называется линейной, а под капотом там идет умножение на скаляр. Так это вот первая арифметика, с которой мы работаем.

Далее рассматривается умножение, и такая штука называется, угадайте как, NIA (Nonlinear Integer Arithmetic), поэтому она нелинейная целочисленная арифметика. Она неразрешима по тем же причинам, по которым была неразрешима [неясный фрагмент].

Затем лектор переходит к арифметике вещественных чисел. С рациональными числами всё обстоит очень грустно, еще и деление появляется. Как это называется, угадайте на самом деле, знать не обязательно — это Tarski (Tarski's algebra / теория Тарского), она разрешима, ну потому что геометрия [неясный фрагмент] часть его продает [возможная ошибка распознавания: порождает], деление [неясный фрагмент].

Теперь, если стереть умножение, получается LRA (Linear Real Arithmetic), она тоже разрешима и хороша. То есть мы видели такую тусовку: LRA, NIA, NRA (Nonlinear Real Arithmetic). В вещественных [неясный фрагмент] NRA тоже разрешима, а в целых [неясный фрагмент] участвовать сходу не уверен, к лекции не готовился.

Ещё бывает вот что, не в теории правда, а скорее в тех формулах, которые мы подаем на солвер. Замечание: у нас же это типа язык первого порядка, там есть кванторы, и я могу задать такое выражение: «существует x такой, что x плюс x равно 5». Вообще, формально я могу, но по-хорошему мы где-то вначале говорим, что мы работаем в такой-то теории. Прежде чем написать квантор ∃x, я должен написать, какого сорта у этого x, то есть на самом деле здесь написано что-то вроде int x такой-то. Вот такие конструкции с ними солверы работают очень плохо. Обычно солверы требуют, чтобы те формулы, которые мы подаем им на вход, квантеров не содержали. Поэтому здесь в реальности написано такое, что QF (что не значит, что теория безквантовая, это значит, что формулы на вход подают в солвер, и они не содержат квантеры, при этом работа в этой теории может задаваться, может не задаваться). По-хорошему солверы угадывают, в какой теории мы работаем, но обычно по-хорошему нужно писать то, что нам генератор тогда не спасёт сам. Про кванторы я не помню, в SMT такого не пишется, потому что обычно SMT, которые сейчас в природе, кванторов не содержат [возможная ошибка распознавания: бывает она не пишется], потому что мы вначале пишем declare-const x какого-то потом типа, а его используем, а не пишется «существует x там типа int» или что-то подобное. Это не совсем честный [неясный фрагмент], это скорее оно дальше. Следующая очень важная теория, которая капец как важна для программистов...

Мы не работаем с интеджерами в прямом смысле этого слова, с целым числом, мы работаем с чем? С векторами. Теория битовых векторов (Bit-vectors) — это первая теория [неясный фрагмент]. Здесь у нас есть бесконечно много сортов, они собственно так и называются: битвектор 1, битвектор 2. Мы фиксируем длину вектора, рассматриваем все вектора, и они населяют один сорт. Берем другую длину — эти вектора населяют другой сорт. И тогда что они умеют делать? Они умеют все эти побитовые логические операции, которые вы привыкли делать: их можно складывать, их можно умножать, их можно сдвигать, можно проводить побитовые операции и так далее. [неясный фрагмент] со знаком или без знака, сейчас разберемся.

Ну еще есть булева логика, по сути это не совсем [возможная ошибка распознавания: булева логика], содержательно это одно и то же, но это просто другой [неясный фрагмент] объект один и тот же. Так вот, булева логика по сути это обычный язык высказываний, их решает SAT-solver, собственно в SMT-solver под капотом встроен SAT-solver. Теперь давайте [неясный фрагмент] в эти солверы.

Мы уже посмотрели на язык SMT-lib, который представляет собой Lisp-подобный выровнеглазный язык [возможная ошибка распознавания: Lisp-подобный язык]. Писать на нём мы подробно не будем, потому что писать хочется на Питоне.

В качестве основного инструмента мы будем пользоваться солвером, который называется Z3. Это сейчас фактически SMT-солвер де-факто, который поддерживает Microsoft (Microsoft Research). Помимо него, есть куча других солверов, например CVC4 [возможная ошибка распознавания], а также Boolector, который заточен именно на теории битовых векторов. Те, кто занимается системами на языке Verilog, наверное, что-то слышали о нём, так как его любят инженеры, работающие с Verilog. Существует множество самых разных SMT-солверов, постоянно выходят новые версии (например, уже появилась версия 4.5, это прикольно), но в рамках курса демонстрироваться будет именно Z3, с помощью которого мы и начнем стандартную работу.

Для демонстрации базовой работы с Z3 создадим экземпляр солвера. Давайте сделаем что-нибудь простое: заведем переменную x, допустим, у нас будет тип int, и мы спросим у солвера, существует ли такое x, для которого x плюс x равно, давайте сначала, 10.

Что здесь произошло? Сначала я объявил какой-то новый символ: x = Int('x'). Символ x, сорт x. То, что в скобочках ('x') — это внутреннее представление для Z3, то, что у него там в строковом виде, а x — это просто переменная, которую я завёл в Питоне. Затем мы добавляем условие: s.add(x + x == 10). Метод add — это добавление некоторого утверждения в нашу теорию, то есть мы считаем, что это должно быть истинно. И спрашиваем у солвера, бывает ли вообще такое с помощью команды s.check().

Здесь на самом деле нет ни одной питоновской операции, все они перегружены в Z3, то есть здесь написано выражение на языке Z3. Когда мы вызываем s.check(), солвер отвечает sat (satisfiable), то есть да, такое бывает. Если мы хотим предъявить само решение, нужно вызвать s.model(). Солвер выдает модель, например, что кси [возможная ошибка распознавания: х] равен пяти, то есть он находит конкретное значение.

Теперь давайте изменим условие и попробуем записать x + x == 5. Бывает ли такое? Солвер отвечает unsat (unsatisfiable), то есть говорит, что решений нет.

Что еще интересного? А давайте вот так сделаем: бывает ли такое, что x равен минус x (x == -x)? Солвер отвечает, что да, бывает (при x = 0).

А давайте я усложню сорт. Тот int, который работает под капотом Z3 — это не питоновский int [неясный фрагмент]. В Питоне целые числа по умолчанию бесконечные, либо там надо что-то включать, а в Z3 это полноценная математическая теория целых чисел. И если добавить еще какие-то ограничения, солвер продолжит работать с ними в рамках своей теории.

Мотивационный программистский пример показывает, как в реальной жизни даже в суперкрутых инвестиционных программах встречаются баги. Рассматривается следующий код: если x < 0, то x = -x, после чего утверждается, что x всегда больше или равен нулю. Лектор напоминает, что такое поведение обсуждалось на первом курсе на матанализе или информатике.

Возникает вопрос, всегда ли это утверждение верно. С целыми числами в математическом смысле такого действительно никогда не бывает, но с целыми числами в компьютерах, которые на самом деле являются битовыми векторами (BitVec), ситуация выглядит иначе. Возникает задача найти такой x, на котором это утверждение нарушается, используя Z3.

Для проверки с помощью Z3 импортируется библиотека z3. Задаётся вопрос о сорте переменной x, и для простоты выбирается 8-битный знаковый битовый вектор (BitVec('x', 8)). Мы хотим найти такой x, для которого проверяемый код ведёт себя неожиданно, то есть исследуется условие, где x < 0, затем x = -x, и проверяется утверждение о значении результата. Лектор отмечает [неясный фрагмент] касательно точного синтаксиса работы со знаками и битовыми векторами в данном эксперименте.

Обсуждая анализ решения и причины переполнения битового вектора, лектор разбирает работу с solver [возможная ошибка распознавания: SMT-solver], который находит такое значение x, при котором возникают определенные особенности или проблемы. Если изначально взять битовый вектор небольшой длиности, например, восьмибитный, то его представление в виде числа интуитивно понятно. Однако, если размерность увеличивается, приходится выполнять дополнительные действия: брать модель, запрашивать значение x из модели и пытаться вручную понять, почему получается именно такой результат и почему конкретное значение x приводит к определенному примеру.

Проверяя поведение операций на примере, лектор рассматривает ситуацию с инвертированием чисел и получением отрицательных значений через дополнительный код. Если проинвертировать число, нарисованное на экране, получается ноль и куча единиц. Подобным образом, если задать solver-у условие вроде равенства битового вектора самому себе с отрицательным знаком ($x = -x$), он закономерно выдает ноль, но при усложнении формул находятся другие интересные краевые случаи.

Лектор подчеркивает важность этого анализа: это не просто игрушечный пример, хотя сам пример выглядит простым, подобные ситуации реально встречаются на практике. Затем приводится другой пример из жизни, очень полезный для программистов. Иногда возникает желание написать определенные выражения, например, когда производится деление на двойки, четверки и так далее с помощью битовых сдвигов или арифметических операций. Лектор задает аудитории вопрос о том, как такие вещи пишет нормальный программист, и предлагает подумать, где здесь кроется подвох.

Этому обычно детишек учат писать, ну вот эти дети... У нас есть там деление, но деление — операция долгая, давайте делать сдвиг теперь, одно и то же. Ну а вот нифига. Давайте попросим умного: за минус один сломается, да? Ну, деление должно давать ноль, а сдвиг дает минус один. А вот вы знали этот пример? Вы знали этот пример или прямо сейчас его нашли? А что? А вы знаете, отлично. Кто еще? Какой-то не новость, что вот это не хвалит операции. Вот давайте представим, что мы этого не знаем. Так, ну первая операция у нас те же самые. Так, что делать дальше? Нет, битвек — ну давайте такого же размера, чтобы не купаться. Так, давайте другой будет работать, а то когда вот раз, два, вот мы такого гада и нашли.

Вот минус единица как раз то самое. На самом деле это работает для любого отрицательного нечетного числа. Ну, давайте пускать, все подумают, я тоже подумаю. Это, видимо, минус три — это сколько будет? Да, минус он будет округлять вверх или на каком смысле? Округляет вниз, только вот не тот низ, как там, что хочется. Так, третий пример — это тоже [неясный фрагмент].

Реальный пример из Java, находившийся в стандартной библиотеке. Пусть у нас есть большой массив с целочисленными индексами, по которому мы можем делать операцию, которая называется бинарный поиск. Мы рассказывали вам такое? Смотрите, вот у нас есть левая граница, вот у нас есть правая граница. Как найти серединку? Это простой вопрос. [неясный фрагмент] правое минус левое — это длина, а нам нужен самый... [неясный фрагмент] $l + r$ пополам, да? Канонический — это вот ответ на несколько вещей, которые все пишут. Вспомнили, да? Никита шарит. А почему это неправильно? Давайте напишем, а потом поймем, почему нужно не так. [неясный фрагмент] как писать надо.

Действительно, отсюда мораль: для всех индексов массива используйте тип size_t, short и int использовать не надо, к тому же беззнаковый. Кто? unsigned, без знака. Но как это вот так вот пишут умные ребята, программисты пишут так, как обычно будет for (int i = 0...). Сейчас, наверное, уже переучили, да? Ну, если сейчас... Как сейчас, я видел вот такой код тоже, и сам так писал, причем у меня не просто счетчик цикла, у меня именно индекс массива вот так. Если маленький — то ладно, если большой — то приколы. Давайте это собственно... [неясный фрагмент]

Мы хотим найти такие числа, чтобы операция приводила к переполнению. На самом деле всё это можно написать в одну строчку, но код пишется по отдельности для простоты, чтобы не запутаться. Нам нужно сделать так, чтобы значения вылетали за границы диапазона, поэтому требуется проверить, что результат не лежит между границами, или записать условие через оператор or: либо значение меньше нижней границы l, либо правая часть больше верхней границы, либо выполняются другие условия, включая то, что l меньше r.

В качестве примера рассмотрим вычисления: если взять числа 207 и 136, то их сумма равна 341. [неясный фрагмент] Если вычесть 256, получаем 87. Деля 87 пополам, получаем 43 с небольшим. Даже если написать unsigned, к хорошему это не приведет. Время лекции еще осталось, а подготовленные примеры закончились.

Далее лектор переходит к обсуждению сюжета мифа об Эдипе для формулировки логической задачи. Вспоминаются действующие лица: Эдип, Иокаста, Лай, Полиник и другие персонажи. Известно, что Эдип — убийца, а требуется доказать или вывести на основе условий, кем приходится Иокаста Эдипу (родители Эдипа, жена и так далее). В процессе обсуждения восстанавливаются детали мифа: ехал царь Лай, ехал или шел по дороге Эдип, они что-то не поделили, Лай ударил Эдипа палкой, тому не понравилось, и он ответил [неясный фрагмент], что является классикой мировой литературы и касается отца Эдипа.

Далее лектор переходит к вопросу о том, как породить новый sort, поскольку стандартных типов вроде int недостаточно, и упоминает создание отдельного сорта, например human. [неясный фрагмент] сорт, так мы его назовем, он может там greek [неясный фрагмент], и массив, после чего происходит возвращение к основному материалу.

Для объявления предикатов требуется использовать предикатный символ, который задается как функция vbl. В процессе работы могут возникать вопросы именования, например, при поиске обозначения для таких понятий, как отцеубийца, когда обсуждается соответствующий термин на английском языке или сорт.

Далее задаются конкретные предикаты и факты о персонажах. Например, предикат parent принимает пару элементов типа human и определяет отношение родительской связи. В качестве примеров фактов вводятся отношения между персонажами мифов: Эдип является родителем Полиника, а Лай (в транскрипте ошибочно названный «клиник») является родителем Эдипа, или другие родственные связи с участием персонажей вроде Ферсандра [возможная ошибка распознавания: Ферсандра]. При работе с автодополнением и синтаксисом важно учитывать особенности работы инструментов, чтобы избежать ошибок перегрузки предикатов.

Далее лектор переходит к проверке отношений и поиску родственников, упоминая Иокасту (в транскрипте — "е каста"), которая является родительницей отцеубийцы (Эдипа), который в свою очередь является родителем... [неясный фрагмент]. Лектор рассуждает о том, как сформулировать и проверить отношения: кто является родителем Эдипа, кто отец-убийца, и проверяет запрос через систему («набили, сад, ура, значит действительно окажется такой»).

Затем лектор задается вопросом, кто у нас так и [неясный фрагмент], и обнаруживает ошибку: «Или где-то я накосячил? Почему-то он считает, что... так, x — это e. Почему-то он считает, что... да, что Иокаста... да, это... почему? Нет, x — это родитель, первый родитель. Да, вот наверху написано. Иокаст — родитель [неясный фрагмент], Иокаст — родитель пыльника. Ну вот x — родитель [неясный фрагмент]. Видимо, этот [неясный фрагмент] не понимает, что это отношение несимметрично немножко».

Лектор предлагает научить систему и задумывается, как объяснить отношение: «Можно просто сказать. Implies. Implies [неясный фрагмент] ладно, напишут просто [неясный фрагмент] not not [неясный фрагмент] или какие-то конкретные а ну да кстати да да да уже так написать что не можем я не умею сходу писать нет вот вот это он не [неясный фрагмент]».

[неясный фрагмент] [возможная ошибка распознавания: древний грек] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент] [неясный фрагмент]