Задача Семёна про зеркалирование матриц
Дан начальный терм и результат, нужно подобрать минимальную программу, которая превращает это терм в нужный результат.
Язык:
-
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 собрать нужный результат). Дерево корректно, если:
- PROJ встречается не более одного раза и (если встречается), является корнем дерева
- Множество листьев дерева (как множество кортежей) равно входному множеству кортежей (не включая результат).