Найти наиболее общие тип следующей лямбды-термины исчисления

Question

У меня возникают проблемы понять, почему они являются наиболее общими типами для соответствующего Чёрча:

2 = λf.λx. f (f x) : (α → α) → α → α 

1 = λf.λx. f x : (α → β) → α → β 

0 = λf.λx. x : β → α → α 

Я думал, что все церковные числительные имел один и тот же тип:

(α → α) → α → α 

Кроме того, как я нашел бы общий тип для добавления оператора

λm.λn.λf.λx. m f (n f x) 

Любая помощь будет действительно оценена, спасибо!

Answer 1

Начнем с цифрой церкви на ноль:

λf.λx. x : β → α → α 

Глядя только на λf.λx. части, можно сделать вывод, что у нас есть функция двух аргументов, следовательно, его тип α → β → γ, где α и β стенд для типы аргументов и γ обозначает тип результата. Теперь тело x дополнительно ограничивает тип: возвращаемый тип нашей функции должен быть таким же, как и тип второго аргумента. Это приводит к α → β → β или после переименования (α ↔ β): λf.λx. x : β → α → α. Это самый общий тип для нуля, так как мы не использовали тот факт, что f должен быть функцией, по сути, нулевой цифрой церкви в нетипизированной лямбда-исчисления не заботятся: она просто забывает о первом аргументе. А так как β является просто заполнителем, вы можете специализироваться на до α → α, что приводит к более конкретному типу для нуля - λf.λx. x : (α → α) → α → α.

Давайте посмотрим на 1:

λf.λx. f x : (α → β) → α → β 

Опять же, это функция двух аргументов: α → β → γ, но на этот раз (смотреть на тело 1) мы знаем, что первый аргумент f является функцией, так f имеет некоторый тип δ → ε, который мы должны заменить на α: (δ → ε) → β → γ. Теперь мы знаем, что мы должны быть в состоянии применить f к x, что означает, что тип x и тип аргумента f «s должен быть равен: δ = β, таким образом, мы достигли (β → ε) → β → γ. Но это еще не все, что мы знаем, f x имеет тип ε, а наша цифра возвращает f x, применяя эту информацию, мы получаем ε = γ. Включая все это, мы приходим к (β → γ) → β → γ или после переименования: λf.λx. f x : (α → β) → α → β. Снова мы не использовали никакой информации о наших интенсивностях использования, поэтому у нас есть самый общий тип и, конечно же, он может быть специализированным (по ограничению β = α) до λf.λx. f x : (α → α) → α → α.

Это 2 «s Обратимся теперь:

λf.λx. f (f x) : (α → α) → α → α 

Я не буду повторять все шаги, на этот раз, но (как промежуточный этап), мы можем прийти к λf.λx. f (f x) : (α → β) → α → β.Обратите внимание, однако, что на этот раз мы корнем результат f: f (f x), и это означает, что входные и выходные типы f должны быть равны, таким образом β = α, а самый общий тип - λf.λx. f (f x) : (α → α) → α → α.

(*) Обратите внимание, что церкви 3, 4 и т.д. имеют один и тот же самый общий тип, как 2 сделать, потому что несколько приложений функции не дают нам дополнительную информацию, чтобы специализироваться тип дальше.

---

Что касается функции добавления λm.λn.λf.λx. m f (n f x), позвольте мне быть немного более лаконична:

• Предположим, что выражение имеет тип α → β → γ → δ → ε.
• m является функцией 2 аргументов: α должно быть ограничено α' → α'' → α'''
• То же самое для n: β должно быть ограничено β' → β'' → β'''
• m «s и n» первый аргумент s имеет тот же тип, который является тип f: α' = β' = γ
• n «s второго типа аргумента является δ
• n 's результат типа равен m' s второго типа аргумента: β''' = α''
• Давайте объединить все выше знания для n : γ → δ → α''
• Same для m : γ → α'' → ε
• Следовательно, тип результата является (γ → α'' → ε) → (γ → δ → α'') → γ → δ → ε

Давайте переименуем переменные, чтобы они выглядели немного красивее:

наиболее общий тип для λm.λn.λf.λx. m f (n f x) является

(β → γ → ε) → (β → α → γ) → β → α → ε.

Давайте посмотрим, что это может быть специализированы к тому, что можно было бы ожидать, что бинарная операция на Чёрча (β = α → α, γ = α, ε = α):

((α → α) → α → α) → ((α → α) → α → α) → (α → α) → α → α.