람다 계산법 (lambda calculus)
쉽게 풀면
람다 계산법은 알론조 처치가 고안한 계산 모델로, 오직 '함수를 만드는 것'과 '함수에 값을 넣어 적용하는 것' 두 가지 연산만으로 이루어져 있다. 숫자도, 참·거짓도, 심지어 반복문까지도 모두 함수만을 이용해 표현할 수 있다는 것이 놀라운 점이다. 튜링 기계와 계산 능력이 정확히 동등하다는 것이 증명되어 있으며, 오늘날 함수형 프로그래밍 언어(예: Haskell, Lisp 계열)의 이론적 뿌리가 되었다.
왜 중요한가
람다 계산법은 함수형 프로그래밍 언어의 이론적 뿌리일 뿐 아니라, 프로그래밍 언어의 의미를 수학적으로 정확히 정의하고 그 성질을 증명하는 데 쓰이는 표준적인 형식 체계입니다. 타입 이론이나 정리 증명기, 프로그램 검증 연구는 대체로 람다 계산법을 확장한 형태 위에서 이루어지기 때문에, 프로그래밍 언어이론(PL) 논문의 상당수가 람다 계산법을 기반 언어로 삼아 결과를 서술합니다. 또한 계산 가능성 이론에서 튜링 기계와 동등한 계산 모델로서 계산이란 무엇인가라는 근본적 질문과도 연결됩니다.
논문에서는 이렇게 쓰입니다
프로그래밍 언어의 핵심 의미론을 수학적으로 정의하고 그 성질(종료성, 타입 안전성 등)을 증명하는 기반으로 인용된다.
프로그램 정적 분석 연구에서 람다 계산법을 대상 언어로 삼아 프로그램의 정지 여부와 관련된 성질을 분석했다는 뜻이다.
정리 증명 및 형식 검증 연구에서 확장된 형태의 람다 계산법이 증명을 기계가 확인 가능한 형태로 표현하는 기초로 쓰인 사례다.
조금 더 깊게 보면
람다 계산법의 핵심 계산 규칙은 함수를 인자에 적용해 값을 바꾸는 베타 축약이며, 이 축약을 반복해 더 이상 줄일 수 없는 형태에 도달하면 계산이 끝났다고 봅니다. 타입이 없는 원래 형태(무제한 람다 계산법)는 계산이 영원히 끝나지 않는 경우도 표현할 수 있는 반면, 여기에 타입 체계를 덧붙인 단순 타입 람다 계산법은 모든 항의 계산이 반드시 끝난다는 종료성을 보장합니다. 이후 다형성, 의존 타입 등을 추가로 도입한 확장판들이 등장했으며, 이런 확장은 커리-하워드 대응을 통해 논리학의 증명 체계와 프로그램의 타입 체계가 근본적으로 대응한다는 관점과도 긴밀하게 연결됩니다.
주의할 점
람다 계산법 자체는 무제한(untyped) 형태에서는 정지하지 않는 계산도 표현할 수 있어, 항상 종료를 보장하려면 타입이 부여된(typed) 람다 계산법을 사용해야 한다.