m в степени 0 в цифрах Черча

Тема по компьютерным наукам на уровне бакалавриата.
При рассмотрении теории я столкнулся с неприятной проблемой, связанной с (0 m) в терминах возведения в степень числительных Чёрча в лямбда-исчислении.
Насколько я знаю, (0 m) при сокращении приводит к λx. x, что не 1 (= m^0), как ожидалось, и даже не входит в церковные цифры.

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

n := λfx. (f^n x) = (f ... (f x))

Во многих литературах говорится, что

EXP(m, n) := λmn. (n m)

возвращает m^n для заданных m и n числительных церкви, и я понимаю, что в большинстве случаев функция отвечает правильно. Но это не тот случай, когда n = 0 так как

(0 m) = ((λfx. x) m) → λx. x

В математике 1 — это элемент идентичности натуральных чисел, рассматриваемых как мультипликативная группа, то есть x * 1 = 1 * x для любого x в N. Итак, если я установлю функцию EXP в виде

EXP’(m, n) := λmn. (n (MUL m) 1)

для MUL(m, n) = m * n это, кажется, работает нормально, совпадая с тем фактом, что m^0 часто определяется как 1 в математике. Также это кажется простым в смысле гипероперации.

ГИПЕРОПЕРАЦИЯ: https://en.m.wikipedia.org/wiki/Hyperoperation

Я ожидаю, что некоторые критические замечания, такие как m^0, не обязательно 1 в математике, а жесткие математики скажут, что все зависит от определений. Но тогда есть ли какая-то логическая поддержка для принятия прежнего стиля EXP(m, n)? Он не возвращает церковные цифры, когда n = 0, поэтому мне все еще кажется, что он плохо определен.

Вопрос

  1. «Почему определение EXP(m, n) := λmn. (n m) обычно принимается для m^n, хотя его вывод может быть не церковным числом для церковных числовых входов?»

  2. «Знаете ли вы какое-нибудь небольшое исправление EXP, чтобы функция хорошо работала для всех числовых входов церкви?»

  3. «Любая проблема или недопонимание моей критики в адрес (0 m)».

Кроме того, существуют ли логические предпосылки для того, чтобы результатом (0 m) было λx. x, что является элементом идентичности композиции функции, а не 1? Это просто совпадение или я слишком серьезно думаю?

Любые идеи приветствуются.

Я хочу следовать определениям алгебры из Википедии, связанным с числительными церкви, если это необходимо.

КОДИРОВАНИЕ ЦЕРКВИ: https://en.m.wikipedia.org/wiki/Church_encoding

Спасибо.


lambda exponentiation computation-theory church-encoding lambda-calculus
person mriryt    schedule 11.01.2020    source источник
comment
Это вопрос, который может лучше подойти для сообщества компьютерных наук в сети обмена стеками.   -  person GhostCat    schedule 11.01.2020

Ответы (1)


arrow_upward
2
arrow_downward

Простое недоразумение: вы говорите «λx. x, что не является 1», но λx. x действительно является числом Чёрча 1. Вы, вероятно, знаете цифру Чёрча 1 как λfx. f x, но простая эта-редукция и альфа-преобразование показывают, что это эквивалентно λx. x.

person Joseph Sible-Reinstate Monica    schedule 11.01.2020
comment
Ага! Вы восполнили недостающую часть. Я идиот. λfx. (f x) = λf. (λx. f x) → η λf. f →αλx. Икс - person mriryt; 11.01.2020