Вы, наверное, предварительно не авторизовались просто.
Нет, я был авторизован.
Тогда не знаю, странно У меня всё открывается. В крайнем случае могу выслать нужные файлы.
А можете скриншот показать?
И у меня так же( Ошибка 404
Оу, ясно, это я права доступа не все настроила. Проверяйте снова!
Спасибо, теперь все хорошо.
Опубликовано домашнее задание 2 по материалам лекций. На самом деле там есть и пара задач по материалам семинара.
Кстати, видео с семинара 1 тоже опубликованы (часть 1, часть 2). Обратите внимание, что при обсуждении бинарного дерева на SML я допустила две ошибки:
- Типовый параметр следует писать
«'a»
, а не«a'»
. - Я соврала, когда говорила об ошибке в случае
val nilbtree = Nil
. На самом деле здесь ошибки не будет, простоnilbtree
получит тип'a btree
. А где там могут быть ошибки, мы узнаем попозже.
Хочу задать вопрос насчет семантического равенства термов: RTError != RTError
?
Думаю, можно считать, что равно, раз уж мы не различаем виды ошибок.
Спасибо, учту.
Как написать оксфордские скобки в LaTeX?
Вот несколько примеров исходного кода лекции.
Сумма натуральных чисел
$$\cfrac{}{\mathrm{Sum}(\mathtt{zero}, n, n)}$$
$$\cfrac{\mathrm{Sum}(n, m, p)}
{\mathrm{Sum}(\mathtt{succ}(n), m, \mathtt{succ}(p))}$$
Индуктивное определение термов:
$$\cfrac{}{ \mathtt{true} \in \mathrm{T} } \quad \cfrac{}{ \mathtt{false} \in \mathrm{T} }
\quad \cfrac{}{ \mathtt{zero} \in \mathrm{T} }$$
$$\cfrac{ t_1 \in \mathrm{T} }{ \mathtt{succ}(t_1) \in \mathrm{T} }$$
$$\cfrac{t_1 \in \mathrm{T} \quad t_2 \in \mathrm{T} \quad t_3 \in \mathrm{T} }
{ \mathtt{if} \ t_1 \ \mathtt{then} \ t_2 \ \mathtt{else} \ t_3 \in \mathrm{T} }$$
Функция интерпретации:
$$\llbracket\mathtt{pred}(t_1)\rrbracket =
\begin{cases}
error,\ \text{если } \llbracket t_1 \rrbracket \notin {\mathbb{N}}\\
0_{\mathbb{N}}, \text{если}\ \llbracket t_1 \rrbracket_{\mathbb{N}} = 0_{\mathbb{N}} \\
\llbracket t_1 \rrbracket_{\mathbb{N}} - 1_{\mathbb{N}}\ \text{иначе}\\
\end{cases}$$
Юлия Вячеславовна, можете, пожалуйста, привести пример для функции countIf
?
За синтаксическую правильность не ручаюсь… Код написан в предположении, что countIf
это каррированная функция.
val tm = If (IsZero (CFalse),
CFalse,
If (CFalse, Succ (CTrue), Pred (CFalse))
)
val countFalse = countIf (fn t => case t of
CFalse => true
| _ => false)
val countFalse_test_1 = countFalse tm = 4
Большое спасибо.
Чтобы воспользоваться \llbracket
и \rrbracket
, нужно еще выполнить \usepackage{stmaryrd}
.
Опубликовано домашнее задание 3 по материалам лекций 4 и 5. Напоминаю, что литература к лекциям (с указанием разделов) приводится в едином pdf-документе, который можно найти на странице курса.