람다 대수

위키백과, 우리 모두의 백과사전.
이동: 둘러보기, 검색

람다 대수(λ-calculus, lambda-calculus)는 이론 컴퓨터과학 및 수리논리학에서 변수의 네임 바인딩대입의 방법을 이용하여 함수 정의, 함수 적용, 귀납적 함수 추상화를 수행하고 수학 연산을 표현하는 형식 체계이다.

람다 대수는 임의의 튜링기계를 시뮬레이션 할 수 있는 보편적인 계산 모델이다. 1930년대 알론조 처치수학기초론을 연구하는 과정에서 람다 대수의 형식을 제안하였다.

람다 대수는 람다 항목들을(lambda terms) 구성하고 람다 항목들에 축약 연산을 수행한다. 가장 간단한 형태의 람다 대수로서, 람다 항목들을 구성할 때 단지 아래의 규칙만을 이용한다:

문법 명칭 설명
x 변수(Variable) 수학/논리의 값이나 파라메터를 대표하는 문자혹은 문자열
(λx.M) 추상화(Abstraction) 함수 정의를 표현: M은 람다 항목. 변수 x는 종속 변수.
(M N) 적용(Application) 함수를 인자에 적용. M과 N은 람다 항목(lambda terms).

위의 규칙을 이용하여 (λxy.(λz.(λx.z x) (λy.z y)) (x y))와 같은 표현식을 만든다. 혼동의 여지가 없으면 괄호는 생략할 수 있다. 경우에 따라, 논리/수학 상수나 연산 항목이 포함된다.

축약 연산은 다음과 같다.

연산 명칭 설명
(λx.M[x]) → (λy.M[y]) 알파-변환 (α-conversion) 표현식의 종속 변수의 이름을 바꾼다. name collision을 방지하기 위해 사용한다.
((λx.M) E) → (M[x:=E]) 베타-축약 (β-reduction) 종속 변수를 추상화 된 표현식의 인자로 치환한다.

De Bruijn indexing 을 이용하면 α-변환은 소거된다. 처치-로서 정리에 의하면, 간소화 방법을 반복 적용하여 얻는 최종 결과는 Beta normal form을 형성한다.

최초의 람다 대수 체계는 논리적인 오류가 있음이 증명되었으나, 처치가 1936년에 그 속에서 계산과 관련된 부분만 따로 빼내어 후에 타입 없는 람다 대수 (untyped lambda calculus)라고 불리게 된 체계를 발표하였다. 또한 1940년에는 더 약한 형태이지만 논리적 모순이 없는 단순 타입 람다 대수 (simply typed lambda calculus)를 도입하였다.

람다 대수는 계산 이론, 언어학 등에 중요한 역할을 하며, 특히 프로그래밍 언어 이론의 발전에 크게 기여했다. 리스프와 같은 함수형 프로그래밍 언어는 람다 대수로부터 직접적인 영향을 받아 탄생했으며, 단순 타입 람다 대수는 현대 프로그래밍 언어의 타입 이론의 기초가 되었다.

설명과 적용[편집]

'람다 대수'는 임의의 튜링 기계 (Turing machine)를 시뮬레이션 할 수 있는 보편적인 계산 모델로서 튜링 완전 (Turing complete)하다.[1] 이름에 관하여는, 람다 표현식람다 항목 의 람다는 그리스 문자 람다 (λ)로서 어떤 함수 내에 어떤 변수를 종속 시키는 것을 나타내기 위하여 이용된다.

람다 대수는 수학, 철학,[2] 언어학,[3][4], 컴퓨터 과학.[5] 등의 여러 분야에 적용될 수 있다. 람다 대수는 프로그래밍 언어 이론의 발달에 중요한 역할을 했다. 람다 대수는 함수형 프로그래밍을 사용하여 구현된다. 또한, 람다 대수는, 현재, 범주론의 연구 토픽에 포함된다.[6]

수학사에서 람다 대수[편집]

람다 대수는 수학자 알론조 처치에 의해 수학기초론 연구의 일환으로 1930년대 소개됐다.[7][8] 최초의 시스템은 스티븐 클레이니존 버클리 로서클리네-로저 역설을 제창하면서 1935년 논리적 모순을 보이기 위해 도입됐다.[9][10]

그 후인 1936년 처치는 독립적으로 현재에는 타입 없는 람다 대수라고 불리는 계산에 관련한 부분을 출판했다.[11] 1940년, 그는 또한 계산적으로는 떨어지지만 논리적으로 무결한 시스템을 공개했다. 이것이 단순 타입 람다 대수이다.[12]

1960년대에 람다 대수와 프로그래밍 언어의 관계가 명확히 밝혀지기 전까지는 λ-대수는 단지 형식주의 (formalism)일 뿐이었다. 감사하게도 Richard Montague와 언어학자들이 λ-대수를 자연어 (natural language)의 의미론에 적용함으로써, λ-대수는 언어학과[13]컴퓨터 과학[14] 양쪽 분야에서 인정받는 위치를 차지했다.

함수의 표현[편집]

함수컴퓨터 과학수학의 기초를 이루는 개념이다. 람다 대수는 함수를 단순하게 표현할 수 있도록 하여 '함수의 계산'이라는 개념을 더 깊이 이해할 수 있게 돕는다.

예를 들어 항등 함수 는 하나의 입력 를 받아 다시 를 결과로 내놓는다고 하자. 한편 함수 는 입력 를 받아 두 수의 제곱의 합을 내놓는다고 하자. 이 두 예제로부터 세 가지 유용한 사실을 알 수 있다.

  1. 함수가 반드시 이름을 가질 필요는 없다. 함수 는 이름을 제거하고 와 같은 형태로 쓸 수 있다. 또한 항등 함수 의 형태로 쓸 수 있다.
  2. 함수의 입력 변수의 이름 또한 필요 없다. 는 변수의 이름은 다르지만 같은 항등 함수를 의미한다. 또한 는 같은 함수를 나타낸다.
  3. 두 개 이상의 입력을 받는 함수는 하나의 입력을 받아 또다른 함수를 출력하는 함수로 다시 쓸 수 있다. 예를 들어, 와 같은 형태로 다시 쓸 수 있다. 함수를 이와 같이 변환하는 것을 커링 (currying)이라고 한다. 위의 함수 는 다음과 같이 단일 입력 함수를 두 번 적용하는 것으로 이해할 수 있다.



핵심 개념[편집]

추상화

는 단일 입력 를 받아 의 표현으로 치환하는 익명의 함수를 지칭한다. 예를 들어 는 함수 람다 추상화이다. 람다 추상화를 통해 함수를 정의한다는 것은 함수를 정의하기만 하고 함수를 수행(호출)하지는 않는다는 것을 의미한다. 람다 추상화를 통해 변수 는 표현 속박된다.

자유 변수

자유 변수(free variable)는 람다 추상화를 통해 표현에 묶이지 않은 변수를 말한다. 자유 변수의 집합은 귀납적으로 정의된다.

  • 의 자유 변수는 뿐이다.
  • 의 자유변수는 를 제외하고 에 등장하는 변수들이다.
  • 두 표현 의 결합 의 자유변수의 집합은 의 자유변수의 집합과 의 자유변수의 집합의 합집합이다.

예를 들어, 에는 자유 변수가 없지만, 에는 자유변수가 하나이다.

축약[편집]

람다 대수식의 의미는 식이 어떻게 축약될 수 있는지에 따라 정의된다. 람다 대수식 축약에는 세 가지가 있다.

  • 알파-변환(α-conversion): 속박 변수를 바꿈
  • 베타-축약(β-reduction): 식의 인수에 함수를 적용
  • 에타-변환(η-conversion): 외연성을 통해 축약 (겉으로 보이는 행동이 같은 함수는 동일 함수로 간주함)

베타-축약을 통해 같은 식으로 변환되면 베타-동치(β-equivalent)라 부른다. 다른 축약도 마찬가지로 각각 알파-동치(α-equivalent), 에타-동치(η-equivalent)로 정의된다. 축약할 수 있는 식(reducible expression)을 줄여서 redex라고 부른다.

알파-변환[편집]

알파-리네이밍(alpha-renaming)이라고 불리기도 하는 알파-변환은 속박 변수의 이름이 바뀌는 것을 허용한다. 예를 들어, 로 바뀌어도 알파-동치이다. 알파-변환은 일반적으로 동치임을 확인하기 위해 사용된다. 정확한 알파-변환의 규칙은 완전히 사소하지 않다. 첫 번째로 추상화로 알파-변환을 수행할 때, 한 변수는 같은 추상화에 속한 경우만 새롭게 이름 붙일 수 있다. 예를 들어, 의 알파-변환은 가 될 수 있으나, 은 될 수 없다. 두 번째로 다른 추상화에 의해 변수가 캡쳐되어 있을 경우 알파-변환을 할 수 없다. 예를 들어, 로 알파-변환될 수 없다. 정적인 스코프를 가지는 프로그래밍 언어에서, 알파-변환은 이름 없는 변수의 이름을 해당 변수를 포함하는 스코프에서 결정하는 이름 분석(name resolution)을 통해 변수의 이름을 결정할 수 있다.

치환[편집]

형태로 쓰여지는 치환은 변수 를 식 과 함께 에 대입하는 과정이다. 치환은 다음과 같은 성질을 가진다. x와 y는 변수, M과 N은 λ 형태의 식이다.

x[x := N] ≡ N
y[x := N] ≡ y (만약 xy 일 경우,)
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
x.M)[x := N] ≡ λx.M
y.M)[x := N] ≡ λy.(M[x := N]) (만약 xy 이고, y ∉ FV(N) 일 경우,)

람다 추상화에 치환하기 위해서는 알파-변환이 필요하다. 예를 들어, 를 치환했을 경우 는 정확하지 않다. 로 치환되어야 알파-동치를 이룰 수 있다.

타입 없는 람다 대수[편집]

타입 없는 람다 대수는 이와 같은 고찰을 바탕으로 함수를 다음과 같은 형식으로 다시 표현한다.

변수 수식

위에서 살펴본 항등함수 는 람다 대수로 표현하면 가 된다.

함수를 실제로 계산하는 것은 베타 축약이라는 과정을 통해 이루어진다. 베타 축약은 다음과 같은 규칙을 갖는다.

: 수식 에서 모든 변수 를 수식 으로 치환한다.

예를 들어 입력값 에 대해 수식 를 리턴하는 함수 가 있다고 하자. 이 함수에 입력 을 적용하는 과정은 와 같이 수식 내의 모든 을 7로 치환한 것으로 표현할 수 있다. 이와 같이 치환 등을 통해 수식을 축약하는 것은 베타 축약의 한 예이다.

같이 보기[편집]

참고 문헌[편집]

각주[편집]

  1. Turing, A. M. (December 1937). “Computability and λ-Definability”. 《The Journal of Symbolic Logic》 2 (4): 153–163. JSTOR 2268280. doi:10.2307/2268280. 
  2. Coquand, Thierry, "Type Theory", The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).
  3. Moortgat, Michael (1988). 《Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus》. Foris Publications. ISBN 9789067653879. 
  4. Bunt, Harry; Muskens, Reinhard, 편집. (2008), 《Computing Meaning》, Springer, ISBN 9781402059575 
  5. Mitchell, John C. (2003), 《Concepts in Programming Languages》, Cambridge University Press, 57쪽, ISBN 9780521780988 .
  6. Pierce, Benjamin C. 《Basic Category Theory for Computer Scientists》. 53쪽. 
  7. Church, A. (1932). “A set of postulates for the foundation of logic”. 《Annals of Mathematics》. Series 2 33 (2): 346–366. JSTOR 1968337. doi:10.2307/1968337. 
  8. For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
  9. Kleene, S. C.; Rosser, J. B. (July 1935). “The Inconsistency of Certain Formal Logics”. 《The Annals of Mathematics》 36 (3): 630. doi:10.2307/1968646. 
  10. Church, Alonzo (December 1942). “Review of Haskell B. Curry, The Inconsistency of Certain Formal Logics”. 《The Journal of Symbolic Logic》 7 (4): 170–171. JSTOR 2268117. doi:10.2307/2268117. 
  11. Church, A. (1936). “An unsolvable problem of elementary number theory”. 《American Journal of Mathematics》 58 (2): 345–363. JSTOR 2371045. doi:10.2307/2371045. 
  12. Church, A. (1940). “A Formulation of the Simple Theory of Types”. 《Journal of Symbolic Logic》 5 (2): 56–68. JSTOR 2266170. doi:10.2307/2266170. 
  13. Partee, B. B. H.; ter Meulen, A.; Wall, R. E. (1990). 《Mathematical Methods in Linguistics》. Springer. 2016년 12월 29일에 확인함. 
  14. Alama, Jesse "The Lambda Calculus", The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).