/cht/a237b – ``chat''

/cht/ – chat

a237ba237b4adbdbd4fa29abf1f646fdcf40a – ``chat''

test message

Тогда можно избавиться от абстракции:

t := F          константа
  | (t -> t)    стрелка
  | (t t)       аппликация
  | x           переменные

Но как тогда определить что такое свободная/связанная переменная?
Имеем (∀x. t) = (x -> t). Значит переменная x в терме t связанная если t имеет вид (t1 -> t2) где t1 редуцируется в x.

Да, охуенно получается.

Примеры вычислений:

(x -> x -> x) F
= (F -> F)

(x -> x -> x) F F
= (F -> F) F
= F

Т.е. когда есть переменная слева от стрелки, то совершается подстановка, а иначе происходит редукция стрелок.

Evaluation rules (t → s means that t evaluates to s):

t1 → t1'
--------------------          (E-App1)
 (t1 t2) → (t1' t2)


      t2 → t2'
--------------------          (E-App2)
 (t1 t2) → (t1 t2')


          t1 → x
--------------------------    (E-AppArr1)
 ((t1 -> t2) s) → [s↦x]t2


 t1 ↛ x    t1 → s    t3 → s 
----------------------------  (E-AppArr2)
    ((t1 -> t2) t3) → t2

Не, хуйня, просто одно обозначение на другое поменяли.

@f1d50@f1d503d4f5dc4ac4a454dcc5ce19b3fb Брутфорс решение:

fn find-fastest-equivalent-program(f, inputs, max-mem) {
    let mut fastest = none;
    let mut best-avg-time = infinity;
    foreach (g in all-programs(max-mem)) {
        if let some(g-avg-time) = find-avg-time(f, g, inputs) {
            if g-avg-time < best-avg-time {
                fastest = some(g);
                best-avg-time = g-avg-time;
            }
        }
    }
    fastest
}
fn find-avg-time(f, g, inputs) {
    let mut g-avg-time = 0;
    foreach (x in inputs) {
        let (time, res) = eval(g, x);
        if res != f(x) { return none; }
        g-avg-time += time / inputs.count;
    }
    some(g-avg-time)
}

Но это хуйня полнейшая, которую невозможно применить на практике.

Наверное для любых двух эквивалентных программ f и g должен существовать набор каких-то элементарных преобразований такой, что применив все эти преобразования к программе f (к её тексту, например) мы получим g. Это гипотеза. Причем преобразования должны быть непрерывными, т.е. после каждого шага преобразования мы должны получать эквивалентную программу.

Такой набор преобразований можно назавать путём из f в g. Если такой путь существует, то значит программы эквалентны. И наоборот.

Найти бы эти элементарные преобразования...

Ну η-reduction (λx.f x = f if x is not a free variable of f) очевидно подходит.

А что ещё?

По сути, это то же самое, что и доказательство теорем. Доказательство импликации A -> B это тоже путь из А в B.

@e2e6b@e2e6b4366d414349b8e0225ef22fbd4d эту гипотезу доказать бы. Но сначала нужно определиться о каких преобразованиях идёт речь.

Если бы ещё каждое такое преобразование уменьшало среднее время, то было бы вообще хорошо.

Ещё одно преобразование: если в коде есть повторение вызова функции ...f(x)...f(x)..., то очевидно это можно улучшить вычислив результат один раз и сохранив в переменную.

@7ea58@7ea582afec2e4ed499b1f43860c48972 ещё дополнительный параметр max-len нужен (максимальная длина программы) иначе оно найдёт ту, которая состоит тупо из пар (x, f(x)) для всех x.

Ешё преобразование: https://en.wikipedia.org/wiki/Loop-invariant_code_motion

Кстати такую хуйню просто можно на уровне линтера запретить.

У каждой программы f есть эквивалентная ей программа вида:

fn g(x) {
    match x {
        x1 -> y1,
        x2 -> y2,
        ...
        xn -> yn,
    }
}

такая что для любого x из конечного можества inputs верно, что f(x) = g(x).

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

Если там есть какой-то очевидный паттерн, то её можно сделать короче. Например, если y1 = y2 = ... = yn = x, то тогда её можно сократить до fn g(x) { x }. Можно конечно и увеличить длину g добавив ненужные пары.

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

Но возникает вопрос, верно ли, что из любой программы f существует путь состоящий только из улучшающих преобразований в любую другую эквивалетную ей и лучшую программу g? Или может оказаться, что мы застранянем в каком-то локальном минимуме и придётся обратно возвращаться?

@3a805@3a805bd7d827449dac388da12285cb81 нет, это не верно. Да, будут локальные минимумы. Потому что f можно улучшить через такое преобразование:

fn g(x) {
    match x {
        x1 -> y1,
        _ -> f(x),
    }
}

если в f вычисление f(x1) было медленнее чем g(x1). Таким образом мы размотаем функцию, дойдём до максимльной разрешённой длины и застрянем. Дальше придётся откатывать эти "улучшения", а это будут ухудшающие преобразования.

Улучшающие преобразования можно разделить на два вида - те, которые увеличивают длину программы и те, которые её уменьшают.

Тогда @3a805@3a805bd7d827449dac388da12285cb81 можно переформулировать заменим "улучшающих преобразований" на "улучшающих сокращающих преобразований".

Но сначала всё таки надо понять верна ли гипотеза @e2e6b@e2e6b4366d414349b8e0225ef22fbd4d

Она говорит о том, что если для программы f каждый элемент её класса эквивалетности представить в виде вершин графа, а ребра - это преобразования, то тогда этот граф связный.

Но есть дополнительные ограничения по памяти и длине.

Ладно, для начала хотя бы без ограничений понять бы.

Единственное только уточнение ещё - это то, что эквивалентность рассматривается только на заданном конечном множестве входов. Обязательно конечном.

Понятно, что каждую программу можно размотать в программу вида @0f0fb@0f0fbbf8456c4bc485588504c06c6c4a Т.е. по крайней мере в эту программу точно есть путь.

Ну и раз так, то значит есть и обратный путь из неё в любую другую эквивалентную программу. Значит гипотеза (без ограничений) точно верна.

Но так не интересно.

На практике мы не можем разматывать проги в @0f0fb@0f0fbbf8456c4bc485588504c06c6c4a

Т.е. на практике невозможно через неё прокладывать каждый путь.

Но если добавить ограничения, то непонятно всё становится. Да, при каких-то ограничениях возможно граф будет связным. Если ограничения слишком жёсткие, то не будет.

В классе эквивалетности [f] программы f: X -> Y на конечном подмножестве I ⊆ X можно ввести линейное отношение порядка. Для любых программ g и h из этого класса отношение g <= h верно тогда и только тогда когда среднее время выполнения программы g на каждом входе из I меньше либо рано среднему времени выполнения программы h на тех же входах.

Рефлексивность очевидна. Транзитивность тоже.

Тотальность тоже.

А вот антисимметричность не выполняется - может быть две разные эквивалентные программы с одинаковым средним временем. Значит всё-таки не линейное отношение.

Значит это предпорядок.

Total preorder.

Для total preorder существует линейный порядок на фактормножестве.

Теперь допустим, что из множества [f] убрали все программы, которые используют больше чем max-mem памяти, а также те длина которых больше max-len.

Определение преобразования (первый блин). Преобразование t - это программа, которая для любой программы f возвращает элемент g из множества [f].

Улучшающее преобразование t - это такое преобразование, что t(f) <= f верно для любого f.

Вопрос: существует ли множество T = {t1, t2, ..., tn} улучшающих преобразований такое, что для любой программы f существует набор (q1, q2, ..., qm), где каждый qi - это элемент T, такой, что программа q1(q2(...qm(f)...)) <= g для любого g из [f].

Очевидно, что да. В качестве t1 можно взять программу @7ea58@7ea582afec2e4ed499b1f43860c48972, n = 1, q1 = t1, m = 1.

Да, поэтому первый блин комом. Нужно менять определение @af80c@af80cd0212234550b416b8a646f98803

Интуитивно, преобразованием программы - это небольшое изменение текста программы за какое-то реалистичное не очень большое время. Но как это сформулировать формально?

Преобразование не обязательно инъективно. Например, преобразование, которое удаляет неиспользуемую переменную. В разных программах может быть в разных местах неиспользуемая переменная и может оказаться, что после преобразования программы будут равны, но исходные программы - нет.

Нужно наверное определиться с моделью вычислений. Так наверное будет проще.

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

Можно рассмотреть DFA, но для реальный программ они будут огроебенными из-за огромного количества стейтов.

Хотелось бы модель вычислений без мутабельности.

В лямбда исчислении я не представляю как ограничение памяти ввести.

По сути, потребление памяти можно наверное измерять как максимальная длина терма в процессе вычисления.

Ну да, в принципе, а что ещё надо? Ничего.

Но у лямбда исчисления ебанутая семантика, с ней сложно будет.

Конкатенативщина остаётся только.

Но это та же хуйня по сути, поэтому всё равно.

@85acf@85acff7e451e4021976f057e9a61c789 Лямбда исчисление надо брать, короче.

Определение длины терма:

|x| = 1
|(t1 t2)| = |t1| + |t2|
|(\x. t)| = |t| + 1

Длина терма равна количеству переменных в терме.

Функция - это лямбда абстракция без свободных переменных. Значение - это функция.
Пусть f - функция, I - какое-то множество значений. Если для любого x из I после каждого шага вычисления (beta редукции) терма (f x) длина получающегося терма не превышает какого-то значения L, то будем говорить, что функция f на множестве I использует не более чем L памяти.

Будем говорить, что терм t находится в L-beta нормальной форме если |t| <= L и либо в t нет beta-редексов, либо редукцию любого бета-редекса в t приводит к увеличению длины терма.

@19f92@19f9282878e24b13a589aeaca7d2d833 к увеличению длины терма, которая больше L.

Нет, лучше так не определять нормальную форму потому что она будет не уникальной.

Надо вот так. Будем говорить, что терм t находится в L-beta нормальной форме если |t| <= L и в t нет beta-редексов.

Аналогично, терм t находится в L-beta-eta нормальной форме если он в L-бета нормальной форме и в нём нет eta-редексов.

Для любых двух термов t и s отношение равенства t = s означает, что с помощью alpha-конверсии, beta и eta редукций их можно преобразовать к одному и тому же терму.
Для любых двух функций f, g и множества значений I отношение эквивалентности f ~ g означает, что (f x) = (g x) для любого x из I.

Для данного L, время вычисления time(t) терма t - это количество шагов (beta-редукций) вычисления этого терма до L-beta-нормальной формы (если её нет, то время вычисления считается бесконечным).

@5dd2e@5dd2ec5a2af049459a3ef52b5acedf2b Нет, неправильно. Вычисление этого терма до значения, а не нормальной формы.

Время вычисления time(t) терма t - это количество шагов (beta-редукций) вычисления этого терма до значения.

Преобразование терма [s->x]q в терм ((\x. q) s) называется gamma-преобразованием. Это обратное к beta-редукции преобразование.

Преобразование терма f в терм (\x. f x), где x не является свободной переменной терма f, называется delta-преобразование. Это обратное к eta-преобразование.

@bb891@bb891f3f05314f0bbf25b2ff777a4e62 Нет, определение верное, вопрос поставлен неправильно.

LT-преобразование - это преобразование p такое, что |p| <= L и для любой программы |f| <= L, time(p f) <= T.

Вопрос состоит в том чтобы найти нужные улучшающие (наверное лучше говорить не ухудшающие) преобразования чтобы выполнялось @a820a@a820a2b2b061484bbbe22fc2bc5ea36c

Вангую скоро будет мода на культурность.

@d987e@d987ed43fb9d4a8e8ded67a9969860eb Надо разбивать функции на классы по сложности и решить проблему оптимизации функций сначала для самого простого класса функций.

Хотя нет, Бордобус - я понял о чём это. Это кто-то из израиля.

@45f0a@45f0a4c043f249f289d2e5ec2016172b Можно выделить класс функций С0(L) - это функции, которые не используют рекурсию (в том числе и другие рекурсивные функции) и длина которых не превышает L.

Функции класса С0(L) могут вызывать друг друга, но только уже определенные функции (чтобы не было рекурсии).
Т.е. если построить граф зависимостей функций, то это будет DAG. Зависимые функции в этом классе можно инлайнить.

Есть 4 способа избавиться от if p { t } else { s } на входах I:
- если t = s, то if можно заменить просто на t
- если t = f(X) и s = g(X) и f ~ g, то будет f(X) если f <= g или g(X) если g <= f
- если p истинно на всех входах I, то будет t
- если p ложно на всех входах I, то будет s

Есть только один спобоб избавиться от let x = t; - только если x не используется.

@5ed8b@5ed8b85a23a441e7b69e278f378e251f Ещё два случая возможны. p может не зависеть от входных переменны и тогда можно его заранее высчитать и подменить if на t либо s. И ещё может быть, что s = t когда p = true/false, например, if x == 5 { 5 } else { x }. Вот тепереь вроде бы всё.

Всё-таки лямбда исчисление неудобная модель для рассуждений.

Лучше вот такая модель вычислений.
Есть натуральные числа: 0, 1, 2, ...
Есть функция инкрементирующая число: succ.
Есть функция сравнения чисел: ==.
Есть условное выражение: if 1 == 3 { 4 } else { 5 }.
Есть булевы значения: 0 - ложь, любое другое число - истина.
Eсть определение функций: fn foo(x, y) { if x == 5 { x } else { succ(y) } }.
Есть определение переменных внутри функции: let x = succ(5);.
Каждая функция числовая, т.е. на вход берёт n чисел и возвращает одно число.
Разрешается рекурсивный вызов определяемой функции.
Внутри функции разрешается вызывать ранее определённые функции.

Она тьюринг полная.

Логиские операторы !, &&, ||, -> легко определяются через if'ы, остальные операторы сравнения чисел <=, !=, <, >, >= тоже легко определить.

Для определения <= нужна рекурсия. Поэтому лучше взять его за основной оператор, а не ==. Тогда == и остальные операторы можно определить через <= без рекурсии.

Каррирования нет, частичного применения нет, функций высшего порядка нет.

Очень простая и удобная модель.

Класс C1(L) - это все рекурсивные функции длины не больше L, которые могут вызывать функции из C0(L).
Класс C2(L) - это все не рекурсивные функции длины не больше L, которые могут вызывать функции из C1(L).
Класс C3(L) - это все рекурсивные функции длины не больше L, которые могут вызывать функции из C1(L) либо C2(L).
Класс C4(L) - это все не рекурсивные функции длины не больше L, которые могут вызывать функции из C3(L).
Класс C3(L) - это все рекурсивные функции длины не больше L, которые могут вызывать функции из C3(L) либо C4(L).
И т.д.

Cn(L), где n = 2k - 1 или n = 2k, k - это количество вложенных рекурсий.

@8188d@8188dd9593234b87ac8fac231bbf8a56 *С5

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

Может такое происходит потому что ты просто физически мелкий?

Интересно, что имликация выражается через <= и если рассмотреть все функции из C0, которые могут использовать только оператор <= и входные переменные, то это будут все логические высказывания исчисления высказываний. И чтобы понять как можно ускорить такую программу, нужно понять как можно сократить логические выражение, а это значит найти какие его части всегда истинны/ложны при любом значении зависящих переменных, а это эквивалетно решению SAT. Прикольно.

495 496 497 498 499 500 501

515