Просто типизированное лямбда-исчисление

---

Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система ${\displaystyle \lambda ^{\rightarrow }}$) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году^[1]. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году^[2].

В базовой версии системы ${\displaystyle \lambda ^{\rightarrow }}$ типы конструируются из набора переменных с помощью единственного бинарного инфиксного конструктора ${\displaystyle \rightarrow }$. По традиции для переменных типа используют греческие буквы, а оператор ${\displaystyle \rightarrow }$ считают правоассоциативным, то есть ${\displaystyle \alpha \rightarrow \beta \to \gamma }$ является сокращением для ${\displaystyle \alpha \rightarrow (\beta \to \gamma )}$. Буквы из второй половины греческого алфавита (${\displaystyle \sigma }$, ${\displaystyle \tau }$, и т.д.) часто используются для обозначения произвольных типов, а не только переменных типа.

Различают две версии просто типизированной системы. Если в качестве термов используются те же термы, что и в бестиповом лямбда-исчислении, то систему называют неявно типизированной или типизированной по Карри. Если же переменные в лямбда-абстракции аннотируются типами, то систему называют явно типизированной или типизированной по Чёрчу. В качестве примера приведём тождественную функцию в стиле Карри: ${\displaystyle \lambda x.~x}$, и в стиле Чёрча: ${\displaystyle \lambda x\!:\!\alpha .~x}$.

Правила редукции не отличаются от правил для бестипового лямбда-исчисления. ${\displaystyle \beta }$-редукция определяется через подстановку

Для ${\displaystyle \eta }$-редукции требуется, чтобы переменная ${\displaystyle x}$ не была свободной в терме ${\displaystyle M}$.

---