람다 대수

람다 대수(λ代數, ) 또는 λ-대수 또는 람다 계산(λ計算) 또는 람다 계산법(λ計算法)은 추상화와 함수 적용 등의 논리 연산을 다루는 형식 체계이다. 람다 대수의 항은 변수와 추상화 및 적용 연산을 통해 구성되며 (비순수 람다 대수에서는 상수 역시 구성에 참여한다), 추상화의 기호로는 그리스 문자 람다(λ)가 사용된다. 람다 대수의 항들에 대하여 알파 동치와 베타 축약 등의 연산을 수행할 수 있다. 알파 동치는 제한 변수를 변경하는 변환으로서 이름 충돌을 방지하기 위해 사용되며, 드 브루인 첨수를 사용할 경우 이는 필요 없다. 베타 축약은 함수 적용을 적절한 치환 연산 결과로 대신하는 변환이며, 베타 축약에 대한 주어진 항의 표준형이 (존재할 경우) 알파 동치 아래 유일하다는 사실은 처치-로서 정리의 따름정리이다.
1930년대 알론조 처치가 수학기초론을 연구하는 과정에서 람다 대수의 형식을 제안하였다. 최초의 람다 대수 체계는 논리적인 오류가 있음이 증명되었으나, 처치가 1936년에 그 속에서 계산과 관련된 부분만 따로 빼내어 후에 유형 없는 람다 대수라고 불리게 된 체계를 발표하였다. 또한 1940년에는 더 약한 형태이지만 논리적 모순이 없는 단순 유형 람다 대수를 도입하였다.
람다 대수는 튜링 완전성을 만족시키며, 보편 튜링 기계와 동치이다. 람다 대수는 프로그래밍 언어 이론에서 중요한 역할을 하며, 리스프를 비롯한 함수형 프로그래밍 언어의 기반이 된다. 람다 대수는 그 밖에도 논리학, 철학, 언어학, 컴퓨터 과학 등의 여러 분야에서 응용된다.
역사.
람다 대수는 수학자 알론조 처치에 의해 수학기초론 연구의 일환으로 1930년대 소개됐다. 최초의 시스템은 스티븐 클레이니와 존 버클리 로서가 클리네-로저 역설을 제창하면서 1935년 논리적 모순을 보이기 위해 도입됐다.
그 후인 1936년 처치는 독립적으로 현재에는 유형 없는 람다 대수라고 불리는 계산에 관련한 부분을 출판했다. 1940년, 그는 또한 계산적으로는 떨어지지만 논리적으로 무결한 시스템을 공개했다. 이것이 단순 유형 람다 대수이다.
1960년대에 람다 대수와 프로그래밍 언어의 관계가 명확히 밝혀지기 전까지는 λ-대수는 단지 형식주의 (formalism)일 뿐이었다. 감사하게도 리처드 몬터규와 언어학자들이 λ-대수를 자연어 (natural language)의 의미론에 적용함으로써, λ-대수는 언어학과컴퓨터 과학 양쪽 분야에서 인정받는 위치를 차지했다.
도입.
함수의 표현.
함수는 컴퓨터 과학과 수학의 기초를 이루는 개념이다. 람다 대수는 함수를 단순하게 표현할 수 있도록 하여 '함수의 계산'이라는 개념을 더 깊이 이해할 수 있게 돕는다.
예를 들어 항등 함수 formula_1는 하나의 입력 formula_2를 받아 다시 formula_2를 결과로 내놓는다고 하자. 한편 함수 formula_4는 입력 formula_2와 formula_6를 받아 두 수의 제곱의 합을 내놓는다고 하자. 이 두 예제로부터 세 가지 유용한 사실을 알 수 있다.
formula_18formula_19formula_20
핵심 개념.
추상화: formula_21는 단일 입력 formula_2를 받아 formula_23의 표현으로 치환하는 익명의 함수를 지칭한다. 예를 들어 formula_24는 함수 formula_25의 람다 추상화이다. 람다 추상화를 통해 함수를 정의한다는 것은 함수를 정의하기만 하고 함수를 수행(호출)하지는 않는다는 것을 의미한다. 람다 추상화를 통해 변수 formula_2는 표현 formula_23에 속박된다.
자유 변수: 자유 변수(free variable)는 람다 추상화를 통해 표현에 묶이지 않은 변수를 말한다. 자유 변수의 집합은 귀납적으로 정의된다.
예를 들어, formula_38에는 자유 변수가 없지만, formula_39에는 자유변수가 formula_6 하나이다.
정의.
람다 대수의 언어는 변수, 상수, 람다 기호, 괄호, 온점으로 구성된다. 변수와 상수는 (후술할) 람다 항의 기초 구성원들이며, 람다 항에 등장하는 자유 변수는 (이후 정의할) 치환 연산을 통해 다른 람다 항으로 치환될 수 있다. 람다 기호는 (후술할) 추상화 연산을 나타내는 기호이다. 괄호와 온점은 이론적으로는 불필요하지만, 여러 가지 편의를 위해 사용된다. 구체적으로, 다음과 같은 데이터가 주어졌다고 하자.
(여기서 formula_42가 최대 원소를 갖지 않는 정렬 전순서 집합이어야 하는 것은 치환의 정의에서 주어진 모든 변수들보다 큰 변수들의 집합의 최소 원소를 취할 수 있어야 하기 때문이다.) 그렇다면, formula_46에 대한 람다 대수의 언어는 다음과 같은 기호들로 구성된다.
람다 항(λ項, )은 변수와 상수들로부터 시작하여 유한 차례 적용 및 추상화를 가하여 얻는, 람다 대수 기호들의 문자열이다. 즉, 이는 다음과 같은 문법을 따른다.
괄호 사용을 줄이기 위해 단순히 formula_64은 formula_65을 나타내고, formula_66은 formula_67을, formula_68 (또는 formula_69)은 formula_70을 나타내는 데 사용할 수 있다. 예를 들어, 변수 formula_2, formula_6, formula_73에 대하여,
는
를 나타낸다.
연산.
자유 변수와 제한 변수.
람다 항에 등장하는 변수들은 자유 변수(自由變數, )와 제한 변수(制限變數, )로 분류된다. 람다 항 formula_54과 변수 formula_2에 대하여, 만약 formula_54에 등장하는 모든 formula_2가 formula_54 속 formula_81과 같은 꼴의 부분 람다 항에 등장한다면 formula_2는 제한 변수이며, 만약 적어도 한 formula_2가 formula_81과 같은 꼴의 부분 람다 항에 등장하지 않는다면 formula_2는 자유 변수이다. 즉, 람다 항 formula_54의 자유 변수의 집합 formula_87는 formula_54의 구조에 따라 다음과 같이 재귀적으로 정의된다.
람다 항 formula_54에 등장하는 변수 가운데 자유 변수가 아닌 것들을 formula_54의 제한 변수라고 한다. 자유 변수를 갖지 않는 람다 항을 닫힌 람다 항(닫힌λ項, )이라고 한다.
예를 들어, 변수 formula_2, formula_6, formula_73에 대하여,
의 자유 변수의 집합은 formula_105이며, 제한 변수의 집합은 formula_106이다.
치환.
주어진 람다 항에 등장하는 자유 변수를 또 다른 람다 항으로 치환(置換, )하는 연산을 정의할 수 있다. 치환 연산의 정의는 자연스러우며, 다만 원래 람다 항의 의미가 변질되는 경우에는 알파 변환이 선행되어야 한다 (이는 아래 네 번째 조건의 세 번째 경우에 해당한다). 구체적으로, 람다 항 formula_54, formula_55 및 변수 formula_2에 대하여, formula_2를 formula_55으로 치환한 formula_54의 치환 실례(置換實例, ) formula_113는 formula_54의 구조에 따라 다음과 같이 재귀적으로 정의된다.
예를 들어,
이다.
알파 동치.
알파 동치(α同値, )는 제한 변수 변경을 통해 주어진 람다 항을 새로운 람다 항으로 변환하는 방법이다. 람다 항 formula_54이 부분 람다 항 formula_126를 가질 경우, 이를 formula_127의 자유 변수가 아닌 변수 formula_6에 대하여 formula_129로 바꾸면 새로운 람다 항을 얻는다. 이와 같은 과정을 유한 번 거듭하여 람다 항 formula_55를 얻을 경우, 두 람다 항 formula_54, formula_55이 서로 알파 동치라고 하며, formula_133라고 표기한다.
예를 들어,
이다.
베타 축약.
베타 축약(β縮約, )은 추상화된 함수의 적용을 적절한 치환 실례로 바꾸는 것을 통해 람다 항을 변환하는 방법이다. 람다 항 formula_54가 부분 람다 항 formula_136를 가질 경우, 이를 formula_137로 대신하여 새로운 람다 항 formula_55를 얻을 수 있다. 이 경우 formula_139이라고 표기한다. 두 람다 항 formula_54, formula_55이 다음 조건을 만족시키면, formula_55이 formula_54의 베타 축약이라고 하며, formula_144이라고 표기한다.
두 람다 항 formula_54, formula_55에 대하여, 다음 두 조건이 서로 동치이며, 이를 만족시키는 formula_54, formula_55을 서로 베타 동치(β同値, )라고 하며, formula_153이라고 표기한다.
람다 항 formula_55이 formula_136와 같은 꼴의 부분 람다 항을 가지지 않는다면, formula_55을 베타 표준형(β標準型, )이라고 한다. 베타 표준형 formula_55이 람다 항 formula_54의 베타 축약이라면 (즉, formula_144이라면), formula_55을 formula_54의 베타 표준형이라고 한다. 처치-로서 정리에 따라, 주어진 람다 항의 베타 표준형이 존재할 경우, 이는 (알파 동치를 무시하면) 유일하다.
응용.
formula_169이 음이 아닌 정수의 집합이라고 하자.
산술의 표현.
람다 대수의 언어를 사용하여 자연수의 페아노 산술을 다음과 같이 표현할 수 있다.
여기서
이다.
μ-재귀 함수의 표현.
μ-재귀 함수는 람다 대수의 언어를 사용하여 표현할 수 있다. 즉, 임의의 부분 재귀 함수 formula_174에 대하여, 다음 두 조건을 만족시키는 람다 항 formula_175가 존재한다. (여기서 formula_176는 점을 가진 집합이다.)