kakadu/matrix-on-the-wall

Задача Семёна про зеркалирование матриц

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

Язык:

• MLT(x,y,...) (y,z,...) = (x,z,...)

  Обычно начальный терм такой формы, но добавлять новые MLT нельзя (при соблюдении условий корректности эта оговорка лишняя).

• EXPAND(...,z) x = (...,z,x)

  Расширяться кортежи могут только тут

• ROTATE(a,...,y,z) = (z,a,...,y)

• PROJ (x1,...,xn) (xi,...,xk) = (xi,...xk) если второй аргумент -- это подмножество первого, иначе пустой кортеж

Вариация постановки задачи.

(Вероятно, более общая и более аккуртаная).

Задача о том, как преобразовать Datalog выражение над многоместными предикатами в выражение над многомерными матрицами.

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

На выходе --- дерево преобразований над кортежами, переводащая множество кортежей в кортеж-результат. Иначе, дерево преобразований над матрицами.

Язык преобразований:

• ROTATE(a,...,y,z) = (z,a,...,y) --- циклический сдвиг кортежа. Соответствует повороту матрицы.
• EXPAND(...,z) x = (...,z,x) --- расширение кортежа. x может входить в изначальный кортеж. То есть элементы в кортеже могут дублироваться. Добавление ещё одного измерения в матрицу.
• PROJ (x1,...,xn) (xi,...,xk) = (xi,...xk) если второй аргумент --- это подпоследовательность первого, иначе пустой кортеж. Удаляем ненужные измерения.
• MULT(x,y,T) (y,z,T) = (x,z,T) --- умножение матриц. Здесь T --- хвост кортежа. Две перемножаемые матрицы должны быть согласованы. Во-первых, иметь одинаковую размерность. Во-вторых, все измерения, кроме первых двух, одинаоквые. Первые два устроены как показано в определении операции.

Построенное дерево должно удовлетворять условию корректности (иначе можно просто за счёт PROJ и EXPAND собрать нужный результат). Дерево корректно, если:

1. PROJ встречается не более одного раза и (если встречается), является корнем дерева
2. Множество листьев дерева (как множество кортежей) равно входному множеству кортежей (не включая результат).