이장에서는 $\lambda-$계산을 형식적으로 소개한다. $\lambda-$계산은 수학과 컴퓨터 과학등 다양한 분야에서 중요한 개념으로 사용되는 형식 언어이다. $\lambda-$계산은 알론조 처치(Alonzo Church)에 의해 1930년대 초에 개발되었으며, 이론적인 컴퓨팅과 함수의 표현에 매우 유용하다.

$\lambda-$계산은 변수, 함수 추상화, 그리고 함수 적용을 사용하여 구성된다. 변수들의 무한한 집합을 $V=\lbrace{v, v', v''..\rbrace}$라고 가정하고, 이 변수들을 이용하여 $\lambda-$계산의 식($\lambda-term$)을 형성한다. 함수 추상화는 람다 기호($\lambda$)와 변수를 사용하여 정의하며, 함수 적용은 괄호를 이용하여 표현한다.
$\lambda-$계산의 특성과 활용 방법에 대해 이해함으로써, $\lambda-$계산이 어떻게 다양한 분야에서 중요한 도구로 사용되는지와 $\lambda-$계산의 응용 가능성과 기본 원리들에 대한 이해를 갖출 수 있을 것이다.

🔗History

17세기 라이프니츠는 다음과 같은 이상적인 제안을 했다.

• 가능한 모든 문제를 기술할 수 있는 범용언어를 만든다.
• 범용언어로 기술되는 모든 문제를 해결하기 위한 결정방법을 찾는다.

수학적 문제에 한정한다면, 라이프니츠의 첫 번째 제안은 프레게와 러셀 이후 어떤 형태의 집합 이론이 일차 술어 논리의 언어로 표현된 것으로 충족되었다.
두 번째 제안은 중요한 철학적 문제가 되었는데, "범용언어로 제시된 모든 문제를 해결할 수 있을까?"라는 질문이였다. 보편적으로, 그러한 것은 불가능하다고 보이지만, 이것을 증명하는 방법은 명확하지 않았다. 이러한 질문은 Entscheidungsproblem(의사결정 문제)로 알려지게 되었다.