A post was merged into an existing topic: (4 курс ФИИТ) Теория языков программирования. Практика
7 posts were split to a new topic: Видеозаписи по курсу «Теория языков программирования» 2015/16 (4 курс ФИИТ)
Не знаю, существенно ли это, но в конце 4-й страницы конспекта лекции 3 должна быть пометка “случаи PRED и IsZero аналогично”.
Да, верно, спасибо!
Вынуждена предупредить, что конспектов лекций, видимо, больше не будет, много времени кушают.
Литература ко всем лекциям будет указана в отдельном файле, его можно найти на странице курса сверху, в разделе «Материалы».
Напомните, пожалуйста, какие задания из лекций 4-5 остались на дом?
- Доказательство детерминированности отношения вычисления для
E-Pred
иE-IsZeroSucc
. - Сформулировать
B-IfFalse
. - Доказательство теоремы для всех случаев, кроме
if t1 then t2 else t3
.
Спасибо! По последнему пункту: все случаи это слишком много, я выберу для домашней парочку.
В первом модуле в качестве мероприятия рубежного контроля предусмотрено компьютерное тестирование в moodle. У нас пропадает лекция 7 марта, я думаю, что в счёт этой пары мы и проведём тестирование в какую-нибудь среду в 15-50. Предположительно 16 марта.
Напоминаю, что завтра, 16 марта, в 15-50 в ММ-1,2 состоится компьютерное тестирование по первому модулю.
Я допроверила текстовые ответы, можно смотреть итоговые баллы.
Тест с вариантами ответа закрыт, можно посмотреть только итоговый балл. Если у кого есть сомнения или вопросы, подходите, посмотрим и обсудим. Можно это сделать на следующей лабораторной работе, например. С некоторыми формулировками можно поспорить, не стесняйтесь, может быть удастся отвоевать больше баллов! Но нужно аргументировать, конечно.
Завтра на семинаре будем программировать на языке лямбда-исчисления. Чтобы понимать, что происходит, нужно предварительно посмотреть лекцию 11:
- часть 1 (синтаксическое равенство термов, альфа-конверсия и альфа-эквивалентность термов, функция переименования переменной в терме);
- [часть 2] (https://www.youtube.com/watch?v=1X9FEGzT4vM&list=PL9zS4WrYQCg5hNEoeITwn99XCvaL1Lixy&index=27) (вычисление функций, бета-редукция, стратегии бета-редукции, операционная семантика лямбда-исчисления для стратегии вызова по значению).
Администрация форума оставляет за собой право удалять или редактировать повторяющиеся посты!
Во-первых, про Y-кобинатор правильная формула такая: [\mathrm{Y}\ \mathrm{F} = \mathrm{F}\ (\mathrm{Y}\ \mathrm{F})]
Далее. То, что ( \mathrm{fix}\ \mathrm{F} ) переходит в (\mathrm{F}\ (\lambda y.\mathrm{B}\ \mathrm{B}\ y)), то есть (\mathrm{F}\ (\lambda y.(\mathrm{fix}\ \mathrm{F})\ y)), это правда. А вот дальше, про применение этого всего к v
, неверно, так как применение лево-ассоциативно, а не право.
Я, кажется, не знаю, как дальше показать, что (\mathrm{fix}\ \mathrm{F}\ v) это (\mathrm{F}\ (\mathrm{fix}\ \mathrm{F})\ v). С удовольствием выдам за доказательство бонусные баллы!
На конкретном примере легко увидеть, как раскручивается рекурсия.
Пусть через fact
обозначен терм if n = 0 then 1 else n * (f (n - 1))
,
а F
это (\lambda f.\lambda n.\mathrm{fact})
В терме (\mathtt{fix}\ \mathrm{F}\ 1) нужно сначала редуцировать левое применение, за несколько шагов (это было на семинаре) переходим к терму (\mathrm{F}\ (\lambda y.(\mathtt{fix}\ \mathrm{F})\ y)\ 1).
Раскрываем F
:
((\lambda f.\lambda n.\mathrm{fact})\ (\lambda y.(\mathtt{fix}\ \mathrm{F})\ y)\ 1 \longrightarrow
(\lambda n.\mathtt{if}\ n = 0\ \mathtt{then}\ 1\ \mathtt{else}\ n * (\mathrm{F}’\ (n - 1)))\ 1 ), где F'
это (\lambda y.(\mathtt{fix}\ \mathrm{F})\ y).
Далее применяем левую внешнюю абстракцию к 1, получаем (1 * (\mathrm{F}’\ 0)), то есть (1 * ((\lambda y.(\mathtt{fix}\ \mathrm{F})\ y)\ 0) \longrightarrow 1 * ((\mathtt{fix}\ \mathrm{F})\ 0))
Вот мы и пришли снова к (\mathtt{fix}\ \mathrm{F}), только теперь оно применяется к 0.
Всё встало на места)
Контрольная работа по второму модулю состоится во время семинара, в следующую среду, 27 апреля, 11-55, а. 304.
Первая часть контрольной пишется без использования конспекта. По окончании первой части листики сдаются, после этого можно приступать ко второй части (с использованием конспекта). Первая часть «понятийная», вторая — «доказательная». Нужно владеть навыками доказательств по индукции.