Лямбда исчисление

Автор: Пользователь скрыл имя, 18 Марта 2012 в 20:08, реферат

Описание работы

Функциональные языки программирования появились в качестве средства для написания программ, не содержащих в явном виде понятий ячеек памяти для хранения значений (переменных) и последовательности вычислений как процесса изменения состояния памяти. Тем не менее, основа для создания таких языков была предложена еще в середине 30-х годов 20-го века Алонзо Черчем (Alonzo Church) и Стефаном Клини (Stephen Kleene). Мы рассмотрим теорию Черча, названную им лямбда-исчислением, в качестве теоретической основы и "минимального" функционального языка программирования.

Работа содержит 1 файл

Лямбда исчисление.docx

— 147.45 Кб (Скачать)

Функции с несколькими аргументами

Заметим для начала, что в лямбда-исчислении отсутствует встроенная поддержка  функций с несколькими аргументами. Разумеется, ее было бы нетрудно добавить, однако того же самого результата проще  достичь через функции высшего порядка (higher-order functions), которые возвращают функции в качестве результата. Допустим, у нас есть терм s с двумя свободными переменными x и y, и мы хотим написать такую функцию f, которая выдавала бы для каждой пары аргументов (v,w) результат подстановки v вместо x и w вместо y. Мы пишем не f = λ(x,y).s, как мы сделали бы это в более богатом языке, а f = λx.λy.s. Это означает, что f есть функция, которая, получив значение v для параметра x, выдает функцию, которая, получив значение w для параметра y, выдает нужный результат. После этого мы поочередно применяем f к аргументам, получая запись f v w (т. е., (f v) w), которая переходит в ((λy.[x ↦ v]s) w), и далее в [y ↦ w][x ↦ v]s. Такое преобразование функций с несколькими аргументами в функции высшего порядка называется каррированием (currying) в честь Хаскелла Карри, современника Чёрча.

Булевские константы Чёрча

Еще одна языковая конструкция, легко кодируемая в лямбда-исчислении — булевские значения и условные выражения. Определим термы tru и fls таким образом:

  tru = λt. λf. t;

  fls = λt. λf. f;

(Этим  термам даны сокращенные имена,  чтобы избежать их смешения с элементарными булевскими константами true и false из главы 3.)

Можно считать, что термы tru и fls представляют собой булевские значения <<истина>> и <<ложь>> в том смысле, что с их помощью мы можем выполнять операцию проверки булевского значения на истинность. А именно, мы можем определить комбинатор test, такой, что test b v w переходит в v, если b равно tru, и в w, если b равно fls.

  test = λl. λm. λn. l m n;

Комбинатор test почти ничего не делает: test b v w просто переходит в b v w. В сущности, булевские значения являются условными выражениеми: они принимают два аргумента и выбирает из них либо первый (если это tru), либо второй (если это fls). Например, терм test tru v w редуцируется таким образом:

 

test tru v w

 

=

(λl. λm. λn. l m b) tru v w

по определению

(λm. λn. tru m b) v w

редукция подчеркнутого выражения

(λn. tru v b) w

редукция подчеркнутого выражения

tru v w

редукция подчеркнутого выражения

=

(λt. λf. t) v w

по определению

(λf. v) w

редукция подчеркнутого выражения

v

редукция подчеркнутого выражения


 
Несложно также определить в виде функций такие булевские операторы, как логическая конъюнкция:

  and = λb. λc. b c fls;

То  есть, and — это функция, которая, получив два булевских значения b и c, возвращает c, если b равно tru и fls, если b равно fls; таким образом, and b c выдает tru, если и b, и c равны tru, и fls, если либо b, либо c окажутся равными fls.

  and tru tru;

 

|> (λt. λf. t)

 

  and tru fls;

 

|> (λt. λf. f)

Упражнение 1   [★]: Определите логические функции or (<<или>>) и not (<<не>>).

Пары

При помощи булевских констант мы можем  закодировать пары значений в виде термов:

  pair = λf.λs.λb. b f s;

  fst = λp. p tru;

  snd = λp. p fls;

Это означает, что pair v w — функция, которая, будучи применена к булевскому значению b, применяет b к v и w. По определению булевских констант, при таком вызове получится v, если bравняется tru, и w, если b равняется fls, так что функции первой и второй проекции fst и snd можно получить, просто подав в пару соответствующие булевские значения. Вот как проверить, что fst (pair v w) →v:

 

fst (pair v w)

 

=

fst ((λf.λs.λb. b f s) v w)

по определению

fst ((λs.λb. b v s) w)

редукция подчеркнутого выражения

fst (λb. b v w)

редукция подчеркнутого выражения

=

(λp. p tru) (λb. b v w)

по определению

(λb. b v w) tru

редукция подчеркнутого выражения

tru v w

редукция подчеркнутого выражения

*

v

как показано ранее.


Числа Чёрча

После всего, что мы видели, представление  чисел в виде лямбда-термов будет лишь ненамного сложней. Числа Чёрча (Church numerals) co, c1, c2, и т. д. можно определить таким образом:

c0 = λs. λz. z;

c1 = λs. λz. s z;

c2 = λs. λz. s (s z);

c3 = λs. λz. s (s (s z));

и т. д. Здесь каждое число n представляется комбинатором cn, который принимает два аргумента, s и z (<<функцию следования>> и <<ноль>>), и n раз применяет s к z. Как и в случае с булевскими константами и парами, такое кодирование превращает числа в активные сущности: число n представляется в виде функции, которая что-то делает n раз — своего рода активное число по основанию 1.

(Читатель  мог уже заметить, что cи fls записываются одним и тем же термом. Такие <<каламбуры>> часто встречаются в языках ассемблера, где одна и та же комбинация битов может представлять собой множество разных значений — целое число, число с плавающей точкой, адрес, четыре символа и т. п., — в зависимости от того, как интерпретируются биты. Аналогичная ситуация в низкоуровневых языках вроде C, где 0 и false тоже представляются одинаково.)

Функцию следования на числах Чёрча можно  определить так:

  scc = λn. λs. λz. s (n s z);

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

Упражнение 2   [★★]: Найдите ещё один способ определения функции следования на числах Чёрча.

Похожим образом, сложение на числах Чёрча можно  осуществлять с помощью терма plus, который принимает в качестве аргументов два числа Чёрча, m и n, и возвращает еще одно число Чёрча — т. е., функцию, которая принимает аргументы s и z, применяет s к z n раз (передавая s и z в качестве аргументов n), а потом применяет s еще m раз к результату:

  plus = λm. λn. λs. λz. m s (n s z);

Для реализации умножения используется еще один трюк: поскольку plus принимает аргументы по одному, применение его к одному аргументу n дает функцию, которая добавляет n к любому данному ей аргументу. Можно передать эту функцию в качестве первого аргумента m, а в качестве второго дать c0, и это будет означать <<применить функцию, добавляющую n к своему аргументу, к нулю и повторить m раз>>, т. е., <<сложить m копий числа n>>.

  times = λm. λn. m (plus n) c0;

Упражнение 3   [★★]: Можно ли определить умножение на числах Чёрча без использования plus?

Упражнение 4   [Рекомендуется,★★]: Определите терм для возведения чисел в степень.

Чтобы проверить, является ли число Чёрча  нулем, нужно найти какую-то подходящую для этой цели пару аргументов, — а именно, нужно применить указанное число к паре термов zz и ss, таких чтобы применение ss к zz один или более раз давало fls, а отсутствие применения давало tru. Понятно, что в качестве zz нужно просто взять tru. Для ss же мы используем функцию, которая игнорирует свой аргумент и всегда возвращает fls:

  iszro = λm. m (λx. fls) tru;

 

  iszro c1;

 

|> (λt. λf. f)

 

  iszro (times c0 c2);

 

|> (λt. λf. t)

Как ни странно, определить вычитание на числах Чёрча намного сложнее, чем  сложение. Для этого можно воспользоваться  следующей довольно хитрой <<функцией предшествования>>, которая возвращает c0, если передать в качестве аргумента c0, и возвращает ci, если передать в качестве аргумента ci+1,:

  zz = pair c0 c0;

  ss = λp. pair (snd p) (plus c1 (snd  p));

  prd = λm. fst (m ss zz);

Это определение работает так: мы используем m в качестве функции и применяем с ее помощью m копий функции ss к начальному значению zz. Каждая копия ss принимает в качестве аргумента пару чисел pair ccи выдает в результате пару pair ccj+1 (см. рис. 5.1). Таким образом, при m-кратном применении ss к pair ccполучается pair cc0, если m = 0, и pair cm-1 cпри положительном m. В обоих случаях, в первом компоненте пары находится искомый предшественник.

 

@C=.2em @R=1.5ex **[r] pair @/_2em/[dd]_ss c0c0 [ddl]_копия [dd]^+1 
 
**[r] pair @/_2em/[dd]_ss c0c1 [ddl]_копия [dd]^+1 
 
**[r] pair @/_2em/[dd]_ss c1c2 [ddl]_копия [dd]^+1 
 
**[r] pair @/_2em/[dd]_ss c2c3 [ddl]_копия [dd]^+1 
 
**[r] pair c3c4 
**[r] ⋮

Figure 5.1: <<Внутренний цикл>> функции предшествования.


 

Упражнение 5   [★★]: Определите функцию вычитания при помощи prd .

Упражнение 6   [★★]: Сколько примерно шагов вычисления (в зависимости от n) требуется, чтобы получить prd cn?

Упражнение 7   [★★]: Напишите функцию equal, которая проверяет два числа на равенство и возвращает Чёрчеву булевскую константу. Например:

  equal c3 c3

 

|> (λt. λf. t)

 

  equal c3 c2

 

|> (λt. λf. f)

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

Упражнение 8   [Рекомендуется,★★★]: Список можно представить в лямбда-исчислении через его функцию свертки fold. (В OCaml эта функция называется fold_left; ее иногда еще называютreduce.) Например, список [x, y, z] становится функцией, которая принимает два аргумента c и n, и возвращает c x (c y (c z n)). Как будет выглядеть представление nil? Напишите функцию cons, которая принимает элемент h и список (то есть, функцию свертки) t, и возвращает подобное представление списка, полученного добавлением h в голову t. Напишите функции isnilи head, каждая из которых принимает список в качестве параметра. Наконец, напишите функцию tail для такого представления списков (это намного сложнее; придется использовать трюк, аналогичный тому, что использовался при определении prd для чисел).

Расширенное исчисление

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

В λNB по сути есть две разные реализации булевских значений и две реализации чисел: настоящие и закодированные методом, описанным в этой главе. Мы можем выбирать между ними при написании программ. Разумеется, эти две реализации нетрудно преобразовать друг в друга. Чтобы перевести булевское значение по Чёрчу в элементарное булевское значение, нужно применить его к значениям true и false:

  realbool = λb. b true false;

Для обратного преобразования используется условное выражение:

  churchbool = λb. if b then tru else fls;

Можно встроить эти преобразования в операции высшего порядка. Вот проверка на равенство для чисел Чёрча, возвращающая настоящее логическое значение:

  realeq = λm. λn. (equal m n) true false;

Аналогично  мы можем преобразовать число  Чёрча в соответствующее элементарное число, применив его к succ и 0:

  realnat = λm. m (λx. succ x) 0;

Мы  не можем напрямую применить m к succ, поскольку сама по себе запись succ не имеет синтаксического смысла: мы определили арифметические выражения так, что succ всегда должен к чему-то применяться. Это требование мы обходим, обернув succ в маленькую функцию, которая всегда возвращает succ от своего аргумента.

Причины, по которым элементарные булевские  и числовые значения оказываются  полезны при работе с примерами, в основном связаны с порядком вычислений. Рассмотрим, например, терм scc c1. Исходя из приведенного выше обсуждения, мы могли бы ожидать, что он должен при вычислении давать число Чёрча c2. На самом деле этого не происходит:

  scc c1;

 

|> (λs. λz. s ((λs'. λz'. s' z') s z))

Этот  терм содержит в себе редекс, который  при вычислении привел бы нас (за два  шага) к c2, однако согласно правилам вызова по значению мы ещё не можем сделать это, поскольку редекс находится внутри лямбда-абстракции.

Никакой фундаментальной проблемы здесь  нет: терм, получающийся при вычислении scc c1, очевидным образом поведенчески эквивалентен (behaviorally equivalent) c2, в том смысле, что применение этого терма к паре аргументов v и w всегда даст тот же результат, что и применение cк тем же аргументам. Однако, необходимость доделать вычисление затрудняет проверку того, что наша функцияscc ведет себя как надо. В случае более сложных арифметических вычислений трудность еще возрастает. Например, times ccдает в результате не c4, а такое чудовищное выражение:

  times c2 c2;

 

|> (λs.

     λz.

       (λs'. λz'. s' (s' z')) s

       ((λs'.

          λz'.

            (λs''. λz''. s'' (s'' z'')) s'

            ((λs''. λz''.z'') s' z'))

       s

       z))

Можно убедиться, что этот терм ведет себя так же, как c4, с помощью проверки на равенство:

  equal c4 (times c2 c2);

 

|> (λt. λf. t)

Однако  более прямой способ — взять times ccи преобразовать в элементарное число:

  realnat (times c2 c2);

 

|> 4

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

Информация о работе Лямбда исчисление