Лекция 5. Структурная индукция (Языки программирования и компиляторы)

preview_player
Показать описание
Принцип структурной индукции. Композиционность. Примеры доказательств: детерминизм, корректность компилятора выражений.
Лекция №5 в курсе "Языки программирования и компиляторы", весна 2018
Преподаватель курса: Дмитрий Юрьевич Булычев, Даниил Андреевич Березун, Екатерина Андреевна Вербицкая, Антон Викторович Подкопаев
  1. Computer Science Center
Рекомендации по теме
Лекция 5. Структурная 1:19:27

Лекция 5. Структурная индукция (Языки программирования и компиляторы)...

Математика это не 0:00:21

Математика это не Ислам

4.2 Как задать 0:04:24

4.2 Как задать множество? - структурная индукция, общее свойство, список...

ТРЯП-5. Структурные свойства 1:27:20

ТРЯП-5. Структурные свойства регулярных языков

Лекция 6. Конструкции 1:15:46

Лекция 6. Конструкции управления (Языки программирования и компиляторы)...

День студента мехмата 0:00:52

День студента мехмата МГУ #мгу #умскул #физика #математика #учеба #подготовкаогэ #подготовкакегэ...

5. Coq. Разбор 1:00:17

5. Coq. Разбор д-ва терминируемости алгоритма Евклида

Математика без Ху%!ни 0:05:31

Математика без Ху%!ни ! ;) Математическая индукция. Метод доказательства формул....

Лекция 5 | 1:25:20

Лекция 5 | Классическая теория кодирования и новые приложения | Виталий Скачек | Лекториум...

Лекция 5 | 1:24:01

Лекция 5 | Языки программирования и компиляторы (2012) | Дмитрий Булычев | CSC | Лекториум...

19. Ординалы и 1:01:13

19. Ординалы и трансфинитная индукция

лекция 5: порядковые 1:18:23

лекция 5: порядковые изоморфизмы, арифметика Пеано

Лекция 1. Языки 1:18:26

Лекция 1. Языки программирования и компиляторы (Введение)...

Олегу Тинькову* запрещён 0:01:56

Олегу Тинькову* запрещён вход на Мехмат МГУ

Лекция 5 | 1:08:17

Лекция 5 | Основы наивной теории множеств | Станислав Сперанский | Лекториум...

Алгебра-1, лекция 5, 1:46:13

Алгебра-1, лекция 5, А.В.Фонарев

Лекция 5 | 1:47:06

Лекция 5 | Синтетическая топология | Георгий Каданцев

Как выучить язык 0:59:30

Как выучить язык - интуитивный метод изучения языка

Как распознать талантливого 0:03:30

Как распознать талантливого математика

Лекция 02. Математическая 0:35:15

Лекция 02. Математическая индукция с нуля. Полная теория...

Неделя 3: Формальные 0:56:50

Неделя 3: Формальные языки, списки, инстансы | Формализация математики на Lean...

Александр Беликов. Основы 0:32:10

Александр Беликов. Основы логики: дедукция и индукция

Лекция 5. С.Л. 1:31:38

Лекция 5. С.Л. Кузнецов. Сохранение типа при бета-редукции. Интуиционистская логика высказываний......

Ю. Сыровецкий - 1:32:05

Ю. Сыровецкий - Функциональное программирование, семинар 5, тема 4.2. Свёртки, WHNF...

Комментарии
Автор

funext для доказательства тут не требуется, у нас буквально одинаковые термы
h1 : s x = z1
h2 : s x = z2

z1 = z2

(symm h1) |> h2 : z1 = z2

то есть даже если делать тактиками, два рерайта перепишут цель в s x = s x, что доказуемо аксимой рефлексивности равенства для любых s и x

AndrewKrasnobaev