Fwd: Ближайший семинар ruSTEP - пятница 5 февраля в 12:00 (мск)
Andrei Klimov
От: Shilov Nikolay <shil...@mail.ru>
Date: вт, 2 февр. 2021 г., 9:39
Subject: Ближайший семинар ruSTEP - пятница 5 февраля в 12:00 (мск)
To: <n.sh...@innopolis.ru>
Александр Коновалов
Добрый день всем!
На семинаре мельком было сказано, что следующая функция вычисления факториала
F(n) := if n = 0 then 1 else n · F(n − 1)
эквивалентна такой функции:
F(n) := P(n, 1)
P(n, m) := if n = 0 then m else P(n − 1, n · m)
(Формулы пишу по памяти, т.к. слайды семинара не выложены.)
Доказательства эквивалентности обоих формул не было, т.к. цель семинара была совсем-совсем другая.
Я хочу показать, что эти две формулы эквивалентны, пользуясь классическими эквивалентными преобразованиями Бёрстола и Дарлингтона.
В ходе преобразований нам потребуются аксиомы, что умножение коммутативно, ассоциативно и имеет нейтральный элемент (единицу):
x·y = y·x
(x·y)·z = x·(y·z) = x·y·z (можно писать без скобок)
x·1 = 1·x = x
Для начала, у нас есть только определение факториала:
F(n) := if n = 0 then 1 else n · F(n − 1)
Введём следующее определение функции:
P(n, m) := m·F(n) (1)
Раскроем (unfold) F(n) в формуле (1) и внесём сомножитель внутрь ветвления:
P(n, m) := m·F(n) =
= m·(if n = 0 then 1 else n · F(n − 1)) =
= if n = 0 then m·1 else m · (n · F(n − 1)) =
/* пользуемся аксиомами */
= if n = 0 then m else (n · m) · F(n − 1) =
= if n = 0 then m else (m · n) · F(n − 1)
Выражение в ветке else является частным случаем формулы (1), свернём (fold) его:
P(n, m) := if n = 0 then m else (m · n) · F(n − 1) =
= if n = 0 then m else P(n − 1, m · n)
Целевое выражение для P мы вывели. Теперь нам надо выразить F(n) через P(n, m):
F(n) =
/* пользуемся аксиомой */
= 1·F(n) =
/* сворачиваем по формуле (1) */
= P(n, 1)
Таким образом, мы вывели определение факториала с хвостовой рекурсией.
Мы преобразовали
F(n) := if n = 0 then 1 else n · F(n − 1)
в
F(n) := P(n, 1)
P(n, m) := if n = 0 then m else P(n − 1, n · m)
Заметим, что в исходной и конечной формулах присутствует единичка. В первой после then, во второй — в вызове P(n, 1). Ниже будет показано, что это разные по смыслу единички.
В докладе рассматривались функциональные схемы программ — программы, в которых реальные операции заменены на некоторые неизвестные (неинтерпретируемые) символы. Рассмотрим теперь схему для функции факториала и попробуем её преобразовать аналогичным образом:
F(x) := if p(x) then c else f(x, F(g(x)))
Здесь неинтерпретируемые символы это p, c, f, g.
В докладе показано, что не пользуясь аксиомами, в эффективный цикл (O(n)) преобразовать эту программу нельзя. Введём аксиомы для двуместной функции f, те же самые:
f(x, y) = f(y, x)
f(x, f(y, z)) = f(f(x, y), z)
f(x, e) = f(e, x) = x
где e — единица для операции f. Заметим, что в общем случае c и e никак не связаны.
(Если я правильно помню терминологию, символы с аксиомами называются полуинтерпретируемыми.)
Поехали. Введём определение:
P(x, y) := f(y, F(x)) (2)
Раскрываем F(x):
P(x, y) := f(y, if p(x) then c else f(x, F(g(x)))) =
= if p(x) then f(y, c) else f(y, f(x, F(g(x)))) =
/* аксиомы */
= if p(x) then f(y, c) else f(f(y, x), F(g(x))) =
= if p(x) then f(y, c) else f(f(x, y), F(g(x))) =
/* свёртка по формуле (2) */
= if p(x) then f(y, c) else P(g(x), f(x, y))
Подставим y := e в формулу (2):
P(x, e) ≡ f(e, F(x)) ≡ F(x)
Таким образом, получили что
F(x) := P(x, e)
P(x, y) := if p(x) then f(y, c) else P(g(x), f(x, y))
Сравнивая эту схему с двумя определениями факториала, видим, что первая единичка (после then) — это c, а вторая (в вызове P(n, 1)) — e.
Прошу прощения, если моё письмо показалось кому-то скучным. Просто я люблю расписывать разные выкладки, преобразования, рисовать графы суперкомпиляции и т.д. Не удержался и в этот раз.
С уважением,
Александр Коновалов
--
Вы получили это сообщение, поскольку подписаны на группу "Метавычисления и специализация программ".
Чтобы отменить подписку на эту группу и больше не получать от нее сообщения, отправьте письмо на электронный адрес metacomputation...@googlegroups.com.
Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/CAM7HiMmZVSc0jyBFpV4gqb8L_kRb5qhJk5Tj%3D1f9Ziv6x5gCpg%40mail.gmail.com.
Arkady Klimov
P(x, fy) := fy ( F(x)) (3)
Если имя начинается на f, то это функция из N в N.
Раскрываем F(x): -- (f x) - закарривание для функций f от двух аргументов
P(x, fy) := fy ( if p(x) then c else f(x, F(g(x)))) =
= if p(x) then fy (c) else fy ( (f x) ( F(g(x)))) =
= if p(x) then fy (c) else (fy o (f x)) (F(g(x))) =
/* свёртка по формуле (3) */
= if p(x) then
fy (c) else P(g(x),
fy o (f x)
)
Подставим y := I в формулу (3), где I - тождественная функция:
P(x, I) ≡ I (F(x)) ≡ F(x)
Таким образом, получили что
F(x) := P(x, I)
P(x, fy) := if p(x) then
fy (c) else P(g(x),
fy o (f x)
)
Фактически здесь fy, (f x) - операторы умножения на целое число, а o - композиция этих операторов (которая здесь дает оператор умножения на произведение).
Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/008901d6fbaf%2454a97a90%24fdfc6fb0%24%40mail.ru.
Александр Коновалов
Добрый день всем!
Аксиома коммутативности мне нужна была, т.к. у Николая Шилова в примере было написано умножение именно в таком порядке: P(n − 1, n · m), порядок я запомнил. А остальные аксиомы…
Вы дополняете входной язык понятием композиции, которая определена как
f(g(x)) ≡ (f • g)(x)
Определение композиции можно считать заменой аксиомы об ассоциативности умножения. Кстати, композиция ассоциативна и её нейтральный элемент I, но это в выкладках не используется.
А определение тождественной функции тоже нужно добавлять к программе:
F(x) := P(x, I)
P(x, fy) := if p(x) then fy(c) else P(g(x), fy • (f x))
I(x) := x
Так что бритва Оккама сломалась, сущностей столько же. 😀
Исходная цель преобразований была в превращении рекурсии в хвостовую. В случае композиции не факт, что вычисление fy(c) не потребует стека линейной глубины.
С уважением,
Александр Коновалов
Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/CAMZpZXnBQcxW8VoKRYjdy-Uco4j%2BLbw0yiB2QugXb%3DOW3dHLUg%40mail.gmail.com.
Arkady Klimov
Добрый день всем!
Аксиома коммутативности мне нужна была, т.к. у Николая Шилова в примере было написано умножение именно в таком порядке: P(n − 1, n · m), порядок я запомнил. А остальные аксиомы…
Вы дополняете входной язык понятием композиции, которая определена как
f(g(x)) ≡ (f • g)(x)
Определение композиции можно считать заменой аксиомы об ассоциативности умножения.
Кстати, композиция ассоциативна и её нейтральный элемент I, но это в выкладках не используется.
А определение тождественной функции тоже нужно добавлять к программе:
F(x) := P(x, I)
P(x, fy) := if p(x) then fy(c) else P(g(x), fy • (f x))
I(x) := xТак что бритва Оккама сломалась, сущностей столько же. 😀
Исходная цель преобразований была в превращении рекурсии в хвостовую. В случае композиции не факт, что вычисление fy(c) не потребует стека линейной глубины.
Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/007601d6fc81%24bed047f0%243c70d7d0%24%40mail.ru.
Александр Коновалов
Добрый вечер, Андрей!
«А в частном, когда композицию можно *выполнить* с порождением результата *того же сорта* (то есть умножением) — не потребует. Тогда умножение является автоматически ассоциативным. Или наоборот: если умножение ассоциативно, то композицию можно выполнить как умножение.»
Не очень понял фокус. Имеется ввиду, что операция f•g может, когда знает о свойствах f и g, порождать не «объект композиции» в общем случае, а что-то другое?
Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/CAMZpZXnA9KLSKStf9Wv4o9%2BhANLKGJT7jwJgW4Ltm%3DZOpzUXzQ%40mail.gmail.com.
Arkady Klimov
Добрый вечер, Андрей!
«А в частном, когда композицию можно *выполнить* с порождением результата *того же сорта* (то есть умножением) — не потребует. Тогда умножение является автоматически ассоциативным. Или наоборот: если умножение ассоциативно, то композицию можно выполнить как умножение.»
Не очень понял фокус. Имеется ввиду, что операция f•g может, когда знает о свойствах f и g, порождать не «объект композиции» в общем случае, а что-то другое?
Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/011b01d6fcae%24cec5b1e0%246c5115a0%24%40mail.ru.
Александр Коновалов
Аркадий!
Я Вас опять в предыдущем письме назвал Андреем, извините. Перед тем, как писал прошлое письмо, я отвечал на письмо Андрея Климова и ошибся.
Спасибо за пояснение. Теперь понял идею. Но всё равно получается, что мы одну аксиому заменяем на другую.
Если рантайм языка знает об ассоциативности композиции, то может оптимизировать конструкции вида f•g•h, чтобы они использовали при выполнении константный стек. Если нет, то некоторые виды композиции в переменной-аккумуляторе будут приводить к линейному стеку.
Композиция f1 • (f2 • (… (fn−1 • fn)…)) даст линейный стек. Композиция ((…(f1 • f2)…) • fn−1) • fn даст стек константной глубины. В рассматриваемой программе композиция будет по первой схеме.
Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/CAMZpZXkMsGidPUO1kKUu2WLsZ1pTX6pHdNCdrq4ziAKNfmKz8A%40mail.gmail.com.