Представление программ в расширенном лямбда-исчислении

В следующих главах мы построим несколько программ для исполнения кода, написанного на функциональных языках, для того, чтобы более тщательно исследовать вопрос о том, как исполняются функциональные программы. До сих пор мы лишь на словах описывали, как следует понимать те или иные конструкции языка Haskell или иного языка функционального программирования. Для того чтобы более точно описать семантику исполнения, следует написать какую-либо программу, способную исполнять предъявленный ей функциональный код. Разумеется, такие программы мы будем описывать на языке Haskell, этот язык достаточно удобен для того, чтобы на нем записывать сложные алгоритмы. Однако в качестве исходного, интерпретируемого языка язык Haskell не очень хорошо приспособлен для демонстрационных целей. В нем слишком много различных конструкций, многие из которых являются просто удобными синтаксическими сокращениями для других, может быть, более общих конструкций (это то, что системные программисты обычно называют «синтаксическим сахаром»). Чтобы не перегружать наши программы излишними деталями, мы возьмем в качестве исходного языка расширенное лямбда-исчисление, простое и в то же время достаточно мощное для того, чтобы можно было на нем выразить любые конструкции функциональных языков программирования.

Прежде всего, поскольку в наших построениях программы, записанные на языке расширенного лямбда-исчисления, являются предметом обработки других программ, следует подумать о том, как удобнее всего представлять конструкции расширенного лямбда-исчисления в наших программах.

Конечно, можно просто считать, что программа на языке расширенного лямбда-исчисления будет представлена строкой текста, однако такое представление, несмотря на его большую общность, является очень неудобным для обработки. Обычно перед тем, как начать исследовать или исполнять некую программу, ее переводят в некоторую промежуточную форму, представляющее собой синтаксическое дерево исходной программы. Мы не будем описывать процесс перевода текста программы в синтаксическое дерево, интересующиеся этим процессом могут обратиться к многочисленной литературе по устройству и построению синтаксических анализаторов в компиляторах языков программирования. Мы же опишем только само синтаксическое дерево — результат синтаксического анализа выражения, записанного в расширенном лямбда-исчислении.

Описание конструкций синтаксического дерева можно сделать в виде описания нового типа данных языка Haskell, в котором определены все конструкции расширенного лямбда-исчисления. Поскольку эти конструкции определены рекурсивно, то и определяемый тип данных тоже, конечно, будет рекурсивным. Мы определим несколько конструкторов для этого типа данных в соответствии с тем, какие конструкции имеются в расширенном лямбда-исчислении. Сам определяемый тип данных будет называться Ехрг (от expression — выражение).

Итак, всего в расширенном лямбда-исчислении имеется пять видов конструкций: константы (мы будем различать три вида констант — целые числа, логические значения и примитивные функции; следовало бы еще ввести константу для представления пустого списка, однако мы для простоты не будем этого делать), переменные, лямбда-выражения, применения функции и блоки (опять же, будем различать два вида блоков — рекурсивный, представленный конструкцией letrec, и нерекурсивный, представленный конструкцией let). Соответственно описание типа лямбда-выражений в виде синтаксического дерева будет содержать восемь конструкторов для описания каждого из типов и подтипов выражений: data Ехрг =.

Integral Integer | — целые константы.

Logical Bool | — логические константы.

Function String | — идентификаторы примитивных функций.

Variable String | — переменная.

Lambda String Expr | — лямбда-выражение.

Application Ехрг Ехрг | — применение функции.

Let String Expr Expr | — простой блок.

Letrec [ (String, Expr)] Expr — рекурсивный блок Каждый из конструкторов имеет один или несколько аргументов в соответствии с тем, какие иодконструкции содержатся в каждой из конструкций расширенного лямбда-исчисления, а для элементарных выражений аргументы конструкторов содержат внешнее представление выражения. Например, конструктор Variable имеет в качестве аргумента String, поскольку переменная представлена некоторой строкой — идентификатором этой переменной, а конструктор Application имеет два аргумента, соответствующих своим подконструкциям: выражение, задающее применяемую функцию, и выражение, задающее аргумент функции.

Приведем пример несложного лямбда-выражения и его представления в виде выражения тина Ехрг на языке Haskell. Пусть исходное лямбдавыражение имеет вид.

let sqr = Ах. * х х in sqr 5.

Здесь в конструкции let отсутствуют рекурсивные обращения к определяемой переменной, это простой блок. Тогда соответствующее синтаксическое дерево может быть представлено следующим выражением на языке Haskell:

Let «sqr» .

• (Lambda «x»
• (Application (Application (Function «*»)
• (Variable «x»))
• (Variable «x»)))
• (Application (Variable «sqr») (Integral 5))

Правила перевода с языка расширенного лямбда-исчисления в выражение типа Ехрг можно записать и более формально, это совсем простое упражнение. Более интересным является вопрос о переводе конструкций такого сложного языка функционального программирования, каким является язык Haskell, в более простой язык расширенного лямбда-исчисления. Мы не будем здесь приводить все детали такой трансформации и, тем более, пытаться построить программу, которая может осуществить такое преобразование, однако наметим основные вехи на пути построения такого преобразования.

Прежде всего, условимся, что мы станем рассматривать только правильные программы на языке Haskell, поэтому будем считать, что в программе не только нет грубых синтаксических ошибок, но и анализ типов данных уже произведен, и ошибок, связанных с неправильным употреблением типов, в программе тоже нет. Таким образом, мы сразу же выводим из рассмотрения все конструкции, необходимые только для определения новых типов данных и описания типов функций. Будем считать, что нам не нужно рассматривать определения классов, конструкции, задающие описания типов тех или иных переменных, задание контекста, конструкцию type и пр. Конструкция data будет представлять для нас интерес только потому, что в ней определяются конструкторы данных, которые впоследствии могут использоваться для построения объектов и в конструкции сопоставления с образцом. Мы можем также проигнорировать модульную структуру программы, и считать, что программа на языке Haskell состоит просто из определений одного уровня.

Определения, из которых состоит программа на языке Haskell, — это определения функций и значений других типов. Можно считать, что исполнение программы состоит в вычислении некоторого выражения в контексте, заданном этими определениями. Таким образом, для того чтобы вычислить выражение в контексте программы, загруженной в интерпретатор, нужно фактически вычислить выражение вида letrec xl = el, х2 = е2,.

xk = ек in е где выписанный блок как раз и представляет собой набор, вообще говоря, рекурсивных определений переменных и некоторое выражение, которое необходимо вычислить. Правда, в языке Haskell определения функций могут быть записаны не только в виде Xi = e_i; но также и в виде набора уравнений, в которых встречаются сопоставления с различными образцами.

Следует сказать, что сопоставление с образцом — это практически единственная конструкция в языке Haskell, которая не имеет прямого аналога в расширенном лямбда-исчислении и потому требует особого обсуждения.

Перед тем как показать, как именно сопоставление с образцом может быть переведено в конструкции расширенного лямбда-исчисления, коротко рассмотрим все остальные конструкции языка Haskell.

Выражения в Haskell строятся из простых значений, которыми являются числа, логические константы и изображения списков. Числа и логические значения мы считаем константами нашего расширенного лямбда-исчисления, так что они не требуют никакого перевода. Что же касается пустого списка и более сложных конструкций в изображении списков, таких как [1, 2, 5 ], [ 1.. ] или даже генератор [х*х | х <- [1.10]], то их можно выразить с помощью применения стандартных конструкторов, стандартных функций или функций, которые легко определить самому. Поэтому можно считать, что такие изображения сложных списков являются частным случаем конструкций применения функций и конструкторов к более простым значениям.

К использованию тех или иных функций сводятся и многие другие конструкции языка Haskell. Например, образование кортежа из k значений может быть выражено применением стандартной функции TUPLE-k, описанной нами в гл. 9, так что, например, изображение кортежа (1, х, [ ]) может быть представлено в расширенном лямбда-исчислении в виде применения функции TUPLE-3 1 х NIL. Здесь NIL — представление для пустого списка, чуть ниже мы рассмотрим его более подробно. Условное выражение if b then el else е2 также представляется в виде применения стандартной функции IF b el е2.

Особое место занимает представление применения стандартных и определенных программистом конструкторов. С помощью конструкторов создаются новые значения, представляющие собой чисто механическое соединение нескольких значений определенного типа наподобие того, как это делается при образовании кортежа. Дополнительно конструктор определяет еще и тег — имя конструктора, которое затем может быть использовано при сопоставлении с образцом. Будем считать, что при анализе определения типа данных все конструкторы получают целые номера, начинающиеся с нуля. Так, если тип данных «двоичное дерево» был определен с помощью описания data Tree, а = Null |.

Tree a (Tree a) (Tree a).

то конструктор Null получает номер 0, а конструктор Tree — номер 1. Аналогично и для стандартного конструктора списков, про который можно сказать, что его определение выглядит как data [а] = [] |.

а: [а].

т.е. определены два конструктора: конструктор пустого списка [ ], получающий номер 0, и конструктор (:), получающий номер 1. Поскольку мы условились, что программа уже прошла анализ правильности, и ошибок в использовании типов данных в ней нет, то номера конструкторов могут быть локальными для каждого определения типа данных — путаницы, каким тегом какой конструктор помечен, не возникнет.

Теперь условимся считать, что применение любого конструктора эквивалентно образованию кортежа, в который входят как минимум тег применяемого конструктора, а также все значения аргументов. Учитывая, что конструкторы, как и все прочие функции, обладают свойством карринга, можно сказать, что представлением любого конструктора языка Haskell в виде выражения расширенного лямбда-исчисления является выражение TUPLE-k tag, где к — число аргументов конструктора, увеличенное на единицу, a tag — номер (тег) конструктора. Таким образом, выражение [10, 15], которое может быть записано с помощью применения стандартных конструкторов в виде 10: (15: [ ]), будет представлено следующим выражением расширенного лямбда-исчисления:

TUPLE-3 1 10 (TUPLE-3 1 15 (TUPLE-1 0)).

(напомним еще раз, что конструктор (:) имеет тег 1 и два аргумента, а конструктор [ ] — тег 0 и ни одного аргумента). Таким образом представление пустого списка, который мы несколькими строками выше записывали в виде NIL, теперь будет выглядеть как (TUPLE-1 0).

В языке Haskell имеются также лямбда-выражения, которые несколько отличаются от лямбда-выражений в расширенном лямбда-исчислении. Однако отличия эти не очень существенны. Первое отличие состоит в том, что лямбда-выражения языка Haskell могут иметь более одного аргумента. Например, обычным представлением функции сложения в Haskell будет лямбда-выражение х у -> х+у. Конечно же, такое лямбда-выражение можно легко переписать так, чтобы в лямбда-выражениях был только один аргумент: х -> у -> х+у. Второе отличие состоит в том, что в качестве формального аргумента в лямбда-выражении может использоваться не только имя переменной, но и образец, с которым производится сопоставление. Это отличие более существенно, и мы его рассмотрим вместе с конструкцией сопоставления с образцом в определении уравнений для функций.

Теперь осталось рассмотреть только одну конструкцию, которая еще не получила своего эквивалентного выражения в расширенном лямбдаисчислении. Это конструкция сопоставления с образцом в определении функции. Сначала нужно понять, что, собственно, представляет собой сопоставление с образцом и как оно используется.

Конструкция сопоставления с образцом несет на себе две основные нагрузки: выбор одного из уравнений при вызове функции и связывание частей фактического аргумента с переменными, входящими в состав образца. Пусть, например, имеются п уравнений, определяющих функцию f. Припишем каждому из уравнений некоторый номер, начиная с нуля и до (п — 1). Не умаляя общности, можно считать, что функция имеет только один аргумент; если это не так, то определение можно разбить на несколько определений, в каждом из которых имеется только один аргумент. Таким образом, в самом общем виде мы можем записать следующие уравнения: f Собразец 0> | = Справая часть 0,0>

| =.

f | =.

I = Справая часть 1,1>

f | = I = справая часть (n-l), l>

Мы должны для функции f построить эквивалентное определение в расширенном лямбда-исчислении, которое будет иметь вид f = Хх.е. Очевидно, что выражение для тела функции должно содержать в себе коды для проверки соответствия аргумента каждому из образцов уравнений (код соответствия образцу), коды для связывания переменных образцов с нужными частями аргумента х (связывающий код), выражения лямбда-исчисления, эквивалентные условиям (код условия), и выражения, соответствующие правым частям уравнений Справая часть i, j> (код правой части). Сначала свяжем с каждым из уравнений, определяющих функцию f, некоторую вспомогательную функцию, осуществляющую все действия по проверке соответствия с образцом, проверке условий и вычисления значения функции в соответствии с правой частью этого уравнения (код уравнения). После этого соединим полученные определения в одно определение функции.

Введем следующие имена вспомогательных функций для заданной функции f. Идентификаторами f₀, f₁,… f_(n-l) обозначим функции, соответствующие кодам каждого из уравнений исходной функции f. Аналогично идентификаторы f_i_pattern будут обозначать коды проверки соответствия каждому из образцов уравнений, идентификаторы f_i_bind — связывающие коды каждого из уравнений, f_i_j_test — коды проверки соответствующих условий и f_i_j_right — коды правых частей уравнений. Тогда в выражении f = Ах. е код тела функции е будет представлять собой последовательную проверку аргумента х на соответствие образцам и условиям уравнений функции f, и его можно записать в расширенном лямбда-исчислении следующим образом: f = Xx. letrec f₀ = Xx. IF (f₀_pattern x).

(let in

IF (f₀_0_test x).

• (f₀_0_right x)
• (IF (f₀_l_test x)
• (f₀_l_right x)

.. (f_l x). .).

).

(f_l x),.

f_l = Xx. IF (f_l_pattern x).

(let in

IF (f_l₀_test x).

• (f_l₀_right x)
• (IF (f_l_l_test x)
• (f_l_l_right x)

... (f₂ x). .).

).

(f₂ x),.

f_(n-l) = Xx. IF (f_(n-l)_pattern x).

(let in

IF (f_(n-l)_0_test x).

(f_(n-1)_0_right x) (IF (f_(n-l)_l_test x) (f_(n-1)_l_right x) … error…).

).

error,.

in f₀ x.

Сделаем необходимые пояснения. Выполнение функции f начинается с того, что вызывается функция проверки соответствия аргумента первому уравнению f₀. Эта функция прежде всего проверит, соответствует ли аргумент первому образцу (выражение f₀_pattern х). Если аргумент не удовлетворяет образцу, то будет вызвана функция второго уравнения f_l и т. д., пока не будет обнаружено соответствие либо ни одно из уравнений не будет признано подходящим, и в этом последнем случае будет сделано обращение к функции error, вызывающей аварийное окончание работы программы. Далее, если соответствие образцу обнаружено, то выполняется связывающий код, в котором каждой из переменных образца ставится в соответствие некоторая часть аргумента. Этот код представляет собой часть блока let и записан в нашем выражении в виде. После выполнения связывания производятся проверки на соответствие аргумента условиям охран, если, конечно, хотя бы одна охрана имеется в уравнении (выражения f_i_j_test х). Это условие проверяется в ситуации, когда уже выполнен связывающий код, и поэтому находится внутри тела соответствующего блока. Если ни одно из условий не выполняется, то будет продолжена проверка уравнений, если же одно из условий выполнено, то исполняется код, соответствующий правой части соответствующего уравнения (выражение f_i_j_right х), и на этом работа функции будет завершена.

Теперь осталось понять, как должны быть написаны все коды, упомянутые, но не реализованные в нашем определении функции f: коды соответствия образцу f_i_pattern, связывающие коды f_i_bind, коды условий f_i_j_test и коды правых частей f_i_j_right. Что касается кодов условий и кодов правых частей, то здесь никаких особенностей в реализации нет. Соответствующие выражения из определяющих уравнений просто переводятся на язык расширенного лямбда-исчисления в соответствии с правилами перевода. Наиболее интересным является вопрос о том, как происходит проверка соответствия образцу в функциях f_i_pattern и как организовано связывание переменных в кодах f_i_bind.

Прежде всего, рассмотрим структуру образца. Напомним, что образцом может быть либо простая переменная (именованная или безымянная), либо константа, либо вызов конструктора, аргументами которого являются другие образцы, либо кортеж из других образцов. Константы и кортежи можно рассматривать как вызовы конструкторов, так что фактически мы имеем только два вида образцов: образец-переменная и образец-вызов конструктора. Однако обычно константы все же представлены иначе, чем результаты применения функций-конструкторов, а в кортежах мы не будем использовать тег конструктора, собирая кортеж просто из его элементов, так что эти случаи тоже лучше рассматривать отдельно. Если образцом является переменная, то код соответствия образцу для любого аргумента выдает истинное значение, поскольку такому образцу соответствует любое значение аргумента. Связывающий код в этом случае также очень прост.

Итак, если в некотором i-м уравнении образцом является переменная z, то функция соответствия образцу f_i_pattern выглядит как Ах. TRUE, а связывающий код f_i_bind — как сопоставление z = х. Отметим, что если переменная образца — безымянная, то связывающий код не нужен вовсе.

Если образцом является константа, то функция соответствия образцу — это просто проверка того факта, что аргументом является то же самое значение, что и значение, представленное этой константой. В данном случае f_i_pattern будет выглядеть как функция (EQ с), где с — константа образца, a EQ — функция сравнения с константой соответствующего типа. Связывающий код для образца-константы не нужен, поскольку никаких переменных такой образец не содержит.

Код сопоставления с образцом в случае, когда образцом является кортеж, просто сводится к кодам сопоставления с образцами, составляющими кортеж. Нужно перед всеми сопоставлениями с элементами кортежа выделить соответствующие части кортежа из фактического аргумента функции. Таким образом, и в коде проверки соответствия образцу, и в связывающем коде просто появляется дополнительное действие — выделение элемента кортежа из аргумента с помощью применения стандартной функции INDEX.

Самым сложным является случай образца-конструктора. Поскольку программа уже прошла проверку соответствия типам, то аргументом функции в этом случае может быть только значение, имеющее вид кортежа, первым элементом которого является номер конструктора. В коде сопоставления с образцом нужно проверить, действительно ли первый элемент кортежа совпадает с номером конструктора из рассматриваемого образца, а если это действительно так, то далее следует проверить, что все остальные элементы кортежа соответствуют тем образцам, которые являются аргументами образца-конструктора.

Поскольку элементы кортежа могут быть выбраны с помощью стандартной функции INDEX, то проверка соответствия номера конструктора первому элементу кортежа будет выглядеть следующим образом:

EQ tag (INDEX 0 х) где tag — номер конструктора в образце. Далее нужно выбрать оставшиеся элементы кортежа с помощью вызовов (INDEX i х) при i, равных 1, 2,…, и применить коды сопоставления с выбранными частями образца. Сам образец-конструктор содержит переменные только в своих аргументах, так что порождать связывающий код для образца в целом нет необходимости за исключением случая, когда некоторая переменная связывается с образцом в целом с помощью конструкции z@pattern, где z — имя переменной, a pattern — образец. В этом случае в связывающий код нужно поместить соответствующее уравнение z = х.

Приведем пример. Пусть одно из уравнений для функции f имеет вид f listQ[t] = е Прежде всего, перепишем образец таким образом, чтобы в нем в явном виде присутствовали все конструкторы: f list@ (t: []) = е Теперь понятно, что в коде сопоставления с образцом нужно будет последовательно сделать две проверки: сначала проверить, что аргумент действительно сформирован с помощью конструктора (:), а если это действительно так, то проверить, что третий элемент кортежа сформирован посредством конструктора [ ]. Если считать, что номер конструктора [ ] - это ноль, а номер конструктора (:) — единица, то функция, реализующая код сопоставления, будет иметь вид Ах. AND (EQ 1 (INDEX 0 х)).

(let testl = Ах. (EQ О (INDEX Ox)) in testl (INDEX 2 х)).

В этом примере функция состоит в применении операции логического «И» для проверки соответствия аргумента внешнему образцу и, если проверка будет закончена успешно, для проверки соответствия частей аргумента второму аргументу конструктора (:). Функция testl вводится во внутреннем блоке для проверки соответствия части аргумента образцу, содержащему конструктор [ ]. Эта функция применяется к части аргумента, выделенной с помощью применения стандартной функции (INDEX 2 х).

Связывающий код для этого примера будет содержать связывание для двух переменных, содержащихся в образце. Переменная list относится ко всему образцу, поэтому соответствующий связывающий код будет иметь вид list = х. Переменная t соответствует части аргумента — второму элементу соответствующего кортежа, так что код связывания для нее имеет вид t = INDEX 1 х. Полностью заголовок блока, содержащий связывающий код, будет иметь вид let 1 = х,.

t = INDEX 1 х in …

Итак, мы научились переводить любые конструкции программ на языке Haskell в выражения расширенного лямбда-исчисления. Конечно, множество деталей требуют более тщательной проработки, однако все принципиальные вопросы решены. Теперь можно заняться исследованием программ, написанных на этом простом языке для того, чтобы понять точный смысл исполнения всех конструкций данного языка.