람다 연산
람다 연산(람다 대수, 람다 계산, 람다 계산법; 영어: lambda calculus)은 수리논리학과 이론 컴퓨터과학에서 사용하는 형식 체계(formal system)로, 함수의 정의, 적용 등을 치환, 바인딩 등을 이용하여 추상화한다. 알론조 처치가 1930년대 처음 발표하였다.
역사
라이프니츠는 다음과 같은 생각을 가지고 있었다.
- 모든 문제들이 서술될 수 있는 '보편적인(universal) 언어'를 만들어라.
- 위의 언어로 서술된 모든 문제를 해결할 수 있는 방법을 찾아라.
첫 번째 것은, 만약 수학적인 문제만으로 제한한다면, 러셀과 프레게 등에 의한 '집합론'의 공리적 서술로 인하여 꽤 만족스러운 결과를 얻었다고 할 수 있다. 하지만 두 번째 것은, 당연히 안 될 것 같지만, 그 증명이 명확하지 않았다. (이는 힐베르트에 의하여 Entscheidungsproblem로 불리게 된다. 직역하면 결정 문제이다.) 이것은 1930년대에 알론조 처치와 앨런 튜링에 의하여 각각 독립적으로 해결되는데, 그 답은 처치-튜링 명제를 가정할 때[1] No이다. 튜링은 후에 이 두 방법으로의 계산 가능성, 즉 계산 가능한 함수들의 모임이 서로 같음을 보였다. 람다 연산이 고안된 이후로, 람다 연산에 기반한 함수 프로그래밍 언어(functional programming language)가 만들어졌다. Reduction machine은 이런 functional language의 실행을 위하여 고안되었다.
- ↑ Church-Turing 명제는 다음을 말한다: 알고리듬으로 계산 가능함과 튜링 기계로의 계산 가능성은 동치이다. 이와 동치 명제로, 알고리듬으로 계산 가능함과 lambda calculus로 표현 가능함은 동치이다.)