🔗History

17세기 라이프니츠는 다음과 같은 이상적인 제안을 했다.

• 가능한 모든 문제를 기술할 수 있는 범용언어를 만든다.
• 범용언어로 기술되는 모든 문제를 해결하기 위한 결정방법을 찾는다.

수학적 문제에 한정한다면, 라이프니츠의 첫 번째 제안은 프레게와 러셀 이후 어떤 형태의 집합 이론이 일차 술어 논리의 언어로 표현된 것으로 충족되었다.
두 번째 제안은 중요한 철학적 문제가 되었는데, "범용언어로 제시된 모든 문제를 해결할 수 있을까?"라는 질문이였다. 보편적으로, 그러한 것은 불가능하다고 보이지만, 이것을 증명하는 방법은 명확하지 않았다. 이러한 질문은 Entscheidungsproblem(의사결정 문제)로 알려지게 되었다.

1936년, Entscheidungsproblem(의사결정 문제)는 알론조 처치(Alonzo Church)와 앨런 튜링(Alan Turing)이 독립적으로 부정하여 해결하였다. 이를 위해서, 직관적인 '결정가능(decidable)'또는 동등한 의미로 '계산가능(computable)'의 형식화가 필요했는데, 처치와 튜링은 두가지 다른 방식으로 계산 모델을 도입하여 해결하였다.

• 처치(1936)는 람다 계산법(lambda calculus)라는 형식 체계를 발명하고, 이 시스템을 통해 계산 가능한 함수의 개념을 정의했다.
• 튜링(1936/7)은 튜링 머신(Turing machines)라고 불리는 기계들을 발명하고, 이러한 기계들을 통해 계산 가능한 개념을 정의했다.

또한 1936년에 튜링은 두 모델이 동일한 강도를 가지며, 두 모델이 같은 계산 가능한 함수들의 클래스를 정의한다는 것을 증명하였다. (Turing 1937)
현재의 폰 노이만 컴퓨터들은 튜링 머신의 개념을 기반으로 한다. 개념적으로, 폰 노이만 컴퓨터들은 랜덤 액세스 레지스터를 갖춘 튜링 머신으로 볼 수 있다. 포트란(Fortran), 파스칼(Pascal)등의 명령형 프로그래밍 언어들과 모든 어셈블리어 언어들은 튜링 머신이 수행되는 방식에 기반하여 작성된다.(명령문의 연속으로써 튜링 머신이 지시된다.)
하스켈(Haskell), 미란다(Miranda), ML 등과 같은 함수형 프로그래밍 언어들은 람다 계산법을 기반으로 한다. 리스프(Lisp)는 이러한 언어들의 초기(비록 함수형언어 생태계에 논란이 있지만..) 예시라고 할 수 있다. 리덕션 머신(reduction machine)은 특히 이러한 함수형 프로그래밍 언어들의 실행을 위해 설계되었다.

리스프는 순수함수형 언어가 아니기 때문에, 하스켈과 같은 몇몇 다른 함수형 언어들과 대조적이다. 리스프는 리덕션 머신 위에서 실행되지만 동시에 명령형 프로그래밍과 변이(mutability)도 허용한다. 이러한 특성 때문에 하스켈과 같은 순수함수형 프로그래머들이 리스프를 선호하지 않으며, 아직까지도 "리스프는 진실로 함수형 언어인가?" 와 같은 논란이 있다. 나는 대학생 때 인공지능 수업에서 리스프를 배웠고, 알고리즘, 데이터 구조 과제를 리스프로 구현하여 제출할 정도로 리스프에 빠진적이 있었다. 특히 국내에 번역서가 입문수준의 1권밖에 없기 때문에, 도서관에서 오래된 원서들을 빌려 읽었던 기억이있다. 유명한 책 중에 SICP(비록 scheme을 사용하지만 상관없다)나 폴 그레이엄이 쓴 책들을 보며 리스프의 매력에 빠져보길 바란다.

🔗Reduction and functional programming

함수형 프로그램은 알고리즘과 입력을 나타내는 표현식 \(E\)로 구성된다. 이 표현식 \(E\)는 일정한 재작성 규칙에 따라 대체될 수 있는데,리덕션은 표현식 \(E\)의 일부분 \(P\)을 주어진 재작성 규칙에 따라 다른 표현식 \(P'\)로 대체하는 것을 의미한다. 기호적으로 표현하면 다음과 같다. \[E[P] \rightarrow E[P'],\] 단 \(P \rightarrow P'\)은 규칙에 따라 대체 가능한 경우이다. 이 리덕션 과정은 결과적으로 더 이상 재작성이 불가능한 부분이 없는 표현식이 나올 때까지 반복된다. 이렇게 얻어진 최종 표현식을 정규형(normal form)이라고 하며, 주어진 함수형 프로그램의 출력값을 나타낸다.

예시: $$ \begin{aligned} (7 + 4) \cdot (8 + 5 \cdot 3) &\rightarrow 11 \cdot (8 + 5 \cdot 3)\\ &\rightarrow 11 \cdot (8 + 15)\\ &\rightarrow 11 \cdot 23\\ &\rightarrow 253. \end{aligned} $$

위의 예시에서 리덕션 규칙은 숫자들에 대한 덧셈과 곱셉의 '표(table)'로 구성된다.
함수형 프로그래밍에서는 리덕션을 통해 기호 연산(symbolic computation)이 가능하다. 예를 들어, 다음과 같이

first of (sort (append ('dog', 'rabbit') (sort (('mouse', 'cat')))))
    -> first of (sort (append ('dog', 'rabbit') ('cat', 'mouse')))
    -> first of (sort ('dog', 'rabbit', 'cat', 'mouse'))
    -> first of ('cat', 'dog', 'mouse', 'rabbit')
    -> 'cat'.

이러한 기호 연산 과정은 append와 sort와 같은 함수들이 일부 재작성 규칙에 의해 정의될 수 있음을 보여준다. 재작성 규칙을 통해 정의된 이러한 함수들은 '콤비네이터(combinator)'라고 불리며, 함수형 프로그래밍에서 기호 데이터를 조작하기 위한 필수적인 도구로 사용된다.

리덕션 시스템은 일반적으로 \(Church-Rosser\) 속성을 만족하는데, 이는 얻어진 정규형이 하위 용어들의 계산 순서에 독립적이라는 것을 나타낸다. 실제로 첫 번째 예시는 다음과 같이 리덕션 될 수 있다.

$$ \begin{aligned} (7 + 4) \cdot (8 + 5 \cdot 3) &\rightarrow (7 + 4) \cdot (8 + 15)\\ &\rightarrow 11 \cdot (8 + 15)\\ &\rightarrow 11 \cdot 23\\ &\rightarrow 253. \end{aligned} $$

혹은 여러 표현식들을 동시에 평가함으로써 더 단순하게 리덕션될 수도 있다.

$$ \begin{aligned} (7 + 4) \cdot (8 + 5 \cdot 3) &\rightarrow 11 \cdot (8 + 15)\\ &\rightarrow 11 \cdot 23\\ &\rightarrow 253. \end{aligned} $$

🔗Application and abstraction

\(\lambda-\)계산의 첫 번째 기본 작업은 적용(\(application\))이다. 표현식 \(F \cdot A\) 또는 \(F A\)는 데이터 \(F\)를 알고리즘으로 간주하여 데이터 \(A\)를 입력으로 적용하는 것을 나타낸다. 이는 두 가지 관점으로 볼 수 있는데, 계산 과정 \(F A\) 또는 이 과정의 출력으로 볼 수 있다. 첫 번째 관점은 변환(conversion)또는 더 나은 리덕션(reduction) 개념으로 포착되며, 두 번째 관점은 모델(의미론) 개념으로 표현된다. 이 이론은 타입에 제한이 없다(type-free). 즉, \(F\)가 자기 자신에게 적용된 \(F F\)와 같은 표현식을 고려할 수 있다. 이는 재귀를 모방하는데 유용하다.

다른 기본 작업은 추상화(\(abstraction\))이다. 만약 \(M \equiv M[x]\)라는 표현식이 \(x\)에 의존한다면, \(\lambda{x}.M[x]\)는 함수 \(x \mapsto M[x]\)를 나타낸다.
적용(\(application\))과 추상화(\(abstraction\))는 다음과 같은 직관적인 공식에서 함께 작동한다. \[(\lambda{x}.2 \cdot x + 1)3 = 2 \cdot 3 + 1 \space\space\space (= 7).\] 즉, \((\lambda{x}.2 \cdot x + 1)3\)은 함수 \(x \mapsto 2 \cdot x + 1\)에 인자 \(3\)을 적용하여 \(2 \cdot 3 + 1\)로 계산되며 값은 \(7\)이 된다. 일반적으로 \((\lambda{x}.M[x])N = M[N]\) 식은 다음과 같이 쓰이기도 한다. \[(\lambda{x}.M)N = M[x \coloneqq N], \qquad (\beta)\] 여기서 \([x := N]\)은 \(x\)에 \(N\)을 대입하는 것을 나타내는데, 놀랍게도 \((\beta)\)가 \(\lambda-\)계산의 유일한 필수적인 공리이지만, 그 결과로 얻어지는 이론은 꽤 복잡하다.

🔗Free and bound variables

추상화\((abstraction)\)는 변수 \(x\)를 \(M\) 안에서 "묶는다\((bind)\)"고 표현한다. 예를 들어, \(\lambda{x}.yx\)에서 \(x\)는 묶여있는 변수(bound variable)이고 \(y\)는 자유 변수(free variable)라고 한다. 치환 \([x := N]\)은 \(x\)의 자유 등장(free occurrences)에만 적용된다 \[yx(\lambda{x}.x)[x := N] \equiv yN(\lambda{x}.x)\]

미적분학에서도 유사한 변수 묶음 개념이 있다. \(\int_{a}^bf(x,y)dx\)에서 변수 \(x\)는 묶여있고 \(y\)는 자유 변수이다.
명료성을 위해, 특정 표현식에 등장하는 묶인 변수들은 자유 변수들과 다르다고 가정한다. 이것은 묶인 변수들의 이름을 변경함으로써 충족할 수 있는데, 예를 들어, \(\lambda{x}.x\)는 \(\lambda{y}.y\)로 바뀔 수 있다. 사실, 이러한 표현식들은 동일한 방식으로 작동한다. \[(\lambda{x}.x)a = a = (\lambda{y}.y)a\] 그리고 사실상 이들은 같은 의도된 알고리즘을 나타낸다. 따라서 묶인 변수들의 이름만 다른 표현식들은 동일한 것으로 간주된다.

🔗Functions of more arguments

여러 인자를 가지는 함수는 적용을 반복함으로써 얻을 수 있다. 이 아이디어는 Schönfinkel(1924)에 의해 제안되었지만, H.B. Curry가 독립적으로 도입한 후 \(currying\)이라는 이름으로 널리 알려졌다. 직관적으로 \(f(x, y)\)가 두 개의 인자에 의존한다면, 다음과 같이 정의할 수 있다. \[F_x = \lambda{y}.f(x,y),\] \[F = \lambda{x}.F_x.\] 그런 다음, \[(Fx)y = F_xy = f(x, y). \qquad (\rho)\]

이렇게 함으로써 두 인자를 가지는 함수 \(f(x, y)\)를 단일 인자 함수 \(F\)로 변환할 수 있다. 이러한 기법은 \(currying\)라고 불리며, 함수형 프로그래밍에서 함수들을 더 유연하게 조작하는 데에 사용된다.

마지막 식은 반복적인 적용에 대해 왼쪽으로 결합\((association)\)하는 것이 편리하다는 것을 보여준다. \[FM_1 ··· M_n \space denotes \space (··((FM_1)M_2)···M_n).\] 식 \((\rho)\)은 그런 다음 다음과 같이 표현된다. \[F{xy} = f(x, y)\] 이와 마찬가지로, 반복적인 추상화는 오른쪽으로 결합하는 것을 사용한다. \[\lambda{x_1} ··· x_n.f(x_1, ...., x_n) \space denotes \space \lambda{x_1}.(\lambda{x_2}.(···(\lambda{x_n}.f(x_1,....x_n))··)).\] 그러면 위에서 정의한 \(F\)에 대해 다음 \[F = \lambda{xy}.f(x, y)\] 그리고 \((\rho)\)는 다음과 같이 표현된다. \[(\lambda{xy}.f(x, y))xy = f(x, y).\] \(n\)개의 인자에 대해 다음과 같이 표현한다. \[(\lambda{x_1}···x_n.f(x_1,···,x_n))x_1···x_n = f(x_1,....,x_n)\] \(n\)번 \((\beta)\)를 사용하여 이 식은 다음과 같이 벡터 표기로 표현된다. \[(\lambda{\vec{x}}.f[{\vec{x}}])\vec{x} = f[\vec{x}];\] 보다 일반적으로 다음과 같이 표현한다. \[(\lambda{\vec{x}}.f[{\vec{x}}])\vec{N} = f[\vec{N}];\]