раздел 44

Логика и типы

Курс от школьной алгебры до книги Пирса «Types and Programming Languages». Ты стажёр Седьмого отдела в портовом Сольске: машина Арбитр, которая тридцать лет помогает суду, впервые зависла на деле, а на первой странице её Кодекса написано, почему так не бывает. Чтобы закрыть дело, научишься разбирать показания формулами, искать контрпримеры, писать доказательства, которые принимает судья, собирать вычислитель и интерпретатор λ-исчисления на Haskell и проверять типы. Финал: читаешь Кодекс целиком и доказываешь, что допущенное дело не зависает. Формулы и выводы проверяет движок прямо в браузере, доказательства читает строгий AI-судья.

81 урок81 тем · 13 кластеров

Начать раздел

Хочу пройти

Без входа у каждого урока видно начало. Войди, чтобы читать целиком, отмечать пройденное и решать задачи. войти

«Логика и типы» покупается один раз и остаётся навсегда: 500 ₽. Оплата пока не подключена, доступ открывается промокодом. ввести промокод

Уроки раздела

Начать раздел

Понятия курса

Понятия разобраны внутри уроков. Нажми на понятие, чтобы открыть урок, где оно объясняется.

Допросы: высказывания

Босс: три свидетеля у переулкаТри свидетеля ночи кражи, часть из них лжёт. Формализовать показания, найти единственный непротиворечивый вариант и объяснить ответ судье.урок 7 · Босс: три свидетеля у переулкаопираются: урок 8
Высказывания и связкиВысказывание как утверждение, которое истинно или ложно. Связки ¬, ∧, ∨, →, ↔ и перевод показаний с русского: «если», «только если», «либо», «ни ... ни».урок 2 · Высказывания и связкиопираются: урок 3
Дело Арбитра: зачем учить логикуМашина суда Сольска зависла, а Кодекс обещает, что так не бывает. Как устроен курс, кто такие Сомова, Вельский и судья, и первое учебное дело о правдивом и лжеце, решённое перебором случаев.урок 1 · Дело Арбитра: зачем учить логикуопираются: урок 2
Нормальные формыКНФ и ДНФ: любую формулу можно записать как список требований или как список сценариев. Функциональная полнота и одна связка NAND, из которой собирается всё.урок 5 · Нормальные формыопираются: урок 6
Равносильные формулыЗаконы де Моргана, дистрибутивность, импликация через ¬A ∨ B и контрапозиция. Как поймать подмену смысла при пересказе и почему ложь влечёт что угодно.урок 4 · Равносильные формулыопираются: урок 5
Таблицы истинностиТаблица как перебор всех случаев. Тавтология, выполнимость, противоречие и следование; строка-контрмодель как доказательство того, что следования нет.урок 3 · Таблицы истинностиопираются: урок 4, урок 79
SAT и DPLLЗадача выполнимости: когда строк в таблице слишком много. Резолюция, единичные дизъюнкты, чистые литералы и откат в алгоритме DPLL; расписание дежурств как SAT.урок 6 · SAT и DPLLопираются: урок 7

Устав порта: предикаты и кванторы

Босс: устав противоречит сам себеСемь пунктов устава порта: формализовать, найти модель, где выполнены все, или показать, что её нет, и решить, какой пункт убрать.урок 13 · Босс: устав противоречит сам себеопираются: урок 14, урок 78
Модели и общезначимостьИстинно в модели, выполнимо, общезначимо. Знак ⊨ и контрмодель как способ опровергнуть следование.урок 11 · Модели и общезначимость: истинно где?опираются: урок 12, урок 79
Отрицание кванторов и играОтрицание переворачивает ∀ в ∃ и обратно; порядок кванторов меняет смысл. Игра верификатора и фальсификатора: кто выигрывает, тот и прав.урок 10 · Отрицание и игра: докажи или опровергниопираются: урок 11
Перевод с кванторамиПункты устава порта в формулы и обратно. Ловушки ∀x (P → Q) против ∀x (P ∧ Q) и ∃x (P ∧ Q) против ∃x (P → Q).урок 9 · Перевод с кванторами: устав порта в формулахопираются: урок 10
Предикаты и кванторыСвойства и отношения вместо отдельных высказываний. Домен, кванторы ∀ и ∃ и как проверить формулу на картинке-модели склада.урок 8 · Предикаты и кванторы: «все» и «кто-то»опираются: урок 9
Свободные и связанные переменныеКакая переменная к какому квантору относится, подстановка терма вместо переменной и захват. Первый шаг к λ-исчислению.урок 12 · Свободные и связанные переменные: кто такой «он»опираются: урок 13, урок 44

Картотека: множества и отношения

ЗамыканияРефлексивное, симметричное и транзитивное замыкание по шагам. R* как «за ноль или больше шагов», то самое ⟶* из TAPL.урок 19 · Замыкания: у кого мог оказаться ключопираются: урок 20, урок 77
Кортежи и отношенияУпорядоченные пары и кортежи, декартово произведение, отношение как множество пар и отношения на нескольких местах.урок 15 · Кортежи и отношения: карточки связейопираются: урок 16
МножестваМножество, элемент, подмножество, объединение, пересечение, разность и множество подмножеств. Запись {x ∈ S | P(x)} и связь операций со связками.урок 14 · Множества: картотека Тимофея Ильичаопираются: урок 15
ПорядкиПредпорядок, частичный и линейный порядок, наибольший и максимальный элементы, верхние грани и решётки; подтипы как порядок.урок 17 · Порядки: кто старше по допускуопираются: урок 18
Свойства отношений и эквивалентностьРефлексивность, симметричность, транзитивность и антисимметричность. Отношение эквивалентности и классы: бригады, работавшие в одну смену.урок 16 · Свойства отношений и эквивалентность: бригадыопираются: урок 17, урок 72
Счётность и диагональСчётные и несчётные множества, диагональный аргумент Кантора и почему любая проверка типов неизбежно отвергает часть хороших программ.урок 20 · Счётность и диагональ: дело, которого нет в спискеопираются: урок 21
ФункцииФункция как отношение, где у каждого входа один выход. Тотальные и частичные функции, инъекции, сюръекции, биекции и композиция.урок 18 · Функции: у каждого ключа один владелецопираются: урок 19

Слушание: доказательства

Босс: предварительное слушаниеТри теоремы о картотеке у судьи Грановича: какой ключ получил Прохор, почему в замыкании нет лишних пар и почему ключ не мог быть в двух руках сразу.урок 25 · Босс: предварительное слушаниеопираются: урок 26
Как писать доказательствоДоказательство, которое проверит другой человек: дано и нужно, объявленный метод, шаг с обоснованием, итог. Типичные дыры: пример вместо общего случая, обратная стрелка, «аналогично», потерянный случай.урок 24 · Как писать доказательство: записка для судьиопираются: урок 25
Как читать математический текстОпределение, лемма, теорема и следствие; посылки и заключение; «пусть» и «возьмём произвольный». Почему «если» в определении значит «тогда и только тогда» и как читать страницу TAPL.урок 21 · Как читать математический текстопираются: урок 22
Кванторы в доказательствахКак доказать «для всех» через произвольный элемент, «существует» через свидетеля и как опровергнуть то и другое: контрпример и доказательство отрицания.урок 23 · Кванторы в доказательствах: пять утверждений Вельскогоопираются: урок 24
Способы доказательстваПрямое доказательство, контрапозиция, доказательство от противного и разбор случаев на примерах про чётность и делимость и на алиби грузчика.урок 22 · Способы доказательства: алиби тремя путямиопираются: урок 23

Цепочка улик: индукция

Босс: опись вложенных уликТип термов и функции над ним на Haskell, затем доказательство у судьи: различных констант в терме не больше, чем его размер (TAPL 3.3.3).урок 31 · Босс: опись вложенных уликопираются: урок 32
Индуктивные определенияМножество термов TAPL гл. 3 как наименьшее множество, замкнутое по правилам. Три равносильных определения из TAPL 3.2: словами, правилами вывода и по этажам S₀, S₁, S₂.урок 28 · Индуктивные определения: правильно оформленное делоопираются: урок 29
Индукция по выводуУтверждение о каждом выводимом суждении доказывается по последнему правилу вывода: по случаю на правило, гипотеза для посылок. Главный инструмент доказательств в TAPL.урок 30 · Индукция по выводу: лист из блокнота Арбенинойопираются: урок 31, урок 40
Математическая индукцияБаза и шаг индукции как ряд домино. Доказательство формулы для любого n и разбор ложной индукции «все лошади одного цвета»: где рвётся цепочка.урок 26 · Индукция: все грузчики заодно?опираются: урок 27
Сильная индукция и фундированные отношенияСильная индукция опирается на все меньшие случаи сразу. Фундированные отношения без бесконечных спусков, почему рекурсия завершается и почему алгоритм Евклида останавливается.урок 27 · Сильная индукция: кончится ли описьопираются: урок 28
Структурная рекурсия и структурная индукцияФункции size, depth и consts над термами, определённые по их устройству, и доказательства по устройству терма. Первая программа на Haskell: алгебраический тип, сопоставление с образцом, рекурсия.урок 29 · Структурная рекурсия: первая программа отделаопираются: урок 30

Протокол: правила вывода

Босс: опечатанные протоколыСвоя система правил для правильно вложенных печатей: выводы в чужой системе, своя система на языке правил и доказательство, что выводится ровно то, что нужно.урок 37 · Босс: опечатанные протоколыопираются: урок 38
Деревья выводаВывод как дерево из экземпляров правил: корень внизу, аксиомы в листьях. Построение снизу вверх и почему лист без правила это не доказательство.урок 33 · Деревья вывода: ступенька за ступенькойопираются: урок 34
Корректность и полнотаВыводимость ⊢ и следование ⊨. Корректность: выводится только истинное. Полнота: выводится всё истинное. Корректность правила как сохранение истины.урок 36 · Корректность и полнота: только правда и вся правдаопираются: урок 37
Натуральная дедукцияПравила введения и удаления для ∧, ∨, →, ¬ и ⊥, допущения и подвыводы, запись Фитча. Равносильности выводом вместо таблиц.урок 34 · Натуральная дедукция: протокол, где каждая строка по правилуопираются: урок 35, урок 78
Правила для кванторовВведение и удаление ∀ и ∃. Условие на произвольное имя в ∀I и на новое имя в ∃E, и почему из одного примера нельзя вывести «для всех».урок 35 · Правила для кванторов: произвольный грузчик и безымянный свидетельопираются: урок 36
Суждения и правила выводаСуждение, правило с чертой: посылки сверху, заключение снизу. Метапеременные, аксиомы, экземпляр правила и как читать правило вслух.урок 32 · Суждения и правила: черта в блокноте Арбенинойопираются: урок 33

Машинный зал: вычисление

Абстрактный и конкретный синтаксисСтрока и дерево: конкретный синтаксис для людей, абстрактный для машины. Грамматика BNF как алгебраический тип данных, печать дерева со скобками.урок 38 · Абстрактный синтаксис: лента и деревоопираются: урок 39
Босс: воспроизвести зависаниеВычислитель Arith из TAPL гл. 4 целиком: шаг, дорога до нормальной формы, вердикт или застрявший терм и место, где дело застряло.урок 42 · Босс: воспроизвести зависаниеопираются: урок 43
Вычисление большим шагомОтношение t ⇓ v и правила B-Value, B-IfTrue, B-Succ и другие (TAPL упр. 3.5.17). Согласие с малым шагом на значениях и чем они различаются на застрявших термах.урок 41 · Большой шаг: вердикт одним махомопираются: урок 42
Вычисление малым шагомОтношение t ⟶ t′ и правила E-IfTrue, E-IfFalse, E-If, E-Succ, E-Pred и E-IsZero (TAPL рис. 3-1, 3-2): дерево вывода одного шага и функция eval1 на Haskell.урок 39 · Малый шаг: как Арбитр переписывает делоопираются: урок 40, урок 45
Значения, нормальные формы и застрявшие термыЗначение, нормальная форма, застрявший терм и многошаговое вычисление t ⟶* t′. Детерминизм одного шага (TAPL 3.5.4) индукцией по выводу.урок 40 · Значения и застрявшие термы: у зависания есть имяопираются: урок 41

Шифр Арбениной: λ-исчисление

Босс: подделка доверенностиИнтерпретатор бестипового λ-исчисления по TAPL гл. 7: имена в индексы, сдвиг, подстановка и вычисление по значению. Разоблачение поддельной доверенности.урок 48 · Босс: подделка доверенностиопираются: урок 49
Индексы де БрёйнаБезымянные термы: переменная как число λ до своей. Контекст для свободных переменных, сдвиг ↑ и подстановка [j ↦ s] по TAPL гл. 6.урок 47 · Индексы де Брёйна: имена, которые нельзя подменитьопираются: урок 48
Кодировки ЧёрчаБулевы значения, условие, пары и натуральные числа из одних функций: tru, fls, test, pair, числа Чёрча, scc, plus, times и iszro.урок 46 · Кодировки Чёрча: числа и «да/нет» из одних функцийопираются: урок 48
Подстановка без захватаСвободные переменные терма, α-эквивалентность и подстановка [x ↦ s] t с переименованием связанной переменной. Как захват имени меняет смысл документа.урок 44 · Подстановка без захвата: поддельная доверенностьопираются: урок 45, урок 47
Синтаксис λ-исчисленияТри вида термов: переменная, абстракция λx. t и применение. Функции как значения, каррирование, соглашения о скобках и первые шаги редукции руками.урок 43 · Синтаксис λ: поручение с пропускомопираются: урок 44
β-редукция и стратегии вычисленияРедекс и β-шаг. Полная β-редукция, нормальный порядок, вызов по имени и вызов по значению; терм Ω, который не завершается, и комбинатор неподвижной точки.урок 45 · β-редукция и стратегии: поручение, которое не кончаетсяопираются: урок 46

Допуск: типы

Безопасность: progress и preservationЛемма о канонических формах, теоремы progress и preservation для арифметики (TAPL 8.3) и почему вместе они значат «типизированный терм не застрянет».урок 50 · Безопасность: продвижение и сохранение типаопираются: урок 51
Босс I: Допуск снова работаетПроверка типов простого λ-исчисления с расширениями и реконструкция стёртых типов на Haskell: архив прогоняется через восстановленный Допуск.урок 57 · Босс I. Допуск снова работаетопираются: урок 58
Простое типизированное λ-исчислениеФункциональные типы T₁ → T₂, контекст Γ, правила T-Var, T-Abs, T-App и деревья типизации суждений Γ ⊢ t : T.урок 51 · Простое типизированное λ-исчисление: ярлык для порученияопираются: урок 52
Расширения: Unit, let, пары, записи, суммыUnit, let, пары и кортежи, записи, суммы и варианты: правила типизации и вычисления из главы 11 TAPL и как расширять проверку типов.урок 53 · Расширения: папки, описи и «либо одно, либо другое»опираются: урок 54
Реконструкция типов и унификацияПеременные типа и подстановки, генерация ограничений, унификация с проверкой вхождения и главные типы (TAPL гл. 22).урок 55 · Реконструкция типов: ярлыки, которые стёрлиопираются: урок 56
Типизированная арифметикаТипы Bool и Nat, отношение типизации t : T по правилам рис. 8-1 и 8-2 TAPL, деревья типизации и лемма инверсии.урок 49 · Типизированная арифметика: ярлык на каждой уликеопираются: урок 50
fix и нормализацияОбщая рекурсия через fix и что она стоит: без fix любой типизированный терм вычисляется до значения (сильная нормализация), с fix уже нет.урок 54 · fix и нормализация: почему Арбенина не дала машине «повторяй, пока не получится»опираются: урок 55
Let-полиморфизм и Хиндли-МилнерСхемы типов ∀a. T, обобщение в let и конкретизация при использовании; алгоритм W выводит главный тип без единой аннотации.урок 56 · Let-полиморфизм и Хиндли-Милнер: одна процедура на все уликиопираются: урок 57
Preservation и лемма подстановкиОслабление контекста, лемма подстановки и доказательство сохранения типа для простого λ-исчисления разбором случаев по выводу (TAPL 9.3).урок 52 · Сохранение типа и лемма подстановки: почему Допуск выключили зряопираются: урок 53

Механический прокурор: Curry-Howard и Lean

Интуиционистская логикаИнтерпретация BHK: доказательство как построение. Почему не выводятся A ∨ ¬A и ¬¬A → A, интуиционистская натуральная дедукция без RAA и модели Крипке с поиском контрмодели.урок 58 · Интуиционистская логика: а чем докажете, каким из двухопираются: урок 59, урок 71
Соответствие Карри-ГовардаТипы как высказывания, термы как доказательства, проверка типов как проверка доказательства (TAPL 9.4). Пары, суммы и функции против ∧, ∨ и →; β-редукция как устранение обходов; почему fix ломает логику.урок 59 · Curry-Howard: типы как высказывания, программы как доказательстваопираются: урок 60, урок 64
Финал: Кодекс прочитанРис. 9-1 TAPL целиком, лемма о канонических формах и progress для простого типизированного λ-исчисления; безопасность из progress и preservation; что читать в TAPL дальше.урок 63 · Финал. Кодекс прочитан
Lean: арифметика и детерминизм шагаТермы арифметики как индуктивный тип, правила вычисления как индуктивное отношение, дерево шага как терм, лемма инверсии через cases и машинное доказательство детерминизма индукцией по выводу.урок 62 · Lean: арифметика Арбитра и детерминизм шагаопираются: урок 63
Lean: доказательства термамиПроверщик доказательств и его ядро, устройство теоремы в Lean, термы для ∧, ∨, →, ¬ и False, sorry и #print axioms, Classical.choice и конструктивные доказательства.урок 60 · Lean: доказательства термамиопираются: урок 61
Lean: тактики и индукцияЦели и тактики intro, exact, apply, constructor, cases, rw, rfl, omega; индуктивные типы и индукция по числам и спискам; доказательства, которые пишет модель, а проверяет ядро.урок 61 · Lean: тактики и индукцияопираются: урок 62, урок 80

Командировка на Монетный двор: субструктурные логики и ресурсы

Аффинная логика и владение в RustMove как трата ресурса, Drop как ослабление, Copy как !, заимствование как разрешение без траты; почему проверка заимствований это аффинная система типов.урок 66 · Аффинная логика и Rust: отдал, значит, потратилопираются: урок 67
Босс K: касса монетного двораПротокол обмена монет: линейная спецификация, вывод корректности в логике разделения, реализация на Haskell с LinearTypes и доказательство у судьи, что монета не появляется из ничего.урок 70 · Босс: касса монетного двораопираются: урок 71
Линейная логикаГипотезы как ресурсы: связки ⊗, ⊸, &, ⊕ и экспонента !, правила секвенциального исчисления, раскладка контекста по посылкам и почему A ⊢ A ⊗ A не выводится.урок 65 · Линейная логика: монета не берётся из воздухаопираются: урок 66
Линейные типы в HaskellРасширение LinearTypes: стрелка a %1 -> b, кратность аргумента, Ur для неограниченных значений и API ресурса, который нельзя закрыть дважды или забыть закрыть.урок 67 · Линейные типы в Haskell: сейф закрывают ровно один разопираются: урок 68
Логика разделенияКуча в утверждениях: emp, x ↦ v, разделяющая конъюнкция *, малые аксиомы для чтения, записи, выделения и освобождения, правило кадра и списки в куче на примере разворота списка.урок 69 · Логика разделения: две бирки на одной полкеопираются: урок 70
Логика ХоараТройки {P} c {Q}, правило присваивания задом наперёд, последовательность, ветвление, инвариант цикла и правило следствия; деревья вывода для маленьких программ.урок 68 · Логика Хоара: монета не берётся из воздухаопираются: урок 69
Структурные правилаСеквенции и три правила, которые натуральная дедукция прячет: ослабление, сокращение, перестановка. Что ломается без каждого из них: аффинные, релевантные, линейные и упорядоченные логики.урок 64 · Структурные правила: что будет, если их убратьопираются: урок 65, урок 77

Командировка в диспетчерскую: модальная и временная логика

Босс L: две стрелкиВзаимное исключение двух постов: требования в LTL, гонка и взаимная блокировка как ленты проверяльщика, нечестное расписание, алгоритм Петерсона на Haskell и индуктивный инвариант у судьи; отказ в безопасную сторону.урок 76 · Босс: две стрелкиопираются: урок 77
Ветвящееся время: CTLСистемы переходов и дерево вычислений, кванторы путей A и E, восемь операторов CTL, алгоритм разметки через неподвижные точки и почему LTL и CTL несравнимы: F G p против AG EF p.урок 74 · CTL: время, которое ветвитсяопираются: урок 75
Линейная временная логика LTLТрассы и лассо, операторы X, F, G, U и слабое W, двойственность, шаблоны требований (отсутствие, ответ, предшествование, повторение), LTLf на конечных журналах, безопасность и живучесть.урок 73 · LTL: всегда, когда-нибудь, до тех пор, покаопираются: урок 74
Модальная логикаОператоры □ и ◇ на моделях Крипке: возможные миры, отношение доступности, истинность в мире, тупики, двойственность ◇ = ¬□¬ и прочтения коробки как необходимости, знания, обязанности и времени.урок 71 · Модальная логика: необходимо и возможноопираются: урок 72
Проверка моделейЯвный перебор состояний: инвариант обходом в ширину с кратчайшим контрпримером, живучесть через лассо, наблюдатель и автомат Бюхи, взрыв состояний и борьба с ним, справедливость, мост к TLC и TLA+; свой проверяльщик на Haskell.урок 75 · Проверка моделей: перебрать всё, найти лассоопираются: урок 76
Системы K, T, S4, S5Аксиома K и правило необходимости, рамки и верность на рамке, соответствие аксиом D, T, B, 4, 5 свойствам доступности, системы K, D, T, S4, S5, логика знания, убеждений и обязанностей.урок 72 · Системы K, T, S4, S5: аксиома как форма стрелокопираются: урок 73

Командировка в редакцию: логики неполного знания

Босс M: «Сольские ведомости»Иск к газете за заметку из противоречивых источников: формализация, сводка Белнапа и правило печати, расчёт доверия к двум источникам по Байесу, немонотонный пересмотр и поправка, записка судье против двух возражений: взрыва и «снять всё».урок 81 · Босс: «Сольские ведомости»
Вероятностная логикаВероятность формулы как сумма весов строк таблицы истинности, законы вероятности, границы для конъюнкции и отсутствие истинностной функциональности, условная вероятность, правило Байеса, байесовские сети и почему P(A → B) не P(B | A).урок 79 · Вероятностная логика: сколько верить источникуопираются: урок 80
Немонотонный выводМонотонность и ослабление, правила по умолчанию Рейтера, предположение о замкнутом мире, отрицание как неудача, Datalog снизу вверх до неподвижной точки, стратификация и безопасность правил; мини-Datalog на Haskell.урок 77 · Немонотонный вывод: по умолчанию и отрицание как неудачаопираются: урок 78
Нечёткость, вероятность и AIПарадокс кучи и нечёткие множества Заде, связки min, max и 1 − x, степень истинности против вероятности, карта логик в рассуждающих машинах, коэффициенты уверенности MYCIN и почему языковая модель не логика: модель предлагает, движок проверяет.урок 80 · Нечёткость, вероятность и машины, которые пишут гладкоопираются: урок 81
Паранепротиворечивые логикиВзрыв и дизъюнктивный силлогизм, четырёхзначная логика Белнапа: истина, ложь, оба, ничего как то, что сказали источники; связки через флажки, выделенные значения, следование без взрыва, потеря modus ponens и тавтологий, Клини и SQL NULL, сводка источников.урок 78 · Паранепротиворечивость: противоречие без взрываопираются: урок 79