ДУШКИН Роман Викторович

*****@***ru

http://roman-dushkin.narod.ru/

Введение в функциональное программирование

ФП 02005-05 01

Майк Гордон
(Mike Gordon)

University of Cambridge

*****@***cam. ac. uk

http://www.cl.cam.ac.uk/users/mjcg/

2018


Аннотация

Ключевые слова:

Содержание

1.        Заголовок 1        3

1.1.        Заголовок 2        3

1.1.1.        Заголовок 3        3

Приложение A        3

Список сокращений

       —        

Введение в л-исчисление

л-исчисление ( или лямбда-исчисление) – это теория функций, первоначально разработанная логиком Алонзо Чёрчем для обоснования математики. Работа проводилась в 1930х годах, за несколько лет до появления цифровых вычислительных машин. Немного раньше, в 1920х годах, Мосес Шонфинкель разработал другую теорию функций, основанную на “комбинаторах”. В 1930х годах, Хаскел Карри доработал и расширил теорию Шонфинкеля и доказал её эквивалентность л-исчислению. Приблизительно в это же время, Клин показал что л-исчисление является универсальной вычислительной системой. Она была одной из первых среди подобных систем, подвергшихся тщательному анализу. В 1950х годах л-исчисление подвигло Джона Маккарти на создание языка программирования LISP. В начале 1960х годов Питер Ландин показал, как можно описать императивные языки  программирования, переведя их в л-исчисление. Кроме того, им был разработан  важный  прототип  языка программирования  ISWIM. Эта  работа  ввела  основные  нотации  функционального  программирования  и  повлияла  на  разработку  как  императивных, так  и  функциональных  языков  программирования. Основываясь  на  этой  работе, Кристофер  Страчей  заложил  основы  для  такой  важной  области  как  денотационная  семантика. Техническая  сторона работы  Страчей, сподвигла  логика  Дана  Скотта  на  создание  теории  доменов, которая  в  настоящее  время  является  одним  из  самых  важных  разделов  теоретических  компьютерных  наук. В  1970-х годах Петер  Хендерсон  и  Джим  Моррис  продолжили  работу  Ландина  и  написали  несколько  важных  статей  о  преимуществах  использования  функционального  программирования  для разработки  программного обеспечения. Приблизительно в это  же  время  Девид  Тёрнер  предложил использовать комбинаторы Карри и Шонфинкеля в качестве машинного кода компьютеров для реализации функциональных языков программирования. Такие  компьютеры  могут  использовать  математические  свойства

НЕ нашли? Не то? Что вы ищете?

л-исчисления для параллельного выполнения программ. В 1980х годах несколько исследовательских групп использовали идеи Хендерсона и Тёрнера для практической реализации функционального программирования, разработав специальную архитектуру для его поддержки (некоторые из которых содержали несколько процессоров). 

  Таким образом, мы видим, что эта неприметная ветвь математической логики лежит в основе важных разработок в теории языков программирования, таких как:

1)Изучение фундаментальных вопросов обработки данных.

2)Разработка языков программирования.

3)Семантика языков программирования.

4)Архитектура компьютеров.

1.1  Синтаксис и семантика л-исчисления.

л-исчисление – это нотация для определения функций. Выражения в этой нотации называются л-выражениями, и каждое такое выражение обозначает функцию. В дальнейшем будет понятно как можно использовать функции для представления большого разнообразия данных и структур данных, таких как числа, пары, списки и т. п. В частности, будет показано как можно представить случайную пару чисел (х, y) с помощью л-выражения.  Примем следующие соглашения об обозначениях: мнемонические названия, соответствующие л-выражениям, будем обозначать жирным шрифтом, или  подчёркнутым текстом;  например, 1 – это

л-выражение (см. 2.3), используемое для обозначения числа 1.

Существуют 3 вида л-выражений:


Переменные: x, y, z и т. д.  Функции, соответствующие переменным,

  определяются тем, какие переменные  связаны  в этой  окрестности.

  Связывание производится абстракциями(см. ниже). Мы  будем

  использовать V, V1, V2 для обозначения  произвольных  переменных.

Апликации функций или комбинации: Если Е1 и Е2 – л-выражения, то (Е1 Е2) – также л-выражение; это означает результат приложения функции, обозначенной Е1 к функции, обозначенной Е2.  Е1  называется “ратором”  ( от английского operator), а Е2 называется “рендом” ( от английского operand).

Например, если

  ( m, n ) функция представленная парой чисел m и n  ( см. 2.2 ),

  а sum – дополнительная функция л-исчисления ( см. 2.5 ), тогда

  приложение (sum(m, n)) означает m+n.

  ( Необходимо заметить, что sum – это л-выражение, тогда как

  “+” – математический символ “метаязыка”( в нашем случае – 

  русского), который мы используем в л-исчислении). 

3.  Абстракции: Если V – переменная, а Е - л-выражение, то лV. E – 

это абстракция со связанной переменной V и телом Е. Такая абстракция представляет собой  функцию с аргументом  a, которая в качестве результата возвращает функцию Е, в окружение, где связанная переменная V означает а. Или, другими словами, абстракция  лV. E представляет собой функцию, которая преобразовывает аргумент E’ в E[E’/V] ( результат замены E’ на V в Е, см. 1.8). Например, лm (x,1)  является функцией добавления единицы.

Используя БНФ, синтаксис л-выражений можно представить следующим образом:

  < л-выражение> ::= <переменная>

  |  (<л-выражение>< л-выражение>)

  |  ( л<переменная>.< л-выражение>)

Если V принадлежит синтаксическому классу <переменная> и Е, Е1, Е2 и т. д. принадлежат синтаксическому классу < л-выражение >, тогда БНФ-нотация упрощается до :

E ::= V|(E1 E2)| лV. E,

Где V - переменные,  ( Е1 Е2 ) – апликации, лV. E – абстрации.

Приведенное описание значения л-выражений,  является нечетким и интуитивным. Логикам (см. Дана Скотт[32]) понадобилось 40 лет для того, чтобы составить строгое описание. Мы не будем углубляться в этот вопрос.

Пример:  ( лx. x ) представляет собой  “тождественную функцию” :

  (( лx. x)E) = E.

Пример:  ( лx. (лf. (f x))) является функцией, которая, будучи применена к Е, даёт (лf. (f x))[E/x], т. е. (лf.(f E)). Последняя, будучи в свою очередь применена к E’ даёт (f E)[E’/f] т. е. (E’ E). Таким образом:

((лx. ( лf. (f x))) E) = (лf. (f E))

и

((лf. (f E)) E') = (E' E).

Упражнение 1

Дайте описание функции (лx. ( лy. y)).

Пример:  В 2.3 дано описано как числа можно представить л-выражениями. Предположим это уже сделано и 0, 1, 2 , … - л-выражения, которые соответственно представляют 0, 1, 2 , … . Предположим также, что add - л-выражение, удовлетворяющее условию:

((add m) n) = m+n.

Тогда (лx. ((add 1) x)) является л-выражением, представляющем собой функцию, которая преобразует n  в 1+n, а 

(лx. (лy. ((add x) y))) представляет собой л-выражение, которое переводит m  в функцию, которая, будучи применена к n  , даёт m+n, т. е. лy. (add m)y)). 

Связь между функцией sum, описанной в начале раздела, и функцией add в предыдущем примере будет объяснена в 2.5.

1.2 Соглашение об обозначениях

Следующие соглашения призваны минимизировать количество скобок в выражениях:

1. Применение  функций  начинается  слева, т. е.  Е1 Е2 … Еn  означает

  (( … ( E1 E2) … ) En). Например:

E1 E2  означает  ( E1 E2)

E1 E2 E3  означает  ((E1 E2) E3)

E1 E2 E3 E4  означает  (((E1 E2) E3) E4)

2.  лV. E1 E2 … En означает (лV. (E1 E2 … En)). Таким образом, границы “ лV” уходят вправо так далеко, насколько это возможно.

3.  лV1 … Vn. E  означает  (лV1. ( … . (лVn. E) … )). Например:

лx y. E  означает  (лx. ( лy. E))

лx y z. E  означает  (лx. ( лy. (лz. E)))

лx y z w. E  означает  (лx. ( лy. (лz. (лw. E))))

Пример:  лx y. add y x  означает  (лx. (лy. ((add y) x))).  

1.3 Свободные и связанные переменные

Вхождения переменной V в л-выражение называется свободным если она не входит в “лV” , иначе оно называется  связанным.  Например:

  ( лx. y x) ( лy. x y) 

  1  1

  2  2  1- свободная,  2- связанная 

1.4  Правила конверсии

В Главе 2 будет объяснено как можно использовать л-выражения для представления объектов данных, таких как числа, строки и т. п.

Например, арифметическое выражение (2 + 3) х 5, также как и его “значение” 25 , может быть представлено как л-выражение. Процесс “упрощения” (2 + 3) х 5 до 25 будет представлен процессом, который мы назовём “конверсией” (или редукцией).  Правила л-конверсии, описанные ниже, несмотря на то, что они носят весьма общий характер, будучи применены к л-выражениям, которые представляют арифметические выражения, моделируют арифметические вычисления.

Существуют 3 типа конверсии : α-конверсия, β-конверсия  и  η-конверсия  ( почему они получили такие названия – неизвестно). Согласно правилам конверсии, нотация  E[E'/V] используется для обозначения  замены E' на каждое  свободное вхождение V  в  Е. Замена  называется  эффективной, тогда и только тогда, когда ни одна из свободных переменных в E' не становится связанной  в  E[E'/V]. Более подробно замена описывается в 1.8. 

Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 5 6 7 8 9 10 11