John Harrison - Введение в функциональное программирование (1108517), страница 14
Текст из файла (страница 14)
считаем ()int эквивалентным int; прижелании можно легко вернуться к прежним обозначениям явным добавлениемсоответствующих частных случаев. Опираясь на приведённое определениеподстановки, введём отношение «тип σ является более общим, чем тип σ 0 »,обозначив его через σ σ 0 .7 Пара типов входит в данное отношение тогда и толькотогда, когда найдётся множество подстановок θ такое, что σ 0 = σθ. Например:αα→αα → boolβ→αα→α6σβ→β(β → β) → boolα→β(β → β) → βС учётом изложенного выше, сформулируем основную теорему данного раздела:Теорема 4.4 Каждый типизируемый терм имеет главный тип, т.
е. дляпроизвольного t : τ найдется тип σ такой, что t : σ и для любого типа σ 0 из t : σ 0следует σ σ 0 .Легко убедиться, что отношение является отношением квазипорядка, тоесть, рефлексивно и транзитивно. Главный тип не уникален, но при этом всеего возможные формы равны с точностью до переименования входящих в нихпеременных типа. В более точной формулировке, если σ и τ являются одновременноглавными типами выражения, то справедливо σ ∼ τ , то есть σ τ и τ σодновременно.Доказательство теоремы о главном типе не требует особых усилий, новвиду большого объёма в рамках данного курса не рассматривается.
Следуетлишь запомнить его основное свойство: процедура доказательства представляетсобой конкретный алгоритм поиска такого типа. Этот алгоритм известен какалгоритм Милнера, либо, чаще, как алгоритм Хиндли-Милнера.8 Все реализацииML и некоторых других функциональных языков включают в себя некоторуюразновидность этого алгоритма, благодаря чему для произвольных выраженийавтоматически выводится их главный тип либо устанавливается невозможностькорректной типизации.7Это отношение рефлексивно, так что формулировка «не менее общий, чем» была бы точнее.Приведённая нами формулировка теоремы была опубликована в работе Milner (1978), но каксама теорема, так и алгоритм были ранее открыты Хиндли в его исследованиях по комбинаторнойлогике.846Глава 4.
Типы4.34.3. Сильная нормализацияСильная нормализацияОбратимся вновь к нашим примерам термов, не имеющих нормальной формы,таким как((λx. x x x) (λx. x x x))−→ ((λx. x x x) (λx. x x x) (λx. x x x))−→ (· · ·)В рамках типизированного лямбда-исчисления подобная ситуация невозможнана основании теоремы о сильной нормализации, доказательство которой слишкомдлинно, чтобы быть здесь приведённым.Теорема 4.5 (О сильной нормализации) Любой типизируемый терм имеетнормальную форму, а любая возможная последовательность редукций, котораяначинается с типизируемого терма, завершается.9На первый взгляд преимущества очевидны — функциональная программа,удовлетворяющая нашей дисциплине типов, может вычисляться в произвольномпорядке, при этом процесс редукции всегда конечен и приводит к единственнойнормальной форме.
(Единственность следует из теоремы Чёрча-Россера, котораяостаётся справедливой и в случае типизированного лямбда-исчисления.) Однако,возможность реализации незавершимых функций необходима для обеспеченияТьюринг-полноты,10 в противном случае мы более не в состоянии определитьпроизвольные вычислимые функции, более того — даже не всё множество всюдуопределённых функций.Мы бы могли пренебречь этим ограничением, если бы оно позволяло намиспользовать все функции, представляющие практический интерес. Однако, этоне так — класс всевозможных функций, представимых в рамках типизированноголямбда-исчисления, оказывается весьма узким.
В работе Schwichtenberg (1976)показано, что класс представимых функций на основе нумералов Чёрча ограниченвсевозможными полиномами либо кусочными функциями на их основе. Отметим,что это strictly intensional: рассмотрев другое представление чисел, получим другойкласс функций. В любом случае, для универсального языка программирования этогонедостаточно.Поскольку все определимые функции являются всюду определёнными, мы,очевидно, не в состоянии давать произвольные рекурсивные определения. (???)В самом деле, оказывается, что обычные комбинаторы неподвижной точки неподдаются типизации; очевидно, что тип Y = λf. (λx.
f (x x))(λx. f (x x)) несуществует, поскольку x применяется к самому себе, будучи связанным лямбдаабстракцией. Для восстановления Тьюринг-полноты введём альтернативный способзадания произвольных рекурсивных функций, не принося в жертву типизацию.9Под «слабой нормализацией» подразумевается первая часть данного утверждения овозможности преобразования произвольного терма в нормальную форму; при этом некоторыепоследовательности редукций могут оказаться бесконечными.10Располагая любым рекурсивным перечислением множества всюду определённых вычислимыхфункций, мы всегда можем определить ещё одну, не входящую в это множество, методомдиагонализации. (Подробнее об этом будет рассказано в курсе теории алгоритмов.)474.3. Сильная нормализацияГлава 4.
ТипыОпределим полиморфный оператор рекурсии, всевозможные типы которого имеютвидRec : ((σ → τ ) → (σ → τ )) → σ → τи дополнительное правило редукции, согласно которому для произвольнойфункции F : (σ → τ ) → (σ → τ ) мы имеемRec F −→ F (Rec F )Начиная с этого момента будем полагать, что рекурсивные определения вида letrec отображаются на эти операторы рекурсии.Дополнительная литератураТипизированное лямбда-исчисление рассматривается, в числе прочего, вработах Barendregt (1984) и Hindley and Seldin (1986).
Основополагающая работа Milner (1978) продолжает оставаться важным источником информации о полиморфнойтипизации, включая алгоритм поиска главного типа. Хорошее введение втипизированное лямбда-исчисление, включающее доказательство теоремы о сильнойнормализации, а также обсуждение некоторых интересных взаимосвязей с логикой,даётся в Girard, Lafont, and Taylor (1989). В данной работе также обсуждаетсяболее развитая версия типизированного лямбда-исчисления под названием System F, в рамках которой возможно определение большинства требуемых на практикефункций даже при сохранении свойства сильной нормализации.Упражнения1.
Справедливо ли, что из Γ ` t : σ для произвольной подстановки θ следует Γ `t : (σθ)?2. Докажите формально теорему 4.3 о сохранении типа для α и β-преобразования.3. Покажите, что свойство сохранения типа необратимо, т. е. что возможнаситуация, когда из справедливости t −→ t0 и Γ ` t0 : σ не следует, что Γ ` t : σ.4. (*) Докажите, что каждый терм типизированного лямбда-исчисления, чейглавный тип равен (α → α) → (α → α), редуцируется до нумерала Чёрча.5. (*) В какой мере процесс проверки типов является обратимым, т. е.допускает вывод терма по его типу? Например, справедливо ли, что в чистомтипизированном лямбда-исчислении с переменными типа, но без констант иоператора рекурсии, любое t : α → β → α на самом деле эквивалентно K =λx y. x в традиционной трактовке лямбда-эквивалентности.
Если это так, токаковы дальнейшие возможности обобщения результата?116. (*) Будем говорить, что некоторое отношение редукции −→ обладаетслабым свойством Чёрча-Россера, если всякий раз, когда t −→ t111Подробнее по данному вопросу см. Mairson (1991).48Глава 4. Типы4.3. Сильная нормализацияи t −→ t2 , найдётся u такое, что t1 −→∗ u и t2 −→∗ u, где −→∗представляет собой рефлексивное транзитивное замыкание −→. Докажителемму Ньюмена, в которой утверждается, что если отношение обладает слабымсвойством Чёрча-Россера и удовлетворяет принципам сильной нормализации,то для −→∗ справедливо свойство Чёрча-Россера.
(Указание: воспользуйтесьтрансфинитной индукцией.)1212Если в ходе доказательства возникнут затруднения, см. работу Huet (1980).494.3. Сильная нормализацияГлава 4. Типы50Глава 5Знакомство с MLВ предыдущих главах мы начали с чистого λ-исчисления, которое затемсистематически расширяли новыми возможностями. Например, мы добавилипримитивную конструкцию let, чтобы сделать полиморфную типизацию болееполезной, а также оператор рекурсии для восстановления вычислительной полноты,потерянной после введения типов.
Двигаясь дальше по этому пути, мы в конечномсчёте приходим к ML, при этом сохранив простоту мировоззрения, сформированногов ходе изучения типизированного λ-исчисления.Очередным этапом на этом пути будет отказ от представления данных (например,натуральных чисел и логических значений) в виде термов лямбда-исчисленияи замена их примитивами, такими как типы bool (для логических значений)и int (для целых чисел).
В дополнение, введём новые конструкторы типов,такие как ×, — желательность подобного шага уже упоминалась в предыдущейглаве. С этими изменениями также связаны новые константы и новые правилапреобразования. Например, выражение 2 + 2 будет вычисляться с использованиеммашинной арифметики вместо представления его в нумералах Чёрча и выполненияβ-преобразований. Эти дополнительные преобразования, рассматриваемые какрасширение обычных λ-операций, часто называются ‘δ-преобразованиями’. В течениекурса мы неоднократно увидим, чем язык ML отличается от чистого λ-исчисления.Первым делом обратимся к фундаментальному вопросу стратегии вычислениявыражений в ML.5.1Энергичное вычислениеКак уже было сказано ранее, с теоретической точки зрения нормальныйпорядок (сверху вниз, слева направо) редукции выражений более предпочтителен,потому что если хоть какая-то стратегия завершается, то и эта тоже.1 Однако,такой подход имеет некоторые практические недостатки. Например, рассмотримследующее выражение:(λx.
x + x + x) (10 + 5)При использовании нормального порядка редукции мы получаем (10 + 5) + (10 +1Данная стратегия подобна некоторым, используемым в традиционных языках, таких как Algol 60, где её называют вызов по имени.515.1. Энергичное вычислениеГлава 5.
Знакомство с ML5) + (10 + 5), так что на следующих шагах мы должны вычислить одно и то жевыражение трижды. На практике это совершенно недопустимо. Существуют дваосновных решения данной проблемы, и эти решения делят мир функциональногопрограммирования на два лагеря.Первое решение — придерживаться нормального порядка редукции, но при этомпытаться оптимизировать реализацию так, чтобы разнообразные подвыражения,возникающие при таком подходе, использовались совместно и никогда невычислялись более одного раза.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
