Имя входного файла: стандартный ввод
Имя выходного файла: стандартный вывод
Ограничение по времени: 5 секунды
Ограничение по памяти: 512 мегабайт
На вход вашей программе дается лямбда-выражение в следующей грамматике:
⟨Выражение⟩ ::= [⟨Применение⟩] \ ⟨Переменная⟩ . ⟨Выражение⟩
⟨Применение⟩ ::= ⟨Применение⟩ ⟨Атом⟩ | ⟨Атом⟩
⟨Атом⟩ ::= ( ⟨Выражение⟩ ) | ⟨Переменная⟩
⟨Переменная⟩ ::= (a-z) {a-z, 0-9, '}*Аргументы-переменные в применении должны разделяться пробелом. В остальных случаях пробелы могут отсутствовать. Любые пробелы между нетерминальными символами (кроме пробела, разделяющего аргументы в применении) — а также начальные и конечные пробелы в строке — должны игнорироваться. Символы табуляции, возврата каретки и перевода строки должны трактоваться как пробелы.
Требуется расставить все недостающие скобки вокруг всех абстракций и применений, и напечатать получившийся результат.
Размер входного файла не превышает 1 МБ.
В единственной строке выходного файла (заканчивающейся переводом строки) должно быть приведено лямбда-выражение с расставленными скобками без каких-либо пробельных символов. Исключение: одиночные пробелы, разделяющие аргументы в применении.
| стандартный ввод |
|---|
\a.\b.a b c (\d.e \f.g) h |
| стандартный вывод |
(\a.(\b.((((a b) c) (\d.(e (\f.g)))) h))) |
| стандартный ввод |
|---|
((a\bbb.c)d)e f g |
| стандартный вывод |
(((((a (\bbb.c)) d) e) f) g) |
Имя входного файла: стандартный ввод
Имя выходного файла: стандартный вывод
Ограничение по времени: 10 секунды
Ограничение по памяти: 512 мегабайт
На вход вашей программе дается лямбда-выражение в следующей грамматике:
⟨Выражение⟩ ::= [⟨Применение⟩] \ ⟨Переменная⟩ . ⟨Выражение⟩
⟨Применение⟩ ::= ⟨Применение⟩ ⟨Атом⟩ | ⟨Атом⟩
⟨Атом⟩ ::= ( ⟨Выражение⟩ ) | ⟨Переменная⟩
⟨Переменная⟩ ::= (a-z) {a-z, 0-9, '}*Аргументы-переменные в применении разделяются пробелом. В остальных случаях пробелы могут отсутствовать. Любые пробелы между нетерминальными символами (кроме пробела, разделяющего аргументы в применении) — а также начальные и конечные пробелы в строке — должны игнорироваться. Символы табуляции и возврата каретки должны трактоваться как пробелы.
Требуется найти наиболее общий тип этого лямбда-выражения и вывести доказательство того, что лямбда-выражение имеет этот тип, а также найти типы свободных переменных, содержащихся в лямбда-выражении, или же сказать, что лямбда-выражение не имеет типа.
В доказательстве вы можете пользоваться следующими правилами:
В единственной строке входного файла содержится лямбда-выражение в грамматике из условия. Длина выражения не превышает 255 символов.
Гарантируется, что имена всех вложенных абстракций различны, а также имена абстракций не совпадают с именами свободных переменных.
Если заданное лямбда-выражение не имеет типа, в единственной строке выходного файла должна быть запись «Expression has no type».
Иначе в файле должно быть доказательство. В файле должны отсутствовать пустые строки. Строки доказательства должны идти в правильном порядке. Каждый отступ должен представляться с помощью «*» — символа «*» (ASCII 42) и трех последовательных пробелов (ACSII 32). В конце каждой строки должно быть описание правила, которое было применено для вывода этой строки. В остальном следуйте формату из примеров.
Выведенный тип должен быть наиболее общим типом для заданного лямбда-выражения.
| стандартный ввод |
|---|
x |
| стандартный вывод |
| `x : t1 |
| стандартный ввод |
(\x. x) (\y. y) |
| стандартный вывод |
| ` |
| стандартный ввод |
\a. a' a z8' |
| стандартный вывод |
| `z8' : t4, a' : (t1 -> (t4 -> t5)) |
Имя входного файла: стандартный ввод
Имя выходного файла: стандартный вывод
Ограничение по времени: 15 секунд
Ограничение по памяти: 1024 мегабайта
Дано лямбда-выражение, требуется провести m (m ∈ N0) бета-редукций этого выражения используя нормальный порядок редукции и мемоизацию, при этом выводить на печать требуется каждое k-е выражение (k ∈ N0, k < m). Формулы нумеруются с 0, если нормальная форма была достигнута на формуле с некратным k номером — на формуле δ s , где k · (n − 1) < s < k · n, — то выдача должна завершиться формулой δ s . Например, редуцирование выражения (λx.x x x x) ((λx.x) (λx.x)) в данных условиях пройдёт через следующие стадии (редуцируемые бета-редексы подчёркнуты):
| обозначение (номер) | формула |
|---|---|
| δ0 | (λx.x x x x) ((λx.x) (λx.x)) |
| δ1 | ((λx.x) (λx.x)) ((λx.x) (λx.x)) ((λx.x) (λx.x)) ((λx.x) (λx.x)) |
| δ2 | (λx.x) (λx.x) (λx.x) (λx.x) |
| δ3 | (λx.x) (λx.x) (λx.x) |
| δ4 | (λx.x) (λx.x) |
| δ5 | (λx.x) |
Если при этом k = 2, то на печать должны быть выведены формулы δ0, δ2, δ4, δ5.
Гарантируется, что суммарная длина всех выражений, которые будут получены в результате s бета-редукций, не превышает 100 миллионов лексем.
Для точного определения условий задачи, давайте напомним два важных определения — нормальный порядок редукций и мемоизацию.
- Рассмотрим лямбда-выражение, расставим все необязательные скобки в нём. Назовём нормальным порядком редукции такой порядок, при котором всегда редуцируется самый левый редекс: то есть редекс, первый символ которого находится левее всего в выражении.
- Чтобы определить мемоизацию, определим некоторое расширенное лямбда-исчисление. Помимо обычных выражений будем рассматривать отложенные подстановки: это переменные с указанием заменяемого выражения в угловых скобках — x<A>. При этом подстановка A[x := B] раскрывается так:
Здесь t — некоторая новая отложенная переменная, ранее в выражении не встречавшаяся.
Естественным образом мы можем определить плоское лямбда-выражение для данного выражения, рассматривая каждую переменную вида x<P> как P.
Тогда шаг редукции с мемоизацией устроен так:
- Выберем редекс (λx.A) B — например, найдём самый левый редекс в плоском лямбда-выражении, соответствующем данному.
- Если (λx.A) содержит вхождение отложенной подстановки y hP i , в которую входит заменяемая переменная x, перед редукцией заменим данное вхождение y<P> на P. Обратите внимание, случай λx.A = y<P> также надо учитывать.
- Все остальные отложенные подстановки в редексе оставим без изменений — рассматриваем, как переменные. Производим редукцию.
- Если редекс целиком находится внутри какой-то отложенной подстановки — редукцию производим во всех отложенных подстановках по той же переменной.
В первой строке приведены числа m и k через пробел. Во второй строке дано лямбда-выражение δ0 в грамматике из предыдущего задания.
Выведите формулы δ0, δk, δk·2, ..., δk·(n−1), δs, по формуле на новой строке.
| стандартный ввод | стандартный вывод |
|---|---|
| 10 1 (\x.x) z |
((\x.x) z) z |
| 100 1 (\x.y) z |
((\x.y) z) y |
| 100 1 (\a.\a.b) c |
((\a.(\a.b)) c) (\v0.b) |
| 100 1 (\a.\x.a) (x y) |
((\a.(\x.a)) (x y)) (\v0.(x y)) |