람다 대수 Lambda Calculus란 무엇인가? (ft. Church Encodings)

(참고) What is Lambda Calculus? (ft. Church Encodings) - YouTube

 

what is lambda calculus 

람다 계산법이란, 계산을 이해하는 한 가지 수학적인 모델이다.

람다 계산법은 3개의 간단한 규칙으로 구성된다. 

람다 계산법은 Ocaml, Haskel 같은 함수형 프로그래밍 언어에 큰 영향을 주었다. 

lambda calculus의 규칙들

1. Variable 변수

x, y, z와 같은 변수를 둔다. 

 

2. Abstraction 추상화

λ 람다 기호와 함께 무언가를 함수로 정의한다. 

함수의 유일한 기본 데이터 형식은 함수이다. 

λ를 사용하는 기본적인 방식은 λ parameter.return 형태이다. 

즉, λx.x는 f(x) = x를 표현하는 방식이며, 

λx.λy.x 는 f(x, y) = x 함수를 의미하는 식이다. 

 

Lambda 대수에서는 수학의 Curring이라는 개념을 사용한다. 

함수형 프로그래밍 언어인 Ocaml에는 Curring이 내장되어 있다. 

Curring이란, 인자를 여러 개 받는 함수를 분리하여 인자를 하나씩만 받는 함수의 체인으로 만드는 방법이다. 

(이 방식으로는 하나의 함수를 반복적으로 부름으로써 함수를 재사용하기 쉽다)

 

그래서 λ(x,y).x y와 같은 형태로 인자 두 개를 동시에 받는 대신, 

λx.λy.x y와 같은 형태로 인자를 받아들인다. 

 

3. Application 적용

 

λ로 묶인 식은 하나의 function이다. 

그렇게 만든 function을 사용하는 법은 λx.λy.x y와 같이 끝에 적용하고자 하는 값을 두면 된다. 

λx.λy.x y 

= f(x, y) = x

= x(y)

 

예시

예 1)

(λx.x) y

=> f(x) = x

=> x(y)

 

예 2)

(λx.(λy.x)) z

=> f(x) = λy.x

=> λy.z

 

예 3)

(λx.(λy.x y)) (λx.x) (z)

=> z

 

big boy problem time

프로그래밍 언어에서 람다 계산법을 사용하려면? 

String, int, Bool 같은 기본적인 데이터 타입을 적용할 수 있어야 한다. 

Alonzo Church, @출처 : History Computer

이 문제를 해결한 사람이 바로 미국의 수학자 Alonzo Church(1903-1995)였다. 

그는 Church Encoding을 고안해서 lambda number를 Lambda Calculus에 적용했다.

 

Church Encoding

Church Encoding은 데이터와 함수를 모델링하는 한 가지 정형화된 방식이다. 

 

- Church-encoded Boolean values

두 개의 인수를 사용해서 true일 때 왼쪽 인수를 반환 false일 때 오른쪽 인수를 반환

true = λa.λb.a : true이면, a parameter를 선택하는 함수

false = λa.λb.b : false이면, b parameter를 선택하는 함수

 

- Church-encoded Natural numbers

pred(n) = (n=0) ? 0 : n-1

 

- Church-encoded Maybe / Either / payment types / rose tree