기반적인 함수적 이론
아래의 문법과 연산만으로 모든 수학적, 컴퓨터적 연산을 구현할 수 있다.
문법
-
$x$ : 변수, 함수에서 쓰이는 매계변수를 표현
-
$(\lambda x . M[x])$ : 람다 추상화, 함수를 정의. $x$를 변수로 받아서 $M[x]$을 반환
($M[x]$: $x$를 포함하는 식 $M$) -
$(\lambda x . M[x]) N$ : 적용, $M$에 $N$을 적용 (이후 $\beta$-축약으로 이용)
연산
-
$(\lambda x.M[x]) \longrightarrow (\lambda y.M[y])$ : $\alpha$-conversion($\alpha$-변환),
이때 $(\lambda x.M[x])$, $(\lambda y.M[y])$를 $\alpha$-equivalent($\alpha$-동치) 라고 함 -
$(\lambda x.M[x])N \longrightarrow_{\beta} M[x:=N]$ : $\beta$-reduction($\beta$-축약), $M$의 $x$를 $N$으로 대체