01. Lambda Calculus란?

1. Intro

1-1. Introduction

: Lambda Calculus(= λ Calculus)는 가장 작은, 범용 프로그래밍 언어이다(Universal Progamming Language). λ Calculus는 계산가능한 함수(Computable Function)를 정의하기 위한 수학적인 시스템으로, Alonzo Church에 의해 1936년에 탄생했다. 원래의 시스템은, Stephen Kleene와 J. B. Rogger가 Kleene-Rosser 역설을 발견한 다음, 논리적으로 일치하지 않는 것으로 나타났다. 그 후 1936년에 Church가 계산(Computation)과 관련된 부분만 따로 발표했는데, 이것이 오늘 날 Untyped λ Calculus라고 불리고 있다. 1940년에는, 계산적으로는 약하지만 논리적으로는 일관된 Simply Typed λ Calculus를 소개했다. 

 

 1960년대까지, λ Calculus는 형식주의에 불과했었다. Richard Montague와 다른 언어학자들의 자연어 의미에서의 응용 덕분에, λ Calculus은 언어학과 컴퓨터 과학에서 입지를 굳힐 수 있게 되었었다.

 

 λ Calculus는 함수형 언어(Functional Language)이며, 다른 함수형 언어처럼 수학적인 함수의 이론에 기반을 둔다.  λ Calculus는 모든 계산을 함수의 관점에서 표현할 수 있다.  λ Calculus가 가진 특성은 AI(Artificial Intelligence), Proof System, Logic Programming 분야에서 사용하기 편하다. 그리고 함수와 데이터를 균등하게 다루며, 표기방법도 간단해서 Side effect도 적다. 그래서,  λ Calculus는 순수 함수형 언어의 모델로 사용된다.

※ 1950년대 개발된 LISP는 함수형 프로그래밍 언어이며 λ Calculus를 코어로 두고 있다. 

1-2. Untyped λ Calculus

: Kleene-Rosser의 역설이 발표된 이후, Church는 아주 코어한 로직만 남기고 다른 로직을 좀 제거했는데, 이것을 Untyped λ Calculus(또는 Pure  λ Calculus)라고 부른다. 오늘날, 우리에게 λ Calculus로 알려져 있는 것이다.

1-3. Typed λ Calculus

: λ 심볼을, 익명 함수 추상화(Anonymous Function Abstraction)를 표시하기 위해 쓰는 타입화된 형식주의. Simply Typed λ Calculus은 Typed λ Calculus의 종류중 하나이며, 오직 하나의 타입 생성자를 갖고 기본 타입과 함수 타입만 갖고 있다.

2. Reference

- Wikipedia Lambda Calculus

- λ Calculus tutorial

- Untyped Lambda Calculus

- A Tutorial Introduction to the Lambda Calculus