(4 курс ФИИТ) Теория языков программирования

Поддержка учебных курсов ФИИТ, 4 курс
#22

A post was merged into an existing topic: (4 курс ФИИТ) Теория языков программирования. Практика

#23

7 posts were split to a new topic: Видеозаписи по курсу «Теория языков программирования» 2015/16 (4 курс ФИИТ)

#24

Опубликован план-конспект лекции 3.

#25

Не знаю, существенно ли это, но в конце 4-й страницы конспекта лекции 3 должна быть пометка “случаи PRED и IsZero аналогично”.

#26

Да, верно, спасибо!

#28

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

Литература ко всем лекциям будет указана в отдельном файле, его можно найти на странице курса сверху, в разделе «Материалы».

#32

Напомните, пожалуйста, какие задания из лекций 4-5 остались на дом?

#33
  1. Доказательство детерминированности отношения вычисления для E-Pred и E-IsZeroSucc.
  2. Сформулировать B-IfFalse.
  3. Доказательство теоремы для всех случаев, кроме if t1 then t2 else t3.
1 лайк
#34

Спасибо! По последнему пункту: все случаи это слишком много, я выберу для домашней парочку.

1 лайк
#36

В первом модуле в качестве мероприятия рубежного контроля предусмотрено компьютерное тестирование в moodle. У нас пропадает лекция 7 марта, я думаю, что в счёт этой пары мы и проведём тестирование в какую-нибудь среду в 15-50. Предположительно 16 марта.

#37

Напоминаю, что завтра, 16 марта, в 15-50 в ММ-1,2 состоится компьютерное тестирование по первому модулю.

#39

Я допроверила текстовые ответы, можно смотреть итоговые баллы.

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

#40

Публикую диалог «что такое тип?» из книжки Aaby, зачитанный на лекции 9:

2 лайка
#41

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

  • часть 1 (синтаксическое равенство термов, альфа-конверсия и альфа-эквивалентность термов, функция переименования переменной в терме);
  • [часть 2] (https://www.youtube.com/watch?v=1X9FEGzT4vM&list=PL9zS4WrYQCg5hNEoeITwn99XCvaL1Lixy&index=27) (вычисление функций, бета-редукция, стратегии бета-редукции, операционная семантика лямбда-исчисления для стратегии вызова по значению).
#42

Администрация форума оставляет за собой право удалять или редактировать повторяющиеся посты!

#43

Во-первых, про 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). С удовольствием выдам за доказательство бонусные баллы!

1 лайк
Видеозаписи по курсу «Теория языков программирования» 2015/16 (4 курс ФИИТ)
#44

На конкретном примере легко увидеть, как раскручивается рекурсия.
Пусть через 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.

#45

Ответ есть в начале лекции 12.

#46

Всё встало на места)

1 лайк
#47

Контрольная работа по второму модулю состоится во время семинара, в следующую среду, 27 апреля, 11-55, а. 304.

Первая часть контрольной пишется без использования конспекта. По окончании первой части листики сдаются, после этого можно приступать ко второй части (с использованием конспекта). Первая часть «понятийная», вторая — «доказательная». Нужно владеть навыками доказательств по индукции.

1 лайк