Диссертация (1150902), страница 4
Текст из файла (страница 4)
А именно, при типизации по Чёрчу терм имеет не более одноготипа, в то время как при типизации по Карри он может иметь один или несколько типов, или быть нетипизируемым вовсе. Так, терм λx : τ.x (при типизациипо Чёрчу) имеет единственный тип τ → τ , где τ — некоторый конкретный тип,5Иногда под типизацией по Чёрчу понимают явно типизированные системы (типы переменных явно указываютсяв синтаксисе языка), а под типизацией по Карри — неявно типизированные (типы присваиваются в процессе компиляции или интерпретации программы).
Путаница возникла в виду того, что сам Чёрч описывал своё исчислениев явном стиле, в то время как Карри использовал неявный стиль. Несмотря на то, что такой взгляд на стили типизации является исторически сложившимся: явно типизированные системы часто описывались и описываются в стилеЧёрча, а неявно типизированные — в стиле Карри, — он всё же является ошибочным.19СинтаксисТипизацияΛCh ::= V | ΛCh ΛCh| λV .ΛτChТипыτ ::= ι | τ → τКонтекстыΓ ::= ∅ | Γ, V : τx:τ ∈ΓΓ ⊢Ch x : τΓ, x : τ ⊢Ch e : σΓ ⊢Ch λxτ .e : τ → σΓ ⊢Ch e1 : τ1 → τ2Γ ⊢Ch e2 : τ2Γ ⊢Ch e1 e2 : τ2Рисунок 5. Простое типизированное лямбда-исчисление в стиле Чёрчауказанный в синтаксисе, например, ι или (ι → ι → ι) → ι → ι → ι и т.д.
Аналогичному терму — λx.x — в представлении Карри соответствует целое множествотипов {α → α | α ∈ τ }.Как уже упоминалось, не все термы бестипового исчисления являются термами простого типизированного, более того, в отличие от бестипового лямбдаисчисления, простое типизированное является строго нормализуемым (StronglyNormalized). Это означает, что каждый допустимый терм имеет нормальную форму, а процедура его нормализации всегда завершается. Так например, терм бестипового лямбда-исчисления ω = (λx.xx)(λx.xx) не имеет нормальной формы ине является допустимым термом простого типизированного лямбда-исчисления.Исчерпывающее описание простого типизированного лямбда-исчисления и егосвойств, а также и описание более богатых систем типов читатель может найти в[30, 31, 83].1.3.
Стратегии вычисленийГоворят, что терм находится в β-нормальной форме (далее — просто в нормальной форме), если он не содержит редексов, т.е. к нему не применима аксиомаβ-редукции. Два терма называются равными с точностью до α-конверсии, еслиони имеют одну и ту же нормальную форму. Вычисление в лямбда-исчисленииесть вычисление нормальной формы терма — нормализация.
Конечно, ввидуТьюринг-полноты λ-исчисления, не все термы имеют нормальную форму, например, вычисление терма, также известного как терм омега (ω, омега-комбинатор,20Редукция под абстракциейРедукция аргументовДаНетДа(Сильная) нормальная формаСлабая нормальная формаS ::= λx.N | x N1 . . . NnW ::= λx.e | x W1 . . . WnНетГоловная нормальная форма Слабая головная нормальная формаH ::= λx.H | x e1 . .
. enE ::= λx.e | x e1 . . . enгде ∀ i ∈ N, ei — произвольный лямбда-термТаблица 1: Нормальные формыOmega-Combinator), ω = σσ = (λx.x x) (λx.x x) расходится. Важным свойством вконтексте нормализации является свойство Чёрча–Россера (Church–Rosser), также известное как свойство ромба: если термы s и t получены из терма n посредством β-редукции, n →∗β s и n →∗β t, то существует такой терм m, что s →∗β m иt →∗β m. Прямым следствием свойства ромба является единственность нормальной формы терма, если таковая существует.
Тем не менее, в аксиоме β-редукцииничего не сказано про порядок, в котором должна выполняться β-редукция терма.Далее в этой главе мы рассмотрим существующие порядки (стратегии, ReductionStrategies) редукции и их свойства.Разнообразие стратегий вычислений в лямбда-исчислении обусловлено, в томчисле, тем, что разные языки программирования создавались для различных целей и, соответственно, имеют разные свойства и реализации.
Несмотря на то, чтоне все порядки редукции приводят терм к нормальной форме, они зачастую завершаются в некоторой “нормальной” 6 для этого порядка форме, которая с точки зрения конкретного порядка редукции считается значением, т.е. термом, который нередуцируется дальше, даже если содержит редексы. Основными свойствами стратегий редукции являются произведение редукции под абстракцией и редукция аргументов. В таблице 1 7 приведены “нормальные” формы, получаемые при всехкомбинациях этих свойств, описанные в терминах контекстно-свободных грамматик.6Данная форма не является нормальной формой в том смысле, что терм, находящийся в ней, может содержатьредексы.
Для того, чтобы такая терминология не вводила в заблуждение, нормальную форму часто называют сильнойнормальной формой, а остальные “нормальные” формы имеют некоторый дополнительный префикс, описывающий“какая именно это нормальная форма”, например, головная нормальная форма (см. раздел 1.4 и таблицу. 1).7Таблица заимствована из статьи П.
Сестофта (P. Sestoft) [86].211.3.1. Слабые порядки редукцииСлабые порядки редукции характеризуются тем, что они рассматривают абстракцию как значение и, соответственно, не производят редукцию под абстракцией.Вызов по имени (Call-by-Name).Стратегия вычисления по имени сначала вы-числяет функцию до значения, лямбда-абстракции, после чего редуцирует её применение к аргументу путём подстановки тела аргумента вместо каждого вхождения переменной, по которой эта абстракция произведена. Это может привести кповторным вычислениям аргументов, если имеется несколько вхождений переменной, по которой производилась абстракция функции.
Формально, на каждомшаге раскрывается самый левый самый внешний редекс, который не находитсяпод лямбда-абстракцией. Таким образом, вызов по имени завершается в слабойголовной нормальной форме.Вызов по значению (Call-by-Value) в отличие от вызова по имени сначала производит редукцию аргументов и лишь потом применяет к ним функции. Формально, на каждом шаге раскрывается самый левый самый внутренний редекс, который не находится под лямбда-абстракцией. Таким образом, вызов по значениюзавершается в слабой нормальной форме.Вызов по необходимости (Call-by-Need)является вызовом по имени8 , в кото-рый добавлена мемоизация. Это означает, что при вычислении аргумента его значение сохраняется и не вычисляется повторно при последующем использованииаргумента.
В чистых функциональных языках, где нет побочных эффектов, результат вызова по имени и вызова по необходимости будет одинаковым, а значит,вызов по необходимости завершается в слабой головной нормальной форме. Одним из наиболее популярных языков, использующих вызов по необходимости,является язык Haskell.8Иногда стратегию вызова по необходимости определяют как вызов по значению, вычисление аргумента в которомотложено до момента его реального использования.
Не составляет труда показать, что это определение эквивалентноприведённому выше.221.3.2. Сильные порядки редукцииНормальный порядокотличается от стратегии вызова по имени тем, что онпроизводит сильную редукцию, т.е. редукцию под абстракцией, а также редукциюаргументов. Первым на каждом шаге раскрывается самый левый самый внешнийредекс. В отличие от других порядков редукции, нормальный порядок редукцииявляется нормализирующим (Normalizing), т.е.
завершается в сильной нормальнойформе терма тогда и только тогда, когда последняя существует. С другой стороны,как и вызов по имени, нормальный порядок редукции может проделывать одну иту же работу несколько раз. Например, (λx.xx)((λy.y)a) → ((λy.y)a)((λy.y)a) →a((λy.y)a) → aa дважды редуцирует редекс (λy.y)a.Аппликативный порядок.В то время как нормальный порядок является силь-ной версией вызова по имени, аппликативный порядок является сильной версиейвызова по значению.
Иными словами, на каждом шаге первым раскрывается самый левый самый глубокий редекс. Например, (λx.xx)((λy.y)a) → (λx.xx)a →aa. Аппликативный порядок, если завершается, приводит терм в сильную нормальную форму. Тем не менее, в отличие от нормального порядка редукции, аппликативный порядок может не завершаться даже в том случае, если терм имеет нормальную форму. Зачастую, это происходит тогда, когда какой-нибудь аргумент функции не имеет нормальной формы и при этом не используется в еётеле.
Например, терм (λx.λy.x)a((λx.xx)(λx.xx)) имеет нормальную форму a, вто время как его аргумент ((λx.xx)(λx.xx)), уже известный нам терм ω, нормальной формы не имеет, и его вычисление расходится. Более того, аппликативныйпорядок редукции не способен редуцировать терм, являющийся применением рекурсивной функции к аргументу, даже если комбинатор рекурсии, используемыйдля определения рекурсивной функции, является специальным комбинатором длявызова по значению.Головная редукция (Head Reduction, Leftmost Head Reduction)производитредукцию только головных редексов.
Редекс называется головным, если его предками в абстрактном синтаксическом дерева терма являются лишь абстракции. Например, редекс (λy.e1 )e2 является головным в терме λx1 . . . . λxn .(λy.e1 )e2 . . . em .Завершается головная редукция в головной нормальной форме. Заметим, что по-23вторное применение головной редукции к аргументам получившейся головнойнормальной формы нормализует терм. Более того, такая стратегия редукции является нормализирующей.Существуют и другие порядки редукции, зачастую являющиеся лишь вариациями и разнообразными комбинациями вышеописанных порядков редукции.Можно упомянуть такие порядки как гибридный (Hybrid) аппликативный порядок, гибридный нормальный порядок или спинальная головная редукция (SpineHead Reduction), и другие (см.
[30, 86]).1.4. Головная нормальная форма и дерево БёмаПроизвольный лямбда-терм M можно записать в следующей форме9 :[M = λ⃗v .U V1 . . . Vn , где U =y(λy.P )Q(1)В первом случае говорят, что терм M находится в головной нормальной форме(Head Normal Form), во втором случае (λy.P )Q образует головной редекс. Заметим, что по определению терм находится в головной нормальной форме тогда итолько тогда, когда он не содержит головных редексов. Важным следствием этогоопределения является то, что головная нормальная форма не обладает свойствомединственности: один и тот же терм может иметь более одной головной нормальной формы — например, головной нормальной формой терма y((λx.x)z) являетсякак терм сам по себе, так и его нормальная форма yz.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
