Теоретические сведения. В программировании часто приходится устана-
вливать различие между понятием “оператор” и понятием “функция”.
В первом случае руководствуются алгебраическими идеями, когда у вся-
кого оператора заранее предполагается арность (известное число аргу-
ментов, называемых операндами). Это число операндов известно заранее,
и оно связано с самим видом конкретного оператора. Другое проявление
операторности -- это работа с функциями, которые хотя и имеют про-
извольный характер, но для каждой из них также заранее известно чи-
сло аргументов. Это старо-традиционная точка зрения на вычисления
и построение исчислений. В ее основе лежит относительное противо-
поставление символа функции или оператора с одной стороны символам
аргументов с другой стороны. Молчаливо предполагается, что объекты
имеются, но они неравноправны: объекты-операторы используются по
одним правилам, а объекты-операнды -- по другим. Наиболее часто ис-
пользуемое предположение касается замещения одних объектов на другие.
В рамках формализаций первого порядка операнды могут замещаться на
другие объекты, а операторы обычно не могут. В этом состоит смысл
ограничения, накладываемого на подстановку в этих системах. Системы
первого порядка называют системами с ограниченным принципом сверты-
вания, поскольку конкретно принятое определение операции подстановки
реализует идею свертывания.
При работе с действительно произвольными функциями рассуждение
о вычислениях приходится вести в терминах применения символа функции
к соответствующему символу аргумента. Еще большая симметрия в тол-
ковании функций и аргументов достигается, если считать их объектами
-- без дополнительных оговорок, -- и исследование процесса вычисления
свести к рассуждению о приложении (апплицировании) одного объекта к
другому. В этом случае на выполнение подстановки можно не накладывать
обременительных ограничений, что позволяет перейти к формализациям
высших порядков. Если порядок такой теории не ограничен, то это тео-
рия с неограниченным принципом свертывания.
Между обоими видами систем можно устанавливать различные свя-
зи, проявляя потенциальные возможности и того, и другого подхода. В
частности, зададимся вопросом, как средствами АВС (пользуясь опера-
торами аппликации и абстракции) выразить содержательное предста-
вление 2-местных, 3-местных, . . ., n-местных функций, трактуемых как
операторы. Воспользуемся следующими соглашениями об обозначениях:
[x, y] = λr.rxy, h : A × B → C,
CurryABC : (A × B → C) → (A → (B → C)).
Таким образом,hсчитается обычным двухместным оператором, аCurry
- преобразованием из операторного вида в аппликативный 1:
CurryABC h = λxy.h[x, y],
λxy.h[x, y] : A → (B → C).
Задача 12.1 Рассмотрим семейство функций h:
h2 : A × B → C,
h3 : A × B × C → D,
h4 : A × B × C × D → E,
. . . : . . . . Найти семейство отображений:
CurryABC, Curry(A×B)CD, Curry(A×B×C)DE, . . . ,
которые каррируют данные функции, то есть переводят их в аппликативный вид.
Решение. В качестве примера рассмотрим каррирование h3 и h4 .
Curry--1. Действительно, пусть h3 : (A × B) × C → D.
Тогда
Λ(A × B)CDh3 = λxy.h3[x, y] : A × B → (C → D).
Теперь мож-
но считать, что Λ(A × B)CDh3 = h0
2, и поэтому следующая идея
1
В теоретических исследованиях вместо обозначения “Curry” часто исполь-
зуется обозначение “Λ”; в дальнейшем будем использовать именно это последнее
обозначение.
состоит в подстановке вместо первой переменной - упорядоченной
пары переменных, то есть
ΛAB(C→ D)(Λ(A × B)CDh3) =
= λuv.(Λ(A × B)CDh3)[u, v]
= λuv.(λxy.h3[x, y])[u, v]
= λuv.(λy.h3[[u, v], y])
= λuvy.(h3[[u, v], y]) : A → (B → (C → D))
= (ΛAB(C→ D) ◦ Λ(A×B)CD) h3.
Curry--2. Пусть теперь h4 : A×B×C×D → E,
где предполагается,
что A×B ×C × D = (A×B ×C)× D = ((A×B)×C)× D.
Тогда рассмотрим преобразование каррирования по шагам.
Шаг 1:
Λ((A×B)×C)DEh4 = λxy.h4[x, y] : ((A×B)×C) → (D → E).
Шаг 2:
Λ((A×B)C(D→ E)(Λ((A×B)×C)DEh4) =
= λuv.(Λ((A×B)×C)DEh4)[u, v]
= λuvy.h4[[u, v], y] : A×B → (C → (D → E)).
Шаг 3:
ΛAB(C→ (D→ E)(λuvy.h4[[u, v], y]) =
= λxy.(λuvy.h4[[u, v], y])[x, y]
= λxyvy.h[[[x, y], v], y].
Обсуждая полученное в пунктах (Curry−1) и (Curry−2) решение,
можно заметить, что функции каррирования имеют вид:
Λ(A×B×C)DE =
= ΛAB(C→ (D→ E)) ◦ Λ(A × B)C(D→ E) ◦ Λ(A×B)×C)DE.
Для целей отыскания решения в общем случае перепишем это ра-
венство в виде:
Λ(A1×A2×A3)A4B =
= ΛA1A2(A3→ (A4→ B)) ◦Λ(A1×A2)A3(A4→ B) ◦Λ((A1×A2)×A3)A4B.
Остается самостоятельно получить соответствующее равенство для
n-местных функций2.
2
Это выполняется индукцией по числу аргументных мест.
|
Главная
Каталог файлов
