Функциональное программирование - лямбда-исчисление

Лямбда-исчисление является основой, разработанной Алонзо Черчем в 1930-х годах для изучения вычислений с функциями.

  • Создание функции - Черч ввел обозначение λx.E для обозначения функции, в которой «x» является формальным аргументом, а «E» - функциональным телом. Эти функции могут быть без имен и без аргументов.

  • Применение функции - Черч использовал обозначение E 1 .E 2 для обозначения применения функции E 1 к фактическому аргументу E 2 . И все функции на один аргумент.

Синтаксис лямбда-исчисления

Исчисление Ламдбы включает в себя три различных типа выражений, т.е.

E :: = x (переменные)

| E 1 E 2 (функция приложения)

| λx.E (создание функции)

Где λx.E называется лямбда-абстракцией, а E называется λ-выражением.

Оценка лямбда-исчисления

Чистое лямбда-исчисление не имеет встроенных функций. Давайте оценим следующее выражение - 

(+ (* 5 6) (* 8 3))

Здесь мы не можем начать с «+», потому что он работает только с числами. Есть два приводимых выражения: (* 5 6) и (* 8 3).

Мы можем уменьшить либо один в первую очередь. Например - 

(+ (* 5 6) (* 8 3)) 
(+ 30 (* 8 3)) 
(+ 30 24) 
= 54

β-редукция Правило

Нам нужно правило редукции для обработки λs 

(λx . * 2 x) 4 
(* 2 4) 
= 8

Это называется β-редукцией.

Формальный параметр может быть использован несколько раз - 

(λx . + x x) 4 
(+ 4 4) 
= 8

Когда есть несколько терминов, мы можем обработать их следующим образом: 

(λx . (λx . + (− x 1)) x 3) 9

Внутренний x принадлежит внутреннему λ, а внешний x принадлежит внешнему. 

(λx . + (− x 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
= 11

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

В выражении каждое появление переменной является либо «свободным» (для λ), либо «связанным» (для λ).

β-редукция (λx. E) y заменяет каждый x , свободный в E, на y . Например -

Связанные переменные

Альфа уменьшение

Альфа-редукция очень проста и может быть выполнена без изменения значения лямбда-выражения. 

λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x)

Например - 

(λx . (λx . + (− x 1)) x 3) 9 
(λx . (λy . + (− y 1)) x 3) 9 
(λy . + (− y 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
11

Теорема Черча-Россера

Теорема Черча-Россера гласит следующее:

  • Если E1 ↔ E2, то существует E, такое, что E1 → E и E2 → E. «Уменьшение любым способом может в конечном итоге привести к тому же результату».

  • Если E1 → E2, а E2 - нормальная форма, то существует нормальное упорядочение E1 до E2. «Уменьшение нормального порядка всегда будет давать нормальную форму, если таковая существует».

Назад Вперёд