Кафедра ИУ9

Проект включает калькулятор арифметических выражений над ординалами и прувер, позволяющий интерактивно исследовать завершаемость систем переписывания термов путём подбора их интерпретации в ординальной алгебре. Проект основан на дипломной работе Пискунова Александра (бакалавриат, выпуск 2022 года)

@Vigorge/provskell

Результат

Введите выражение и нажмите «Привести к КНФ», чтобы получить результат

Система переписывания термов

Интерпретация в ординальной алгебре

Определите систему переписывания термов, чтобы продолжить

Результат

Определите систему переписывания термов и подберите её интерпретацию в ординальной алгебре, чтобы получить результат

Примеры

f (g (x)) = g (f (f (x)))

f (Z) = Z

f (Z, x) = x

f (s (x), Z) = f (x, s (Z))

f (s (x), s (y)) = f (x, f (s (x), y))

p (u (x), u (y)) = u (p (x, y))

p (p (x, y), z) = p (x, p (y, z))

a (s (x), y) = s (a (x, y))

m (s (x), y) = a (m (x, y), y)

a (Z, x) = x

m (Z, x) = Z

n (o (x, y)) = a (n (x), n (y))

n (a (x, y)) = o (n (x), n (y))

a (x, o (y, z)) = o (a (x, y), a (x, z))

n (n (x)) = x

Provskell

Ординальный калькулятор

Введите выражение

Результат

Интерактивный прувер

Система переписывания термов

Интерпретация в ординальной алгебре

Примеры