John Harrison - Введение в функциональное программирование (1108517), страница 8
Текст из файла (страница 8)
Еёпостроение начинается с определения формальных правил конструирования22Глава 2. Лямбда-исчисление2.4. Комбинаторывыражений, в которые не входит λ-абстракция, но входят комбинаторы. Далеевместо α, β и η-преобразований вводятся правила преобразования для выражений,включающих комбинаторы, например, K x y −→ x. Такая теория будет иметьмножество аналогий в традиционном λ-исчислении, например, теорема ЧёрчаРоссера оказывается справедливой и для приведённого выше определения редукции.Кроме того, полностью устраняются сложности со связыванием переменных. Темне менее, мы считаем полученный формализм не слишком интуитивным, посколькукомбинаторные выражения нередко бывают весьма неясными.Помимо важной роли, которую комбинаторы играют в логике, они также имеюти определённый практический потенциал. Как мы уже кратко упоминали (подробноеизложение ожидается в следующих разделах), λ-исчисление может считатьсяпростым функциональным языком, основой для более развитых и практическиприменимых языков, наподобие ML.
Теорема о комбинаторной полноте даётоснование говорить, что выражения λ-исчисления могут быть «скомпилированы» в«машинный код» комбинаторов. Эта терминология из теории языковых процессоровоказывается на самом деле вполне уместной. Комбинаторы применялись каксредство реализации функциональных языков, в том числе и на уровне аппаратногообеспечения, предназначенного для вычисления комбинаторных выражений.Дополнительная литератураЭнциклопедическая, но при этом доступная работа по теории λ-исчисления —Barendregt (1984). Другой популярный учебник — Hindley and Seldin (1986).
Обе этикниги содержат доказательства результатов, которые мы приводим без обоснования.Вторая часть Gordon (1988) представляет собой упрощенное изложение предмета,ориентированное на его применение в прикладной математике. Существенная частьданного курса базируется на последней работе.Упражнения1. Найдите нормальную форму терма (λx x x. x) a b c.2. Пусть twice = λf x. f (f x). Каков интуитивный смысл twice? Найдитенормальную форму twice twice twice f x. (Напомним, что операцияприменения функции левоассоциативна.)3. Найдите терм t такой, что t −→ t.
Можно ли утверждать, что терм имеетβнормальную форму тогда и только тогда, когда из t −→ t0 следует t ≡α t0 ?4. В каком случае справедливо s[t/x][u/y] ≡α s[u/y][t/x]?5. Постройте выражение, равносильное λfкомбинаторы I, K и S.x. f (xx), используя лишь6. Найдите единственный комбинатор X такой, что все λ-термы эквивалентнытермам, построенным композицией X и переменных. Указание: положите A =λp. p K S K, а затем рассмотрите A A A и A (A A).232.4. КомбинаторыГлава 2.
Лямбда-исчисление7. Докажите, что терм X является комбинатором неподвижной точки тогда итолько тогда, когда он представляет собой неподвижную точку комбинатора Gтакого, что G = λy m. m(y m).24Глава 3λ-исчисление как языкпрограммирования«Проблема разрешимости» (также известная как Entscheidungsproblem) былаодним из основных предметов изучения логиков 1930-х. Формулировка задачитакова: существует ли некоторая систематическая (механическая) процедураопределения истинности утверждения в логике первого порядка? Положительныйответ на этот вопрос имел бы фундаментальное философское и, возможно,практическое значение: принципиальную возможность решить большое количестворазнообразных сложных математических задач исключительно при помощинекоторого фиксированного метода (в настоящий момент используется терминалгоритм) без привлечения дополнительных творческих усилий.Очевидно, что проблема разрешимости непроста, поскольку требует точногоопределения понятия «систематической» либо «механической» процедуры на языкематематики.
В работе Turing (1936) даётся, вероятно, лучший анализ этой задачи.В ней также утверждается, что механическими можно считать действия, которыемогут быть в принципе выполнены достаточно умным клерком, не обладающимзнаниями об объекте этих действий. Абстрагирование поведения такого клеркапривело в дальнейшем к известному понятию «машины Тьюринга». Вопреки тому,что эта концепция была чисто математической, а роль исполнителя действийпервоначально предназначалась человеку, мы можем также рассматривать машинуТьюринга как очень простой компьютер. Несмотря на простоту, эта машина способнапроделать любые вычисления, доступные реальным машинным исполнителям.1Вычислительную модель, эквивалентную по своей полноте машине Тьюринга,принято называть полной по Тьюрингу либо Тьюринг-полной.Почти одновременно с Тьюрингом, другими авторами были предложенынезависимые определения понятия «механической процедуры», большая частькоторых оказалась эквивалентной машине Тьюринга по своей вычислительнойполноте.
В частности, лямбда-исчисление, первоначально предназначенное нароль формальной основы математики, также возможно трактовать и как языкпрограммирования, в котором исполнение программ сводится к последовательности1В действительности, машина Тьюринга обладает большей вычислительной полнотой за счетотсутствия ограничений на объем доступной памяти.
Строго говоря, любой существующийкомпьютер алгоритмически эквивалентен конечному автомату, но для удобства принято такжеполагать объем его памяти бесконечным.25Глава 3. Лямбда-исчисление как язык программированиябета-преобразований. В самом деле, Чёрч ещё до публикации работ Тьюрингасделал предположение, что множество операций, представимых в рамкахлямбда-исчисления, является формальным эквивалентом интуитивного понятия«механической процедуры». Этот постулат был в дальнейшем назван тезисом Чёрча.В работе Church (1936) показано, что из этого тезиса следует неразрешимостьEntscheidungsproblem.
Тьюринг впоследствии доказал, что множество функций,представимых в рамках лямбда-исчисления, в точности совпадает со множествомфункций, вычислимых машиной Тьюринга. Этот результат послужил ещё однимдоводом в пользу справедливости тезиса Чёрча.С точки зрения современных программистов, программы для машины Тьюрингамогут считаться достаточно примитивной разновидностью машинных кодов. Всамом деле, очень вероятно, что именно машины Тьюринга, в особенности такназываемая «универсальная машина»,2 оказали решающее влияние на разработкусовременных компьютерных архитектур с хранимой программой; впрочем, степеньэтого влияния и его природа продолжают служить объектом дискуссий (Robinson 1994).
Примечательно то, что некоторые другие альтернативные определения«механической процедуры», часто сформулированные задолго до появленияэлектронных компьютеров, достаточно точно соответствуют реальным методампрограммирования. Например, алгоритмы Маркова (формальная вычислительнаямодель, популярная в Советском Союзе) могут считаться основой языкапрограммирования SNOBOL. В дальнейшем нас будет интересовать аналогичноевлияние лямбда-исчисления на эволюцию функциональных языков.Язык LISP, второй (после FORTRAN) старейший язык высокого уровня,использует некоторые понятия лямбда-исчисления, в частности, обозначение(LAMBDA · · ·) для безымянных функций, но в целом ему не соответствует.
Всамом деле, как ранние версии языка, так и некоторые его современные диалектыиспользуют принцип динамического связывания имён переменных, несовместимыйс лямбда-исчислением (подробное обсуждение см. ниже). Более того, в раннихверсиях отсутствовала приемлемая поддержка понятия функций высших порядков,зато имелся существенный объем императивных конструкций. Но несмотря на это,LISP заслуживает внимания как первый функциональный язык программирования,в котором также впервые были реализованы многие сопутствующие возможности,такие как автоматическое распределение памяти и «сборка мусора».Влияние лямбда-исчисления на языки программирования приобрело реальныйвес с появлением в 1960-х работ Лэндина и Стрейчи. В частности, Лэндин показал,что множество свойств распространённых в то время (императивных) языковможет успешно анализироваться в терминах лямбда-исчисления, к примеру, понятиеобластей видимости переменных в Algol 60.
В работе Landin (1966) было предложеноиспользовать лямбда-исчисление как основу языков программирования, примеромчего послужил функциональный язык ISWIM («If you See What I Mean»—досл.«Если вам понятно, о чём речь»). Эта публикация завоевала в дальнейшем широкуюизвестность и стала отправной точкой в разработке многих других языков, нашедшихпрактическое применение.Язык ML ведёт свою историю с появления в роли метаязыка (откуда,2Универсальной называется машина Тьюринга, способная воспроизводить работу любой другой,т.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
