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

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

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

1 симпатия

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

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

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

1 симпатия

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

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

1 симпатия

Богдан, напишите, пожалуйста, сколько у вас баллов за вторую часть, а то я себе не отметила. На почту или здесь в личных сообщениях.

Проверила модуль 1. Лабораторную 4 ещё исправлю, остальное просьба проверить. Если что не так, завтра исправим, сообщайте.

Всё, я выставила все баллы в мудл и БРС! Ура! Проверяйте. Если у кого-то что-то пропустила, сообщайте, исправлю.

Я буду в среду с 11-55 по расписанию в а. 304. Кому нужно поставить в зачётку, можно подходить в любое время. Всем остальным (у кого нет зачёта) подходить в 11-55. Если есть возможность, берите ноутбуки. Если нет, как-нибудь решим с дисплейными классами.

Зачётов пока нет у следующих студентов: Абащикова, Антонова, Борисов, Гаврилова, Маросеев, Машталов, Остапенко, Рыбников, Селютин, Сухаревский.

У некоторых студентов ситуация неплохая, но для получения зачёта нужно попытаться выполнить (можно делать это частично в среду, в том числе на паре в 13-45):

  • Абащикова: лаб-3, д/з по программированию 3, д/з по программированию 6.
  • Антонова: д/з по программированию 6, д/з по лекциям 6.
  • Гаврилова: д/з по программированию 6, письменное задание на паре.
  • Маросеев: д/з по программированию 3, д/з по программированию 6, д/з по программированию 7, письменное задание на паре.

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

А, ещё Кочергу забыла. Бонусные баллы в зачёт не считаются же. Михаилу нужно выполнить д/з по программированию 6 и лаб-7.

Извините, хотела узнать, а переписывание теста в БРС Вы учитывали, а то в поле 1-й контрольной работы у меня ничего не изменилось?

Да, действительно, пропустила. Тогда вам только задание по программированию.

Спасибо, а можно спросить, если не получится прийти в среду, можно загрузить все на гитхаб, а подойти в какой-то другой день?

Загрузить нужно, сдать можно очно в другой день.

Здравствуйте. К сожалению, не нашел себя в списке студентов, у которых до зачета далеко. Как и баллов в БРС, несмотря на то, что первые задания еще сдавал. В мудле задание висит проверенное, на курс подписался еще одним из самых первых. P.s. Игорь Сороканюк, 9 группа

Юлия Вячеславовна, а письменная работа, написанная на последней лекции, была учтена?

Поскольку вы не подавали признаков жизни, я и не ставила вам ничего. Выставила ваши 2 балла в БРС.

1 симпатия

Да, выставлена в добор.