John Harrison - Введение в функциональное программирование (1108517), страница 10
Текст из файла (страница 10)
f n x требуется «отбросить» одно из применений f . Вкачестве первого шага введём на множестве пар функцию PREFN такую, чтоPREFN f (true, x) = (false, x)иPREFN f (false, x) = (false, f x)Предположив, что подобная функция существует, можно показать,что (PREFN f )n+1 (true, x) = (false, f n x). В свою очередь, этого достаточно, чтобызадать функцию PRE, не испытывая особых затруднений. Определение PREFN,удовлетворяющее нашим нуждам, таково:4PREFN = λf p. (false, if fst p then snd p else f (snd p)В свою очередь,4PRE n = λf x. snd(n (PREFN f ) (true, x))Доказательство корректности этого определения предлагается читателю в качествеупражнения.313.2. Рекурсивные функцииГлава 3.
Лямбда-исчисление как язык программирования3.2Рекурсивные функцииВозможность определения рекурсивных функций является краеугольным камнемфункционального программирования, поскольку в его рамках это единственныйобщий способ реализовать итерацию. На первый взгляд, сделать подобное средствамилямбда-исчисления невозможно.
В самом деле, именование функций представляетсянепременной частью рекурсивных определений, так как в противном случае неясно,как можно сослаться на функцию в её собственном определении, не зацикливаясь.Тем не менее, существует решение и этой проблемы, которое, однако, удалось найтилишь ценой значительных усилий, подобно построению функции PRE.Ключом к решению оказалось существование так называемых комбинаторовнеподвижной точки. Замкнутый терм Y называется комбинатором неподвижнойточки, если для произвольного терма f выполняется равенство f (Y f ) = Y f .Другими словами, комбинатор неподвижной точки определяет по заданному терму fего фиксированную точку, т.
е. находит такой терм x, что f (x) = x. Первый примертакого комбинатора, найденный Карри, принято обозначать Y . Своим появлениемон обязан парадоксу Рассела, чем объясняется его другое популярное название —«парадоксальный комбинатор». Мы определилиR = λx. ¬(x x),после чего обнаружили справедливостьR R = ¬(R R)Таким образом, R R представляет собой неподвижную точку операцииотрицания. Отсюда, чтобы построить универсальный комбинатор неподвижнойточки, нам потребуется лишь обобщить данное выражение, заменив ¬ произвольнойфункцией, заданной аргументом f . В результате мы получаем4Y = λf.
(λx. f (x x))(λx. f (x x))Убедиться в справедливости этого определения несложно:Yf ====(λf. (λx. f (x x))(λx. f (x x))) f(λx. f (x x))(λx. f (x x))f ((λx. f (x x))(λx. f (x x)))f (Y f )Однако, несмотря на математическую корректность, предложенное решениене слишком привлекательно с точки зрения программирования, посколькуоно справедливо лишь в смысле лямбда-эквивалентности, но не редукции (впоследнем выражении мы применяли обратное бета-преобразование). С учётомэтих соображений альтернативное определение Тьюринга может оказаться болеепредпочтительным:4T = (λx y.
y (x x y)) (λx y. y (x x y))(Доказательство справедливости T f −→ f (T f ) предоставляется читателю вкачестве упражнения.) Однако, мы можем без особого ущерба для строгости32Глава 3. Лямбда-исчисление как язык программирования3.3. LET-выраженияизложения считать, что Y f может подвергаться бета-редукции в соответствиис последовательностью редукции для рекурсивных функций. Рассмотрим, каккомбинатор неподвижной точки (например, Y ) может применяться для реализациирекурсии. Воспользуемся в качестве примера вычислением факториала.
Мы хотимопределить функцию fact следующим образом:fact(n) = if ISZERO n then 1 else n ∗ fact(PRE n)Прежде всего, преобразуем эту функцию в эквивалентную:fact = λn. if ISZERO n then 1 else n ∗ fact(PRE n)которая, в свою очередь, эквивалентнаfact = (λf n. if ISZERO n then 1 else n ∗ f (PRE n)) factОтсюда следует, что fact представляет собой неподвижную точку такой функции F :F = λf n. if ISZERO n then 1 else n ∗ f (PRE n)В результате всё, что нам потребуется, это положить fact = Y F . Аналогичнымспособом можно воспользоваться и в случае взаимно рекурсивных функций,т. е. множества функций, определения которых зависят друг от друга.
Такиеопределения, какf1f2...fn====F 1 f1 · · · fnF 2 f1 · · · fn...F n f1 · · · fnмогут быть при помощи кортежей преобразованы в одно:(f1 , f2 , . . . , fn ) = (F1 f1 · · · fn , F2 f1 · · · fn , . . . , Fn f1 · · · fn )Положив t = (f1 , f2 , . . . , fn ), видим, что каждая из функций в правой частиравенства может быть вычислена по заданному t применением соответствующейфункции-селектора: fi = (t)i . Применив абстракцию по переменной t, получаемуравнение в канонической форме t = F t, решением которого является t = Y F ,откуда в свою очередь находятся значения отдельных функций.3.3Let-выраженияВозможность использования безымянных функций была нами ранеепреподнесена как одно из достоинств лямбда-исчисления.
Более того, именаоказались необязательными даже при определении рекурсивных функций. Однако,зачастую всё же удобно иметь возможность давать выражениям имена с тем,чтобы избежать утомительного повторения больших термов. Простая форма такогоименования может быть реализована как ещё один вид синтаксической глазуриповерх чистого лямбда-исчисления:4let x = s in t = (λx. t) s333.3. LET-выраженияГлава 3. Лямбда-исчисление как язык программированияПростой пример применения этой конструкции работает, как и ожидается:(let z = 2 + 3 in z + z) = (λz.
z + z) (2 + 3) = (2 + 3) + (2 + 3)Мы можем добиться как последовательного, так и параллельного связываниямножества имён с выражениями. Первый случай реализуется простыммногократным применением конструкции связывания, приведённой выше. Вовтором случае введём возможность одновременного задания множества связываний,отделяемых друг от друга служебным словом and:let x1 = s1 and · · · and xn = sn in tБудем рассматривать эту конструкцию как синтаксическую глазурь для(λ(x1 , . .
. , xn ). t) (s1 , . . . , sn )Продемонстрируем различия в семантике последовательного и параллельногосвязывания на примере:let x = 1 in let x = 2 in let y = x in x + yиlet x = 1 in let x = 2 and y = x in x + yдают в результате 4 и 3 соответственно.В дополнение к этому разрешим связывать выражения с именами, за которымиследует список параметров; такая форма конструкции let представляет собой ещёодну разновидность синтаксической глазури, позволяющую трактовать f x1 · · · xn =t как f = λx1 · · · xn .
t. Наконец, помимо префиксной формы связывания let x =s in t введём постфиксную, которая в некоторых случаях оказывается удобнее длявосприятия:t where x = sНапример, мы можем написать так: y < y 2 where y = 1 + x.Обычно конструкции let и where интерпретируются, как показано выше, безпривлечения рекурсии. Например,let x = x − 1 in · · ·связывает x с уменьшенным на единицу значением, которое уже было связано сименем x в охватывающем контексте, а не пытается найти неподвижную точкувыражения x = x−1.5 В случае, когда нам требуется рекурсивная интерпретация, этоможет быть указано добавлением служебного слова rec в конструкции связывания(т.
е. использованием let rec и where rec соответственно). Например,let rec fact(n) = if ISZERO n then 1 else n ∗ fact(PRE n)Это выражение может считаться сокращённой формой записи let fact = Y F , гдеF = λf n. if ISZERO n then 1 else n ∗ f (PRE n),как было показано выше.5Неподвижная точка этого выражения существует, но соответствующий лямбда-терм не имеетнормальной формы, т.
е. в известном смысле не определен. Семантика незавершимых термовдостаточно сложна и не будет нами рассматриваться. В действительности, основной вопросзаключается в наличии у терма не нормальной, а так называемой головной нормальной формы,что подробнее рассматривается в работах Barendregt (1984) и Abramsky (1990).34Глава 3. Лямбда-исчисление3.4. Достижениекак языкуровняпрограммированияполноценного языка программирования3.4ДостижениеуровняпрограммированияполноценногоязыкаНа данный момент мы ввели достаточно обширный набор средств«синтаксической глазировки», реализующих удобочитаемый синтаксис поверхчистого лямбда-исчисления. Примечательно то, что этих средств достаточнодля определения функции факториала в форме, очень близкой к языку ML.В связи с этим возникает вопрос, уместно ли считать лямбда-исчисление,расширенное предложенными обозначениями, практически пригодным языкомпрограммирования?В конечном счёте, программа представляет собой единственное выражение.Однако, использование let для именования различных важных подвыражений,делает вполне естественной трактовку программы как множества определенийразличных вспомогательных функций, за которыми следует итоговое выражение,например:let rec fact(n) = if ISZERO n then 1 else n ∗ fact(PRE n) in···f act(6)Эти определения вспомогательных функций могут трактоваться сматематической точки зрения как уравнения.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
