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

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

@Ulysses подбросил отличную ссылку на интерактивный вводный курс в LaTeX. Это ваш шанс!

Есть ещё курс по LaTeX на Coursera на русском.

#19

А напишите, пожалуйста, кто-нибудь, какие случаи функций/доказательств из лекции 3 остались на дом (кроме size, который целиком)?

#20
  1. Перевести в правила вывода термы pred(t), iszero(t).
  2. Значения функции Consts для pred(n) и iszero(n).
  3. Значения функции depth для true, zero, succ(n), iszero(n).
  4. Доказательство |Consts(t)| <= size(t) для true, false, succ(n), pred(n), iszero(n).
  5. Функции интерпретации для false, succ(n), iszero(n).

Также на дом осталось описание индукции по размеру.

2 лайка
#21

Отлично, спасибо!

#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 курс ФИИТ)