Русская Википедия:Просто типизированное лямбда-исчисление
Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система <math>\lambda^\rightarrow</math>) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году[1]. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году[2].
Формальное описание
Синтаксис типов и термов
В базовой версии системы <math>\lambda^\rightarrow</math> типы конструируются из набора переменных с помощью единственного бинарного инфиксного конструктора <math>\rightarrow</math>. По традиции для переменных типа используют греческие буквы, а оператор <math>\rightarrow</math> считают правоассоциативным, то есть <math>\alpha\rightarrow\beta\to\gamma</math> является сокращением для <math>\alpha\rightarrow(\beta\to\gamma)</math>. Буквы из второй половины греческого алфавита (<math>\sigma</math>, <math>\tau</math>, и т.д.) часто используются для обозначения произвольных типов, а не только переменных типа.
Различают две версии просто типизированной системы. Если в качестве термов используются те же термы, что и в бестиповом лямбда-исчислении, то систему называют неявно типизированной или типизированной по Карри. Если же переменные в лямбда-абстракции аннотируются типами, то систему называют явно типизированной или типизированной по Чёрчу. В качестве примера приведём тождественную функцию в стиле Карри: <math>\lambda x.~x</math>, и в стиле Чёрча: <math>\lambda x\!:\!\alpha.~x</math>.
Правила редукции
Правила редукции не отличаются от правил для бестипового лямбда-исчисления. <math>\beta</math>-редукция определяется через подстановку
- <math>(\lambda x\!:\!\sigma.~M)~N\ \to_{\beta}\ M[x:=N]</math>.
<math>\eta</math>-редукция определяется так
- <math>\lambda x\!:\!\sigma.~M~x\ \to_{\eta}\ M</math>.
Для <math>\eta</math>-редукции требуется, чтобы переменная <math>x</math> не была свободной в терме <math>M</math>.
Контексты типизации и утверждения типизации
Контекстом называется множество утверждений о типизации переменных, разделённых запятой, например,
- <math>f\!:\!(\beta\to\gamma),g\!:\!(\alpha\to\beta),x\!:\!\alpha</math>
Контексты обычно обозначают прописными греческими буквами: <math>\Gamma,\Delta</math>. В контекст можно добавить «свежую» для этого контекста переменную: если <math>\Gamma</math> — допустимый контекст, не содержащий переменной <math>x</math>, то <math>\Gamma,x\!:\!\alpha</math> — тоже допустимый контекст.
Общий вид утверждения о типизации таков:
- <math>\Gamma\vdash M\!:\!\sigma</math>
Это читается следующим образом: в контексте <math>\Gamma</math> терм <math>M</math> имеет тип <math>\sigma</math>.
Правила типизации (по Чёрчу)
В просто типизированном лямбда-исчислении приписывание типов термам осуществляется по приведённым ниже правилам.
Аксиома. Если переменной <math>x</math> присвоен в контексте тип <math>\sigma</math>, то в этом контексте <math>x</math> имеет тип <math>\sigma</math>. В виде правила вывода:
| <math>{x\!:\!\sigma \in \Gamma}\over{\Gamma \vdash x\!:\!\sigma }</math> |
Правило введения <math>\rightarrow</math>. Если в некотором контексте, расширенном утверждением, что <math>x</math> имеет тип <math>\sigma</math>, терм <math>M</math> имеет тип <math>\tau</math>, то в упомянутом контексте (без <math>x</math>), лямбда-абстракция <math>\lambda x\!:\!\sigma.~M</math> имеет тип <math>\sigma \to \tau</math>. В виде правила вывода:
| <math>{\Gamma,x\!:\!\sigma\vdash M\!:\!\tau}\over{\Gamma\vdash (\lambda x\!:\!\sigma.~M)\!:\!(\sigma \to \tau)}</math> |
Правило удаления <math>\rightarrow</math>. Если в некотором контексте терм <math>M</math> имеет тип <math>\sigma \to \tau</math>, а терм <math>N</math> имеет тип <math>\sigma</math>, то применение <math>M~N</math> имеет тип <math>\tau</math>. В виде правила вывода:
| <math>{\Gamma\vdash M\!:\!(\sigma\to\tau)\quad\Gamma\vdash N\!:\!\sigma}\over{\Gamma\vdash (M~N)\!:\!\tau}</math> |
Первое правило позволяет приписать тип свободным переменным, задав их в контексте. Второе правило позволяет типизировать лямбда-абстракцию стрелочным типом, убирая из контекста связываемую этой абстракцией переменную. Третье правило позволяет типизировать аппликацию (применение) при условии, что левый аппликант имеет подходящий стрелочный тип.
Примеры утверждений о типизации в стиле Чёрча:
- <math>x\!:\!\alpha\vdash x\!:\!\alpha</math> (аксиома)
- <math>\vdash (\lambda x\!:\!\alpha.~x)\!:\!(\alpha\to\alpha)</math> (введение <math>\rightarrow</math>)
- <math>f\!:\!(\beta\to\gamma\to\delta),y\!:\!\beta\vdash (f~y)\!:\!(\gamma\to\delta)</math> (удаление <math>\rightarrow</math>)
Свойства
- Просто типизированная система обладает свойством типовой безопасности: при <math>\beta</math>-редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.
- В 1967 году Уильям Тэйт доказал[3], что <math>\beta</math>-редукция для просто типизированной системы обладает свойством сильной нормализации: любой допустимый терм за конечное число <math>\beta</math>-редукций приводится к единственной нормальной форме. Как следствие <math>\beta\eta</math>-эквивалентность термов оказывается разрешимой в этой системе.
- Изоморфизм Карри — Ховарда связывает просто типизированное лямбда-исчисление с так называемой «минимальной логикой» (фрагментом интуиционистской логики высказываний, включающим только импликацию): населённые типы являются в точности тавтологиями этой логики, а термы соответствуют доказательствам, записанным в форме естественного вывода.
Примечания
Литература
- Шаблон:Книга
- Перевод на русский язык: Шаблон:Книга
- Шаблон:Статья
