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

Начнем с числительного Черча для нуля:

λ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 должны быть равны: δ = β, таким образом, мы достигли (β → ε) → β → γ. Но это еще не все, что мы знаем, f x имеет тип ε, а наш нумерал возвращает f x, применяя эту информацию, мы получаем ε = γ. Включив все это, мы получаем (β → γ) → β → γ, или после переименования: λf.λx. f x : (α → β) → α → β. Опять же, мы не использовали никакой информации о наших намерениях использования, поэтому у нас самый общий тип и, конечно же, он может быть специализирован (по ограничению β = α) до λf.λx. f x : (α → α) → α → α.

Теперь очередь 2:

λ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 является функцией двух аргументов: α должно быть ограничено до α' → α'' → α'''
• То же самое для n: β должно быть ограничено до β' → β'' → β'''
• Первый аргумент m и n имеет тот же тип, что и f: α' = β' = γ
• Второй аргумент n имеет тип δ.
• Тип результата n равен второму типу аргумента m: β''' = α''
• Давайте объединим все вышеперечисленные знания для n : γ → δ → α''
• То же самое для m : γ → α'' → ε
• Следовательно, тип результата (γ → α'' → ε) → (γ → δ → α'') → γ → δ → ε

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

самый общий тип для λm.λn.λf.λx. m f (n f x) это

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

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

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