John Harrison - Введение в функциональное программирование (1108517), страница 15
Текст из файла (страница 15)
В самой реализации выражения представляютсяв виде ориентированных ациклических графов, а не в виде деревьев. Этот подходизвестен как ленивое (lazy) или вызов по необходимости (call-by-need) вычисление,поскольку выражения вычисляются только тогда, когда необходимо.Вторым решением является попытка перевернуть с ног на голову теоретическиеразмышления о стратегии редукции и вычислять аргументы функции до началаеё собственного вычисления. Этот подход известен как аппликативный порядок илиэнергичное вычисление. Последнее имя возникло из-за того, что аргументы функциивычисляются даже тогда, когда они не нужны, например, t в (λx. y) t.
Конечно,применение аппликативного порядка означает, что процесс вычисления некоторыхвыражений может зацикливаться, тогда как он завершается при работе в ленивомрежиме. Но это считается допустимым, поскольку подобных ситуаций достаточнолегко избежать на практике. В любом случае, стратегия энергичного вычисленияявляется стандартной для многих языков программирования, таких как C, где еёназывают вызов по значению (call by value).ML использует энергичное вычисление по двум основным причинам. Управлениередукцией и совместным использованием подвыражений, которое требуется приленивом вычислении, является достаточно сложным, и реализация может бытьотносительно неэффективной и трудной.
Если программист не проявит должнойосторожности, то память может заполниться невычисленными выражениями,так что в общем случае оценить потребление памяти программой будетзатруднительно. В действительности, многие реализации ленивого вычислениястараются оптимизировать его путём использования энергичного вычисления втех местах, где семантика не отличается.2 В противоположность этому, в MLмы всегда сначала вычисляем аргументы функций, и только затем выполняемβ-редукцию — это просто, эффективно и легко реализуется с использованиемстандартных технологий построения компиляторов.Второй причиной для выбора аппликативного порядка вычислений служит то,что ML не является чистым функциональным языком, а имеет императивныевозможности (переменные, присваивание и т.п.). Следовательно, порядоквычисления подвыражений может изменить семантику, а не просто влияет наэффективность. Если используется ленивое вычисление, то для программистастановится практически невозможным отчётливо представить (в нетривиальнойпрограмме) когда и какое подвыражение вычисляется.
С другой стороны, вэнергичной системе, подобной ML, достаточно лишь помнить соответствующиепростые правила.Однако, важно осознавать, что стратегия вычислений ML не просто редукцияснизу вверх, в противоположность нормальному порядку. В действительности ML2Они стараются выполнить анализ строгости — один из видов статического анализа, которыйчасто помогает определить, что аргументы должны быть вычислены (Mycroft 1981).52Глава 5. Знакомство с ML5.1.
Энергичное вычислениеникогда не вычисляет содержимое λ-абстракций. (В частности, он никогда нередуцирует η-редексы, а только β-редексы.) При вычислении (λx. s[x]) t, сначалавычисляется t. Однако s[x] не затрагивается, поскольку оно является содержимымλ-абстракции. Кроме того, любое подвыражение t, которое является содержимымλ-абстракции, также остаётся нетронутым. Вот точные правила вычисления:• Константы вычисляются сами в себя.• Вычисления заканчиваются на λ-абстракциях, и не затрагиваютсодержимого. В частности, не выполняется η-преобразование.их• При вычислении комбинации s t сначала вычисляются оба терма, s и t.Потом, при условии что результатом вычисления s является λ-абстракция,производится самое внешнее β-преобразование, и процесс повторяется.Порядок вычисления s и t отличается в зависимости от версии ML.
В той версии,которую мы будем использовать, сначала всегда вычисляется t. Строго говоря, мытакже должны задать правило для let-выражений, поскольку, как упоминалось,они теперь считаются примитивами. Однако, с точки зрения стратегии вычислений,они как и прежде могут рассматриваться как применение λ-абстракции к аргументу,который будет вычислен первым. Для того, чтобы сделать это явным, правило дляlet x = s in tгласит, что сначала вычисляются все s, а результат подставляется вместо x в t, послечего вычисляется новое значение t. Рассмотрим некоторые примеры вычислениявыражений:(λx.
(λy. y + y) x)(2 + 2) −→−→−→−→(λx. (λy. y + y) x)4(λy. y + y)44+48Заметим, что подтерм (λy. y + y) x не редуцируется, поскольку он находитсяв пределах λ-абстракции. Однако, редуцируемые термы, не находящиеся внутриλ-абстракций обоих функций, а также аргумент, редуцируются до того, каквычисляется применение функции, например, второй шаг будет следующим:((λf x. f x) (λy. y + y)) (2 + 2) −→−→−→−→((λf x. f x) (λy. y + y)) 4(λx. (λy. y + y) x) 4(λy. y + y) 44+4Тот факт, что ML не вычисляет содержимое λ-абстракций, является ключевымдля опытных программистов на ML. Он даёт возможность точного контроля надвычислением выражений и может использоваться для имитации многих полезныхвозможностей ленивой стратегии.
Простейшие примеры этого будут рассмотрены вследующем разделе.535.2. Результаты энергичного вычисления5.2Глава 5. Знакомство с MLРезультаты энергичного вычисленияИспользование энергичного вычисления заставляет нас объявить примитиваминекоторые дополнительные языковые конструкции, определив для них специальныеметоды редукции, вместо того, чтобы реализовать их напрямую в терминахλ-исчисления. В частности, мы не можем больше рассматривать условнуюконструкциюif b then e1 else e2как применение обычного трехкомпонентного (тернарного) оператораCOND b e1 e2Причина заключается в том, что по правилам энергичного вычисления мы всегдадолжны вычислить все выражения, b, e1 и e2 , до вычисления COND.
Как правило,последствия этого фатальны. Например, заново рассмотрим наше определениефункции вычисления факториала:let rec fact(n) = if ISZERO n then 1 else n ∗ fact(PRE n)Если условное выражение будет вычислять все свои аргументы, то привычислении fact(0), ветвь ‘else’ также должна быть вычислена, что в своюочередь вызывает вычисление fact(PRE 0). Но это также потребует вычисленияfact(PRE (PRE 0)), и т.д.
Соответственно, вычисление превратится в бесконечныйцикл.Таким образом, мы делаем условное выражение примитивной конструкцией именяем обычную стратегию редукции так, что сначала вычисляется логическоевыражение, а затем — только одна соответствующая ветвь условия.А что происходит с самим процессом рекурсии? Мы предложили интерпретациюрекурсивных определений в терминах рекурсивного оператора Rec с его собственнымправилом редукции:Rec f −→ f (Rec f )который также будет зацикливаться при использовании стратегии энергичноговычисления:Rec f −→ f (Rec f ) −→ f (f (Rec f )) −→ f (f (f (Rec f ))) −→ · · ·Однако, достаточно лишь очень простого изменения правил редукции, чтобырешить эту проблему:Rec f −→ f (λx. Rec f x)Теперь λ-абстракция в правой части правила означает, что λx.
Rec f xвычисляется само в себя (то есть, не вычисляется вовсе), и только после того, каквыражение было редуцировано в ходе подстановки этой λ-абстракции в терм f ,вычисление продолжается.54Глава 5. Знакомство с ML5.35.3. Семейство языков MLСемейство языков MLМы говорили о ‘ML’ так, как будто это один язык. На самом деле существуетмного вариантов ML, в том числе и ‘Lazy ML’ — реализация университета Chalmersв Швеции, которая базируется на ленивых вычислениях. Наиболее популярнаяверсия ML в образовании — это ‘Standard ML’, но мы будем использовать другую,которая называется CAML (‘camel’) Light.3 Мы выбрали CAML Light по следующимпричинам:• реализация имеет небольшой объём и хорошо переносима между платформами,так что она эффективно работает на Unix, PC, Mac, и других.• Система очень проста синтаксически и семантически, что делает её достаточнопростой для изучения.• Система хорошо подходит для практического использования.
Например, онаимеет интерфейс к библиотекам на языке C и поддерживает стандартнуюраздельную компиляцию, совместимую с make.Однако, мы будем изучать достаточно общие техники, так что любой написанныйкод может быть запущен (с небольшими синтаксическими изменениями) на любойверсии ML, и часто, на других функциональных языках.5.4Запуск MLML уже установлен на рабочий сервер (Thor). Для того, чтобы использовать его,вам необходимо добавить каталог с исполняемыми файлами CAML в переменнуюсреды PATH. Это может быть сделано следующим образом (предполагая, что выиспользуете командный процессор bash или другой из его семейства):PATH="$PATH:/home/jrh13/caml/bin"export PATHЧтобы не вводить эти команды при каждом входе на сервер, вы можете вставитьих в конец вашего файла .bash_profile или его эквивалента для вашего командногопроцессора.
Теперь, для использования CAML в интерактивном режиме, вам простонадо набрать camllight, и программа должна запуститься и выдать приглашение(‘#’):$ camllight>Caml Light version 0.73#Для того, чтобы выйти из системы, просто наберите ctrl/d или quit();; встроке ввода. Если вы заинтересованы в установке CAML Light на ваш собственныйкомпьютер, то вы должны прочитать следующую Web-страницу для полученияподробной информации:http://pauillac.inria.fr/caml/3Это имя означает ‘Categorical Abstract Machine’, метод реализации, лежащий в её основе.555.5. Взаимодействие с ML5.5Глава 5.
Знакомство с MLВзаимодействие с MLКогда ML выдаст вам строку приглашения, вы можете вводить выражения,завершённые двумя последовательными знаками “точка с запятой”. Принятоговорить, что ML находится в режиме диалога (который также имеет жаргонноеназвание REPL, read-eval-print loop): выражения считываются, вычисляются ивыводятся результаты. Например, ML может быть использован как простойкалькулятор:#10 + 5;;- : int = 15Система не только возвращает ответ, но также выдаёт тип выражения, которыйопределяется автоматически.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
