람다 기초

알론도 처지(Alonzo Church)가 1930년대에 발표한 추론 또는 계산 모델의 일종이다. 람다 대수는 결정문제(decision problem)를 해결하기 위해, 계산가능성(computability) 혹은 계산가능한 함수(computable function)가 무엇인지를 명확히 정의하는데 사용한다.

하스켈의 문법을 소개하기 전에 람다 대수부터 설명하는 이유는 람다 대수가 함수형 언어의 계산 모델이기 때문이다. 그리고 대부분의 함수형 프로그래밍 언어는 람다 대수를 기반으로 구성되어 있기 때문이다. 함수형 언어에서 우리가 함수를 정의, 전달, 반환하는 거의 모든 것들에 람다 대수의 원리를 따르고 있다. 좀 더 자세한 내용이 궁금하다면 1, 2를 참고하자.

Lambda Calculus

수학자 힐베르트(David Hilbert)가 어떤 수학적인 명제가 입력으로 주어질 때 참과 거짓을 알아내는 알고리즘을 연구하였다. 1931년에 괴델(Kurt Gödel)이 힐베르트의 연구에 대해서 그러한 알고리즘은 존재하지 않고, 존재할 수 없음을 불완전성 정리 (Incompleteness Theorem)로 증명한다. 증명의 핵심은 모든 수학적인 논리 체계에는 논리 자체적으로 증명할 수 없는 명제들이 존재한다는 것으로 일단 풀 수 없는 문제가 존재함을 알게 된 이후에 많은 학자들은 '풀 수 있는 문제'에 대해서 연구에 몰두한다.

다양한 연구의 결과로 클레이너(Kleene Star)가 시작하고 처치(Alonzo Church)가 공헌한 재귀함수(Recursive Function), 알론도 처치의 람다 대수(λ-calculus), 포스트(Emil Leon Post)의 포스트 시스템(Post Canonical Systems) 그리고 전산학도들에게 가장 친숙한 튜링(Alan Turing)의 튜링기계(Turing Machine) 등이 발표되었다.

결국 1937년에 처치와 튜링이 각자 독자적인 연구에 의해서 모든 계산 가능한 연산들(알고리즘적인), 즉 튜링 기계로 수행될 수 있는 연산들은 처치의 방법을 적용할 수 있고, 그 역도 성립한다는 것이 밝혀졌다. 람다 대수는 임의의 튜링 기계(Turing machine)를 시뮬레이션 할 수 있는 보편적인 계산 모델로서 튜링 완전(turing complete)하다는 것으로, 이 결과를 바탕으로 계산 가능성 이론(computability theory)이 객관적이고 수학적인 특성을 갖는다는 것이 설득력을 얻게 되었다.

소프트웨어가 의미하는 것을 수학적으로 표현한 모델의 하나로 람다 대수를 꼽을 수 있다. 람다 대수는 직관적으로 계산 가능한 모든 것들을 표현할 수 있으며 소프트웨어가 계산하는 과정을 람다 대수를 이용하여 표현할 수 있다. 람다 대수를 확장하여 계산이라는 과정 중에서 발생하는 타입(type)이 올바른 것인지를 판단할 수 있도록 타입이라는 개념을 추가한 타입을 갖는 람다 대수(Typed Lambda Calculus)도 있다.

하스켈은 람다 대수로 시작한다.

함수형 프로그래밍

함수형 프로그래밍은 수학에서 사용하는 함수로 모델링 된 함수에 의존하는 컴퓨터 프로그래밍 방법이다. 함수형 프로그래밍의 핵심은 프로그램이 함수 표현식(expression)의 조합이라는 것이다. 표현식에는 구체적인 값, 변수 및 함수가 포함된다. 함수를 조금 더 구체적으로 정의하자면, 인수 또는 입력으로 평가하거나 계산할 수 있는 표현식이다. Haskell이나 여타의 함수형 프로그래밍에서 일반적으로 first-class로 부르며 함수를 값, 인수, 또는 입력으로 사용할 수 있다. 함수형 프로그래밍 언어는 람다 대수를 기반으로 한다. 일반적으로 몇몇 언어는 람다 대수를 사용하여 변환할 수 없는 함수나 몇가지 기능을 언어에 통합하지만, 하스켈은 순수 함수형 언어이다.

순수 함수형 언어에서 말하는 '순수'(pure)는 참조 투명성이라 불리는 것을 의미하는 것으로, 참조 투명성이란 동일한 함수를 평가할 때 순수 함수형 언어는 항상 같은 결과를 반환한다는 것을 의미한다.

람다라는 단어를 사용하지 않는다고 해도, 이 글을 읽는 대부분의 독자는 함수에 대해서 어느 정도 지식이 있을 것으로 생각된다. 수학적으로 함수는 입력 집합과 출력 집합 사이의 관계를 의미한다. 함수는 관계를 정의하고 표현한다. 두 입력에 관한 덧셈을 하나의 출력으로 정의하면 덧셈 함수를 만들 수 있다.

예를 들어, 1) 𝑓(1) = 𝐴, 2) 𝑓(2) = 𝐵 , 3) 𝑓(3) = 𝐶 과 같이 숫자 {1,2,3}과 {𝐴,𝐵,𝐶}의 관계를 정의했다면, 예외없이 {1}은 {A}를 반환한다. 다시 말하지만, 예외는 없다. 만약 4) 𝑓(1) = 𝑋, 5) 𝑓(1) = 𝑌, 6) 𝑓(2) = 𝑍과 같다면 𝑓(1)은 함수가 아니다.

다시 처음으로 돌아가서, 참조투명성을 설명하는 과정에서 입력은 출력을 예측할 수 있어야 한다. 1) 𝑓(1) = 𝐴, 2) 𝑓(2) = 𝐴, 3) 𝑓(3) = 𝐴은 함수인가? 둘 이상의 입력에 대해 동일한 출력을 갖는 것은 유효한 함수이다. 예를 들어, 5보다 작은 값을 테스트하는 함수가 필요하다고 가정했을 때, 입력이 5보다 작으면 True를 반환하고 다른 모든 경우에는 False를 반환하는 것이 상식적이다. 다른 입력이 동일한 출력으로 이어질 수 있다. 따라서 입력과 출력의 관계가 함수에 의해 정의되고 입력과 함수 정의를 알면 출력을 (언제나, 항상) 예측할 수 있어야하며, 예측된다.

𝑓(𝑥) = 𝑥 + 1이란 함수는 x라는 하나의 인수를 필요로 한다. 입력 𝑥 및 출력 간의 관계는 함수 본문에 설명되어 있듯이 𝑥가 무엇이든 1을 더하고 결과를 반환하는 것이다. 이 함수의 𝑥에 1을 입력하면 𝑓(1) = 1 + 1이 되고, 그 결과는 𝑓(1) = 2가 된다. 수학에서 사용하는 함수처럼 입력을 출력 집합과 연관시켜 사용하는 것이 함수형 프로그래밍을 이해하는데 중요하다.

람다 표현식(λ-expression)

람다 대수는 expression, variable 및 abstraction라는 세 가지 기본적인 구성 요소를 가진다. expression은 모든 구성요소의 상위 집합을 의미한다. 1) expression은 variable 또는 abstraction(일반적으로 function으로 정의) 혹은 그것들을 결합된 것 일 수 있다. 가장 간단한 expression은 single variable(단일 변수)이다. 2) variable에는 어떤 의미나 값을 나타내는 것이 아니라 함수의 입력을 위한 이름일 뿐이다. 3) abstraction은 기능(function)으로, head와 body를 가지고 있으며 head는 λ(lambda)와 variable, body는 또 다른 expression이며 이름을 지정하지 않는다.

Identity function인 𝑓(𝑥) = 𝑥를 람다 대수 형태로 나타낸 λx.x에서 λx는 head이다. head에서 x는 단일 매개 변수로 body에서 같은 이름의 모든 변수와 연결된다. . 이후에 위치한 x는 body로 람다가 적용되었을 때 반환하는 표현으로 이것은 bound variable이다. 점(.)은 람다의 매개 변수와 본문을 구분한다.

Alpha equivalence

variable은 어떤 의미나 값을 나타내는 것이 아니라 placeholder 역할을 할 뿐이다. 따라서 𝜆𝑥.𝑥, 𝜆𝑑.𝑑 그리고 𝜆𝑧.𝑧은 동일한 람다 대수이다. 모두 같은 기능을 한다.

Beta reduction

인수(argument)를 함수에 적용 할 때, abstraction은 body에 바운딩된 모든 변수에 body의 abstraction에 적용한다. abstraction의 head는 변수를 바인딩 하는 것이다. 이렇게 변수를 바인딩하여 하는 과정하여 head를 축약하는 과정을 beta reduction이라 한다.

𝜆𝑥.𝑥에 숫자 2를 사용((𝜆𝑥.𝑥) 2)하여 beta reduction을 적용할 때 𝑥에 2를 적용하고, 함수 본문의 각 바인딩 된 변수.x에 2를 대입하고 head를 제거한다. 바인딩 된 변수는 𝑥이고, identity function이기 때문에 2를 반환한다. (λ𝑥.ƒ𝑥) E의 beta reduction을 적용하면 f E이며, (λ𝑥.(λ𝑦.add 𝑥 𝑦)) 3의 beta reduction을 적용하면 λ𝑦.add 3 𝑦이다.

람다 대수에서 별다른 제안이 없다면 표현식을 분명하게 표기하기 위해 괄호를 사용한다. 예를 들어, 표현식 (𝑥)=𝑥와 동일하다. 혼란을 피하기 위해 함수의 적용(application)은 왼쪽으로 결합한다. 𝜆𝑥.𝑥)(𝜆𝑦.𝑦)𝑧의 계산을 진행해보자. 계산을 위해서 한가지 표기법을 도입하자. λ𝑦.𝑦 𝑧에서 모든 𝑦는 𝑧로 대체된다는 것을 표현하기 위해서 [𝑦 : = 𝑧] 표기법을 사용한다.

람다 대수 (𝜆𝑥.𝑥)(𝜆𝑦.𝑦)𝑧를 계산해보자.

(𝜆𝑥.𝑥)(𝜆𝑦.𝑦)𝑧
== ((𝜆𝑥.𝑥)(𝜆𝑦.𝑦))𝑧  // (𝜆𝑥.𝑥)(𝜆𝑦.𝑦)에 𝑧를 적용
== [𝑥 ∶= (𝜆𝑦.𝑦)]𝑧   // 𝜆𝑥.𝑥에서 𝑥는 (𝜆𝑦.𝑦)로 축약
== (𝜆𝑦.𝑦)𝑧          // (𝜆𝑦.𝑦)에 𝑧를 적용
== [𝑦 ∶= 𝑧]         // (𝜆𝑦.𝑦)에서 𝑦는 𝑧로 축약
== 𝑧                // 𝑧를 축약

Free variables

λ로 시작하지 않는 variable을 free variable(자유 변수) 혹은 non-local(비지역)이라 한다. 𝜆𝑥.𝑥𝑦에서 자유 변수는 𝑦이다. (𝜆𝑥.𝑥𝑦)𝑧을 계산해보자.

(𝜆𝑥.𝑥𝑦)𝑧
= [𝑥 ∶= 𝑧]
= (𝑧)𝑦
= 𝑧𝑦

자유 변수가 없는 표현식을 닫혀 있다(closed)라고 하며, 닫힌 람다 표현식(Closed lambda expression)을 컴비네이터(combinator)라고 한다.

Multiple arguments

각 람다는 하나의 매개 변수만 바인딩 할 수 있으며 하나의 인수만 적용 할 수 있다. 여러개의 인수가 필요한 함수에는 여러 개의 중첩 된 head가 있다. 한 번 적용하고 첫 번째(맨 왼쪽) head를 제거하면 다음 head가 적용된다. 1920 년대 Moses Schönfinkel에 의해 발견되었지만, Haskell Curry의 이름을 따서 명명되었으며, 일반적으로는 currying이라고 부른다. 두 개의 중첩된 lambdas가 적용된 𝜆𝑥𝑦.𝑥𝑦은 𝜆𝑥.(𝜆𝑦.𝑥𝑦)으로 구분할 수 있다.

𝜆𝑥𝑦.𝑥𝑦 1 2
= (𝜆𝑥𝑦.𝑥𝑦) 1 2
= (𝜆𝑥(𝜆𝑦.𝑥𝑦)) 1 2 
= [𝑥 ∶= 1]
= (𝜆𝑦.1𝑦) 2
= [𝑦 ∶= 2]
= 1 2

또 다른 예제로 (𝜆𝑥𝑦.𝑥𝑦)(𝜆𝑧.𝑎)을 계산해보자.

(𝜆𝑥𝑦.𝑥𝑦)(𝜆𝑧.𝑎) 1
= (𝜆𝑥(𝜆𝑦.𝑥𝑦))(𝜆𝑧.𝑎) 1 
= [𝑥 ∶= (𝜆𝑧.𝑎)]
= (𝜆𝑦.(𝜆𝑧.𝑎)𝑦) 1
= [𝑦 ∶= 1]
= (𝜆𝑧.𝑎) 1
= [𝑧 ∶= 1] // 본문에 𝑧가 없으모로 1을 대입할 수 없음
= 𝑎 

조금 더 복잡한 예제를 계산해보자.

(𝜆𝑥𝑦𝑧.𝑥𝑧(𝑦𝑧))(𝜆𝑚𝑛.𝑚)(𝜆𝑝.𝑝)
= (𝜆𝑥.𝜆𝑦.𝜆𝑧.𝑥𝑧(𝑦𝑧))(𝜆𝑚.𝜆𝑛.𝑚)(𝜆𝑝.𝑝)
= (𝜆𝑦.𝜆𝑧(𝜆𝑚.𝜆𝑛.𝑚)𝑧(𝑦𝑧))(𝜆𝑝.𝑝)
= 𝜆𝑧(𝜆𝑚.𝜆𝑛.𝑚)(𝑧)((𝜆𝑝.𝑝)𝑧)
= 𝜆𝑧(𝜆𝑛.𝑧)((𝜆𝑝.𝑝)𝑧)
= 𝜆𝑧.𝑧
= 𝑧