함수형 프로그래밍-Lambda Calculus

Lambda 미적분은 1930 년대 Alonzo Church에서 함수 계산을 연구하기 위해 개발 한 프레임 워크입니다.

Function creation − 교회는 표기법을 도입했습니다 λx.E'x'가 형식 인수이고 'E'가 기능 본문 인 함수를 나타냅니다. 이러한 함수는 이름과 단일 인수가 없을 수 있습니다.
Function application − 교회는 표기법을 사용했습니다. E₁.E₂ 기능의 적용을 표시 E₁ 실제 논쟁에 E₂. 그리고 모든 함수는 단일 인수에 있습니다.

Lambda Calculus의 구문

Lamdba 미적분에는 세 가지 유형의 표현이 포함됩니다.

E :: = x (변수)

| E ₁ E ₂(기능 적용)

| λx.E (함수 생성)

어디 λx.E 이를 Lambda 추상화라고하며 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 . + (− 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

Church-Rosser Theorem은 다음과 같이 말합니다.

E1 ↔ E2라면 E1 → E, E2 → E와 같은 E가 존재합니다.
E1 → E2이고 E2가 정규형이면 E1에서 E2 로의 정규 차수 감소가 있습니다. "정상 차수 감소는 존재한다면 항상 정규 형태를 생성 할 것입니다."